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 Knuth_Bendix_Order.Term_Aux Knuth_Bendix_Order.Order_Pair Polynomial_Factorization.Missing_List Status Precedence Multiset_Extension2 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) 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 + 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 S_imp_NS: "S ⊆ NS" and ws_status: "i ∈ set (status σσ fn) ⟹ simple_arg_pos NS 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 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 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) ∧ (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) 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 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) 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) 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 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) 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 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"]] 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 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]]) 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) 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 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" 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 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<i. wpo_ns (?mmss ! j) (?mmts ! 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: "(∀j<i. wpo_ns (?mmss ! j) (?mmts ! j))" and S: "wpo_s (?mmss ! i) (?mmts ! i)" by auto with IH have "(∀j<i. wpo_ns (?Mmss ! j) (?Mmts ! j))" "wpo_s (?Mmss ! i) (?Mmts ! i)" by auto with i len have "fst (lex_ext wpo n ?Mmss ?Mmts)" unfolding lex_ext_iff by auto with Lex 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 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 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 =