theory Term_Order
imports
TRS.Trs
Auxx.List_Order
Complexity
Weighted_Path_Order.Precedence
Weighted_Path_Order.Status
begin
locale compat =
fixes S :: "'a rel"
and NS :: "'a rel"
assumes compat: "NS O S ⊆ S"
begin
lemma trCompat: "NS^* O S ⊆ S" using compat by (rule compat_tr_compat)
lemma trans_split_NS_S_union:
assumes "r^* ⊆ (NS ∪ S)^*"
shows "r^* ⊆ S O S^* O NS^* ∪ NS^*"
proof(rule subrelI)
fix x y
assume "(x, y) ∈ r^*"
with assms have "(x,y) ∈ (NS ∪ S)^*" by auto
then show "(x,y) ∈ S O S^* O NS^* ∪ NS^*" using compatible_rtrancl_split[where S = S and NS = NS] compat by auto
qed
end
locale redpair = SN_ars S for
S :: "('f,'v)trs" + fixes
NS :: "('f,'v)trs"
assumes
wm_NS: "ctxt.closed NS"
and subst_S: "subst.closed S"
and subst_NS: "subst.closed NS"
begin
lemmas S_stable = subst.closedD[OF subst_S]
lemmas NS_stable = subst.closedD[OF subst_NS]
lemmas NS_mono = ctxt_closed_one[OF wm_NS]
end
locale redpair_order = redpair S NS + pre_order_pair S NS for S NS :: "('f,'v)trs"
context redpair
begin
lemma redpair_order: "redpair_order (S^+) (NS^*)" (is "redpair_order ?S ?NS")
proof
show "subst.closed ?NS" by (rule subst.closed_rtrancl[OF subst_NS])
show "subst.closed ?S" by (rule subst.closed_trancl[OF subst_S])
show "ctxt.closed ?NS" by (rule ctxt.closed_rtrancl[OF wm_NS])
show "SN ?S" by (rule SN_imp_SN_trancl[OF SN])
show "refl ?NS" by (rule refl_rtrancl)
show "trans ?NS" by (rule trans_rtrancl)
show "trans ?S" by (rule trans_trancl)
qed
lemma subst_NSS: "subst.closed (NS ∪ S)"
using subst_S and subst_NS by blast
lemma mono_NSS: "ctxt.closed S ⟹ ctxt.closed (NS ∪ S)" using wm_NS by blast
lemma mono_rstep_NSS:
assumes mono: "ctxt.closed S"
shows "rstep (NS ∪ S) ⊆ NS ∪ S"
proof -
from rstep_subset[OF mono_NSS[OF mono] subst_NSS]
show ?thesis by auto
qed
lemma mono_rstep_S:
assumes mono: "ctxt.closed S"
shows "rstep S ⊆ S"
proof -
from rstep_subset[OF mono subst_S]
show ?thesis by auto
qed
lemma mono_rstep_NSS_rtrancl:
assumes mono: "ctxt.closed S"
shows "(rstep (NS ∪ S))^* ⊆ (NS ∪ S)^*"
by (rule rtrancl_mono[OF mono_rstep_NSS[OF mono]])
lemma rstep_NS: "rstep NS ⊆ NS"
using rstep_subset[OF wm_NS subst_NS] by simp
lemma rstep_NS_rtrancl: "(rstep NS)^* ⊆ NS^*"
by (rule rtrancl_mono[OF rstep_NS])
end
locale pre_redtriple = redpair S NS
for S NS :: "('f,'v)trs" +
fixes NST :: "('f,'v)trs"
assumes compat_NST: "NST O S ⊆ S"
and subst_NST: "subst.closed NST"
locale pre_redtriple_order = pre_redtriple S NS NST + redpair_order S NS
for S NS NST :: "('f,'v)trs" +
assumes trans_NST: "trans NST"
lemma (in pre_redtriple) pre_redtriple_order:
"pre_redtriple_order (S^+) (NS^*) (NST^*)"
(is "pre_redtriple_order ?S ?NS ?NST")
proof -
from redpair_order interpret redpair_order ?S ?NS .
show ?thesis
proof
show "subst.closed ?NST" by (rule subst.closed_rtrancl[OF subst_NST])
show "?NST O ?S ⊆ ?S" unfolding trancl_unfold_left
proof (clarsimp)
fix x y z u
assume "(x,y) ∈ ?NST" and "(y,z) ∈ S" and zu: "(z,u) ∈ S^*"
with compat.trCompat[unfolded compat_def, OF compat_NST] have "(x,z) ∈ S" by blast
with zu show "(x,u) ∈ S O S^*" by auto
qed
show "trans ?NST" by (rule trans_rtrancl)
qed
qed
locale root_redtriple = pre_redtriple S NS NST for S NS NST :: "('f,'v)trs" +
assumes
compat_NS_root: "(s,t) ∈ NS ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ NST"
begin
lemma nrrstep_imp_NST: assumes R: "R ⊆ NS"
and step: "(s,t) ∈ nrrstep R"
shows "(s,t) ∈ NST"
proof -
from step[unfolded nrrstep_def']
obtain l r C σ where one: "(l,r) ∈ R" "C ≠ □" "s = C⟨l⋅σ⟩" "t = C⟨r⋅σ⟩" by auto
then obtain f bef D aft where "C = More f bef D aft" by (cases C, auto)
with one have id: "s = Fun f (bef @ D⟨l⋅σ⟩ # aft)" "t = Fun f (bef @ D⟨r⋅σ⟩ # aft)" by auto
from one R have "(l,r) ∈ NS" by auto
with subst_NS have "(l⋅σ,r⋅σ) ∈ NS" unfolding subst.closed_def by auto
from ctxt.closedD[OF wm_NS this] have "(D⟨l⋅σ⟩,D⟨r⋅σ⟩) ∈ NS" .
from compat_NS_root[OF this]
show "(s,t) ∈ NST" unfolding id .
qed
lemma compat_NSs_root:
"(s,t) ∈ NS^* ⟹ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ NST^*"
by (induct rule: rtrancl_induct, insert compat_NS_root[of _ _ f bef aft], force+)
lemma nrrsteps_imp_NST: assumes R: "R ⊆ NS"
and steps: "(s,t) ∈ (nrrstep R)^*"
shows "(s,t) ∈ NST^*"
using steps
by (induct rule: converse_rtrancl_induct, insert nrrstep_imp_NST[OF R], force+)
lemma nrrstep_compat: "nrrstep NS O S ⊆ S"
proof
fix s t
assume "(s,t) ∈ nrrstep NS O S"
then obtain u where NS: "(s,u) ∈ nrrstep NS" and u: "(u,t) ∈ S" by auto
from compat_NST nrrstep_imp_NST[OF subset_refl NS] u show "(s,t) ∈ S" by auto
qed
lemma compat_NSTs: "(s,t) ∈ NST^* ⟹ (t,u) ∈ S ⟹ (s,u) ∈ S"
by (induct rule: converse_rtrancl_induct, insert compat_NST, auto)
end
sublocale root_redtriple ⊆ nrr: compat S "nrrstep NS ∪ NST"
by (unfold_locales, insert nrrstep_compat compat_NST, auto)
locale redtriple = pre_redtriple S NS NST + compat_pair S NS for S NS NST :: "('f,'v)trs"
+ assumes S_imp_NS: "S ⊆ NS"
sublocale redtriple ⊆ both: compat S "NS ∪ NST"
by (unfold_locales, insert compat_NS_S compat_NST, auto)
sublocale redtriple ⊆ NS: compat S NS
by (unfold_locales, insert compat_NS_S compat_NST, auto)
locale redtriple_order = redtriple S NS NST + pre_redtriple_order S NS NST + order_pair S NS for S NS NST :: "('f,'v)trs" +
assumes refl_NST: "refl NST"
sublocale redtriple_order ⊆ SN_order_pair
by (unfold_locales, rule SN)
locale root_redtriple_order = root_redtriple S NS NST + pre_redtriple_order S NS NST for S NS NST :: "('f,'v)trs"
lemma (in redtriple) redtriple_order: "redtriple_order (S^+) (NS^*) (NST^*)"
(is "redtriple_order ?S ?NS ?NST")
proof -
from pre_redtriple_order interpret pre_redtriple_order ?S ?NS ?NST .
show ?thesis
proof
show "?NS O ?S ⊆ ?S" unfolding trancl_unfold_left by (simp add: order_simps)
show "?S O ?NS ⊆ ?S" unfolding trancl_unfold_right by (simp add: order_simps)
show "refl ?NST" by (rule refl_rtrancl)
show "?S ⊆ ?NS" using trancl_mono[OF _ S_imp_NS] by force
qed
qed
lemma (in root_redtriple) root_redtriple_order: "root_redtriple_order (S^+) (NS^*) (NST^*)"
proof -
let ?NS = "NS^*"
let ?NST = "NST^*"
let ?S = "S^+"
from pre_redtriple_order interpret pre_redtriple_order ?S ?NS ?NST .
show ?thesis
proof
fix s t f bef aft u
assume st: "(s,t) ∈ ?NS"
have "(s,t) ∈ (rstep NS)^*" by (rule set_mp[OF rtrancl_mono st], auto)
from nrrsteps_imp_NST[OF _ rsteps_ctxt_imp_nrrsteps[OF this, of "More f bef □ aft"]]
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ?NST" by auto
qed
qed
sublocale redtriple ⊆ root_redtriple
proof (unfold_locales)
fix s t f bef aft u
assume NS: "(s,t) ∈ NS"
from ctxt_closed_one[OF wm_NS NS, of f bef aft]
have "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ NS" .
then show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ NST"
oops
lemma (in redpair_order) all_ctxt_closed: "all_ctxt_closed F NS"
by (rule trans_ctxt_imp_all_ctxt_closed[OF trans_NS refl_NS wm_NS])
fun ce_trs :: "('f × nat) ⇒ ('f,'v)trs"
where "ce_trs (c,n) =
{(Fun c (t # s # replicate n (Var undefined)), t) | t s. True}
∪ {(Fun c (t # s # replicate n (Var undefined)), s) | t s. True}"
fun comb :: "('f × nat) ⇒ ('f,'v)term list ⇒ ('f,'v)term" where
"comb (c,n) (t # ts) = Fun c (t # comb (c,n) ts # replicate n (Var undefined))"
lemma ce_trs_sound: "t ∈ set ts ⟹ (comb cn ts, t) ∈ (rstep (ce_trs cn))^+"
proof (induct ts, simp)
case (Cons s ss)
obtain c n where cn: "cn = (c,n)" by force
show ?case
proof (cases "s = t")
case True
with cn have "(comb cn (s # ss),s) ∈ ce_trs cn" by simp
then have "(comb cn (s # ss),t) ∈ rstep (ce_trs cn)" using True by blast
then show ?thesis using True by force
next
case False
then have ind: "(comb cn ss, t) ∈ (rstep (ce_trs cn))^+" using Cons by auto
from cn have "(comb cn (s # ss),comb cn ss) ∈ ce_trs cn" by simp
then have "(comb cn (s # ss),comb cn ss) ∈ rstep (ce_trs cn)" by blast
with ind show ?thesis by auto
qed
qed
declare ce_trs.simps[simp del] comb.simps[simp del]
type_synonym 'f af = "('f × nat) ⇒ nat set"
fun af_regarded_pos :: "'f af ⇒ ('f,'v)term ⇒ pos ⇒ bool"
where "af_regarded_pos π t [] = True"
| "af_regarded_pos π (Fun f ts) (Cons i p) = (i < length ts ∧ i ∈ π (f,length ts) ∧ af_regarded_pos π (ts ! i) p)"
| "af_regarded_pos π (Var _) (Cons i p) = False"
lemma af_regarded_pos_append: "af_regarded_pos μ t (p @ q) =
(af_regarded_pos μ t p ∧ af_regarded_pos μ (t |_p) q)"
by (induct p arbitrary: t, simp, case_tac t, auto)
definition af_inter :: "'f af ⇒ 'f af ⇒ 'f af" where
"af_inter π μ f = π f ∩ μ f"
lemma af_regarded_pos_af_inter:
"af_regarded_pos (af_inter π μ) t p = (af_regarded_pos π t p ∧ af_regarded_pos μ t p)"
proof (induct p arbitrary: t)
case (Cons i p t)
then show ?case by (cases t, auto simp: af_inter_def)
qed simp
definition af_compatible :: "'f af ⇒ ('f,'v)trs ⇒ bool"
where "af_compatible π ord ≡
(∀ f bef s t aft. length bef ∈ π (f, (Suc (length bef + length aft))) ∨
(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ord)"
context
fixes μ :: "'f af"
begin
definition af_monotone :: "('f,'v)trs ⇒ bool"
where "af_monotone ord ≡
(∀ f bef s t aft. length bef ∈ μ (f, (Suc (length bef + length aft)))
⟶ (s,t) ∈ ord ⟶ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ord)"
lemma af_monotoneD: assumes "af_monotone ord"
and "length bef ∈ μ (f, (Suc (length bef + length aft)))"
and "(s,t) ∈ ord"
shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ord"
using assms unfolding af_monotone_def by auto
lemma af_monotoneI:
assumes "⋀ f bef s t aft.
length bef ∈ μ (f, (Suc (length bef + length aft))) ⟹
(s,t) ∈ ord ⟹(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ ord"
shows "af_monotone ord"
using assms unfolding af_monotone_def by auto
lemma ctxt_closed_imp_af_monotone: assumes "ctxt.closed ord"
shows "af_monotone ord"
by (rule af_monotoneI[OF ctxt_closed_one[OF assms]])
lemma af_monotone_af_regarded_posD: assumes mono: "af_monotone ord"
and *: "af_regarded_pos μ (C⟨s⟩) (hole_pos C)" and st: "(s,t) ∈ ord"
shows "(C⟨s⟩, C⟨t⟩) ∈ ord"
using *
proof (induct C)
case (More f bef C aft)
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
from More(2) have i: "?i ∈ μ (f,?n)" and af: "af_regarded_pos μ (C⟨s⟩) (hole_pos C)" by auto
from More(1)[OF af] have "(C⟨s⟩, C⟨t⟩) ∈ ord" by auto
from af_monotoneD[OF mono i this] show ?case by simp
qed (insert st, auto)
end
definition af_subset :: "'f af ⇒ 'f af ⇒ bool" where
"af_subset π μ ≡ ∀ f. π f ⊆ μ f"
lemma af_subset_refl[simp]: "af_subset μ μ" unfolding af_subset_def by auto
lemma af_subset_af_monotone: "af_subset μ μ' ⟹ af_monotone μ' ord ⟹ af_monotone μ ord"
unfolding af_subset_def af_monotone_def by force
lemma af_compatible_af_regarded_ctxt: assumes af: "af_compatible π ord"
and ctxt: "ctxt.closed ord"
and not: "¬ af_regarded_pos π (C⟨u⟩) (hole_pos C)"
shows "(C⟨s⟩,C⟨t⟩) ∈ ord"
using not
proof (induct C)
case Hole
then show ?case by simp
next
case (More f bef C aft)
let ?i = "length bef"
let ?n = "Suc (?i + length aft)"
let ?pi = "?i ∈ π (f,?n)"
show ?case
proof (cases ?pi)
case True
with More(2) have "¬ af_regarded_pos π (C⟨u⟩) (hole_pos C)" by simp
from More(1)[OF this] have "(C⟨s⟩, C⟨t⟩) ∈ ord" .
from ctxt_closed_one[OF ctxt this]
show ?thesis by auto
next
case False
with af[unfolded af_compatible_def, rule_format, of bef f]
show ?thesis by auto
qed
qed
definition full_af :: "'f af" where "full_af fn ≡ {0 ..< snd fn}"
definition empty_af :: "'f af" where "empty_af fn ≡ {}"
lemma full_af: "af_compatible full_af r" unfolding af_compatible_def full_af_def by auto
lemma empty_af: "af_monotone empty_af r" unfolding af_monotone_def empty_af_def by auto
lemma af_monotone_full_af_imp_ctxt_closed:
assumes mono: "af_monotone full_af r"
shows "ctxt.closed r"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume st: "(s,t) ∈ r"
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r"
by (rule af_monotoneD[OF mono _ st], auto simp: full_af_def)
qed
lemma af_regarded_poss: "af_regarded_pos π t p ⟹ p ∈ poss t"
proof (induct p arbitrary: t)
case Nil
show ?case by simp
next
case (Cons i p t)
show ?case
proof (cases t)
case (Var x)
show ?thesis using Cons(2) unfolding Var by simp
next
case (Fun f ts)
show ?thesis using Cons(2) Cons(1)[of "ts ! i"] unfolding Fun by auto
qed
qed
lemma af_regarded_full: "af_regarded_pos full_af t p = (p ∈ poss t)"
proof (induct p arbitrary: t)
case Nil
show ?case by simp
next
case (Cons i p t)
show ?case
proof (cases t)
case (Var x)
show ?thesis unfolding Var by simp
next
case (Fun f ts)
show ?thesis using Cons[of "ts ! i"] unfolding Fun by (auto simp: full_af_def)
qed
qed
lemma af_steps_imp_orient: assumes tran: "trans r"
and refl: "refl r"
and ctxt: "ctxt.closed r"
and len: "length ts = length (ss :: ('f,'v)term list)"
and steps: "∀i<length ts. p i ⟶ (ts ! i, ss ! i) ∈ r"
and compat: "∀ bef s t aft. ((length ts = Suc (length bef + length aft)) ⟶ (p (length bef) ∨ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r))"
shows "(Fun f ts, Fun f ss) ∈ r"
proof -
from trans_refl_imp_rtrancl_id[OF tran refl] have r: "r^* = r" by auto
let ?rel = "λ i. if p i then r else UNIV"
have "(Fun f ts, Fun f ss) ∈ r^*"
proof (rule args_steps_imp_steps_gen[OF _ len, of ?rel])
fix i
assume i: "i < length ss"
with len steps show "(ts ! i, ss ! i) ∈ (?rel i)^*" by auto
next
fix bef aft :: "('f,'v)term list" and s t
assume rel: "(s,t) ∈ ?rel (length bef)" and len': "length ss = Suc (length bef + length aft)"
from compat[rule_format, OF len'[unfolded len[symmetric]]]
have "p (length bef) ∨ (Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r" .
then show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ r^*"
proof
assume "p (length bef)"
with rel have "(s,t) ∈ r" by auto
from ctxt_closed_one[OF ctxt this] show ?thesis by auto
qed auto
qed
then show ?thesis unfolding r .
qed
locale af_redpair = redpair S NS for S NS :: "('f,'v)trs"+
fixes π :: "'f af"
assumes af_compat: "af_compatible π NS"
begin
lemma af_redpair_order: "af_redpair (S^+) (NS^*) π"
proof -
let ?NS = "NS^*"
let ?S = "S^+"
from redpair_order interpret redpair_order ?S ?NS .
show ?thesis
proof
show "af_compatible π ?NS" using af_compat
unfolding af_compatible_def by blast
qed
qed
end
definition ce_compatible :: "('f,'v)trs ⇒ bool" where
"ce_compatible rel = (∃ n. ∀ m. m ≥ n ⟶ (∀ c. ce_trs (c,m) ⊆ rel))"
lemma ce_compatibleE: assumes "ce_compatible rel"
obtains n where "⋀ c m. m ≥ n ⟹ ce_trs (c,m) ⊆ rel"
using assms unfolding ce_compatible_def by blast
locale ce_redpair = redpair S NS for S NS :: "('f,'v)trs"+
assumes NS_ce_compat: "ce_compatible NS"
begin
lemma ce_redpair_order: "ce_redpair (S^+) (NS^*)"
proof -
let ?S = "S^+"
let ?NS = "NS^*"
from redpair_order interpret redpair_order ?S ?NS .
show ?thesis using NS_ce_compat
by (unfold_locales; unfold ce_compatible_def; blast)
qed
end
locale ce_af_redpair = ce_redpair S NS + af_redpair S NS π
for S NS :: "('f,'v)trs" and π
locale ce_redtriple = redtriple S NS NST + ce_redpair S NS for S NS NST :: "('f,'v)trs"
begin
lemma ce_redtriple_order: "ce_redtriple (S^+) (NS^*) (NST^*)"
proof -
let ?S = "S^+"
let ?NS = "NS^*"
let ?NST = "NST^*"
from redtriple_order ce_redpair_order interpret redtriple_order ?S ?NS ?NST + ce_redpair ?S ?NS .
show ?thesis by (unfold_locales)
qed
end
locale ce_af_root_redtriple = root_redtriple S NS NST + ce_af_redpair S NS π for S NS NST :: "('f,'v)trs" and π +
fixes π' :: "'f af"
assumes af_compat': "af_compatible π' NST"
locale ce_af_root_redtriple_order = root_redtriple_order S NS NST + ce_af_root_redtriple S NS NST π π' for S NS NST :: "('f,'v)trs" and π π'
locale ce_af_redtriple = ce_redtriple S NS NST + ce_af_redpair S NS π for S NS NST :: "('f,'v)trs" and π
locale ce_af_redtriple_order = ce_redtriple S NS NST + ce_af_redpair S NS π + redtriple_order S NS NST for S NS NST :: "('f,'v)trs" and π
sublocale ce_af_redtriple_order ⊆ ce_af_redtriple ..
lemma (in ce_af_redtriple) ce_af_redtriple_order: "ce_af_redtriple_order (S^+) (NS^*) (NST^*) π"
proof -
let ?S = "S^+"
let ?NS = "NS^*"
let ?NST = "NST^*"
from redtriple_order ce_redpair_order af_redpair_order interpret redtriple_order ?S ?NS ?NST + ce_redpair ?S ?NS + af_redpair ?S ?NS π .
show ?thesis by (unfold_locales)
qed
locale mono_ce_redtriple = redtriple S NS NST + ce_redpair S NS for S NS NST :: "('f,'v)trs" +
assumes S_ce_compat: "ce_compatible S"
begin
lemma mono_ce_redtriple_order: "mono_ce_redtriple (S^+) (NS^*) (NST^*)"
proof -
let ?S = "S^+"
let ?NS = "NS^*"
let ?NST = "NST^*"
have subset: "⋀ x. x ∈ S ⟹ x ∈ ?S" by auto
from redtriple_order ce_redpair_order interpret redtriple_order ?S ?NS ?NST + ce_redpair ?S ?NS .
show ?thesis using S_ce_compat subset
by (unfold_locales; unfold ce_compatible_def; blast)
qed
lemma orient_implies_var_cond:
assumes ctxt: "ctxt.closed S"
and lr: "(l,r) ∈ NS ∪ S"
shows "vars_term r ⊆ vars_term l"
proof (rule ccontr)
interpret both: redpair "S^+" "((NS ∪ S)^*)"
by (unfold_locales, insert ctxt wm_NS subst_S subst_NS SN, auto intro: SN_imp_SN_trancl)
interpret order: redtriple_order "S^+" "NS^*" "NST^*" by (rule redtriple_order)
from S_ce_compat obtain c n where ce: "ce_trs (c,n) ⊆ S"
unfolding ce_compatible_def by blast
define t where "t = comb (c,n) [l]"
have "(t,l) ∈ (rstep (ce_trs (c,n)))^+"
unfolding t_def
by (rule ce_trs_sound, simp)
with rstep_subset[OF ctxt subst_S ce] have tl: "(t,l) ∈ S^+" by (metis trancl_mono)
assume "¬ ?thesis"
then obtain x where xr: "x ∈ vars_term r" and xl: "x ∉ vars_term l" by auto
define σ where "σ ≡ λ y. if y = x then Fun c [t] else Var y"
from lr have "(l,r) ∈ (NS ∪ S)^*" by auto
from subst.closedD[OF both.subst_NS this]
have "(l ⋅ σ, r ⋅ σ) ∈ (NS ∪ S)^*" by auto
also have "l ⋅ σ = l ⋅ Var"
by (rule term_subst_eq, insert xl, auto simp: σ_def)
also have "… = l" by simp
finally have step: "(l, r ⋅ σ) ∈ (NS ∪ S)^*" by auto
have "r ⋅ σ ⊵ Var x ⋅ σ"
by (rule supteq_subst, insert xr, auto)
also have "Var x ⋅ σ = Fun c [t]" unfolding σ_def by auto
also have "Fun c [t] ⊳ t" by auto
finally have rt: "r ⋅ σ ⊳ t" by simp
from NS.trCompat obtain A B where NSS: "NS^* O S = A" and S: "S = A ∪ B" by blast+
from tl step rt have tt: "(t,t) ∈ (S^+ O (NS ∪ S)^*) O {⊳}" by auto
have "S^+ O (NS ∪ S)^* ⊆ S^+ O ((NS^* O S)^* ∪ (NS^* O S)^* O NS^*)" by regexp
also have "… ⊆ S^+ O (S^* ∪ S^* O NS^*)" unfolding NSS unfolding S by regexp
also have "… = S^+ O NS^*" by regexp
also have "… ⊆ S^+" by (rule order.compat_S_NS)
finally have tt: "(t,t) ∈ S^+ O {⊳}" using tt by auto
let ?rel = "(S^+ ∪ {⊳})"
from tt have tt: "(t,t) ∈ ?rel O ?rel" by auto
then have tt: "(t,t) ∈ ?rel^+" by regexp
from SN_imp_SN_trancl[OF SN_imp_SN_union_supt[OF both.SN ctxt.closed_trancl[OF ctxt]]]
have "SN (?rel^+)" .
then show False using refl_not_SN[OF tt] by blast
qed
end
locale mono_ce_af_redtriple = ce_af_redtriple S NS NST π + mono_ce_redtriple S NS NST for S NS NST :: "('f,'v)trs" and π
locale mono_ce_af_redtriple_order = mono_ce_af_redtriple S NS NST π + redtriple_order S NS NST for S NS NST :: "('f,'v)trs" and π
sublocale mono_ce_af_redtriple_order ⊆ ce_af_redtriple_order ..
lemma (in mono_ce_af_redtriple) mono_ce_af_redtriple_order: "mono_ce_af_redtriple_order (S^+) (NS^*) (NST^*) π"
proof -
let ?S = "S^+"
let ?NS = "NS^*"
let ?NST = "NST^*"
from ce_af_redtriple_order mono_ce_redtriple_order interpret ce_af_redtriple_order ?S ?NS ?NST π + mono_ce_redtriple ?S ?NS ?NST .
show ?thesis ..
qed
locale cpx_term_rel =
fixes S :: "('f,'v)trs"
and cpx_class :: "('f,'v)complexity_measure ⇒ complexity_class ⇒ bool"
assumes cpx_class: "⋀ cm cc. cpx_class cm cc ⟹ deriv_bound_measure_class S cm cc"
locale cpx_ce_af_redtriple_order =
ce_af_redtriple_order S NS NST π + cpx_term_rel S cpx_class
for S NS NST :: "('f, 'v) trs" and π μ :: "'f af" and cpx_class +
assumes μ: "af_monotone μ S"
locale ws_redpair_order = redpair_order S NS + order_pair S NS
for S NS :: "('f,'v)trs" +
fixes σ :: "'f status"
assumes ws_status: "i ∈ set (status σ f) ⟹ simple_arg_pos NS f i"
and S_imp_NS: "S ⊆ NS"
begin
lemmas σ = status[of σ]
lemma NS_arg: assumes i: "i ∈ set (status σ (f,length ts))"
shows "(Fun f ts, ts ! i) ∈ NS"
by (rule ws_status[OF i, unfolded simple_arg_pos_def fst_conv, rule_format],
insert σ[of f "length ts"] i, auto)
lemma NS_subterm: assumes all: "⋀ f k. set (status σ (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 ce_σ: assumes "{0,1} ⊆ set (status σ (f,Suc (Suc k)))"
shows "ce_trs (f,k) ⊆ 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 NS_arg[of 0 f ?ss] NS_arg[of 1 f ?ss] assms
have "(s,t) ∈ NS" unfolding s by (cases, auto)
}
then show ?thesis by auto
qed
end
locale ss_redpair_order = ws_redpair_order +
assumes ss_status: "i ∈ set (status σ f) ⟹ simple_arg_pos S f i"
and S_non_empty: "S ≠ {}"
definition "supteqrel R = ({⊳} ∪ rstep R)⇧*"
lemma supteqrel_refl [simp]: "(t, t) ∈ supteqrel R" by (auto simp: supteqrel_def)
interpretation relto_pair: order_pair "(relto R E)⇧+" "(R ∪ E)⇧*"
apply unfold_locales
apply (fact refl_rtrancl)
apply (fact trans_trancl)
apply (fact trans_rtrancl) by regexp+
interpretation suptrel_pair: order_pair "suptrel R" "supteqrel R"
unfolding suptrel_def unfolding supteqrel_def by standard
lemma supteqrel_subst:
"(s, t) ∈ supteqrel R ⟹ (s ⋅ σ, t ⋅ σ) ∈ supteqrel R"
by (auto simp: supteqrel_def) (metis supt_rsteps_stable)
end