# Theory WPO

```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)"

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 irrefl_S: "irrefl S"
and S_imp_NS: "S ⊆ NS"
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_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 irrefl_S show False unfolding irrefl_def by auto
qed

lemmas σ = status[of σσ]
lemma σE: "i ∈ set (σ (f, length ss)) ⟹ ss ! i ∈ set ss" by (rule status_aux)

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 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 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› 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 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 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 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 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
from wpo_ns_imp_NS[OF ge1] wpo_ns_imp_NS[OF ge2]
have suA: "(s,u) ∈ NS" by (rule trans_NS_point)
note wpo_simp = wpo.simps[of t u]
show "wpo_ns s u"
proof (cases u)
case u: (Fun h us)
let ?h = "(h,length us)"
obtain pns where prc: "prc ?g ?h = (False,pns)" using prl2[OF pri, of ?h] by (cases "prc ?g ?h", auto)
from prc wpo_ns_imp_NS[OF ge2] tuS ge2 Fun u empty have pns unfolding wpo_simp
by (auto split: if_splits simp: Let_def)
with prc have prc: "prc ?g ?h = (False, True)" by auto
from prl3[OF pri, of ?h] prc have pri': "prl ?h" by auto
from prc wpo_ns_imp_NS[OF ge2] tuS ge2 Fun u empty have empty': "σ ?h = []" unfolding wpo_simp
by (auto split: if_splits simp: Let_def dest: lex_ext_arg_empty mul_ext_arg_empty)
from pri' empty' suA show ?thesis unfolding Var u by (auto simp: wpo.simps)
next
case u: (Var z)
from wpo_ns_imp_NS[OF ge2] tuS ge2 Fun u empty wpo_simp
have ssimple "large ?g" by auto
show ?thesis
proof (cases "x = z")
case True
thus ?thesis using suA Var u by (simp add: wpo.simps)
next
case False
from suA[unfolded Var u] have ns: "(Var x, Var z) ∈ NS" by auto
have "(a,b) ∈ NS" for a b using subst_NS[OF ns, of "λ z. if z = x then a else b"] False by auto
hence "NS = UNIV" by auto
from ss_S_non_empty[OF `ssimple`] this compat_S_NS obtain a where "(a,a) ∈ S" by auto
with irrefl_S show ?thesis unfolding irrefl_def by auto
qed
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)
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

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_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 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)

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 ⋅ δ))"
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 eval_term.simps length_map Mul
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"
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 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 + order_pair +
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: ```