diff --git a/thys/Weighted_Path_Order/KBO_as_WPO.thy b/thys/Weighted_Path_Order/KBO_as_WPO.thy --- a/thys/Weighted_Path_Order/KBO_as_WPO.thy +++ b/thys/Weighted_Path_Order/KBO_as_WPO.thy @@ -1,421 +1,422 @@ subsection \A restricted equality between KBO and WPO\ text \The remaining difficulty to make KBO an instance of WPO is the different treatment of lexicographic comparisons, which is unrestricted in KBO, but there is a length-restriction in WPO. Therefore we will only show that KBO is an instance of WPO if we compare terms with bounded arity.\ text \This restriction does however not prohibit us from lifting properties of WPO to KBO. For instance, for several properties one can choose a large-enough bound restriction of WPO, since there are only finitely many arities occurring in a property.\ theory KBO_as_WPO imports WPO KBO_Transformation begin definition bounded_arity :: "nat \ ('f \ nat)set \ bool" where "bounded_arity b F = (\ (f,n) \ F. n \ b)" lemma finite_funas_term[simp,intro]: "finite (funas_term t)" by (induct t, auto) context weight_fun begin definition "weight_le s t \ (vars_term_ms (SCF s) \# vars_term_ms (SCF t) \ weight s \ weight t)" definition "weight_less s t \ (vars_term_ms (SCF s) \# vars_term_ms (SCF t) \ weight s < weight t)" lemma weight_le_less_iff: "weight_le s t \ weight_less s t \ weight s < weight t" by (auto simp: weight_le_def weight_less_def) lemma weight_less_iff: "weight_less s t \ weight_le s t \ weight s < weight t" by (auto simp: weight_le_def weight_less_def) abbreviation "weight_NS \ {(t,s). weight_le s t}" abbreviation "weight_S \ {(t,s). weight_less s t}" lemma weight_le_mono_one: assumes S: "weight_le s t" shows "weight_le (Fun f (ss1 @ s # ss2)) (Fun f (ss1 @ t # ss2))" (is "weight_le ?s ?t") proof - from S have w: "weight s \ weight t" and v: "vars_term_ms (SCF s) \# vars_term_ms (SCF t)" by (auto simp: weight_le_def) have v': "vars_term_ms (SCF ?s) \# vars_term_ms (SCF ?t)" using mset_replicate_mono[OF v] by simp have w': "weight ?s \ weight ?t" using sum_list_replicate_mono[OF w] by simp from v' w' show ?thesis by (auto simp: weight_le_def) qed lemma weight_le_ctxt: "weight_le s t \ weight_le (C\s\) (C\t\)" by (induct C, auto intro: weight_le_mono_one) lemma SCF_stable: assumes "vars_term_ms (SCF s) \# vars_term_ms (SCF t)" shows "vars_term_ms (SCF (s \ \)) \# vars_term_ms (SCF (t \ \))" unfolding scf_term_subst using vars_term_ms_subst_mono[OF assms]. lemma SN_weight_S: "SN weight_S" proof- from wf_inv_image[OF wf_less] have wf: "wf {(s,t). weight s < weight t}" by (auto simp: inv_image_def) show ?thesis by (unfold SN_iff_wf, rule wf_subset[OF wf], auto simp: weight_less_def) qed lemma weight_less_imp_le: "weight_less s t \ weight_le s t" by (simp add: weight_less_def weight_le_def) lemma weight_le_Var_Var: "weight_le (Var x) (Var y) \ x = y" by (auto simp: weight_le_def) end context kbo begin lemma kbo_altdef: "kbo s t = (if weight_le t s then if weight_less t s then (True, True) else (case s of Var y \ (False, (case t of Var x \ x = y | Fun g ts \ ts = [] \ least g)) | Fun f ss \ (case t of Var x \ (True, True) | Fun g ts \ if pr_strict (f, length ss) (g, length ts) then (True, True) else if pr_weak (f, length ss) (g, length ts) then lex_ext_unbounded kbo ss ts else (False, False))) else (False, False))" by (simp add: weight_le_less_iff weight_le_def) end context admissible_kbo begin lemma weight_le_stable: assumes "weight_le s t" shows "weight_le (s \ \) (t \ \)" using assms weight_stable_le SCF_stable by (auto simp: weight_le_def) lemma weight_less_stable: assumes "weight_less s t" shows "weight_less (s \ \) (t \ \)" using assms weight_stable_lt SCF_stable by (auto simp: weight_less_def) lemma simple_arg_pos_weight: "simple_arg_pos weight_NS (f,n) i" unfolding simple_arg_pos_def proof (intro allI impI, unfold snd_conv fst_conv) fix ts :: "('f,'a)term list" assume i: "i < n" and len: "length ts = n" from id_take_nth_drop[OF i[folded len]] i[folded len] obtain us vs where id: "Fun f ts = Fun f (us @ ts ! i # vs)" and us: "us = take i ts" and len: "length us = i" by auto have "length us < Suc (length us + length vs)" by auto from scf[OF this, of f] obtain j where [simp]: "scf (f, Suc (length us + length vs)) (length us) = Suc j" by (rule lessE) show "(Fun f ts, ts ! i) \ weight_NS" unfolding weight_le_def id by (auto simp: o_def) qed lemma weight_lemmas: shows "refl weight_NS" and "trans weight_NS" and "trans weight_S" and "weight_NS O weight_S \ weight_S" and "weight_S O weight_NS \ weight_S" by (auto intro!: refl_onI transI simp: weight_le_def weight_less_def) interpretation kbo': admissible_kbo w w0 pr_strict' pr_weak' least scf by (rule admissible_kbo') context assumes least_global: "\ f g. least f \ pr_weak g (f,0)" and least_trans: "\ f g. least f \ pr_weak (f,0) g \ least (fst g) \ snd g = 0" fixes n :: nat begin lemma kbo_instance_of_wpo_with_assms: "wpo_with_assms weight_S weight_NS (\f g. (pr_strict f g, pr_weak f g)) (\(f, n). n = 0 \ least f) full_status False (\f. False)" apply (unfold_locales) apply (auto simp: weight_lemmas SN_weight_S pr_SN pr_strict_irrefl weight_less_stable weight_le_stable weight_le_mono_one weight_less_imp_le - simple_arg_pos_weight) - apply (force dest: least_global least_trans simp: pr_strict)+ - apply (auto simp: pr_strict least dest:pr_weak_trans) + simple_arg_pos_weight) + apply (force dest: least_global least_trans simp: pr_strict)+ + using SN_on_irrefl[OF SN_weight_S] + apply (auto simp: pr_strict least irrefl_def dest:pr_weak_trans) done interpretation wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = "\f g. (pr_strict f g, pr_weak f g)" and prl = "\(f,n). n = 0 \ least f" and c = "\_. Lex" and ssimple = False and large = "\f. False" and \\ = full_status and n = n by (rule kbo_instance_of_wpo_with_assms) lemma kbo_as_wpo_with_assms: assumes "bounded_arity n (funas_term t)" shows "kbo s t = wpo.wpo s t" proof - define m where "m = size s + size t" from m_def assms show ?thesis proof (induct m arbitrary: s t rule: less_induct) case (less m s t) hence IH: "size si + size ti < size s + size t \ bounded_arity n (funas_term ti) \ kbo si ti = wpo.wpo si ti" for si ti :: "('f,'a)term" by auto note wpo_sI = arg_cong[OF wpo.wpo.simps, of fst, THEN iffD2] note wpo_nsI = arg_cong[OF wpo.wpo.simps, of snd, THEN iffD2] note bounded = less(3) show ?case proof (cases s) case s: (Var x) have "\ weight_less t (Var x)" by (metis leD weight.simps(1) weight_le_less_iff weight_less_imp_le weight_w0) thus ?thesis by (cases t, auto simp add: s kbo_altdef wpo.wpo.simps) next case s: (Fun f ss) show ?thesis proof (cases t) case t: (Var y) { assume "weight_le t s" then have "\s' \ set ss. weight_le t s'" apply (auto simp: s t weight_le_def) by (metis scf set_scf_list weight_w0) then obtain s' where s': "s' \ set ss" and "weight_le t s'" by auto from this(2) have "wpo.wpo_ns s' t" proof (induct s') case (Var x) then show ?case by (auto intro!:wpo_nsI simp: t weight_le_Var_Var) next case (Fun f' ss') from this(2) have "\s'' \ set ss'. weight_le t s''" apply (auto simp: t weight_le_def) by (metis scf set_scf_list weight_w0) then obtain s'' where "s'' \ set ss'" and "weight_le t s''" by auto with Fun(1)[OF this] Fun(2) show ?case by (auto intro!: wpo_nsI simp: t in_set_conv_nth) qed with s' have "\s' \ set ss. wpo.wpo_ns s' t" by auto } then show ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t] by (auto simp add: s t weight_less_iff set_conv_nth, auto) next case t: (Fun g ts) { fix j assume "j < length ts" hence "ts ! j \ set ts" by auto hence "funas_term (ts ! j) \ funas_term t" unfolding t by auto with bounded have "bounded_arity n (funas_term (ts ! j))" unfolding bounded_arity_def by auto } note bounded_tj = this note IH_tj = IH[OF _ this] show ?thesis proof (cases "\ weight_le t s \ weight_less t s") case True thus ?thesis unfolding wpo.wpo.simps[of s t] kbo_altdef[of s t] unfolding s t by (auto simp: weight_less_iff) next case False let ?f = "(f,length ss)" let ?g = "(g,length ts)" from False have wle: "weight_le t s = True" "weight_less t s = False" "(s, t) \ weight_NS \ True" "(s, t) \ weight_S \ False" by auto have lex: "(Lex = Lex \ Lex = Lex) = True" by simp have sig: "set (wpo.\ ?f) = {.. ?g) = {.. ?f) = ss" "map ((!) ts) (wpo.\ ?g) = ts" by (auto simp: map_nth) have sizes: "i < length ss \ size (ss ! i) < size s" for i unfolding s by (simp add: size_simp1) have sizet: "i < length ts \ size (ts ! i) < size t" for i unfolding t by (simp add: size_simp1) have wpo: "wpo.wpo s t = (if \i\{.. (\j\{.. = lex_ext wpo.wpo n ss ts" by (rule lex_ext_cong[OF refl refl refl], rule IH_tj, auto dest!: sizes sizet) finally have kbo: "kbo s t = (if pr_strict ?f ?g then (True, True) else if pr_weak ?f ?g then lex_ext wpo.wpo n ss ts else (False, False))" . show ?thesis proof (cases "\i\{..i\{..This is the main theorem. It tells us that KBO can be seen as an instance of WPO, under mild preconditions: the parameter $n$ for the lexicographic extension has to be chosen high enough to cover the arities of all terms that should be compared.\ lemma defines "prec \ ((\f g. (pr_strict' f g, pr_weak' f g)))" and "prl \ (\(f, n). n = 0 \ least f)" shows kbo_encoding_is_valid_wpo: "wpo_with_assms weight_S weight_NS prec prl full_status False (\f. False)" and kbo_as_wpo: "bounded_arity n (funas_term t) \ kbo s t = wpo.wpo n weight_S weight_NS prec prl full_status (\_. Lex) False (\f. False) s t" unfolding prec_def prl_def subgoal by (intro admissible_kbo.kbo_instance_of_wpo_with_assms[OF admissible_kbo'] least_pr_weak' least_pr_weak'_trans) apply (subst kbo'_eq_kbo[symmetric]) apply (subst admissible_kbo.kbo_as_wpo_with_assms[OF admissible_kbo' least_pr_weak' least_pr_weak'_trans, symmetric], (auto)[3]) by auto text \As a proof-of-concept we show that now properties of WPO can be used to prove these properties for KBO. Here, as example we consider closure under substitutions and strong normalization, but the following idea can be applied for several more properties: if the property involves only terms where the arities are bounded, then just choose the parameter $n$ large enough. This even works for strong normalization, since in an infinite chain of KBO-decreases $t_1 > t_2 > t_3 > ...$ all terms have a weight of at most the weight of $t_1$, and this weight is also a bound on the arities.\ lemma KBO_stable_via_WPO: "S s t \ S (s \ (\ :: ('f,'a) subst)) (t \ \)" proof - let ?terms = "{t, t \ \}" (* collect all rhss of comparisons *) let ?prec = "((\f g. (pr_strict' f g, pr_weak' f g)))" let ?prl = "(\(f, n). n = 0 \ least f)" have "finite (\ (funas_term ` ?terms))" by auto from finite_list[OF this] obtain F where F: "set F = \ (funas_term ` ?terms)" by auto (* since there only finitely many symbols, we can take n as the maximal arity *) define n where "n = max_list (map snd F)" (* now get a WPO for this choice of n *) interpret wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = ?prec and prl = ?prl and c = "\_. Lex" and ssimple = False and large = "\f. False" and \\ = full_status and n = n by (rule kbo_encoding_is_valid_wpo) { fix t assume "t \ ?terms" hence "funas_term t \ set F" unfolding F by auto hence "bounded_arity n (funas_term t)" unfolding bounded_arity_def using max_list[of _ "map snd F", folded n_def] by fastforce } (* for all the terms we have that KBO = WPO *) note kbo_as_wpo = kbo_as_wpo[OF this] (* and finally transfer the existing property of WPO to KBO *) from wpo.WPO_S_subst[of s t \] show "S s t \ S (s \ \) (t \ \)" using kbo_as_wpo by auto qed lemma weight_is_arity_bound: "weight t \ b \ bounded_arity b (funas_term t)" proof (induct t) case (Fun f ts) have "sum_list (map weight ts) \ weight (Fun f ts)" using sum_list_scf_list[of ts "scf (f,length ts)", OF scf] by auto also have "\ \ b" using Fun by auto finally have sum_b: "sum_list (map weight ts) \ b" . { fix t assume t: "t \ set ts" from split_list[OF this] have "weight t \ sum_list (map weight ts)" by auto with sum_b have "bounded_arity b (funas_term t)" using t Fun by auto } note IH = this have "length ts = sum_list (map (\ _. 1) ts)" by (induct ts, auto) also have "\ \ sum_list (map weight ts)" apply (rule sum_list_mono) subgoal for t using weight_gt_0[of t] by auto done also have "\ \ b" by fact finally have len: "length ts \ b" by auto from IH len show ?case unfolding bounded_arity_def by auto qed (auto simp: bounded_arity_def) lemma KBO_SN_via_WPO: "SN {(s,t). S s t}" proof fix f :: "nat \ ('f,'a)term" assume "\i. (f i, f (Suc i)) \ {(s, t). S s t}" hence steps: "S (f i) (f (Suc i))" for i by auto define n where "n = weight (f 0)" have w_bound: "weight (f i) \ n" for i proof (induct i) case (Suc i) from steps[of i] have "weight (f (Suc i)) \ weight (f i)" unfolding kbo.simps[of "f i"] by (auto split: if_splits) with Suc show ?case by simp qed (auto simp: n_def) let ?prec = "((\f g. (pr_strict' f g, pr_weak' f g)))" let ?prl = "(\(f, n). n = 0 \ least f)" (* now get a WPO for this choice of n *) interpret wpo: wpo_with_assms where S = weight_S and NS = weight_NS and prc = ?prec and prl = ?prl and c = "\_. Lex" and ssimple = False and large = "\f. False" and \\ = full_status and n = n by (rule kbo_encoding_is_valid_wpo) have "kbo (f i) (f (Suc i)) = wpo.wpo (f i) (f (Suc i))" for i by (rule kbo_as_wpo[OF weight_is_arity_bound[OF w_bound]]) (* for all the terms in the infinite sequence f 0, f 1, ... we have that KBO = WPO *) (* and finally derive contradiction to SN-property of WPO *) from steps[unfolded this] wpo.WPO_S_SN show False by auto qed end end \ No newline at end of file diff --git a/thys/Weighted_Path_Order/LPO.thy b/thys/Weighted_Path_Order/LPO.thy --- a/thys/Weighted_Path_Order/LPO.thy +++ b/thys/Weighted_Path_Order/LPO.thy @@ -1,117 +1,117 @@ section \The Lexicographic Path Order as an instance of WPO\ text \We first directly define the strict- and non-strict lexicographic path orders (LPO) w.r.t.\ some precedence, and then show that it is an instance of WPO. For this instance we use the trivial reduction pair in WPO ($\emptyset$, UNIV) and the status is the full one, i.e., taking parameters [0,..,n-1] for each n-ary symbol.\ theory LPO imports WPO begin context fixes "pr" :: "('f \ nat \ 'f \ nat \ bool \ bool)" and prl :: "'f \ nat \ bool" and n :: nat begin fun lpo :: "('f, 'v) term \ ('f, 'v) term \ bool \ bool" where "lpo (Var x) (Var y) = (False, x = y)" | "lpo (Var x) (Fun g ts) = (False, ts = [] \ prl (g,0))" | "lpo (Fun f ss) (Var y) = (let con = (\ s \ set ss. snd (lpo s (Var y))) in (con,con))" | "lpo (Fun f ss) (Fun g ts) = ( if (\ s \ set ss. snd (lpo s (Fun g ts))) then (True,True) else (let (prs,prns) = pr (f,length ss) (g,length ts) in if prns \ (\ t \ set ts. fst (lpo (Fun f ss) t)) then if prs then (True,True) else lex_ext lpo n ss ts else (False,False)))" end locale lpo_with_assms = precedence prc prl for prc :: "'f \ nat \ 'f \ nat \ bool \ bool" and prl :: "'f \ nat \ bool" and n :: nat begin sublocale wpo_with_assms n "{}" UNIV prc prl full_status "\ _. Lex" False "\ _. False" - by (unfold_locales, auto simp: refl_on_def trans_def simple_arg_pos_def) + by (unfold_locales, auto simp: refl_on_def trans_def simple_arg_pos_def irrefl_def) abbreviation "lpo_pr \ lpo prc prl n" abbreviation "lpo_s \ \ s t. fst (lpo_pr s t)" abbreviation "lpo_ns \ \ s t. snd (lpo_pr s t)" lemma lpo_eq_wpo: "lpo_pr s t = wpo s t" proof - note simps = wpo.simps show ?thesis proof (induct s t rule: lpo.induct[of _ prc prl n]) case (1 x y) then show ?case by (simp add: simps) next case (2 x g ts) then show ?case by (auto simp: simps) next case (3 f ss y) then show ?case by (auto simp: simps[of "Fun f ss" "Var y"] Let_def set_conv_nth) next case IH: (4 f ss g ts) have id: "\ s. (s \ {}) = False" "\ s. (s \ UNIV) = True" and "(\i\{0..si\set ss. wpo_ns si t)" by (auto, force simp: set_conv_nth) have id': "map ((!) ss) (\ (f, length ss)) = ss" for f ss by (intro nth_equalityI, auto) have ex: "(\i\set (\ (f, length ss)). wpo_ns (ss ! i) (Fun g ts)) = (\ si \ set ss. lpo_ns si (Fun g ts))" using IH(1) unfolding set_conv_nth by auto obtain prs prns where prc: "prc (f, length ss) (g, length ts) = (prs, prns)" by force have lex: "(Lex = Lex \ Lex = Lex) = True" by simp show ?case unfolding lpo.simps simps[of "Fun f ss" "Fun g ts"] term.simps id id' if_False if_True lex Let_def ex prc split proof (rule sym, rule if_cong[OF refl refl], rule if_cong[OF conj_cong[OF refl] if_cong[OF refl refl] refl]) assume "\ (\si\set ss. lpo_ns si (Fun g ts))" note IH = IH(2-)[OF this prc[symmetric] refl] from IH(1) show "(\j\set (\ (g, length ts)). wpo_s (Fun f ss) (ts ! j)) = (\t\set ts. lpo_s (Fun f ss) t)" unfolding set_conv_nth by auto assume "prns \ (\t\set ts. lpo_s (Fun f ss) t)" "\ prs" note IH = IH(2-)[OF this] show "lex_ext wpo n ss ts = lex_ext lpo_pr n ss ts" using IH by (intro lex_ext_cong, auto) qed qed qed abbreviation "LPO_S \ {(s,t). lpo_s s t}" abbreviation "LPO_NS \ {(s,t). lpo_ns s t}" theorem LPO_SN_order_pair: "SN_order_pair LPO_S LPO_NS" unfolding lpo_eq_wpo by (rule WPO_SN_order_pair) theorem LPO_S_subst: "(s,t) \ LPO_S \ (s \ \, t \ \) \ LPO_S" for \ :: "('f,'a)subst" using WPO_S_subst unfolding lpo_eq_wpo . theorem LPO_NS_subst: "(s,t) \ LPO_NS \ (s \ \, t \ \) \ LPO_NS" for \ :: "('f,'a)subst" using WPO_NS_subst unfolding lpo_eq_wpo . theorem LPO_NS_ctxt: "(s,t) \ LPO_NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ LPO_NS" using WPO_NS_ctxt unfolding lpo_eq_wpo . theorem LPO_S_ctxt: "(s,t) \ LPO_S \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ LPO_S" using WPO_S_ctxt unfolding lpo_eq_wpo by auto theorem LPO_S_subset_LPO_NS: "LPO_S \ LPO_NS" using WPO_S_subset_WPO_NS unfolding lpo_eq_wpo . theorem supt_subset_LPO_S: "{\} \ LPO_S" using supt_subset_WPO_S unfolding lpo_eq_wpo by auto theorem supteq_subset_LPO_NS: "{\} \ LPO_NS" using supteq_subset_WPO_NS unfolding lpo_eq_wpo by auto end end diff --git a/thys/Weighted_Path_Order/Precedence.thy b/thys/Weighted_Path_Order/Precedence.thy --- a/thys/Weighted_Path_Order/Precedence.thy +++ b/thys/Weighted_Path_Order/Precedence.thy @@ -1,43 +1,46 @@ subsection \Precedence\ text \A precedence consists of two compatible relations (strict and non-strict) on symbols such that the strict relation is strongly normalizing. In the formalization we model this via a function "prc" (precedence-compare) which returns two Booleans, indicating whether the one symbol is strictly or weakly bigger than the other symbol. Moreover, there also is a function "prl" (precedence-least) which gives quick access to whether a symbol is least in precedence, i.e., without comparing it to all other symbols explicitly.\ theory Precedence imports "Abstract-Rewriting.Abstract_Rewriting" begin -locale precedence = +locale irrefl_precedence = fixes prc :: "'f \ 'f \ bool \ bool" and prl :: "'f \ bool" assumes prc_refl: "prc f f = (False, True)" - and prc_SN: "SN {(f, g). fst (prc f g)}" + and prc_stri_imp_nstri: "fst (prc f g) \ snd (prc f g)" and prl: "prl g \ snd (prc f g) = True" and prl3: "prl f \ snd (prc f g) \ prl g" and prc_compat: "prc f g = (s1, ns1) \ prc g h = (s2, ns2) \ prc f h = (s, ns) \ (ns1 \ ns2 \ ns) \ (ns1 \ s2 \ s) \ (s1 \ ns2 \ s)" - and prc_stri_imp_nstri: "fst (prc f g) \ snd (prc f g)" begin - lemma prl2: assumes g: "prl g" shows "fst (prc g f) = False" proof (rule ccontr) assume "\ ?thesis" then obtain b where gf: "prc g f = (True, b)" by (cases "prc g f", auto) obtain b1 b2 where gg: "prc g g = (b1, b2)" by force obtain b' where fg: "prc f g = (b', True)" using prl[OF g, of f] by (cases "prc f g", auto) from prc_compat[OF gf fg gg] gg have gg: "fst (prc g g)" by auto - with SN_on_irrefl[OF prc_SN] show False by blast + with prc_refl[of g] show False by auto qed abbreviation "pr \ (prc, prl)" end +locale precedence = irrefl_precedence + + constrains prc :: "'f \ 'f \ bool \ bool" + and prl :: "'f \ bool" + assumes prc_SN: "SN {(f, g). fst (prc f g)}" + end diff --git a/thys/Weighted_Path_Order/RPO.thy b/thys/Weighted_Path_Order/RPO.thy --- a/thys/Weighted_Path_Order/RPO.thy +++ b/thys/Weighted_Path_Order/RPO.thy @@ -1,129 +1,129 @@ section \The Recursive Path Order as an instance of WPO\ text \This theory defines the recursive path order (RPO) that given two terms provides two Booleans, whether the terms can be strictly or non-strictly oriented. It is proven that RPO is an instance of WPO, and hence, carries over all the nice properties of WPO immediately.\ theory RPO imports WPO begin context fixes "pr" :: "'f \ nat \ 'f \ nat \ bool \ bool" and prl :: "'f \ nat \ bool" and c :: "'f \ nat \ order_tag" and n :: nat begin fun rpo :: "('f, 'v) term \ ('f, 'v) term \ bool \ bool" where "rpo (Var x) (Var y) = (False, x = y)" | "rpo (Var x) (Fun g ts) = (False, ts = [] \ prl (g,0))" | "rpo (Fun f ss) (Var y) = (let con = (\ s \ set ss. snd (rpo s (Var y))) in (con,con))" | "rpo (Fun f ss) (Fun g ts) = ( if (\ s \ set ss. snd (rpo s (Fun g ts))) then (True,True) else (let (prs,prns) = pr (f,length ss) (g,length ts) in if prns \ (\ t \ set ts. fst (rpo (Fun f ss) t)) then if prs then (True,True) else if c (f,length ss) = Lex \ c (g,length ts) = Lex then lex_ext rpo n ss ts else if c (f,length ss) = Mul \ c (g,length ts) = Mul then mul_ext rpo ss ts else (length ss \ 0 \ length ts = 0, length ts = 0) else (False,False)))" end locale rpo_with_assms = precedence prc prl for prc :: "'f \ nat \ 'f \ nat \ bool \ bool" and prl :: "'f \ nat \ bool" and c :: "'f \ nat \ order_tag" and n :: nat begin sublocale wpo_with_assms n "{}" UNIV prc prl full_status c False "\ _. False" - by (unfold_locales, auto simp: refl_on_def trans_def simple_arg_pos_def) + by (unfold_locales, auto simp: refl_on_def trans_def simple_arg_pos_def irrefl_def) abbreviation "rpo_pr \ rpo prc prl c n" abbreviation "rpo_s \ \ s t. fst (rpo_pr s t)" abbreviation "rpo_ns \ \ s t. snd (rpo_pr s t)" lemma rpo_eq_wpo: "rpo_pr s t = wpo s t" proof - note simps = wpo.simps show ?thesis proof (induct s t rule: rpo.induct[of _ prc prl c n]) case (1 x y) then show ?case by (simp add: simps) next case (2 x g ts) then show ?case by (auto simp: simps) next case (3 f ss y) then show ?case by (auto simp: simps[of "Fun f ss" "Var y"] Let_def set_conv_nth) next case IH: (4 f ss g ts) have id: "\ s. (s \ {}) = False" "\ s. (s \ UNIV) = True" and "(\i\{0..si\set ss. wpo_ns si t)" by (auto, force simp: set_conv_nth) have id': "map ((!) ss) (\ (f, length ss)) = ss" for f ss by (intro nth_equalityI, auto) have ex: "(\i\set (\ (f, length ss)). wpo_ns (ss ! i) (Fun g ts)) = (\ si \ set ss. rpo_ns si (Fun g ts))" using IH(1) unfolding set_conv_nth by auto obtain prs prns where prc: "prc (f, length ss) (g, length ts) = (prs, prns)" by force show ?case unfolding rpo.simps simps[of "Fun f ss" "Fun g ts"] term.simps id id' if_False if_True Let_def ex prc split proof (rule sym, rule if_cong[OF refl refl], rule if_cong[OF conj_cong[OF refl] if_cong[OF refl refl if_cong[OF refl _ if_cong]] refl]) assume "\ (\si\set ss. rpo_ns si (Fun g ts))" note IH = IH(2-)[OF this prc[symmetric] refl] from IH(1) show "(\j\set (\ (g, length ts)). wpo_s (Fun f ss) (ts ! j)) = (\t\set ts. rpo_s (Fun f ss) t)" unfolding set_conv_nth by auto assume "prns \ (\t\set ts. rpo_s (Fun f ss) t)" "\ prs" note IH = IH(2-)[OF this] { assume "c (f, length ss) = Lex \ c (g, length ts) = Lex" from IH(1)[OF this] show "lex_ext wpo n ss ts = lex_ext rpo_pr n ss ts" by (intro lex_ext_cong, auto) } { assume "\ (c (f, length ss) = Lex \ c (g, length ts) = Lex)" "c (f, length ss) = Mul \ c (g, length ts) = Mul" from IH(2)[OF this] show "mul_ext wpo ss ts = mul_ext rpo_pr ss ts" by (intro mul_ext_cong, auto) } qed auto qed qed abbreviation "RPO_S \ {(s,t). rpo_s s t}" abbreviation "RPO_NS \ {(s,t). rpo_ns s t}" theorem RPO_SN_order_pair: "SN_order_pair RPO_S RPO_NS" unfolding rpo_eq_wpo by (rule WPO_SN_order_pair) theorem RPO_S_subst: "(s,t) \ RPO_S \ (s \ \, t \ \) \ RPO_S" for \ :: "('f,'a)subst" using WPO_S_subst unfolding rpo_eq_wpo . theorem RPO_NS_subst: "(s,t) \ RPO_NS \ (s \ \, t \ \) \ RPO_NS" for \ :: "('f,'a)subst" using WPO_NS_subst unfolding rpo_eq_wpo . theorem RPO_NS_ctxt: "(s,t) \ RPO_NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ RPO_NS" using WPO_NS_ctxt unfolding rpo_eq_wpo . theorem RPO_S_ctxt: "(s,t) \ RPO_S \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ RPO_S" using WPO_S_ctxt unfolding rpo_eq_wpo by auto theorem RPO_S_subset_RPO_NS: "RPO_S \ RPO_NS" using WPO_S_subset_WPO_NS unfolding rpo_eq_wpo . theorem supt_subset_RPO_S: "{\} \ RPO_S" using supt_subset_WPO_S unfolding rpo_eq_wpo by auto theorem supteq_subset_RPO_NS: "{\} \ RPO_NS" using supteq_subset_WPO_NS unfolding rpo_eq_wpo by auto end end diff --git a/thys/Weighted_Path_Order/WPO.thy b/thys/Weighted_Path_Order/WPO.thy --- a/thys/Weighted_Path_Order/WPO.thy +++ b/thys/Weighted_Path_Order/WPO.thy @@ -1,1637 +1,1715 @@ section \The Weighted Path Order\ text \This is a version of WPO that also permits multiset comparisons of lists of terms. It therefore generalizes RPO.\ theory WPO imports Knuth_Bendix_Order.Lexicographic_Extension First_Order_Terms.Subterm_and_Context Knuth_Bendix_Order.Order_Pair Polynomial_Factorization.Missing_List Status Precedence Multiset_Extension2 + HOL.Zorn begin datatype order_tag = Lex | Mul locale wpo = fixes n :: nat and S NS :: "('f, 'v) term rel" and "prc" :: "('f \ nat \ 'f \ nat \ bool \ bool)" and prl :: "'f \ nat \ bool" and \\ :: "'f status" and c :: "'f \ nat \ order_tag" and ssimple :: bool and large :: "'f \ nat \ bool" begin fun wpo :: "('f, 'v) term \ ('f, 'v) term \ bool \ bool" where "wpo s t = (if (s,t) \ S then (True, True) else if (s,t) \ NS then (case s of Var x \ (False, (case t of Var y \ x = y | Fun g ts \ status \\ (g, length ts) = [] \ prl (g, length ts))) | Fun f ss \ if \ i \ set (status \\ (f, length ss)). snd (wpo (ss ! i) t) then (True, True) else (case t of Var _ \ (False, ssimple \ large (f, length ss)) | Fun g ts \ (case prc (f, length ss) (g, length ts) of (prs, prns) \ if prns \ (\ j \ set (status \\ (g, length ts)). fst (wpo s (ts ! j))) then if prs then (True, True) else let ss' = map (\ i. ss ! i) (status \\ (f, length ss)); ts' = map (\ i. ts ! i) (status \\ (g, length ts)); cf = c (f,length ss); cg = c (g,length ts) in if cf = Lex \ cg = Lex then lex_ext wpo n ss' ts' else if cf = Mul \ cg = Mul then mul_ext wpo ss' ts' else (length ss' \ 0 \ length ts' = 0, length ts' = 0) else (False, False)))) else (False, False))" declare wpo.simps [simp del] abbreviation wpo_s (infix "\" 50) where "s \ t \ fst (wpo s t)" abbreviation wpo_ns (infix "\" 50) where "s \ t \ snd (wpo s t)" abbreviation "WPO_S \ {(s,t). s \ t}" abbreviation "WPO_NS \ {(s,t). s \ t}" lemma wpo_s_imp_ns: "s \ t \ s \ t" using lex_ext_stri_imp_nstri unfolding wpo.simps[of s t] by (auto simp: Let_def mul_ext_stri_imp_nstri split: term.splits if_splits prod.splits) +lemma S_imp_wpo_s: "(s,t) \ S \ s \ t" by (simp add: wpo.simps) + end declare wpo.wpo.simps[code] definition strictly_simple_status :: "'f status \ ('f,'v)term rel \ bool" where "strictly_simple_status \ rel = (\ f ts i. i \ set (status \ (f,length ts)) \ (Fun f ts, ts ! i) \ rel)" -locale wpo_with_assms = wpo + - SN_order_pair + precedence + +definition trans_precedence where "trans_precedence prc = (\ f g h. + (fst (prc f g) \ snd (prc g h) \ fst (prc f h)) \ + (snd (prc f g) \ fst (prc g h) \ fst (prc f h)) \ + (snd (prc f g) \ snd (prc g h) \ snd (prc f h)))" + + + +locale wpo_with_basic_assms = wpo + + order_pair + irrefl_precedence + constrains S :: "('f, 'v) term rel" and NS :: _ and prc :: "'f \ nat \ 'f \ nat \ bool \ bool" and prl :: "'f \ nat \ bool" and ssimple :: bool and large :: "'f \ nat \ bool" and c :: "'f \ nat \ order_tag" and n :: nat and \\ :: "'f status" assumes subst_S: "(s,t) \ S \ (s \ \, t \ \) \ S" and subst_NS: "(s,t) \ NS \ (s \ \, t \ \) \ NS" - and ctxt_NS: "(s,t) \ NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ NS" + and irrefl_S: "irrefl S" and S_imp_NS: "S \ NS" - and ws_status: "i \ set (status \\ fn) \ simple_arg_pos NS fn i" + and ss_status: "ssimple \ i \ set (status \\ fn) \ simple_arg_pos S fn i" and large: "ssimple \ large fn \ fst (prc fn gm) \ snd (prc fn gm) \ status \\ gm = []" and large_trans: "ssimple \ large fn \ snd (prc gm fn) \ large gm" - and ss_status: "ssimple \ i \ set (status \\ fn) \ simple_arg_pos S fn i" and ss_S_non_empty: "ssimple \ S \ {}" begin +abbreviation "\ \ status \\" lemma ss_NS_not_UNIV: "ssimple \ NS \ UNIV" proof assume "ssimple" "NS = UNIV" with ss_S_non_empty obtain a b where "(a,b) \ S" "(b,a) \ NS" by auto from compat_S_NS_point[OF this] have "(a,a) \ S" . - with SN show False by fast + with irrefl_S show False unfolding irrefl_def by auto qed -abbreviation "\ \ status \\" - - lemmas \ = status[of \\] - -lemma NS_arg: assumes i: "i \ set (\ (f,length ts))" - shows "(Fun f ts, ts ! i) \ NS" - by (rule ws_status[OF i, unfolded simple_arg_pos_def fst_conv, rule_format], - insert \[of f "length ts"] i, auto) - -lemma NS_subterm: assumes all: "\ f k. set (\ (f,k)) = {0 ..< k}" - shows "s \ t \ (s,t) \ NS" -proof (induct s t rule: supteq.induct) - case (refl) - from refl_NS show ?case unfolding refl_on_def by blast -next - case (subt s ss t f) - from subt(1) obtain i where i: "i < length ss" and s: "s = ss ! i" unfolding set_conv_nth by auto - from NS_arg[of i f ss, unfolded all] s i have "(Fun f ss, s) \ NS" by auto - from trans_NS_point[OF this subt(3)] show ?case . -qed - - lemma \E: "i \ set (\ (f, length ss)) \ ss ! i \ set ss" by (rule status_aux) -lemma wpo_ns_refl: - shows "s \ s" -proof (induct s) - case (Fun f ss) - { - fix i - assume si: "i \ set (\ (f,length ss))" - from NS_arg[OF this] have "(Fun f ss, ss ! i) \ NS" . - with si Fun[OF \E[OF si]] have "wpo_s (Fun f ss) (ss ! i)" unfolding wpo.simps[of "Fun f ss" "ss ! i"] - by auto - } note wpo_s = this - let ?ss = "map (\ i. ss ! i) (\ (f,length ss))" - have rec11: "snd (lex_ext wpo n ?ss ?ss)" - by (rule all_nstri_imp_lex_nstri, insert \E[of _ f ss], auto simp: Fun) - have rec12: "snd (mul_ext wpo ?ss ?ss)" - unfolding mul_ext_def Let_def snd_conv - by (intro ns_mul_ext_refl_local, - unfold locally_refl_def, auto simp: in_multiset_in_set[of ?ss] intro!: Fun status_aux) - from rec11 rec12 show ?case using refl_NS_point prc_refl wpo_s - by (cases "c (f,length ss)", auto simp: wpo.simps[of "Fun f ss" "Fun f ss"]) -qed (simp add: wpo.simps refl_NS_point) - lemma wpo_ns_imp_NS: "s \ t \ (s,t) \ NS" using S_imp_NS by (cases s, auto simp: wpo.simps[of _ t], cases t, auto simp: refl_NS_point split: if_splits) lemma wpo_s_imp_NS: "s \ t \ (s,t) \ NS" by (rule wpo_ns_imp_NS[OF wpo_s_imp_ns]) -lemma S_imp_wpo_s: "(s,t) \ S \ s \ t" by (simp add: wpo.simps) - -lemma Var_not_S[simp]: "(Var x, t) \ S" -proof - assume st: "(Var x, t) \ S" - from SN_imp_minimal[OF SN, rule_format, of undefined UNIV] - obtain s where "\ u. (s,u) \ S" by blast - with subst_S[OF st, of "\ _. s"] - show False by auto -qed - lemma wpo_least_1: assumes "prl (f,length ss)" and "(t, Fun f ss) \ NS" and "\ (f,length ss) = []" shows "t \ Fun f ss" proof (cases t) case (Var x) with assms show ?thesis by (simp add: wpo.simps) next case (Fun g ts) let ?f = "(f,length ss)" let ?g = "(g,length ts)" obtain s ns where "prc ?g ?f = (s,ns)" by force with prl[OF assms(1), of ?g] have prc: "prc ?g ?f = (s,True)" by auto show ?thesis using assms(2) unfolding Fun unfolding wpo.simps[of "Fun g ts" "Fun f ss"] term.simps assms(3) by (auto simp: prc lex_ext_least_1 mul_ext_def ns_mul_ext_bottom Let_def) qed lemma wpo_least_2: assumes "prl (f,length ss)" (is "prl ?f") and "(Fun f ss, t) \ S" and "\ (f,length ss) = []" shows "\ Fun f ss \ t" proof (cases t) case (Var x) with Var show ?thesis using assms(2-3) by (auto simp: wpo.simps split: if_splits) next case (Fun g ts) let ?g = "(g,length ts)" obtain s ns where "prc ?f ?g = (s,ns)" by force with prl2[OF assms(1), of ?g] have prc: "prc ?f ?g = (False,ns)" by auto show ?thesis using assms(2) assms(3) unfolding Fun by (simp add: wpo.simps[of _ "Fun g ts"] lex_ext_least_2 prc mul_ext_def s_mul_ext_bottom_strict Let_def) qed - lemma wpo_least_3: assumes "prl (f,length ss)" (is "prl ?f") and ns: "Fun f ss \ t" and NS: "(u, Fun f ss) \ NS" and ss: "\ (f,length ss) = []" and S: "\ x. (Fun f ss, x) \ S" and u: "u = Var x" shows "u \ t" proof (cases "(Fun f ss, t) \ S \ (u, Fun f ss) \ S \ (u, t) \ S") case True with wpo_ns_imp_NS[OF ns] NS compat_NS_S_point compat_S_NS_point have "(u, t) \ S" by blast from wpo_s_imp_ns[OF S_imp_wpo_s[OF this]] show ?thesis . next case False from trans_NS_point[OF NS wpo_ns_imp_NS[OF ns]] have utA: "(u, t) \ NS" . show ?thesis proof (cases t) case t: (Var y) with ns False ss have *: "ssimple" "large (f,length ss)" by (auto simp: wpo.simps split: if_splits) show ?thesis proof (cases "x = y") case True thus ?thesis using ns * False utA ss unfolding wpo.simps[of u t] wpo.simps[of "Fun f ss" t] unfolding t u term.simps by (auto split: if_splits) next case False from utA[unfolded t u] have "(Var x, Var y) \ NS" . from False subst_NS[OF this, of "\ z. if z = x then v else w" for v w] have "(v,w) \ NS" for v w by auto hence "NS = UNIV" by auto with ss_NS_not_UNIV[OF \ssimple\] have False by auto thus ?thesis .. qed next case (Fun g ts) let ?g = "(g,length ts)" obtain s ns where "prc ?f ?g = (s,ns)" by force with prl2[OF \prl ?f\, of ?g] have prc: "prc ?f ?g = (False,ns)" by auto show ?thesis proof (cases "\ ?g") case Nil with False Fun assms prc have "prc ?f ?g = (False,True)" by (auto simp: wpo.simps split: if_splits) with prl3[OF \prl ?f\, of ?g] have "prl ?g" by auto show ?thesis using utA unfolding Fun by (rule wpo_least_1[OF \prl ?g\], simp add: Nil) next case (Cons t1 tts) have "\ wpo_s (Fun f ss) (ts ! t1)" by (rule wpo_least_2[OF \prl ?f\ S ss]) with \wpo_ns (Fun f ss) t\ False Fun Cons have False by (simp add: ss wpo.simps split: if_splits) then show ?thesis .. qed qed qed (* Transitivity / compatibility of the orders *) -lemma wpo_compat: " - (s \ t \ t \ u \ s \ u) \ +lemma wpo_compat': assumes SN: "\ f. prl f \ SN S" (* it is not clear whether this is really required *) + shows "(s \ t \ t \ u \ s \ u) \ (s \ t \ t \ u \ s \ u) \ (s \ t \ t \ u \ s \ u)" (is "?tran s t u") proof (induct "(s,t,u)" arbitrary: s t u rule: wf_induct[OF wf_measures[of "[\ (s,t,u). size s, \ (s,t,u). size t, \ (s,t,u). size u]"]]) case 1 note ind = 1[simplified] show "?tran s t u" proof (cases "(s,t) \ S \ (t,u) \ S \ (s,u) \ S") case True { assume st: "wpo_ns s t" and tu: "wpo_ns t u" from wpo_ns_imp_NS[OF st] wpo_ns_imp_NS[OF tu] True compat_NS_S_point compat_S_NS_point have "(s,u) \ S" by blast from S_imp_wpo_s[OF this] have "wpo_s s u" . } with wpo_s_imp_ns show ?thesis by blast next case False then have stS: "(s,t) \ S" and tuS: "(t,u) \ S" and suS: "(s,u) \ S" by auto show ?thesis proof (cases t) note [simp] = wpo.simps[of s u] wpo.simps[of s t] wpo.simps[of t u] case (Var x) note wpo.simps[simp] show ?thesis proof safe assume "wpo_s t u" with Var tuS show "wpo_s s u" by (auto split: if_splits) next assume gr: "wpo_s s t" and ge: "wpo_ns t u" from wpo_s_imp_NS[OF gr] have stA: "(s,t) \ NS" . from wpo_ns_imp_NS[OF ge] have tuA: "(t,u) \ NS" . from trans_NS_point[OF stA tuA] have suA: "(s,u) \ NS" . show "wpo_s s u" proof (cases u) case (Var y) with ge \t = Var x\ tuS have "t = u" by (auto split: if_splits) with gr show ?thesis by auto next case (Fun h us) let ?h = "(h,length us)" from Fun ge Var tuS have us: "\ ?h = []" and pri: "prl ?h" by (auto split: if_splits) - from gr Var tuS obtain f ss where s: "s = Fun f ss" by (cases s, auto split: if_splits) + from gr Var tuS ge stS obtain f ss where s: "s = Fun f ss" by (cases s, auto split: if_splits) let ?f = "(f,length ss)" from s gr Var False obtain i where i: "i \ set (\ ?f)" and sit: "ss ! i \ t" by (auto split: if_splits) from trans_NS_point[OF wpo_ns_imp_NS[OF sit] tuA] have siu: "(ss ! i,u) \ NS" . from wpo_least_1[OF pri siu[unfolded Fun us] us] have "ss ! i \ u" unfolding Fun us . with i have "\ i \ set (\ ?f). ss ! i \ u" by blast with s suA show ?thesis by simp qed next assume ge1: "wpo_ns s t" and ge2: "wpo_ns t u" show "wpo_ns s u" proof (cases u) case (Var y) - with ge2 \t = Var x\ have "t = u" by (auto split: if_splits) + with ge2 \t = Var x\ tuS have "t = u" by (auto split: if_splits) with ge1 show ?thesis by auto next case (Fun h us) let ?h = "(h,length us)" - from Fun ge2 Var have us: "\ ?h = []" and pri: "prl ?h" by (auto split: if_splits) + from Fun ge2 Var tuS have us: "\ ?h = []" and pri: "prl ?h" by (auto split: if_splits) show ?thesis unfolding Fun us by (rule wpo_least_1[OF pri trans_NS_point[OF wpo_ns_imp_NS[OF ge1] wpo_ns_imp_NS[OF ge2[unfolded Fun us]]] us]) qed qed next case (Fun g ts) let ?g = "(g,length ts)" let ?ts = "set (\ ?g)" let ?t = "Fun g ts" from Fun have t: "t = ?t" . show ?thesis proof (cases s) case (Var x) show ?thesis proof safe assume gr: "wpo_s s t" - with Var Fun show "wpo_s s u" by (auto simp: wpo.simps split: if_splits) + with Var Fun stS show "wpo_s s u" by (auto simp: wpo.simps split: if_splits) next assume ge: "wpo_ns s t" and gr: "wpo_s t u" - with Var Fun have pri: "prl ?g" and "\ ?g = []" by (auto simp: wpo.simps split: if_splits) + with Var Fun stS have pri: "prl ?g" and "\ ?g = []" by (auto simp: wpo.simps split: if_splits) with gr Fun show "wpo_s s u" using wpo_least_2[OF pri, of u] False by auto next assume ge1: "wpo_ns s t" and ge2: "wpo_ns t u" - with Var Fun have pri: "prl ?g" and empty: "\ ?g = []" by (auto simp: wpo.simps split: if_splits) + with Var Fun stS have pri: "prl ?g" and empty: "\ ?g = []" by (auto simp: wpo.simps split: if_splits) from wpo_ns_imp_NS[OF ge1] Var Fun empty have ns: "(Var x, Fun g ts) \ NS" by simp show "wpo_ns s u" proof (rule wpo_least_3[OF pri ge2[unfolded Fun empty] wpo_ns_imp_NS[OF ge1[unfolded Fun empty]] empty _ Var], rule) fix v assume S: "(Fun g ts, v) \ S" + from compat_NS_S_point[OF ns S] have xv: "(Var x, v) \ S" . + from assms[OF pri] have SN: "SN S" . from SN_imp_minimal[OF SN, rule_format, of undefined UNIV] obtain s where "\ u. (s,u) \ S" by blast - with compat_NS_S_point[OF subst_NS[OF ns, of "\ _. s"] subst_S[OF S, of "\ _. s"]] + with subst_S[OF xv, of "\ _. s"] show False by auto qed qed next case (Fun f ss) let ?s = "Fun f ss" let ?f = "(f,length ss)" let ?ss = "set (\ ?f)" from Fun have s: "s = ?s" . let ?s1 = "\ i \ ?ss. ss ! i \ t" let ?t1 = "\ j \ ?ts. ts ! j \ u" let ?ls = "length ss" let ?lt = "length ts" obtain ps pns where prc: "prc ?f ?g = (ps,pns)" by force let ?tran2 = "\ a b c. ((wpo_ns a b) \ (wpo_s b c) \ (wpo_s a c)) \ ((wpo_s a b) \ (wpo_ns b c) \ (wpo_s a c)) \ ((wpo_ns a b) \ (wpo_ns b c) \ (wpo_ns a c)) \ ((wpo_s a b) \ (wpo_s b c) \ (wpo_s a c))" from s have "\ s' \ set ss. size s' < size s" by (auto simp: size_simps) with ind have ind2: "\ s' t' u'. \s' \ set ss\ \ ?tran s' t' u'" by blast with wpo_s_imp_ns have ind3: "\ us s' t' u'. \s' \ set ss; t' \ set ts\ \ ?tran2 s' t' u'" by blast let ?mss = "map (\ i. ss ! i) (\ ?f)" let ?mts = "map (\ j. ts ! j) (\ ?g)" have ind3': "\ us s' t' u'. \s' \ set ?mss; t' \ set ?mts\ \ ?tran2 s' t' u'" by (rule ind3, auto simp: status_aux) { assume ge1: "s \ t" and ge2: "t \ u" from wpo_ns_imp_NS[OF ge1] have stA: "(s,t) \ NS" . from wpo_s_imp_NS[OF ge2] have tuA: "(t,u) \ NS" . from trans_NS_point[OF stA tuA] have suA: "(s,u) \ NS" . have "s \ u" proof (cases ?s1) case True from this obtain i where i: "i \ ?ss" and ges: "ss ! i \ t" by auto from \E[OF i] have s': "ss ! i \ set ss" . with i s s' ind2[of "ss ! i" t u, simplified] ges ge2 have "ss ! i \ u" by auto then have "ss ! i \ u" by (rule wpo_s_imp_ns) with i s suA show ?thesis by (cases u, auto simp: wpo.simps split: if_splits) next case False show ?thesis proof (cases ?t1) case True from this obtain j where j: "j \ ?ts" and ges: "ts ! j \ u" by auto from \E[OF j] have t': "ts ! j \ set ts" by auto from j t' t stS False ge1 s have ge1': "s \ ts ! j" unfolding wpo.simps[of s t] by (auto split: if_splits prod.splits) from t' s t ge1' ges ind[rule_format, of s "ts ! j" u, simplified] show "s \ u" using suA size_simps supt.intros unfolding wpo.simps[of s u] by (auto split: if_splits) next case False from t this ge2 tuS obtain h us where u: "u = Fun h us" by (cases u, auto simp: wpo.simps split: if_splits) let ?u = "Fun h us" let ?h = "(h,length us)" let ?us = "set (\ ?h)" let ?mus = "map (\ k. us ! k) (\ ?h)" from s t u ge1 ge2 have ge1: "?s \ ?t" and ge2: "?t \ ?u" by auto from stA stS s t have stAS: "((?s,?t) \ S) = False" "((?s,?t) \ NS) = True" by auto from tuA tuS t u have tuAS: "((?t,?u) \ S) = False" "((?t,?u) \ NS) = True" by auto note ge1 = ge1[unfolded wpo.simps[of ?s ?t] stAS, simplified] note ge2 = ge2[unfolded wpo.simps[of ?t ?u] tuAS, simplified] obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force from \\ ?s1\ t ge1 have st': "\ j \ ?ts. ?s \ ts ! j" by (auto split: if_splits prod.splits) from \\ ?t1\ t u ge2 tuS have tu': "\ k \ ?us. ?t \ us ! k" by (auto split: if_splits prod.splits) from \\ ?s1\ s t ge1 stS st' have fg: "pns" by (cases ?thesis, auto simp: prc) from \\ ?t1\ u ge2 tu' have gh: "pns2" by (cases ?thesis, auto simp: prc2) from \\ ?s1\ have "?s1 = False" by simp note ge1 = ge1[unfolded this[unfolded t] if_False term.simps prc split] from \\ ?t1\ have "?t1 = False" by simp note ge2 = ge2[unfolded this[unfolded u] if_False term.simps prc2 split] note compat = prc_compat[OF prc prc2 prc3] from fg gh compat have fh: "pns3" by simp { fix k assume k: "k \ ?us" from \E[OF this] have "size (us ! k) < size u" unfolding u using size_simps by auto with tu'[folded t] \s \ t\ ind[rule_format, of s t "us ! k"] k have "s \ us ! k" by blast } note su' = this show ?thesis proof (cases ps3) case True with su' s u fh prc3 suA show ?thesis by (auto simp: wpo.simps) next case False from False fg gh compat have nfg: "\ ps" and ngh: "\ ps2" and *: "ps = False" "ps2 = False" by blast+ note ge1 = ge1[unfolded * if_False] note ge2 = ge2[unfolded * if_False] show ?thesis proof (cases "c ?f") case Mul note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this from ge1[unfolded cf cg] have mul1: "snd (mul_ext wpo ?mss ?mts)" by (auto split: if_splits) from ge2[unfolded cg ch] have mul2: "fst (mul_ext wpo ?mts ?mus)" by (auto split: if_splits) from mul1 mul2 mul_ext_compat[OF ind3', of ?mss ?mts ?mus] have "fst (mul_ext wpo ?mss ?mus)" by auto with s u fh su' prc3 cf ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this from gh u ge2 tu' prc2 ngh cg ch have us_e: "?mus = []" by simp from gh u ge2 tu' prc2 ngh cg ch have ts_ne: "?mts \ []" by (auto split: if_splits) from ns_mul_ext_bottom_uniqueness[of "mset ?mts"] have "\f. snd (mul_ext f [] ?mts) \ ?mts = []" unfolding mul_ext_def by (simp add: Let_def) with ts_ne fg \\ ?s1\ t ge1 st' prc nfg cf cg have ss_ne: "?mss \ []" by (cases ss) auto from us_e ss_ne s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed next case Lex note cg = this from fg \\ ?s1\ t ge1 st' prc nfg cf cg have ts_e: "?mts = []" by simp with gh \\ ?t1\ u ge2 tu' prc2 ngh cg show ?thesis by (cases "c ?h") (simp_all add: lex_ext_least_2) qed next case Lex note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this from fg \\ ?s1\ t ge1 st' prc nfg cf cg have ts_e: "?mts = []" by simp with gh \\ ?t1\ u ge2 tu' prc2 ngh cg show ?thesis by (cases "c ?h") (auto simp: Let_def s_mul_ext_def s_mul_ext_bottom mul_ext_def elim: mult2_alt_sE) next case Lex note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this from gh u ge2 tu' ngh cg ch have us_e: "?mus = []" by simp from gh u ge2 tu' ngh cg ch have ts_ne: "?mts \ []" by simp from lex_ext_iff[of _ _ "[]" ?mts] have "\f. snd (lex_ext f n [] ?mts) \ ?mts = []" by simp with ts_ne fg t ge1 st' nfg cf cg have ss_ne: "?mss \ []" by auto from us_e ss_ne s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this from fg t ge1 st' nfg cf cg have lex1: "snd (lex_ext wpo n ?mss ?mts)" by auto from gh u ge2 tu' ngh cg ch have lex2: "fst (lex_ext wpo n ?mts ?mus)" by auto from lex1 lex2 lex_ext_compat[OF ind3', of ?mss ?mts ?mus] have "fst (lex_ext wpo n ?mss ?mus)" by auto with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed qed qed qed qed qed } moreover { assume ge1: "s \ t" and ge2: "t \ u" from wpo_s_imp_NS[OF ge1] have stA: "(s,t) \ NS" . from wpo_ns_imp_NS[OF ge2] have tuA: "(t,u) \ NS" . from trans_NS_point[OF stA tuA] have suA: "(s,u) \ NS" . have "s \ u" proof (cases ?s1) case True from True obtain i where i: "i \ ?ss" and ges: "ss ! i \ t" by auto from \E[OF i] have s': "ss ! i \ set ss" by auto with s s' ind2[of "ss ! i" t u, simplified] ges ge2 have "ss ! i \ u" by auto with i s' s suA show ?thesis by (cases u, auto simp: wpo.simps split: if_splits) next case False show ?thesis proof (cases ?t1) case True from this obtain j where j: "j \ ?ts" and ges: "ts ! j \ u" by auto from \E[OF j] have t': "ts ! j \ set ts" . from j t' t stS False ge1 s have ge1': "s \ ts ! j" unfolding wpo.simps[of s t] by (auto split: if_splits prod.splits) from t' s t ge1' ges ind[rule_format, of s "ts ! j" u, simplified] show "s \ u" using suA size_simps supt.intros unfolding wpo.simps[of s u] by (auto split: if_splits) next case False show ?thesis proof (cases u) case u: (Fun h us) let ?u = "Fun h us" let ?h = "(h,length us)" let ?us = "set (\ ?h)" let ?mss = "map (\ i. ss ! i) (\ ?f)" let ?mts = "map (\ j. ts ! j) (\ ?g)" let ?mus = "map (\ k. us ! k) (\ ?h)" note \E = \E[of _ f ss] \E[of _ g ts] \E[of _ h us] from s t u ge1 ge2 have ge1: "?s \ ?t" and ge2: "?t \ ?u" by auto from stA stS s t have stAS: "((?s,?t) \ S) = False" "((?s,?t) \ NS) = True" by auto from tuA tuS t u have tuAS: "((?t,?u) \ S) = False" "((?t,?u) \ NS) = True" by auto note ge1 = ge1[unfolded wpo.simps[of ?s ?t] stAS, simplified] note ge2 = ge2[unfolded wpo.simps[of ?t ?u] tuAS, simplified] let ?lu = "length us" obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force from \\ ?s1\ t ge1 have st': "\ j \ ?ts. ?s \ ts ! j" by (auto split: if_splits prod.splits) from \\ ?t1\ t u ge2 tuS have tu': "\ k \ ?us. ?t \ us ! k" by (auto split: if_splits prod.splits) from \\ ?s1\ s t ge1 stS st' have fg: "pns" by (cases ?thesis, auto simp: prc) from \\ ?t1\ u ge2 tu' have gh: "pns2" by (cases ?thesis, auto simp: prc2) from \\ ?s1\ have "?s1 = False" by simp note ge1 = ge1[unfolded this[unfolded t] if_False term.simps prc split] from \\ ?t1\ have "?t1 = False" by simp note ge2 = ge2[unfolded this[unfolded u] if_False term.simps prc2 split] note compat = prc_compat[OF prc prc2 prc3] from fg gh compat have fh: "pns3" by simp { fix k assume k: "k \ ?us" from \E(3)[OF this] have "size (us ! k) < size u" unfolding u using size_simps by auto with tu'[folded t] wpo_s_imp_ns[OF \s \ t\] ind[rule_format, of s t "us ! k"] k have "s \ us ! k" by blast } note su' = this show ?thesis proof (cases ps3) case True with su' s u fh prc3 suA show ?thesis by (auto simp: wpo.simps) next case False from False fg gh compat have nfg: "\ ps" and ngh: "\ ps2" and *: "ps = False" "ps2 = False" by blast+ note ge1 = ge1[unfolded * if_False] note ge2 = ge2[unfolded * if_False] show ?thesis proof (cases "c ?f") case Mul note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this from fg t ge1 st' nfg cf cg have mul1: "fst (mul_ext wpo ?mss ?mts)" by auto from gh u ge2 tu' ngh cg ch have mul2: "snd (mul_ext wpo ?mts ?mus)" by auto from mul1 mul2 mul_ext_compat[OF ind3', of ?mss ?mts ?mus] have "fst (mul_ext wpo ?mss ?mus)" by auto with s u fh su' prc3 cf ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this from gh u ge2 tu' ngh cg ch have us_e: "?mus = []" by simp from fg t ge1 st' nfg cf cg s_mul_ext_bottom_strict have ss_ne: "?mss \ []" by (cases ?mss) (auto simp: Let_def mul_ext_def) from us_e ss_ne s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed next case Lex note cg = this from fg t ge1 st' prc nfg cf cg s_mul_ext_bottom_strict have ss_ne: "?mss \ []" by (auto simp: mul_ext_def) from fg t ge1 st' nfg cf cg have ts_e: "?mts = []" by simp show ?thesis proof (cases "c ?h") case Mul note ch = this with gh u ge2 tu' ngh cg ch ns_mul_ext_bottom_uniqueness have "?mus = []" by simp with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom suA show ?thesis unfolding wpo.simps[of s u] by (simp add: Let_def mul_ext_def s_mul_ext_def mult2_alt_s_def) next case Lex note ch = this from lex_ext_iff[of _ _ "[]" ?mus] have "\f. snd (lex_ext f n [] ?mus) \ ?mus = []" by simp with ts_e gh u ge2 tu' ngh cg ch have "?mus = []" by simp with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom suA show ?thesis unfolding wpo.simps[of s u] by (simp add: mul_ext_def) qed qed next case Lex note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this from fg t ge1 st' nfg cf cg have ss_ne: "?mss \ []" by simp from fg t ge1 st' nfg cf cg have ts_e: "?mts = []" by simp show ?thesis proof (cases "c ?h") case Mul note ch = this from ts_e gh u ge2 tu' ngh cg ch ns_mul_ext_bottom_uniqueness[of "mset ?mus"] have "?mus = []" by (simp add: mul_ext_def Let_def) with ss_ne s u fh su' prc3 cf cg ch s_mul_ext_bottom suA show ?thesis unfolding wpo.simps[of s u] by (simp add: mul_ext_def) next case Lex note ch = this from gh u ge2 tu' prc2 ngh cg ch have "?mus = []" by simp with ss_ne s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by (simp add: lex_ext_iff) qed next case Lex note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this from gh u ge2 tu' ngh cg ch have us_e: "?mus = []" by simp have "\f. fst (lex_ext f n ?mss ?mts) \ ?mss \ []" by (cases ?mss) (simp_all add: lex_ext_iff) with fg t ge1 st' prc nfg cf cg have ss_ne: "?mss \ []" by simp with us_e s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this from fg t ge1 st' nfg cf cg have lex1: "fst (lex_ext wpo n ?mss ?mts)" by auto from gh u ge2 tu' ngh cg ch have lex2: "snd (lex_ext wpo n ?mts ?mus)" by auto from lex1 lex2 lex_ext_compat[OF ind3', of ?mss ?mts ?mus] have "fst (lex_ext wpo n ?mss ?mus)" by auto with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed qed qed qed next case (Var z) from ge2 \\ ?t1\ tuS have "ssimple" "large ?g" unfolding Var t by (auto simp: wpo.simps split: if_splits) from large[OF this, of ?f] have large: "fst (prc ?g ?f) \ snd (prc ?g ?f) \ \ ?f = []" by auto obtain fgs fgns where prc_fg: "prc ?f ?g = (fgs,fgns)" by (cases "prc ?f ?g", auto) from ge1 \\ ?s1\ stS have weak_fg: "snd (prc ?f ?g)" unfolding s t using prc_fg by (auto simp: wpo.simps split: if_splits) - from refl_not_SN[of ?f] prc_SN have prc_irrefl: "\ fst (prc ?f ?f)" by auto + have prc_irrefl: "\ fst (prc ?f ?f)" using prc_refl by simp from large have False proof assume "fst (prc ?g ?f)" with weak_fg have "fst (prc ?f ?f)" by (metis prc_compat prod.collapse) with prc_irrefl show False by auto next assume weak: "snd (prc ?g ?f) \ \ ?f = []" let ?mss = "map (\ i. ss ! i) (\ ?f)" let ?mts = "map (\ j. ts ! j) (\ ?g)" { assume "fst (prc ?f ?g)" with weak have "fst (prc ?f ?f)" by (metis prc_compat prod.collapse) with prc_irrefl have False by auto } hence "\ fst (prc ?f ?g)" by auto with ge1 \\ ?s1\ stS prc_fg have "fst (lex_ext wpo n ?mss ?mts) \ fst (mul_ext wpo ?mss ?mts) \ ?mss \ []" unfolding wpo.simps[of s t] unfolding s t by (auto simp: Let_def split: if_splits) with weak have "fst (lex_ext wpo n [] ?mts) \ fst (mul_ext wpo [] ?mts)" by auto thus False using lex_ext_least_2 by (auto simp: mul_ext_def Let_def s_mul_ext_bottom_strict) qed thus ?thesis .. qed qed qed } moreover { assume ge1: "s \ t" and ge2: "t \ u" and ngt1: "\ s \ t" and ngt2: "\ t \ u" from wpo_ns_imp_NS[OF ge1] have stA: "(s,t) \ NS" . from wpo_ns_imp_NS[OF ge2] have tuA: "(t,u) \ NS" . from trans_NS_point[OF stA tuA] have suA: "(s,u) \ NS" . from ngt1 stA have "\ ?s1" unfolding s t by (auto simp: wpo.simps split: if_splits) from ngt2 tuA have "\ ?t1" unfolding t by (cases u, auto simp: wpo.simps split: if_splits) have "s \ u" proof (cases u) case u: (Var x) from t \\ ?t1\ ge2 tuA ngt2 have large: "ssimple" "large ?g" unfolding u by (auto simp: wpo.simps split: if_splits) from s t ngt1 ge1 have "snd (prc ?f ?g)" by (auto simp: wpo.simps split: if_splits prod.splits) from large_trans[OF large this] suA large show ?thesis unfolding wpo.simps[of s u] using s u by auto next case u: (Fun h us) let ?u = "Fun h us" let ?h = "(h,length us)" let ?us = "set (\ ?h)" let ?mss = "map (\ i. ss ! i) (\ ?f)" let ?mts = "map (\ j. ts ! j) (\ ?g)" let ?mus = "map (\ k. us ! k) (\ ?h)" from s t u ge1 ge2 have ge1: "?s \ ?t" and ge2: "?t \ ?u" by auto from stA stS s t have stAS: "((?s,?t) \ S) = False" "((?s,?t) \ NS) = True" by auto from tuA tuS t u have tuAS: "((?t,?u) \ S) = False" "((?t,?u) \ NS) = True" by auto note ge1 = ge1[unfolded wpo.simps[of ?s ?t] stAS, simplified] note ge2 = ge2[unfolded wpo.simps[of ?t ?u] tuAS, simplified] from s t u ngt1 ngt2 have ngt1: "\ ?s \ ?t" and ngt2: "\ ?t \ ?u" by auto note ngt1 = ngt1[unfolded wpo.simps[of ?s ?t] stAS, simplified] note ngt2 = ngt2[unfolded wpo.simps[of ?t ?u] tuAS, simplified] from \\ ?s1\ t ge1 have st': "\ j \ ?ts. ?s \ ts ! j" by (cases ?thesis, auto) from \\ ?t1\ u ge2 have tu': "\ k \ ?us. ?t \ us ! k" by (cases ?thesis, auto) let ?lu = "length us" obtain ps2 pns2 where prc2: "prc ?g ?h = (ps2,pns2)" by force obtain ps3 pns3 where prc3: "prc ?f ?h = (ps3,pns3)" by force from \\ ?s1\ t ge1 st' have fg: "pns" by (cases ?thesis, auto simp: prc) from \\ ?t1\ u ge2 tu' have gh: "pns2" by (cases ?thesis, auto simp: prc2) note compat = prc_compat[OF prc prc2 prc3] from \\ ?s1\ have "?s1 = False" by simp note ge1 = ge1[unfolded this[unfolded t] if_False term.simps prc split] from \\ ?t1\ have "?t1 = False" by simp note ge2 = ge2[unfolded this[unfolded u] if_False term.simps prc2 split] from compat fg gh have fh: pns3 by blast { fix k assume k: "k \ ?us" from \E[OF this] have "size (us ! k) < size u" unfolding u using size_simps by auto with tu'[folded t] \s \ t\ ind[rule_format, of s t "us ! k"] k have "s \ us ! k" by blast } note su' = this from \\ ?s1\ st' ge1 ngt1 s t have nfg: "\ ps" by (simp, cases ?thesis, simp, cases ps, auto simp: prc fg) from \\ ?t1\ tu' ge2 ngt2 t u have ngh: "\ ps2" by (simp, cases ?thesis, simp, cases ps2, auto simp: prc2 gh) show "s \ u" proof (cases "c ?f") case Mul note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this from fg t ge1 st' nfg cf cg have mul1: "snd (mul_ext wpo ?mss ?mts)" by auto from gh u ge2 tu' ngh cg ch have mul2: "snd (mul_ext wpo ?mts ?mus)" by auto from mul1 mul2 mul_ext_compat[OF ind3', of ?mss ?mts ?mus] have "snd (mul_ext wpo ?mss ?mus)" by auto with s u fh su' prc3 cf ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this from gh u ge2 tu' ngh cg ch have us_e: "?mus = []" by simp with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed next case Lex note cg = this from fg t ge1 st' nfg cf cg have ts_e: "?mts = []" by simp show ?thesis proof (cases "c ?h") case Mul note ch = this with gh u ge2 tu' ngh cg ch have "?mus = []" by simp with s u fh su' prc3 cf cg ch ns_mul_ext_bottom suA show ?thesis unfolding wpo.simps[of s u] by (simp add: ns_mul_ext_def mul_ext_def Let_def mult2_alt_ns_def) next case Lex note ch = this have "\f. snd (lex_ext f n [] ?mus) \ ?mus = []" by (simp_all add: lex_ext_iff) with ts_e gh u ge2 tu' ngh cg ch have "?mus = []" by simp with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp qed qed next case Lex note cf = this show ?thesis proof (cases "c ?g") case Mul note cg = this from fg t ge1 st' prc nfg cf cg have ts_e: "?mts = []" by simp show ?thesis proof (cases "c ?h") case Mul note ch = this with ts_e gh u ge2 tu' ngh cg ch ns_mul_ext_bottom_uniqueness[of "mset ?mus"] have "?mus = []" by (simp add: Let_def mul_ext_def) with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by simp next case Lex note ch = this with gh u ge2 tu' prc2 ngh cg ch have "?mus = []" by simp with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by (simp add: lex_ext_least_1) qed next case Lex note cg = this show ?thesis proof (cases "c ?h") case Mul note ch = this with gh u ge2 tu' ngh cg ch have "?mus = []" by simp with s u fh su' prc3 cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by (simp add: lex_ext_least_1) next case Lex note ch = this from st' ge1 s t fg nfg cf cg have lex1: "snd (lex_ext wpo n ?mss ?mts)" by (auto simp: prc) from tu' ge2 t u gh ngh cg ch have lex2: "snd (lex_ext wpo n ?mts ?mus)" by (auto simp: prc2) from lex1 lex2 lex_ext_compat[OF ind3', of ?mss ?mts ?mus] have "snd (lex_ext wpo n ?mss ?mus)" by auto with fg gh su' s u fh cf cg ch suA show ?thesis unfolding wpo.simps[of s u] by (auto simp: prc3) qed qed qed qed } ultimately show ?thesis using wpo_s_imp_ns by auto qed qed qed qed -lemma subterm_wpo_s_arg: assumes i: "i \ set (\ (f,length ss))" - shows "Fun f ss \ ss ! i" -proof - - have refl: "ss ! i \ ss ! i" by (rule wpo_ns_refl) - with i have "\ t \ set (\ (f,length ss)). ss ! i \ ss ! i" by auto - with NS_arg[OF i] i - show ?thesis by (auto simp: wpo.simps split: if_splits) -qed - -lemma subterm_wpo_ns_arg: assumes i: "i \ set (\ (f,length ss))" - shows "Fun f ss \ ss ! i" - by (rule wpo_s_imp_ns[OF subterm_wpo_s_arg[OF i]]) +context + assumes ssimple: "strictly_simple_status \\ NS" +begin +lemma NS_arg': + assumes i: "i \ set (\ (f,length ts))" + shows "(Fun f ts, ts ! i) \ NS" + using assms ssimple unfolding simple_arg_pos_def strictly_simple_status_def by simp -lemma wpo_ns_pre_mono: fixes f and bef aft :: "('f,'v)term list" - defines "\f \ \ (f, Suc (length bef + length aft))" - assumes rel: "(wpo_ns s t)" - shows "(\j\set \f. Fun f (bef @ s # aft) \ (bef @ t # aft) ! j) - \ (Fun f (bef @ s # aft), (Fun f (bef @ t # aft))) \ NS - \ (\ i < length \f. ((map ((!) (bef @ s # aft)) \f) ! i) \ ((map ((!) (bef @ t # aft)) \f) ! i))" - (is "_ \ _ \ ?three") -proof - - let ?ss = "bef @ s # aft" - let ?ts = "bef @ t # aft" - let ?s = "Fun f ?ss" - let ?t = "Fun f ?ts" - let ?len = "Suc (length bef + length aft)" - let ?f = "(f, ?len)" - let ?\ = "\ ?f" - from wpo_ns_imp_NS[OF rel] have stA: "(s,t) \ NS" . - have ?three unfolding \f_def - proof (intro allI impI) +lemma wpo_ns_refl': + shows "s \ s" +proof (induct s) + case (Fun f ss) + { fix i - assume "i < length ?\" - then have id: "\ ss. (map ((!) ss) ?\) ! i = ss ! (?\ ! i)" by auto - show "wpo_ns ((map ((!) ?ss) ?\) ! i) ((map ((!) ?ts) ?\) ! i)" - proof (cases "?\ ! i = length bef") - case True - then show ?thesis unfolding id using rel by auto - next - case False - from append_Cons_nth_not_middle[OF this, of s aft t] wpo_ns_refl - show ?thesis unfolding id by auto - qed - qed - have "\j\set ?\. wpo_s ?s ((bef @ t # aft) ! j)" (is ?one) - proof - fix j - assume j: "j \ set ?\" - then have "j \ set (\ (f,length ?ss))" by simp - from subterm_wpo_s_arg[OF this] - have s: "wpo_s ?s (?ss ! j)" . - show "wpo_s ?s (?ts ! j)" - proof (cases "j = length bef") - case False - then have "?ss ! j = ?ts ! j" by (rule append_Cons_nth_not_middle) - with s show ?thesis by simp - next - case True - with s have "wpo_s ?s s" by simp - with rel wpo_compat have "wpo_s ?s t" by blast - with True show ?thesis by simp - qed - qed - with \?three\ ctxt_NS[OF stA] show ?thesis unfolding \f_def by auto -qed + assume si: "i \ set (\ (f,length ss))" + from NS_arg'[OF this] have "(Fun f ss, ss ! i) \ NS" . + with si Fun[OF status_aux[OF si]] have "wpo_s (Fun f ss) (ss ! i)" unfolding wpo.simps[of "Fun f ss" "ss ! i"] + by auto + } note wpo_s = this + let ?ss = "map (\ i. ss ! i) (\ (f,length ss))" + have rec11: "snd (lex_ext wpo n ?ss ?ss)" + by (rule all_nstri_imp_lex_nstri, insert \E[of _ f ss], auto simp: Fun) + have rec12: "snd (mul_ext wpo ?ss ?ss)" + unfolding mul_ext_def Let_def snd_conv + by (intro ns_mul_ext_refl_local, + unfold locally_refl_def, auto simp: in_multiset_in_set[of ?ss] intro!: Fun status_aux) + from rec11 rec12 show ?case using refl_NS_point wpo_s + by (cases "c (f,length ss)", auto simp: wpo.simps[of "Fun f ss" "Fun f ss"] prc_refl) +qed (simp add: wpo.simps refl_NS_point) -lemma wpo_ns_mono: - assumes rel: "s \ t" - shows "Fun f (bef @ s # aft) \ Fun f (bef @ t # aft)" -proof - - let ?ss = "bef @ s # aft" - let ?ts = "bef @ t # aft" - let ?s = "Fun f ?ss" - let ?t = "Fun f ?ts" - let ?len = "Suc (length bef + length aft)" - let ?f = "(f, ?len)" - let ?\ = "\ ?f" - from wpo_ns_pre_mono[OF rel] - have id: "(\j\set ?\. wpo_s ?s ((bef @ t # aft) ! j)) = True" - "((?s,?t) \ NS) = True" - "length ?ss = ?len" "length ?ts = ?len" - by auto - have "snd (lex_ext wpo n (map ((!) ?ss) ?\) (map ((!) ?ts) ?\))" - by (rule all_nstri_imp_lex_nstri, intro allI impI, insert wpo_ns_pre_mono[OF rel], auto) - moreover have "snd (mul_ext wpo (map ((!) ?ss) ?\) (map ((!) ?ts) ?\))" - by (rule all_nstri_imp_mul_nstri, intro allI impI, insert wpo_ns_pre_mono[OF rel], auto) - ultimately show ?thesis unfolding wpo.simps[of ?s ?t] term.simps id prc_refl - using order_tag.exhaust by (auto simp: Let_def) -qed - -lemma wpo_stable: fixes \ :: "('f,'v)subst" +lemma wpo_stable': fixes \ :: "('f,'v)subst" shows "(s \ t \ s \ \ \ t \ \) \ (s \ t \ s \ \ \ t \ \)" (is "?p s t") proof (induct "(s,t)" arbitrary:s t rule: wf_induct[OF wf_measure[of "\ (s,t). size s + size t"]]) case (1 s t) from 1 have "\ s' t'. size s' + size t' < size s + size t \ ?p s' t'" by auto note IH = this[rule_format] let ?s = "s \ \" let ?t = "t \ \" note simps = wpo.simps[of s t] wpo.simps[of ?s ?t] show "?case" proof (cases "((s,t) \ S \ (?s,?t) \ S) \ ((s,t) \ NS \ \ wpo_ns s t)") case True then show ?thesis proof assume "(s,t) \ S \ (?s,?t) \ S" with subst_S[of s t \] have "(?s,?t) \ S" by blast from S_imp_wpo_s[OF this] have "wpo_s ?s ?t" . with wpo_s_imp_ns[OF this] show ?thesis by blast next assume "(s,t) \ NS \ \ wpo_ns s t" with wpo_ns_imp_NS have st: "\ wpo_ns s t" by auto with wpo_s_imp_ns have "\ wpo_s s t" by auto with st show ?thesis by blast qed next case False then have not: "((s,t) \ S) = False" "((?s,?t) \ S) = False" and stA: "(s,t) \ NS" and ns: "wpo_ns s t" by auto from subst_NS[OF stA] have sstsA: "(?s,?t) \ NS" by auto from stA sstsA have id: "((s,t) \ NS) = True" "((?s,?t) \ NS) = True" by auto note simps = simps[unfolded id not if_False if_True] show ?thesis proof (cases s) case (Var x) note s = this show ?thesis proof (cases t) case (Var y) note t = this - show ?thesis unfolding simps(1) unfolding s t using wpo_ns_refl[of "\ y"] by auto + show ?thesis unfolding simps(1) unfolding s t using wpo_ns_refl'[of "\ y"] by auto next case (Fun g ts) note t = this let ?g = "(g,length ts)" show ?thesis proof (cases "\ x") case (Var y) then show ?thesis unfolding simps unfolding s t by simp next case (Fun f ss) let ?f = "(f, length ss)" show ?thesis proof (cases "prl ?g") case False then show ?thesis unfolding simps unfolding s t Fun by auto next case True obtain s ns where "prc ?f ?g = (s,ns)" by force with prl[OF True, of ?f] have prc: "prc ?f ?g = (s, True)" by auto show ?thesis unfolding simps unfolding s t Fun by (auto simp: Fun prc mul_ext_def ns_mul_ext_bottom Let_def intro!: all_nstri_imp_lex_nstri[of "[]", simplified]) qed qed qed next case (Fun f ss) note s = this let ?f = "(f,length ss)" let ?ss = "set (\ ?f)" { fix i assume i: "i \ ?ss" and ns: "wpo_ns (ss ! i) t" from IH[of "ss ! i" t] \E[OF i] ns have "wpo_ns (ss ! i \ \) ?t" using s by (auto simp: size_simps) then have "wpo_s ?s ?t" using i sstsA \[of f "length ss"] unfolding simps unfolding s by force with wpo_s_imp_ns[OF this] have ?thesis by blast } note si_arg = this show ?thesis proof (cases t) case t: (Var y) show ?thesis proof (cases "\i\?ss. wpo_ns (ss ! i) t") case True then obtain i where si: "i \ ?ss" and ns: "wpo_ns (ss ! i) t" unfolding s t by auto from si_arg[OF this] show ?thesis . next case False with ns[unfolded simps] s t have ssimple and largef: "large ?f" by (auto split: if_splits) from False s t not have "\ wpo_s s t" unfolding wpo.simps[of s t] by auto moreover have "wpo_ns ?s ?t" proof (cases "\ y") case (Var z) show ?thesis unfolding wpo.simps[of ?s ?t] not id unfolding s t using Var \ssimple\ largef by auto next case (Fun g ts) let ?g = "(g,length ts)" obtain ps pns where prc: "prc ?f ?g = (ps,pns)" by (cases "prc ?f ?g", auto) from prc_stri_imp_nstri[of ?f ?g] prc have ps: "ps \ pns" by auto { fix j assume "j \ set (\ ?g)" with set_status_nth[OF refl this] ss_status[OF \ssimple\ this] t Fun have "(t \ \, ts ! j) \ S" by (auto simp: simple_arg_pos_def) with sstsA have S: "(s \ \, ts ! j) \ S" by (metis compat_NS_S_point) hence "wpo_s (s \ \) (ts ! j)" by (rule S_imp_wpo_s) } note ssimple = this from large[OF \ssimple\ largef, of ?g, unfolded prc] have "ps \ pns \ \ ?g = []" by auto thus ?thesis using ssimple unfolding wpo.simps[of ?s ?t] not id unfolding s t using Fun prc ps by (auto simp: lex_ext_least_1 mul_ext_def Let_def ns_mul_ext_bottom) qed ultimately show ?thesis by blast qed next case (Fun g ts) note t = this let ?g = "(g,length ts)" let ?ts = "set (\ ?g)" obtain prs prns where p: "prc ?f ?g = (prs, prns)" by force note ns = ns[unfolded simps, unfolded s t p term.simps split] show ?thesis proof (cases "\ i \ ?ss. wpo_ns (ss ! i) t") case True with si_arg show ?thesis by blast next case False then have id: "(\ i \ ?ss. wpo_ns (ss ! i) (Fun g ts)) = False" unfolding t by auto note ns = ns[unfolded this if_False] let ?mss = "map (\ s . s \ \) ss" let ?mts = "map (\ t . t \ \) ts" from ns have prns and s_tj: "\ j. j \ ?ts \ wpo_s (Fun f ss) (ts ! j)" by (auto split: if_splits) { fix j assume j: "j \ ?ts" from \E[OF this] have "size s + size (ts ! j) < size s + size t" unfolding t by (auto simp: size_simps) from IH[OF this] s_tj[OF j, folded s] have wpo: "wpo_s ?s (ts ! j \ \)" by auto from j \[of g "length ts"] have "j < length ts" by auto with wpo have "wpo_s ?s (?mts ! j)" by auto } note ss_ts = this note \E = \E[of _ f ss] \E[of _ g ts] show ?thesis proof (cases prs) case True with ss_ts sstsA p \prns\ have "wpo_s ?s ?t" unfolding simps unfolding s t by (auto split: if_splits) with wpo_s_imp_ns[OF this] show ?thesis by blast next case False let ?mmss = "map ((!) ss) (\ ?f)" let ?mmts = "map ((!) ts) (\ ?g)" let ?Mmss = "map ((!) ?mss) (\ ?f)" let ?Mmts = "map ((!) ?mts) (\ ?g)" have id_map: "?Mmss = map (\ t. t \ \) ?mmss" "?Mmts = map (\ t. t \ \) ?mmts" unfolding map_map o_def by (auto simp: set_status_nth) let ?ls = "length (\ ?f)" let ?lt = "length (\ ?g)" { fix si tj assume *: "si \ set ?mmss" "tj \ set ?mmts" have "(wpo_s si tj \ wpo_s (si \ \) (tj \ \)) \ (wpo_ns si tj \ wpo_ns (si \ \) (tj \ \))" proof (intro IH add_strict_mono) from *(1) have "si \ set ss" using set_status_nth[of _ _ _ \\] by auto then show "size si < size s" unfolding s by (auto simp: termination_simp) from *(2) have "tj \ set ts" using set_status_nth[of _ _ _ \\] by auto then show "size tj < size t" unfolding t by (auto simp: termination_simp) qed hence "wpo_s si tj \ wpo_s (si \ \) (tj \ \)" "wpo_ns si tj \ wpo_ns (si \ \) (tj \ \)" by blast+ } note IH' = this { fix i assume "i < ?ls" "i < ?lt" then have i_f: "i < length (\ ?f)" and i_g: "i < length (\ ?g)" by auto with \[of f "length ss"] \[of g "length ts"] have i: "\ ?f ! i < length ss" "\ ?g ! i < length ts" unfolding set_conv_nth by auto then have "size (ss ! (\ ?f ! i)) < size s" "size (ts ! (\ ?g ! i)) < size t" unfolding s t by (auto simp: size_simps) then have "size (ss ! (\ ?f ! i)) + size (ts ! (\ ?g ! i)) < size s + size t" by simp from IH[OF this] i i_f i_g have "(wpo_s (?mmss ! i) (?mmts ! i) \ wpo_s (?mss ! (\ ?f ! i)) (?mts ! (\ ?g ! i)))" "(wpo_ns (?mmss ! i) (?mmts ! i) \ wpo_ns (?mss ! (\ ?f ! i)) (?mts ! (\ ?g ! i)))" by auto } note IH = this consider (Lex) "c ?f = Lex" "c ?g = Lex" | (Mul) "c ?f = Mul" "c ?g = Mul" | (Diff) "c ?f \ c ?g" by (cases "c ?f"; cases "c ?g", auto) thus ?thesis proof cases case Lex from Lex False ns have "snd (lex_ext wpo n ?mmss ?mmts)" by (auto split: if_splits) from this[unfolded lex_ext_iff snd_conv] have len: "(?ls = ?lt \ ?lt \ n)" and choice: "(\i< ?ls. i < ?lt \ (\j wpo_s (?mmss ! i) (?mmts ! i)) \ (\i< ?lt. wpo_ns (?mmss ! i) (?mmts ! i)) \ ?lt \ ?ls" (is "?stri \ ?nstri") by auto from choice have "?stri \ (\ ?stri \ ?nstri)" by blast then show ?thesis proof assume ?stri then obtain i where i: "i < ?ls" "i < ?lt" and NS: "(\jjprns\ have "wpo_s ?s ?t" unfolding simps unfolding s t by (auto split: if_splits) with wpo_s_imp_ns[OF this] show ?thesis by blast next assume "\ ?stri \ ?nstri" then have ?nstri and nstri: "\ ?stri" by blast+ with IH have "(\i< ?lt. wpo_ns (?Mmss ! i) (?Mmts ! i)) \ ?lt \ ?ls" by auto with len have "snd (lex_ext wpo n ?Mmss ?Mmts)" unfolding lex_ext_iff by auto with Lex ss_ts sstsA p \prns\ have ns: "wpo_ns ?s ?t" unfolding simps unfolding s t by (auto split: if_splits) { assume "wpo_s s t" from Lex this[unfolded simps, unfolded s t term.simps p split id] False have "fst (lex_ext wpo n ?mmss ?mmts)" by (auto split: if_splits) from this[unfolded lex_ext_iff fst_conv] nstri have "(\i< ?lt. wpo_ns (?mmss ! i) (?mmts ! i)) \ ?lt < ?ls" by auto with IH have "(\i< ?lt. wpo_ns (?Mmss ! i) (?Mmts ! i)) \ ?lt < ?ls" by auto then have "fst (lex_ext wpo n ?Mmss ?Mmts)" using len unfolding lex_ext_iff by auto with Lex ss_ts sstsA p \prns\ have ns: "wpo_s ?s ?t" unfolding simps unfolding s t by (auto split: if_splits) } with ns show ?thesis by blast qed next case Diff thus ?thesis using ns ss_ts sstsA p \prns\ unfolding simps unfolding s t by (auto simp: Let_def split: if_splits) next case Mul from Mul False ns have ge: "snd (mul_ext wpo ?mmss ?mmts)" by (auto split: if_splits) have ge: "snd (mul_ext wpo ?Mmss ?Mmts)" unfolding id_map by (rule nstri_mul_ext_map[OF _ _ ge], (intro IH', auto)+) { assume gr: "fst (mul_ext wpo ?mmss ?mmts)" have gr\: "fst (mul_ext wpo ?Mmss ?Mmts)" unfolding id_map by (rule stri_mul_ext_map[OF _ _ gr], (intro IH', auto)+) } note gr = this from ge gr show ?thesis using ss_ts \prns\ unfolding simps unfolding s t term.simps p split subst_apply_term.simps length_map Mul by (simp add: id_map id) qed qed qed qed qed qed qed +lemma subterm_wpo_s_arg': assumes i: "i \ set (\ (f,length ss))" + shows "Fun f ss \ ss ! i" +proof - + have refl: "ss ! i \ ss ! i" by (rule wpo_ns_refl') + with i have "\ t \ set (\ (f,length ss)). ss ! i \ ss ! i" by auto + with NS_arg'[OF i] i + show ?thesis by (auto simp: wpo.simps split: if_splits) +qed + +context + fixes f s t bef aft + assumes ctxt_NS: "(s,t) \ NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ NS" + and SN: "\f. prl f \ SN S" +begin + +lemma wpo_ns_pre_mono': + defines "\f \ \ (f, Suc (length bef + length aft))" + assumes rel: "(wpo_ns s t)" + shows "(\j\set \f. Fun f (bef @ s # aft) \ (bef @ t # aft) ! j) + \ (Fun f (bef @ s # aft), (Fun f (bef @ t # aft))) \ NS + \ (\ i < length \f. ((map ((!) (bef @ s # aft)) \f) ! i) \ ((map ((!) (bef @ t # aft)) \f) ! i))" + (is "_ \ _ \ ?three") +proof - + let ?ss = "bef @ s # aft" + let ?ts = "bef @ t # aft" + let ?s = "Fun f ?ss" + let ?t = "Fun f ?ts" + let ?len = "Suc (length bef + length aft)" + let ?f = "(f, ?len)" + let ?\ = "\ ?f" + from wpo_ns_imp_NS[OF rel] have stA: "(s,t) \ NS" . + have ?three unfolding \f_def + proof (intro allI impI) + fix i + assume "i < length ?\" + then have id: "\ ss. (map ((!) ss) ?\) ! i = ss ! (?\ ! i)" by auto + show "wpo_ns ((map ((!) ?ss) ?\) ! i) ((map ((!) ?ts) ?\) ! i)" + proof (cases "?\ ! i = length bef") + case True + then show ?thesis unfolding id using rel by auto + next + case False + from append_Cons_nth_not_middle[OF this, of s aft t] wpo_ns_refl' + show ?thesis unfolding id by auto + qed + qed + have "\j\set ?\. wpo_s ?s ((bef @ t # aft) ! j)" (is ?one) + proof + fix j + assume j: "j \ set ?\" + then have "j \ set (\ (f,length ?ss))" by simp + from subterm_wpo_s_arg'[OF this] + have s: "wpo_s ?s (?ss ! j)" . + show "wpo_s ?s (?ts ! j)" + proof (cases "j = length bef") + case False + then have "?ss ! j = ?ts ! j" by (rule append_Cons_nth_not_middle) + with s show ?thesis by simp + next + case True + with s have "wpo_s ?s s" by simp + with rel wpo_compat'[OF SN] have "wpo_s ?s t" by fast + with True show ?thesis by simp + qed + qed + with \?three\ ctxt_NS[OF stA] show ?thesis unfolding \f_def by auto +qed + +lemma wpo_ns_mono': + assumes rel: "s \ t" + shows "Fun f (bef @ s # aft) \ Fun f (bef @ t # aft)" +proof - + let ?ss = "bef @ s # aft" + let ?ts = "bef @ t # aft" + let ?s = "Fun f ?ss" + let ?t = "Fun f ?ts" + let ?len = "Suc (length bef + length aft)" + let ?f = "(f, ?len)" + let ?\ = "\ ?f" + from wpo_ns_pre_mono'[OF rel] + have id: "(\j\set ?\. wpo_s ?s ((bef @ t # aft) ! j)) = True" + "((?s,?t) \ NS) = True" + "length ?ss = ?len" "length ?ts = ?len" + by auto + have "snd (lex_ext wpo n (map ((!) ?ss) ?\) (map ((!) ?ts) ?\))" + by (rule all_nstri_imp_lex_nstri, intro allI impI, insert wpo_ns_pre_mono'[OF rel], auto) + moreover have "snd (mul_ext wpo (map ((!) ?ss) ?\) (map ((!) ?ts) ?\))" + by (rule all_nstri_imp_mul_nstri, intro allI impI, insert wpo_ns_pre_mono'[OF rel], auto) + ultimately show ?thesis unfolding wpo.simps[of ?s ?t] term.simps id prc_refl + using order_tag.exhaust by (auto simp: Let_def) +qed + +end +end +end + +locale wpo_with_assms = wpo_with_basic_assms + SN_order_pair + precedence + + constrains S :: "('f, 'v) term rel" and NS :: _ + and prc :: "'f \ nat \ 'f \ nat \ bool \ bool" + and prl :: "'f \ nat \ bool" + and ssimple :: bool + and large :: "'f \ nat \ bool" + and c :: "'f \ nat \ order_tag" + and n :: nat + and \\ :: "'f status" + assumes ctxt_NS: "(s,t) \ NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ NS" + and ws_status: "i \ set (status \\ fn) \ simple_arg_pos NS fn i" +begin + +lemma ssimple: "strictly_simple_status \\ NS" + using ws_status set_status_nth unfolding strictly_simple_status_def simple_arg_pos_def by fastforce + +lemma trans_prc: "trans_precedence prc" + unfolding trans_precedence_def +proof (intro allI, goal_cases) + case (1 f g h) + show ?case using prc_compat[of f g _ _ h] by (cases "prc f g"; cases "prc g h"; cases "prc f h", auto) +qed + +lemma NS_arg: assumes i: "i \ set (\ (f,length ts))" + shows "(Fun f ts, ts ! i) \ NS" + using NS_arg'[OF ssimple i] . + +lemma NS_subterm: assumes all: "\ f k. set (\ (f,k)) = {0 ..< k}" + shows "s \ t \ (s,t) \ NS" +proof (induct s t rule: supteq.induct) + case (refl) + from refl_NS show ?case unfolding refl_on_def by blast +next + case (subt s ss t f) + from subt(1) obtain i where i: "i < length ss" and s: "s = ss ! i" unfolding set_conv_nth by auto + from NS_arg[of i f ss, unfolded all] s i have "(Fun f ss, s) \ NS" by auto + from trans_NS_point[OF this subt(3)] show ?case . +qed + +lemma wpo_ns_refl: "s \ s" + using wpo_ns_refl'[OF ssimple] . + + +lemma Var_not_S[simp]: "(Var x, t) \ S" +proof + assume st: "(Var x, t) \ S" + from SN_imp_minimal[OF SN, rule_format, of undefined UNIV] + obtain s where "\ u. (s,u) \ S" by blast + with subst_S[OF st, of "\ _. s"] + show False by auto +qed + + +(* Transitivity / compatibility of the orders *) +lemma wpo_compat: " + (s \ t \ t \ u \ s \ u) \ + (s \ t \ t \ u \ s \ u) \ + (s \ t \ t \ u \ s \ u)" + by (rule wpo_compat'[OF SN]) + +lemma subterm_wpo_s_arg: assumes i: "i \ set (\ (f,length ss))" + shows "Fun f ss \ ss ! i" + by (rule subterm_wpo_s_arg'[OF ssimple i]) + +lemma subterm_wpo_ns_arg: assumes i: "i \ set (\ (f,length ss))" + shows "Fun f ss \ ss ! i" + by (rule wpo_s_imp_ns[OF subterm_wpo_s_arg[OF i]]) + +lemma wpo_ns_mono: + assumes rel: "s \ t" + shows "Fun f (bef @ s # aft) \ Fun f (bef @ t # aft)" + by (rule wpo_ns_mono'[OF ssimple ctxt_NS SN rel]) + +lemma wpo_ns_pre_mono: fixes f and bef aft :: "('f,'v)term list" + defines "\f \ \ (f, Suc (length bef + length aft))" + assumes rel: "(wpo_ns s t)" + shows "(\j\set \f. Fun f (bef @ s # aft) \ (bef @ t # aft) ! j) + \ (Fun f (bef @ s # aft), (Fun f (bef @ t # aft))) \ NS + \ (\ i < length \f. ((map ((!) (bef @ s # aft)) \f) ! i) \ ((map ((!) (bef @ t # aft)) \f) ! i))" + unfolding \f_def + by (rule wpo_ns_pre_mono'[OF ssimple ctxt_NS SN rel]) + +lemma wpo_stable: fixes \ :: "('f,'v)subst" + shows "(s \ t \ s \ \ \ t \ \) \ (s \ t \ s \ \ \ t \ \)" + by (rule wpo_stable'[OF ssimple]) + lemma WPO_S_SN: "SN WPO_S" proof - { fix t :: "('f,'v)term" let ?S = "\x. SN_on WPO_S {x}" note iff = SN_on_all_reducts_SN_on_conv[of WPO_S] { fix x have "?S (Var x)" unfolding iff[of "Var x"] proof (intro allI impI) fix s assume "(Var x, s) \ WPO_S" then have False by (cases s, auto simp: wpo.simps split: if_splits) then show "?S s" .. qed } note var_SN = this have "?S t" proof (induct t) case (Var x) show ?case by (rule var_SN) next case (Fun f ts) let ?Slist = "\ f ys. \ i \ set (\ f). ?S (ys ! i)" let ?r3 = "{((f,ab), (g,ab')). ((c f = c g) \ (?Slist f ab \ (c f = Mul \ fst (mul_ext wpo (map ((!) ab) (\ f)) (map ((!) ab') (\ g)))) \ (c f = Lex \ fst (lex_ext wpo n (map ((!) ab) (\ f)) (map ((!) ab') (\ g)))))) \ ((c f \ c g) \ (map ((!) ab) (\ f) \ [] \ (map ((!) ab') (\ g)) = []))}" let ?r0 = "lex_two {(f,g). fst (prc f g)} {(f,g). snd (prc f g)} ?r3" { fix ab { assume "\S. S 0 = ab \ (\i. (S i, S (Suc i)) \ ?r3)" then obtain S where S0: "S 0 = ab" and SS: "\i. (S i, S (Suc i)) \ ?r3" by auto let ?Sf = "\i. fst (fst (S i))" let ?Sn = "\i. snd (fst (S i))" let ?Sfn = "\ i. fst (S i)" let ?Sts = "\i. snd (S i)" let ?Sts\ = "\i. map ((!) (?Sts i)) (\ (?Sfn i))" have False proof (cases "\i. c (?Sfn i) = Mul") case True let ?r' = "{((f,ys), (g,xs)). (\ yi \set ((map ((!) ys) (\ f))). SN_on WPO_S {yi}) \ fst (mul_ext wpo (map ((!) ys) (\ f)) (map ((!) xs) (\ g)))}" { fix i from True[rule_format, of i] and True[rule_format, of "Suc i"] and SS[rule_format, of i] have "(S i, S (Suc i)) \ ?r'" by auto } then have Hf: "\ SN_on ?r' {S 0}" unfolding SN_on_def by auto from mul_ext_SN[of wpo, rule_format, OF wpo_ns_refl] and wpo_compat wpo_s_imp_ns have tmp: "SN {(ys, xs). (\y\set ys. SN_on {(s, t). wpo_s s t} {y}) \ fst (mul_ext wpo ys xs)}" (is "SN ?R") by blast have id: "?r' = inv_image ?R (\ (f,ys). map ((!) ys) (\ f))" by auto from SN_inv_image[OF tmp] have "SN ?r'" unfolding id . from SN_on_subset2[OF subset_UNIV[of "{S 0}"], OF this] have "SN_on ?r' {(S 0)}" . with Hf show ?thesis .. next case False note HMul = this show ?thesis proof (cases "\i. c (?Sfn i) = Lex") case True let ?r' = "{((f,ys), (g,xs)). (\ yi \set ((map ((!) ys) (\ f))). SN_on WPO_S {yi}) \ fst (lex_ext wpo n (map ((!) ys) (\ f)) (map ((!) xs) (\ g)))}" { fix i from SS[rule_format, of i] True[rule_format, of i] True[rule_format, of "Suc i"] have "(S i, S (Suc i)) \ ?r'" by auto } then have Hf: "\ SN_on ?r' {S 0}" unfolding SN_on_def by auto from wpo_compat have "\ x y z. wpo_ns x y \ wpo_s y z \ wpo_s x z" by blast from lex_ext_SN[of "wpo" n, OF this] have tmp: "SN {(ys, xs). (\y\set ys. SN_on WPO_S {y}) \ fst (lex_ext wpo n ys xs)}" (is "SN ?R") . have id: "?r' = inv_image ?R (\ (f,ys). map ((!) ys) (\ f))" by auto from SN_inv_image[OF tmp] have "SN ?r'" unfolding id . then have "SN_on ?r' {(S 0)}" unfolding SN_defs by blast with Hf show False .. next case False note HLex = this from HMul and HLex have "\i. c (?Sfn i) \ c (?Sfn (Suc i))" proof (cases ?thesis, simp) case False then have T: "\i. c (?Sfn i) = c (?Sfn (Suc i))" by simp { fix i have "c (?Sfn i) = c (?Sfn 0)" proof (induct i) case (Suc j) then show ?case by (simp add: T[rule_format, of j]) qed simp } then show ?thesis using HMul HLex by (cases "c (?Sfn 0)") auto qed then obtain i where Hdiff: "c (?Sfn i) \ c (?Sfn (Suc i))" by auto from Hdiff have Hf: "?Sts\ (Suc i) = []" using SS[rule_format, of i] by auto show ?thesis proof (cases "c (?Sfn (Suc i)) = c (?Sfn (Suc (Suc i)))") case False then show ?thesis using Hf and SS[rule_format, of "Suc i"] by auto next case True show ?thesis proof (cases "c (?Sfn (Suc i))") case Mul with True and SS[rule_format, of "Suc i"] have "fst (mul_ext wpo (?Sts\ (Suc i)) (?Sts\ (Suc (Suc i))))" by auto with Hf and s_mul_ext_bottom_strict show ?thesis by (simp add: Let_def mul_ext_def s_mul_ext_bottom_strict) next case Lex with True and SS[rule_format, of "Suc i"] have "fst (lex_ext wpo n (?Sts\ (Suc i)) (?Sts\ (Suc (Suc i))))" by auto with Hf show ?thesis by (simp add: lex_ext_iff) qed qed qed qed } } then have "SN ?r3" unfolding SN_on_def by blast have SN1:"SN ?r0" proof (rule lex_two[OF _ prc_SN \SN ?r3\]) let ?r' = "{(f,g). fst (prc f g)}" let ?r = "{(f,g). snd (prc f g)}" { fix a1 a2 a3 assume "(a1,a2) \ ?r" "(a2,a3) \ ?r'" then have "(a1,a3) \ ?r'" by (cases "prc a1 a2", cases "prc a2 a3", cases "prc a1 a3", insert prc_compat[of a1 a2 _ _ a3], force) } then show "?r O ?r' \ ?r'" by auto qed let ?m = "\ (f,ts). ((f,length ts), ((f, length ts), ts))" let ?r = "{(a,b). (?m a, ?m b) \ ?r0}" have SN_r: "SN ?r" using SN_inv_image[OF SN1, of ?m] unfolding inv_image_def by fast let ?SA = "(\ x y. (x,y) \ S)" let ?NSA = "(\ x y. (x,y) \ NS)" let ?rr = "lex_two S NS ?r" define rr where "rr = ?rr" from lex_two[OF compat_NS_S SN SN_r] have SN_rr: "SN rr" unfolding rr_def by auto let ?rrr = "inv_image rr (\ (f,ts). (Fun f ts, (f,ts)))" have SN_rrr: "SN ?rrr" by (rule SN_inv_image[OF SN_rr]) let ?ind = "\ (f,ts). ?Slist (f,length ts) ts \ ?S (Fun f ts)" have "?ind (f,ts)" proof (rule SN_induct[OF SN_rrr, of ?ind]) fix fts assume ind: "\ gss. (fts,gss) \ ?rrr \ ?ind gss" obtain f ts where Pair: "fts = (f,ts)" by force let ?f = "(f,length ts)" note ind = ind[unfolded Pair] show "?ind fts" unfolding Pair split proof (intro impI) assume ts: "?Slist ?f ts" let ?t = "Fun f ts" show "?S ?t" proof (simp only: iff[of ?t], intro allI impI) fix s assume "(?t,s) \ WPO_S" then have "?t \ s" by simp then show "?S s" proof (induct s, simp add: var_SN) case (Fun g ss) note IH = this let ?s = "Fun g ss" let ?g = "(g,length ss)" from Fun have t_gr_s: "?t \ ?s" by auto show "?S ?s" proof (cases "\ i \ set (\ ?f). ts ! i \ ?s") case True then obtain i where "i \ set (\ ?f)" and ge: "ts ! i \ ?s" by auto with ts have "?S (ts ! i)" by auto show "?S ?s" proof (unfold iff[of ?s], intro allI impI) fix u assume "(?s,u) \ WPO_S" with wpo_compat ge have u: "ts ! i \ u" by blast with \?S (ts ! i)\[unfolded iff[of "ts ! i"]] show "?S u" by simp qed next case False note oFalse = this from wpo_s_imp_NS[OF t_gr_s] have t_NS_s: "(?t,?s) \ NS" . show ?thesis proof (cases "(?t,?s) \ S") case True then have "((f,ts),(g,ss)) \ ?rrr" unfolding rr_def by auto with ind have ind: "?ind (g,ss)" by auto { fix i assume i: "i \ set (\ ?g)" have "?s \ ss ! i" by (rule subterm_wpo_ns_arg[OF i]) with t_gr_s have ts: "?t \ ss ! i" using wpo_compat by blast have "?S (ss ! i)" using IH(1)[OF \E[OF i] ts] by auto } note SN_ss = this from ind SN_ss show ?thesis by auto next case False with t_NS_s oFalse have id: "(?t,?s) \ S = False" "(?t,?s) \ NS = True" by simp_all let ?ls = "length ss" let ?lt = "length ts" let ?f = "(f,?lt)" let ?g = "(g,?ls)" obtain s1 ns1 where prc1: "prc ?f ?g = (s1,ns1)" by force note t_gr_s = t_gr_s[unfolded wpo.simps[of ?t ?s], unfolded term.simps id if_True if_False prc1 split] from oFalse t_gr_s have f_ge_g: "ns1" by (cases ?thesis, auto) from oFalse t_gr_s f_ge_g have small_ss: "\ i \ set (\ ?g). ?t \ ss ! i" by (cases ?thesis, auto) with Fun \E[of _ g ss] have ss_S: "?Slist ?g ss" by auto show ?thesis proof (cases s1) case True then have "((f,ts),(g,ss)) \ ?r" by (simp add: prc1) with t_NS_s have "((f,ts),(g,ss)) \ ?rrr" unfolding rr_def by auto with ind have "?ind (g,ss)" by auto with ss_S show ?thesis by auto next case False consider (Diff) "c ?f \ c ?g" | (Lex) "c ?f = Lex" "c ?g = Lex" | (Mul) "c ?f = Mul" "c ?g = Mul" by (cases "c ?f"; cases "c ?g", auto) thus ?thesis proof cases case Diff with False oFalse f_ge_g t_gr_s small_ss prc1 t_NS_s have "((f,ts),(g,ss)) \ ?rrr" unfolding rr_def by (cases "c ?f"; cases "c ?g", auto) with ind have "?ind (g,ss)" using Pair by auto with ss_S show ?thesis by simp next case Lex from False oFalse t_gr_s small_ss f_ge_g Lex have lex: "fst (lex_ext wpo n (map ((!) ts) (\ ?f)) (map ((!) ss) (\ ?g)))" by auto from False lex ts f_ge_g Lex have "((f,ts),(g,ss)) \ ?r" by (simp add: prc1) with t_NS_s have "((f,ts),(g,ss)) \ ?rrr" unfolding rr_def by auto with ind have "?ind (g,ss)" by auto with ss_S show ?thesis by auto next case Mul from False oFalse t_gr_s small_ss f_ge_g Mul have mul: "fst (mul_ext wpo (map ((!) ts) (\ ?f)) (map ((!) ss) (\ ?g)))" by auto from False mul ts f_ge_g Mul have "((f,ts),(g,ss)) \ ?r" by (simp add: prc1) with t_NS_s have "((f,ts),(g,ss)) \ ?rrr" unfolding rr_def by auto with ind have "?ind (g,ss)" by auto with ss_S show ?thesis by auto qed qed qed qed qed qed qed qed with Fun show ?case using \E[of _ f ts] by simp qed } from SN_I[OF this] show "SN {(s::('f, 'v)term, t). fst (wpo s t)}" . qed theorem WPO_SN_order_pair: "SN_order_pair WPO_S WPO_NS" proof show "refl WPO_NS" using wpo_ns_refl unfolding refl_on_def by auto show "trans WPO_NS" using wpo_compat unfolding trans_def by blast show "trans WPO_S" using wpo_compat wpo_s_imp_ns unfolding trans_def by blast show "WPO_NS O WPO_S \ WPO_S" using wpo_compat by blast show "WPO_S O WPO_NS \ WPO_S" using wpo_compat by blast show "SN WPO_S" using WPO_S_SN . qed theorem WPO_S_subst: "(s,t) \ WPO_S \ (s \ \, t \ \) \ WPO_S" for \ using wpo_stable by auto theorem WPO_NS_subst: "(s,t) \ WPO_NS \ (s \ \, t \ \) \ WPO_NS" for \ using wpo_stable by auto theorem WPO_NS_ctxt: "(s,t) \ WPO_NS \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ WPO_NS" using wpo_ns_mono by blast theorem WPO_S_subset_WPO_NS: "WPO_S \ WPO_NS" using wpo_s_imp_ns by blast context (* if \ is the full status, then WPO_S is a simplification order *) assumes \_full: "\ f k. set (\ (f,k)) = {0 ..< k}" begin lemma subterm_wpo_s: "s \ t \ s \ t" proof (induct s t rule: supt.induct) case (arg s ss f) from arg[unfolded set_conv_nth] obtain i where i: "i < length ss" and s: "s = ss ! i" by auto from \_full[of f "length ss"] i have ii: "i \ set (\ (f,length ss))" by auto from subterm_wpo_s_arg[OF ii] s show ?case by auto next case (subt s ss t f) from subt wpo_s_imp_ns have "\ s \ set ss. wpo_ns s t" by blast from this[unfolded set_conv_nth] obtain i where ns: "ss ! i \ t" and i: "i < length ss" by auto from \_full[of f "length ss"] i have ii: "i \ set (\ (f,length ss))" by auto from subt have "Fun f ss \ t" by auto from NS_subterm[OF \_full this] ns ii show ?case by (auto simp: wpo.simps split: if_splits) qed (* Compatibility of the subterm relation with the order relation: a subterm is smaller *) lemma subterm_wpo_ns: assumes supteq: "s \ t" shows "s \ t" proof - from supteq have "s = t \ s \ t" by auto then show ?thesis proof assume "s = t" then show ?thesis using wpo_ns_refl by blast next assume "s \ t" from wpo_s_imp_ns[OF subterm_wpo_s[OF this]] show ?thesis . qed qed lemma wpo_s_mono: assumes rels: "s \ t" shows "Fun f (bef @ s # aft) \ Fun f (bef @ t # aft)" proof - let ?ss = "bef @ s # aft" let ?ts = "bef @ t # aft" let ?s = "Fun f ?ss" let ?t = "Fun f ?ts" let ?len = "Suc (length bef + length aft)" let ?f = "(f, ?len)" let ?\ = "\ ?f" from wpo_s_imp_ns[OF rels] have rel: "wpo_ns s t" . from wpo_ns_pre_mono[OF rel] have id: "(\j\set ?\. wpo_s ?s ((bef @ t # aft) ! j)) = True" "((?s,?t) \ NS) = True" "length ?ss = ?len" "length ?ts = ?len" by auto let ?lb = "length bef" from \_full[of f ?len] have lb_mem: "?lb \ set ?\" by auto then obtain i where \i: "?\ ! i = ?lb" and i: "i < length ?\" unfolding set_conv_nth by force let ?mss = "map ((!) ?ss) ?\" let ?mts = "map ((!) ?ts) ?\" have "fst (lex_ext wpo n ?mss ?mts)" unfolding lex_ext_iff fst_conv proof (intro conjI, force, rule disjI1, unfold length_map id, intro exI conjI, rule i, rule i, intro allI impI) show "wpo_s (?mss ! i) (?mts ! i)" using \i i rels by simp next fix j assume "j < i" with i have j: "j < length ?\" by auto with wpo_ns_pre_mono[OF rel] show "?mss ! j \ ?mts ! j" by blast qed moreover obtain lb nlb where part: "partition ((=) ?lb) ?\ = (lb, nlb)" by force hence mset_\: "mset ?\ = mset lb + mset nlb" by (induct ?\, auto) let ?mlbs = "map ((!) ?ss) lb" let ?mnlbs = "map ((!) ?ss) nlb" let ?mlbt = "map ((!) ?ts) lb" let ?mnlbt = "map ((!) ?ts) nlb" have id1: "mset ?mss = mset ?mnlbs + mset ?mlbs" using mset_\ by auto have id2: "mset ?mts = mset ?mnlbt + mset ?mlbt" using mset_\ by auto from part lb_mem have lb: "?lb \ set lb" by auto have "fst (mul_ext wpo ?mss ?mts)" unfolding mul_ext_def Let_def fst_conv proof (intro s_mul_extI_old, rule id1, rule id2) from lb show "mset ?mlbs \ {#}" by auto { fix i assume "i < length ?mnlbt" then obtain j where id: "?mnlbs ! i = ?ss ! j" "?mnlbt ! i = ?ts ! j" "j \ set nlb" by auto with part have "j \ ?lb" by auto hence "?ss ! j = ?ts ! j" by (auto simp: nth_append) thus "(?mnlbs ! i, ?mnlbt ! i) \ WPO_NS" unfolding id using wpo_ns_refl by auto } fix u assume "u \# mset ?mlbt" hence "u = t" using part by auto moreover have "s \# mset ?mlbs" using lb by force ultimately show "\ v. v \# mset ?mlbs \ (v,u) \ WPO_S" using rels by force qed auto ultimately show ?thesis unfolding wpo.simps[of ?s ?t] term.simps id prc_refl using order_tag.exhaust by (auto simp: Let_def) qed theorem WPO_S_ctxt: "(s,t) \ WPO_S \ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) \ WPO_S" using wpo_s_mono by blast theorem supt_subset_WPO_S: "{\} \ WPO_S" using subterm_wpo_s by blast theorem supteq_subset_WPO_NS: "{\} \ WPO_NS" using subterm_wpo_ns by blast end end end