section ‹The Weighted Path Order›
theory WPO
imports
QTRS.Term_Order
QTRS.Lexicographic_Extension
begin
definition af_compatible_status :: "'f af ⇒ 'f status ⇒ bool"
where
"af_compatible_status π σ ⟷ (∀ f m. set (status σ (f, m)) ⊆ π (f, m))"
lemma af_compatible_status_full_af: "af_compatible_status full_af σ"
unfolding af_compatible_status_def full_af_def using status[of σ] by auto
context
fixes "pr" :: "('f × nat ⇒ 'f × nat ⇒ bool × bool)"
and prl :: "'f × nat ⇒ bool"
and n :: nat
and S NS :: "('f, 'v) term rel"
and σ :: "'f status"
begin
fun wpo :: "('f, 'v) term ⇒ ('f, 'v) term ⇒ bool × bool"
where
"wpo s t =
(case s of
Var x ⇒ (False,
(case t of
Var y ⇒ x = y
| Fun g ts ⇒ (s, t) ∈ NS ∧ status σ (g, length ts) = [] ∧ prl (g, length ts)))
| Fun f ss ⇒
if (s, t) ∈ S then (True, True)
else if (s, t) ∈ NS then
if ∃ i ∈ set (status σ (f, length ss)). snd (wpo (ss ! i) t) then (True, True)
else
(case t of
Var _ ⇒ (False, False)
| Fun g ts ⇒
(case pr (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 lex_ext wpo n (map (λ i. ss ! i) (status σ (f, length ss)))
(map (λ i. ts ! i) (status σ (g, length ts)))
else (False, False)))
else (False, False))"
declare wpo.simps [simp del]
lemma wpo_s_imp_ns: "fst (wpo s t) ⟹ snd (wpo s t)"
using lex_ext_stri_imp_nstri
unfolding wpo.simps[of s t]
by (auto simp: split: term.splits if_splits prod.splits)
end
locale wpo_alg_pr = ws_redpair_order S NS σσ + precedence prc prl
for NS S :: "('f, 'v) trs"
and prc :: "'f × nat ⇒ 'f × nat ⇒ bool × bool"
and prl :: "'f × nat ⇒ bool"
and n :: nat
and σσ :: "'f status"
begin
abbreviation "σ ≡ status σσ"
abbreviation "wpo_pr ≡ wpo prc prl n S NS σσ"
abbreviation "wpo_s ≡ λ s t. fst (wpo_pr s t)"
abbreviation "wpo_ns ≡ λ s t. snd (wpo_pr s t)"
lemmas wpo_s_imp_ns = wpo_s_imp_ns[of prc prl n S NS σσ]
lemmas wpo_simps = wpo.simps[of prc prl n S NS σσ]
definition "S_wpo ≡ {(s,t). wpo_s s t}"
definition "NS_wpo ≡ {(s,t). wpo_ns s t}"
lemma σE: "i ∈ set (σ (f, length ss)) ⟹ ss ! i ∈ set ss" by (rule status_aux)
lemma wpo_ns_refl:
shows "wpo_ns s s"
proof (induct s)
case (Fun f ss)
{
fix i
assume si: "i ∈ set (σ (f,length ss))"
from NS_arg[OF this] have "(Fun f ss, ss ! i) ∈ NS" .
with si Fun[OF σE[OF si]] have "wpo_s (Fun f ss) (ss ! i)" unfolding wpo_simps[of "Fun f ss" "ss ! i"]
by auto
} note wpo_s = this
let ?ss = "map (λ i. ss ! i) (σ (f,length ss))"
have rec11: "snd (lex_ext wpo_pr n ?ss ?ss)"
by (rule all_nstri_imp_lex_nstri, insert σE[of _ f ss], auto simp: Fun)
thus ?case using refl_NS_point prc_refl wpo_s
by (auto simp: wpo_simps[of "Fun f ss" "Fun f ss"])
qed (simp add: wpo_simps)
lemma wpo_ns_imp_NS: "wpo_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: "wpo_s s t ⟹ (s,t) ∈ NS"
by (rule wpo_ns_imp_NS[OF wpo_s_imp_ns])
lemma S_imp_wpo_s: assumes st: "(s,t) ∈ S"
shows "wpo_s s t"
proof (cases s)
case (Fun f ss)
thus ?thesis using st by (auto simp: wpo_simps)
next
case (Var x)
from SN_imp_minimal[OF SN, rule_format, of undefined UNIV]
obtain s where "⋀ u. (s,u) ∉ S" by blast
with S_stable[OF st[unfolded Var], of "λ _. s"]
have False by auto
thus ?thesis by auto
qed
lemma wpo_least_1: assumes "prl (f,length ss)"
and "(t, Fun f ss) ∈ NS"
and "σ (f,length ss) = []"
shows "wpo_ns 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 (simp add: prc lex_ext_least_1)
qed
lemma wpo_least_2: assumes "prl (f,length ss)" (is "prl ?f")
and "(Fun f ss, t) ∉ S"
and "σ (f,length ss) = []"
shows "¬ wpo_s (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 lex_ext_least_2 prc)
qed
lemma wpo_least_3: assumes "prl (f,length ss)" (is "prl ?f")
and ns: "wpo_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"
shows "wpo_ns u t"
proof (cases "(Fun f ss, t) ∈ S ∨ (u, Fun f ss) ∈ S ∨ (u, t) ∈ S")
case True
thm compat_S_NS_point
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 (Var x)
with ns False ss have False by (simp add: wpo_simps split: if_splits)
thus ?thesis ..
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)
thus ?thesis ..
qed
qed
qed
lemma wpo_compat[rule_format]:
shows "
((wpo_ns s t) ∧ (wpo_s t u) ⟶ (wpo_s s u)) ∧
((wpo_s s t) ∧ (wpo_ns t u) ⟶ (wpo_s s u)) ∧
((wpo_ns s t) ∧ (wpo_ns t u) ⟶ (wpo_ns s u))" (is "?tran s t u")
proof (rule
wf_induct[OF wf_measures[of "[λ (s,t,u). size s, λ (s,t,u). size t, λ (s,t,u). size u]"],
of "λ (s,t,u). ?tran s t u" "(s,t,u)", simplified], clarify)
fix s t u :: "('f,'v)term"
assume ind: "∀ s' t' u'. (size s' < size s ⟶ ?tran s' t' u') ∧ (size s' = size s ∧ (size t' < size t ∨ size t' = size t ∧ size u' < size u) ⟶ ?tran s' t' u')"
let ?GR = "λ s t. (wpo_s s t)"
let ?GE = "λ s t. (wpo_ns s t)"
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
hence 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]
{
assume "?GR t u"
with Var have False by (cases u, auto)
}
moreover
{
assume gr: "?GR s t" and ge: "?GE 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" .
have "?GR s u"
proof (cases u)
case (Var y)
with ge ‹t = Var x› have "t = u" by auto
with gr show ?thesis by auto
next
case (Fun h us)
let ?h = "(h,length us)"
from Fun ge Var have us: "σ ?h = []" and pri: "prl ?h" by auto
from gr Var obtain f ss where s: "s = Fun f ss" by (cases s, auto)
let ?f = "(f,length ss)"
from s gr Var False obtain i where i: "i ∈ set (σ ?f)" and sit: "wpo_ns (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 "?GE (ss ! i) u" unfolding Fun us .
with i have "∃ i ∈ set (σ ?f). ?GE (ss ! i) u" by auto
with s suA show ?thesis by simp
qed
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u"
have "?GE s u"
proof (cases u)
case (Var y)
with ge2 ‹t = Var x› have "t = u" by auto
with ge1 show ?thesis by auto
next
case (Fun h us)
let ?h = "(h,length us)"
from Fun ge2 Var have us: "σ ?h = []" and pri: "prl ?h" by auto
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
}
ultimately show ?thesis by blast
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)
{
assume gr: "?GR s t"
with Var Fun have False by (auto simp: wpo_simps)
}
moreover
{
assume ge: "?GE s t" and gr: "?GR t u"
with Var Fun have pri: "prl ?g" and "σ ?g = []" by (auto simp: wpo_simps)
with gr Fun have False using wpo_least_2[OF pri, of u] False by auto
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u"
with Var Fun have pri: "prl ?g" and empty: "σ ?g = []" by (auto simp: wpo_simps)
from wpo_ns_imp_NS[OF ge1] Var Fun empty have ns: "(Var x, Fun g ts) ∈ NS" by simp
have "?GE s u"
proof (rule wpo_least_3[OF pri ge2[unfolded Fun empty]
wpo_ns_imp_NS[OF ge1[unfolded Fun empty]] empty], rule)
fix v
assume S: "(Fun g ts, v) ∈ S"
from SN_imp_minimal[OF SN, rule_format, of undefined UNIV]
obtain s where "⋀ u. (s,u) ∉ S" by blast
with compat_NS_S_point[OF NS_stable[OF ns, of "λ _. s"] S_stable[OF S, of "λ _. s"]]
show False by auto
qed
}
ultimately show ?thesis by blast
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. ?GE (ss ! i) t"
let ?t1 = "∃ j ∈ ?ts. ?GE (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; u' ∈ set us⟧ ⟹ ?tran2 s' t' u'" by blast
{
assume ge1: "?GE s t" and ge2: "?GR 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 "?GR s u"
proof (cases ?s1)
case True
from this obtain i where i: "i ∈ ?ss" and ges: "?GE (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 "?GR (ss ! i) u" by auto
hence "?GE (ss ! i) u" by (rule wpo_s_imp_ns)
with i s suA show ?thesis by (cases u, auto simp: wpo_simps)
next
case False
show ?thesis
proof (cases ?t1)
case True
from this obtain j where j: "j ∈ ?ts" and ges: "?GE (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': "?GR 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 "?GR 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 ?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: "?GE ?s ?t" and ge2: "?GR ?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. ?GR ?s (ts ! j)" by (auto split: if_splits prod.splits)
from ‹¬ ?t1› t u ge2 tuS have tu': "∀ k ∈ ?us. ?GR ?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)
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] ‹?GE s t›
ind[rule_format, of s t "us ! k"] k have "?GR 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" by blast+
from fg ‹¬ ?s1› t ge1 st' prc nfg
have lex1: "snd (lex_ext wpo_pr n ?mss ?mts)" by auto
from gh ‹¬ ?t1› u ge2 tu' prc2 ngh
have lex2: "fst (lex_ext wpo_pr n ?mts ?mus)" by auto
note σE = σE[of _ f ss] σE[of _ g ts] σE[of _ h us]
from lex1 lex2 lex_ext_compat[OF ind3, of ?mss ?mts ?mus]
have "fst (lex_ext wpo_pr n ?mss ?mus)" using σE by force
with s u fh su' prc3 suA show ?thesis by (simp add: wpo_simps)
qed
qed
qed
}
moreover
{
assume ge1: "?GR s t" and ge2: "?GE 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 "?GR s u"
proof (cases ?s1)
case True
from True obtain i where i: "i ∈ ?ss" and ges: "?GE (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 "?GE (ss ! i) u" by auto
with i s' s suA show ?thesis by (cases u, auto simp: wpo_simps)
next
case False
show ?thesis
proof (cases ?t1)
case True
from this obtain j where j: "j ∈ ?ts" and ges: "?GE (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': "?GR 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 "?GR 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 ?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: "?GR ?s ?t" and ge2: "?GE ?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. ?GR ?s (ts ! j)" by (auto split: if_splits prod.splits)
from ‹¬ ?t1› t u ge2 tuS have tu': "∀ k ∈ ?us. ?GR ?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)
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 ‹?GR s t›]
ind[rule_format, of s t "us ! k"] k have "?GR 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" by blast+
from fg ‹¬ ?s1› t ge1 st' prc nfg
have lex1: "fst (lex_ext wpo_pr n ?mss ?mts)" by auto
from gh ‹¬ ?t1› u ge2 tu' prc2 ngh
have lex2: "snd (lex_ext wpo_pr n ?mts ?mus)" by auto
from lex1 lex2 lex_ext_compat[OF ind3, of ?mss ?mts ?mus]
have "fst (lex_ext wpo_pr n ?mss ?mus)" using σE by force
with s u fh su' prc3 suA show ?thesis by (simp add: wpo_simps)
qed
qed
qed
}
moreover
{
assume ge1: "?GE s t" and ge2: "?GE t u" and ngt1: "¬ ?GR s t" and ngt2: "¬ ?GR 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)
from t ‹¬ ?t1› ge2 tuA ngt2 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 ?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: "?GE ?s ?t" and ge2: "?GE ?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: "¬ ?GR ?s ?t" and ngt2: "¬ ?GR ?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. ?GR ?s (ts ! j)" by (cases ?thesis, auto)
from ‹¬ ?t1› u ge2 have tu': "∀ k ∈ ?us. ?GR ?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 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] ‹?GE s t›
ind[rule_format, of s t "us ! k"] k have "?GR 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)
from ‹¬ ?s1› st' ge1 s t fg nfg
have lex1: "snd (lex_ext wpo_pr n ?mss ?mts)" by (auto simp: prc)
from ‹¬ ?t1› tu' ge2 t u gh ngh
have lex2: "snd (lex_ext wpo_pr n ?mts ?mus)" by (auto simp: prc2)
note σE = σE[of _ f ss] σE[of _ g ts] σE[of _ h us]
from lex1 lex2 lex_ext_compat[OF ind3, of ?mss ?mts ?mus]
have "snd (lex_ext wpo_pr n ?mss ?mus)" using σE by force
with fg gh su' s u fh suA
have "?GE s u" by (auto simp: prc3 wpo_simps)
}
ultimately
show ?thesis using wpo_s_imp_ns by auto
qed
qed
qed
qed
lemma subterm_wpo_s_arg: assumes i: "i ∈ set (σ (f,length ss))"
shows "wpo_s (Fun f ss) (ss ! i)"
proof -
have refl: "wpo_ns (ss ! i) (ss ! i)" by (rule wpo_ns_refl)
with i have "∃ t ∈ set (σ (f,length ss)). wpo_ns (ss ! i) (ss ! i)" by auto
with NS_arg[OF i] i
show ?thesis by (auto simp: wpo_simps)
qed
lemma subterm_wpo_ns_arg: assumes i: "i ∈ set (σ (f,length ss))"
shows "wpo_ns (Fun f ss) (ss ! i)"
by (rule wpo_s_imp_ns[OF subterm_wpo_s_arg[OF i]])
lemma wpo_ns_pre_mono: fixes f and bef aft :: "('f,'v)term list"
defines "σf ≡ σ (f, Suc (length bef + length aft))"
assumes rel: "(wpo_ns s t)"
shows "(∀j∈set σf.
wpo_s (Fun f (bef @ s # aft)) ((bef @ t # aft) ! j))
∧ (Fun f (bef @ s # aft), (Fun f (bef @ t # aft))) ∈ NS
∧ (∀ i < length σf. wpo_ns ((map (op ! (bef @ s # aft)) σf) ! i) ((map (op ! (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 ?σ"
hence id: "⋀ ss. (map (op ! ss) ?σ) ! i = ss ! (?σ ! i)" by auto
show "wpo_ns ((map (op ! ?ss) ?σ) ! i) ((map (op ! ?ts) ?σ) ! i)"
proof (cases "?σ ! i = length bef")
case True
thus ?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 ?σ"
hence "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
hence "?ss ! j = ?ts ! j" by (rule append_Cons_nth_not_middle)
with s show ?thesis by simp
next
case True
with s have "wpo_s ?s s" by simp
with rel wpo_compat have "wpo_s ?s t" by blast
with True show ?thesis by simp
qed
qed
with ‹?three› NS_mono[OF stA] show ?thesis unfolding σf_def by auto
qed
lemma wpo_ns_mono: assumes rel: "(wpo_ns s t)"
shows "(wpo_ns (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_pr n (map (op ! ?ss) ?σ) (map (op ! ?ts) ?σ))"
by (rule all_nstri_imp_lex_nstri, intro allI impI, insert wpo_ns_pre_mono[OF rel], auto)
thus ?thesis unfolding wpo_simps[of ?s ?t] term.simps id prc_refl
by auto
qed
lemma wpo_stable: fixes δ :: "('f,'v)subst"
shows "((wpo_s s t) ⟶ (wpo_s (s ⋅ δ) (t ⋅ δ))) ∧ ((wpo_ns s t) ⟶ (wpo_ns (s ⋅ δ) (t ⋅ δ)))"
(is "?p s t")
proof (rule wf_induct[OF wf_measure, of "λ (s,t). size s + size t" "λ (s,t). ?p s t" "(s,t)", simplified], clarify)
fix s t :: "('f,'v)term"
assume "∀ s' t'. size s' + size t' < size s + size t ⟶ ?p s' t'"
note IH = this[rule_format]
let ?s = "s ⋅ δ"
let ?t = "t ⋅ δ"
note simps = wpo_simps[of s t] wpo_simps[of ?s ?t]
show "?p s t"
proof (cases "((s,t) ∈ S ∨ (?s,?t) ∈ S) ∨ ((s,t) ∉ NS ∨ ¬ wpo_ns s t)")
case True
thus ?thesis
proof
assume "(s,t) ∈ S ∨ (?s,?t) ∈ S"
with S_stable[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
hence not: "((s,t) ∈ S) = False" "((?s,?t) ∈ S) = False"
and stA: "(s,t) ∈ NS" and ns: "wpo_ns s t" by auto
from NS_stable[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)
thus ?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 thus ?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 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)
hence "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 (Var y) note t = this
from ns[unfolded simps] obtain i
where si: "i ∈ ?ss" and ns: "wpo_ns (ss ! i) t"
unfolding s t by (auto split: if_splits)
from si_arg[OF this] show ?thesis .
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
hence 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 (op ! ss) (σ ?f)"
let ?mmts = "map (op ! ts) (σ ?g)"
let ?Mmss = "map (op ! ?mss) (σ ?f)"
let ?Mmts = "map (op ! ?mts) (σ ?g)"
let ?ls = "length (σ ?f)"
let ?lt = "length (σ ?g)"
from False ns have "snd (lex_ext wpo_pr 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
{
fix i
assume "i < ?ls" "i < ?lt"
hence 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
hence "size (ss ! (σ ?f ! i)) < size s" "size (ts ! (σ ?g ! i)) < size t" unfolding s t by (auto simp: size_simps)
hence "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
from choice have "?stri ∨ (¬ ?stri ∧ ?nstri)" by blast
thus ?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_pr n ?Mmss ?Mmts)" unfolding lex_ext_iff
by auto
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
assume "¬ ?stri ∧ ?nstri"
hence ?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_pr n ?Mmss ?Mmts)" unfolding lex_ext_iff
by auto
with 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 this[unfolded simps, unfolded s t term.simps p split id] False
have "fst (lex_ext wpo_pr 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
hence "fst (lex_ext wpo_pr n ?Mmss ?Mmts)" using len unfolding lex_ext_iff by auto
with 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
qed
qed
qed
qed
qed
qed
lemma wpo_s_SN: "SN {(s,t). wpo_s s t}"
proof -
{
fix t :: "('f,'v)term"
let ?Rp = "wpo_s"
let ?R = "{(s,t). ?Rp s t}"
let ?S = "λx. SN_on ?R {x}"
note iff = SN_on_all_reducts_SN_on_conv[of ?R]
{
fix x
have "?S (Var x)" unfolding iff[of "Var x"]
proof (intro allI impI)
fix s
assume "(Var x, s) ∈ ?R"
hence False by (cases s, auto simp: wpo_simps)
thus "?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')). ?Slist f ab ∧ fst (lex_ext wpo_pr n (map (op ! ab) (σ f)) (map (op ! ab') (σ g)))}"
let ?r0 = "lex_two {(f,g). fst (prc f g)} {(f,g). snd (prc f g)} ?r3"
let ?ge = "wpo_ns"
let ?gr = ?Rp
{
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 ?r' = "{((f,ys), (g,xs)).
(∀ yi ∈set ((map (op ! ys) (σ f))). SN_on {(s, t). wpo_s s t} {yi})
∧ fst (lex_ext wpo_pr n (map (op ! ys) (σ f)) (map (op ! xs) (σ g)))}"
{
fix i
from SS[rule_format, of i]
have "(S i, S (Suc i)) ∈ ?r'" by auto
}
hence 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_pr" n, OF wpo_s_imp_ns this]
have tmp: "SN {(ys, xs). (∀y∈set ys. SN_on {(s, t). wpo_s s t} {y}) ∧ fst (lex_ext wpo_pr n ys xs)}"
(is "SN ?R") .
have id: "?r' = inv_image ?R (λ (f,ys). map (op ! ys) (σ f))" by auto
from SN_inv_image[OF tmp]
have "SN ?r'" unfolding id .
hence "SN_on ?r' {(S 0)}" unfolding SN_defs by blast
with Hf have False ..
}
hence "SN_on ?r3 {ab}" unfolding SN_on_def unfolding singleton_iff ..
}
hence "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'"
hence "(a1,a3) ∈ ?r'"
by (cases "prc a1 a2", cases "prc a2 a3", cases "prc a1 a3",
insert prc_compat[of a1 a2 _ _ a3], force)
}
thus "?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"
def 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) ∈ ?R"
hence "?gr ?t s" by simp
thus "?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: "?gr ?t ?s" by auto
show "?S ?s"
proof (cases "∃ i ∈ set (σ ?f). ?ge (ts ! i) ?s")
case True
then obtain i where "i ∈ set (σ ?f)" and ge: "?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) ∈ ?R"
with wpo_compat ge have u: "?gr (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
hence "((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 "?ge ?s (ss ! i)"
by (rule subterm_wpo_ns_arg[OF i])
with t_gr_s have ts: "?gr ?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). ?gr ?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
hence "((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
from False oFalse t_gr_s small_ss f_ge_g
have lex: "fst (lex_ext wpo_pr n (map (op ! ts) (σ ?f)) (map (op ! ss) (σ ?g)))"
by (cases ?thesis, auto)
from False lex ts f_ge_g 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
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_pr s t)}" .
qed
abbreviation "WPO_S ≡ {(s,t). wpo_s s t}"
abbreviation "WPO_NS ≡ {(s,t). wpo_ns s t}"
lemma wpo_redtriple_order: "redtriple_order WPO_S WPO_NS WPO_NS"
proof
show "SN WPO_S" using wpo_s_SN .
show "subst.closed WPO_S" using wpo_stable by auto
show "subst.closed WPO_NS" using wpo_stable by auto
show "ctxt.closed WPO_NS" using wpo_ns_mono one_imp_ctxt_closed[of WPO_NS] by blast
show "refl WPO_NS" using wpo_ns_refl unfolding refl_on_def by auto
show "trans WPO_NS" using wpo_compat unfolding trans_def by blast
show "trans WPO_S" using wpo_compat wpo_s_imp_ns unfolding trans_def by blast
show "WPO_NS O WPO_S ⊆ WPO_S" using wpo_compat by blast
show "WPO_S O WPO_NS ⊆ WPO_S" using wpo_compat by blast
show "WPO_S ⊆ WPO_NS" using wpo_s_imp_ns by blast
qed
lemma ce_σ: assumes "{0,1} ⊆ set (σ (f,Suc (Suc k)))"
shows "ce_trs (f,k) ⊆ WPO_S ∧ ce_trs (f,k) ⊆ WPO_NS"
proof -
{
fix s t :: "('f,'v)term"
assume "(s,t) ∈ ce_trs (f,k)"
from this[unfolded ce_trs.simps]
obtain u v where s: "s = Fun f (u # v # replicate k (Var undefined))" (is "_ = Fun _ ?ss")
and t: "t = u ∨ t = v" by auto
from t subterm_wpo_s_arg[of 0 f ?ss] subterm_wpo_s_arg[of 1 f ?ss] assms
have "(s,t) ∈ WPO_S" unfolding s by (cases, auto)
}
thus ?thesis using wpo_s_imp_ns by blast
qed
context
fixes π :: "'f af"
assumes af_NS: "af_compatible π NS"
and af_σ: "af_compatible_status π σσ"
begin
lemma af_σ: "i < m ⟹ i ∈ π (f,m) ∨ i ∉ set (σ (f,m))"
using af_σ[unfolded af_compatible_status_def] by blast
lemma wpo_af_compatible: "af_compatible π WPO_NS"
unfolding af_compatible_def
proof (intro allI)
fix f and bef aft :: "('f,'v)term list" and s t
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
let ?ss = "bef @ s # aft"
let ?ts = "bef @ t # aft"
let ?s = "Fun f ?ss"
let ?t = "Fun f ?ts"
let ?σ = "σ (f,?n)"
show "?i ∈ π (f, ?n) ∨ (?s, ?t) ∈ WPO_NS"
proof (cases "?i ∈ π (f, ?n)")
case False
have i: "?i < ?n" by auto
from af_σ[OF i, of f] False have iσ: "?i ∉ set ?σ" by auto
from af_NS[unfolded af_compatible_def, rule_format, of bef f aft s t] False
have id: "((?s, ?t) ∈ NS) = True" "length ?ss = ?n" "length ?ts = ?n" by auto
have "∀j∈set ?σ. wpo_s ?s (?ts ! j)" (is ?one)
proof
fix j
assume j: "j ∈ set ?σ"
with iσ have ji: "j ≠ ?i" by auto
hence id: "?ts ! j = ?ss ! j" by (rule append_Cons_nth_not_middle)
show "wpo_s ?s (?ts ! j)" unfolding id
by (rule subterm_wpo_s_arg, insert j, auto)
qed
hence one: "?one = True" by simp
have two: "map (op ! ?ts) ?σ = map (op ! ?ss) ?σ" (is "?mts = ?mss")
proof (rule nth_equalityI, force, unfold length_map, intro allI impI)
fix i
assume i: "i < length ?σ"
with iσ have "?σ ! i ≠ ?i" unfolding set_conv_nth by auto
thus "?mts ! i = ?mss ! i" using i by (simp add: nth_append)
qed
have "snd (lex_ext wpo_pr n ?mss ?mts)" unfolding two
by (rule all_nstri_imp_lex_nstri, insert wpo_ns_refl, auto)
hence "wpo_ns ?s ?t" unfolding wpo_simps[of ?s ?t] term.simps id one
prc_refl by auto
thus ?thesis by blast
qed simp
qed
end
lemma wpo_ce_af_redtriple_order:
assumes ce: "∃n. ∀m≥n. ∀ f. {0,1} ⊆ set (σ (f, Suc (Suc m)))"
and pi: "af_compatible π NS" "af_compatible_status π σσ"
shows "mono_ce_af_redtriple_order WPO_S WPO_NS WPO_NS π"
proof -
interpret redtriple_order WPO_S WPO_NS WPO_NS by (rule wpo_redtriple_order)
from assms obtain n where "⋀ m f. m ≥ n ⟹ {0,1} ⊆ set (σ (f, Suc (Suc m)))" by blast
from ce_σ[OF this] have "∃n. ∀m≥n. ∀c. ce_trs (c, m) ⊆ WPO_NS ∧ ce_trs (c,m) ⊆ WPO_S" by blast
with wpo_af_compatible[OF pi]
show ?thesis using full_af by (unfold_locales, blast+)
qed
context
assumes all: "⋀ f k. set (σ (f,k)) = {0 ..< k}"
begin
lemma subterm_wpo_s: "s ⊳ t ⟹ wpo_s 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 all[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: "wpo_ns (ss ! i) t" and i: "i < length ss" by auto
from all[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 all this] ns ii
show ?case by (auto simp: wpo_simps)
qed
lemma subterm_wpo_ns: assumes supteq: "s ⊵ t" shows "wpo_ns s t"
proof -
from supteq have "s = t ∨ s ⊳ t" by auto
thus ?thesis
proof
assume "s = t" thus ?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: "wpo_s s t"
shows "(wpo_s (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
from all[of f ?len] have "length bef ∈ set ?σ" by auto
then obtain i where σi: "?σ ! i = length bef" and i: "i < length ?σ"
unfolding set_conv_nth by force
let ?mss = "map (op ! ?ss) ?σ"
let ?mts = "map (op ! ?ts) ?σ"
have "fst (lex_ext wpo_pr 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 "wpo_ns (?mss ! j) (?mts ! j)" by blast
qed
thus ?thesis unfolding wpo_simps[of ?s ?t] term.simps id prc_refl
by auto
qed
lemma ctxt_closed_WPO_S: "ctxt.closed WPO_S"
by (rule one_imp_ctxt_closed[of WPO_S], insert wpo_s_mono, auto)
lemma wpo_mono_ce_af_redtriple_order:
"mono_ce_af_redtriple_order WPO_S WPO_NS WPO_NS full_af"
by (rule wpo_ce_af_redtriple_order,
insert all full_af af_compatible_status_full_af, auto)
end
end
end