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
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)
qed (simp add: wpo.simps refl_NS_point)
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 eval_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"
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: "⋀ 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 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_irrefl: "¬ (s ≻ s)"
proof
assume "s ≻ s"
thus False
proof (induct s)
case Var
thus False using irrefl_S by (auto simp: wpo.simps irrefl_def split: if_splits)
next
case (Fun f ss)
let ?s = "Fun f ss"
let ?n = "length ss"
let ?f = "(f,length ss)"
let ?sub = "∃i∈set (σ ?f). ss ! i ≽ ?s"
{
fix i
assume i: "i ∈ set (σ ?f)" and ge: "ss ! i ≽ ?s"
with status[of σσ f ?n] have "i < ?n" by auto
hence "ss ! i ∈ set ss" by auto
from Fun(1)[OF this] have not: "¬ (ss ! i ≻ ss ! i)" by auto
from ge subterm_wpo_s_arg[OF i] have "ss ! i ≻ ss ! i"
using wpo_compat by blast
with not have False ..
}
hence id0: "?sub = False" by auto
from irrefl_S refl_NS have id1: "((?s,?s) ∈ S) = False" "((?s,?s) ∈ NS) = True"
unfolding irrefl_def refl_on_def by auto
let ?ss = "map ((!) ss) (σ ?f)"
define ss' where "ss' = ?ss"
have "set ss' ⊆ set ss" using status[of σσ f ?n] by (auto simp: ss'_def)
note IH = Fun(1)[OF set_mp[OF this]]
from Fun(2)[unfolded wpo.simps[of ?s ?s] id1 id0 if_False if_True term.simps prc_refl split Let_def]
have "fst (lex_ext wpo n ss' ss') ∨ fst (mul_ext wpo ss' ss')"
by (auto split: if_splits simp: ss'_def)
thus False
proof
assume "fst (lex_ext wpo n ss' ss')"
with lex_ext_irrefl[of ss' wpo n] IH show False by auto
next
assume "fst (mul_ext wpo ss' ss')"
with mul_ext_irrefl[of ss' wpo, OF _ _ wpo_s_imp_ns] IH wpo_compat
show False by blast
qed
qed
qed
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 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 rel])
lemma wpo_stable: fixes δ :: "('f,'v)subst"
shows "(s ≻ t ⟶ s ⋅ δ ≻ t ⋅ δ) ∧ (s ≽ t ⟶ s ⋅ δ ≽ t ⋅ δ)"
by (rule wpo_stable'[OF ssimple])
theorem wpo_order_pair: "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
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
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
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
text ‹If we demand strong normalization of the underlying order and the precedence,
then also WPO is strongly normalizing.›
locale wpo_with_SN_assms = wpo_with_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"
begin
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_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 -
interpret order_pair WPO_S WPO_NS by (rule wpo_order_pair)
show ?thesis
proof
show "SN WPO_S" using WPO_S_SN .
qed
qed
end
end