chapter ‹AC-Dependency Pairs›
theory AC_Dependency_Pairs
imports
"Check-NT.Relative_DP_Framework"
"Check-NT.AC_Rewriting"
"../AC_Rewriting/AC_Equivalence"
"../Orderings/Subterm_Multiset"
begin
lemma chain_reshuffling:
fixes P Q R E :: "'a rel"
and M :: "'a ⇒ bool"
defines "M' ≡ {(s,t). M t} :: 'a rel"
defines "S ≡ ((Q ∪ E) ∩ M')⇧* O ((P ∪ R) ∩ M')"
assumes f: "⋀ i. (f i, f (Suc i)) ∈ S"
shows "¬ SN_rel_ext P Q R E M ∨ (∃ t. M t ∧ ¬ SN_on (relto (R ∩ M') (E ∩ M')) {t})"
proof -
def QE ≡ "(Q ∪ E) ∩ M'"
def Q' ≡ "relto (Q ∩ M') QE"
def PR ≡ "(P ∪ R) ∩ M'"
def P' ≡ "P ∩ M'"
def A ≡ "(P ∪ Q ∪ R ∪ E) ∩ M'"
def g ≡ "λ i. f (Suc i)"
have g: "⋀ i. (g i, g (Suc i)) ∈ S" unfolding g_def using f by auto
from f[unfolded S_def]
have M: "⋀ i. M (g i)" unfolding M'_def g_def by auto
from g have "∀ i. ∃ hi. (g i, hi) ∈ QE⇧* ∧ (hi, g (Suc i)) ∈ PR" unfolding S_def QE_def PR_def by blast
from choice[OF this] obtain h where gh: "⋀ i. (g i, h i) ∈ QE⇧*" and hg: "⋀ i. (h i, g (Suc i)) ∈ PR" by blast
def j ≡ "λ i :: nat. i div 2"
def f ≡ "λ i. (if even i then g else h) (j i)"
def t ≡ "λ i. (if even i then
if (f i, f (Suc i)) ∈ Q' then top_ns else normal_ns else
if (f i, f (Suc i)) ∈ P' then top_s else normal_s)"
have "QE ⊆ A" unfolding QE_def A_def by auto
hence QE: "QE⇧* ⊆ A⇧*" by (rule rtrancl_mono)
show ?thesis
proof (cases "INFM i. t i ∈ {top_s,top_ns}")
case True
have "¬ SN_rel_ext (A⇧* O (P ∩ M') O A⇧*) (A⇧* O ((P ∪ Q) ∩ M') O A⇧*) (A⇧* O ((P ∪ R) ∩ M') O A⇧*) (A⇧*) M"
unfolding SN_rel_ext_def not_not
proof (rule exI[of _ f], rule exI[of _ t], intro conjI allI)
fix i
have M: "M (g (j i))" by fact
show "M (f i)"
proof (cases "even i")
case True
thus ?thesis using M unfolding f_def by auto
next
case False
hence id: "f i = h (j i)" unfolding f_def by auto
from gh[of "j i"] M have "M (h (j i))" unfolding QE_def M'_def
by (induct, auto)
thus ?thesis using id by simp
qed
show "(f i, f (Suc i)) ∈ SN_rel_ext_step (A⇧* O (P ∩ M') O A⇧*) (A⇧* O ((P ∪ Q) ∩ M') O A⇧*)
(A⇧* O ((P ∪ R) ∩ M') O A⇧*) (A⇧*) (t i)"
proof (cases "even i")
case True
hence fi: "f i = g (j i)" and fsi: "f (Suc i) = h (j i)" and jsi: "j (Suc i) = j i"
unfolding f_def j_def by auto
show ?thesis
proof (cases "(f i, f (Suc i)) ∈ Q'")
case True
hence t: "t i = top_ns" unfolding t_def using `even i` by auto
with True QE fi fsi show ?thesis by (auto simp: Q'_def)
next
case False
hence t: "t i = normal_ns" unfolding t_def using `even i` by auto
with gh[of "j i"] QE fi fsi jsi show ?thesis by auto
qed
next
case False
hence fi: "f i = h (j i)" and fsi: "f (Suc i) = g (Suc (j i))" and jsi: "j (Suc i) = Suc (j i)"
unfolding f_def j_def by auto
show ?thesis
proof (cases "(f i, f (Suc i)) ∈ P'")
case True
hence t: "t i = top_s" unfolding t_def using `odd i` by auto
with True QE fi fsi show ?thesis by (auto simp: P'_def)
next
case False
hence t: "t i = normal_s" unfolding t_def using `odd i` by auto
with hg[of "j i"] QE fi fsi jsi show ?thesis by (auto simp: PR_def)
qed
qed
show "∃⇩∞i. t i ∈ {top_s, normal_s}"
unfolding INFM_nat_le
proof
fix i
show "∃ j ≥ i. t j ∈ {top_s, normal_s}"
by (rule exI[of _ "2 * i + 1"], auto simp: t_def)
qed
qed (rule True)
with SN_rel_ext_trans[of P Q R E M, folded M'_def, folded A_def]
have "¬ SN_rel_ext P Q R E M" by blast
thus ?thesis ..
next
case False
then obtain k where k: "⋀ i. i ≥ k ⟹ t i ∉ {top_s, top_ns}"
unfolding INFM_nat_le by auto
{
fix i
assume i: "i ≥ k"
hence "2 * i ≥ k" by auto
from k[OF this, unfolded t_def f_def j_def]
have nmem: "(g i, h i) ∉ Q'" by auto
have sub: "⋀ A B. (A ∪ B)⇧* ⊆ B⇧* ∪ relto A (A ∪ B)" by regexp
from set_mp[OF sub gh[of i, unfolded QE_def Int_Un_distrib2]] nmem
have gh: "(g i, h i) ∈ (E ∩ M')⇧*" unfolding QE_def Q'_def Int_Un_distrib2 by blast
from i have "2 * i + 1 ≥ k" by auto
from k[OF this, unfolded t_def f_def j_def]
have nmem: "(h i, g (Suc i)) ∉ P'" by auto
with hg[of i] have hg: "(h i, g (Suc i)) ∈ R ∩ M'" unfolding PR_def P'_def by auto
note gh hg
} note gh = this
def f ≡ "λ i. g (k + i)"
{
fix i
have "(f i, f (Suc i)) ∈ relto (R ∩ M') (E ∩ M')"
unfolding f_def using gh[of "k + i"] by auto
}
hence "¬ SN_on (relto (R ∩ M') (E ∩ M')) {f 0}" by (rule steps_imp_not_SN_on)
with M[of k]
show ?thesis unfolding f_def by auto
qed
qed
lemma defined_symbol_finite_rel_dpp:
assumes fin: "finite_rel_dpp (P', Q', {}, R, E)"
and P: "⋀ s t. (s,t) ∈ P - P' ⟹ root s ∈ Some ` D ∧ root t ∈ Some ` C"
and Q: "⋀ s t. (s,t) ∈ Q - Q' ⟹ root s ∈ Some ` C ∧ root t ∈ Some ` C"
and Q': "⋀ s t. (s,t) ∈ Q' ⟹ root s ∈ Some ` D ∧ root t ∈ Some ` D"
and P': "⋀ s t. (s,t) ∈ P' ⟹ root s ∈ Some ` D ∧ root t ∈ Some ` D"
and CD: "C ∩ D = {}"
and C: "⋀ f. f ∈ C ⟹ ¬ defined (R ∪ E) f"
and wf: "wf_trs (R ∪ E)"
shows "finite_rel_dpp (P, Q, {}, R, E)"
proof
fix s t σ
assume chain: "min_relchain (P, Q, {}, R, E) s t σ"
note * = chain[unfolded min_relchain.simps]
note P = P[of "s i" "t i" for i]
note Q = Q[of "s i" "t i" for i]
note P' = P'[of "s i" "t i" for i]
note Q' = Q'[of "s i" "t i" for i]
note all = P Q P' Q'
from * have st: "⋀ i. (s i, t i) ∈ P ∪ Q" by auto
{
fix j
assume "root (t j) ∈ Some ` C"
hence tj: "root (t j ⋅ σ j) ∈ Some ` C" by (cases "t j", auto)
from * have steps: "(t j ⋅ σ j, s (Suc j) ⋅ σ (Suc j)) ∈ (rstep (R ∪ E))^*" by auto
have "(t j ⋅ σ j, s (Suc j) ⋅ σ (Suc j)) ∈ (nrrstep (R ∪ E))^*"
by (rule rsteps_imp_nrrsteps[OF _ C _ steps], insert wf tj, (force simp: wf_trs_def)+)
from nrrsteps_imp_eq_root_arg_rsteps[OF this] tj
have sj: "root (s (Suc j) ⋅ σ (Suc j)) ∈ Some ` C"
by auto
with st[of "Suc j"] all[of "Suc j"]
have "root (s (Suc j)) ∈ Some ` C" by (cases "s (Suc j)", auto)
} note tC_sC = this
{
fix j
assume sj: "root (s j) ∈ Some ` C"
from st[of j] sj CD all[of j] have "root (t j) ∈ Some ` C"
by force
} note sC_tC = this
show False
proof (cases "∃ i. root (s i) ∈ Some ` C")
case True
then obtain i where si: "root (s i) ∈ Some ` C" by auto
{
fix j
assume "j ≥ i"
hence "root (s j) ∈ Some ` C"
proof (induct j)
case 0
with si show ?case by simp
next
case (Suc j)
show ?case
proof (cases "j ≥ i")
case False
with Suc(2) have "Suc j = i" by auto
thus ?thesis using si by auto
next
case True
from Suc(1)[OF this] have IH: "root (s j) ∈ Some ` C" .
from tC_sC[OF sC_tC[OF this]] show ?thesis .
qed
qed
hence "(s j, t j) ∉ P" using all[of j] CD
by force
} note noP = this
with *[unfolded INFM_nat_le] show False by blast
next
case False
hence C: "⋀ i. root (s i) ∉ Some ` C" by auto
let ?D = "(P - P') ∪ (Q - Q')"
{
fix i
from C[of "Suc i"] have C: "root (s (Suc i)) ∉ Some ` C" .
with tC_sC[of i] have "root (t i) ∉ Some ` C" by auto
with all[of i] CD st[of i]
have "(s i, t i) ∉ ?D" by auto
} note D = this
have " ∃i. min_relchain (P - ?D, Q - ?D, {}, R, E) (shift s i) (shift t i) (shift σ i)"
by (rule min_relchain_split_top[OF chain], insert D, auto simp: min_relchain.simps)
hence "¬ finite_rel_dpp (P - ?D, Q - ?D, {}, R, E)" unfolding finite_rel_dpp_def by blast
moreover have "finite_rel_dpp (P - ?D, Q - ?D, {}, R, E)"
by (rule finite_rel_dpp_pairs_mono[OF fin], auto)
ultimately show False ..
qed
qed
context size_preserving_trs
begin
interpretation subteq_redpair: SN_order_pair "suptrel R" "supteqrel R"
by (standard, auto intro: SN_suptrel)
end
definition "strictly_finite P Q R E ⟷ ¬ (∃s t σ. min_relchain (P, Q, R, {}, E) s t σ)"
definition "weakly_finite P Q R E ⟷ ¬ (∃s t σ. min_relchain (P, Q, {}, R, E) s t σ)"
lemma strictly_finite_imp_SN_rel_ext:
assumes "strictly_finite P Q R E"
shows "SN_rel_ext (rrstep P) (rrstep Q) (rstep R) (rstep E) (λt. SN_on (relstep R E) {t})"
using assms no_chain_imp_SN_rel_ext[of P Q R "{}" E] unfolding strictly_finite_def by auto
lemma weakly_finite_imp_SN_rel_ext:
assumes "weakly_finite P Q R E"
shows "SN_rel_ext (rrstep P) (rrstep Q) {} (rstep (R ∪ E)) (λt. SN_on (relstep R E) {t})"
using assms no_chain_imp_SN_rel_ext[of P Q "{}" R E] unfolding weakly_finite_def rstep_union by auto
lemma strictly_finite_SN:
assumes "strictly_finite P Q R E"
defines "M' ≡ λt. SN_on (relstep R E) {t}"
defines "M ≡ {(s, t). M' t}"
defines "S ≡ ((rrstep Q ∪ rstep E) ∩ M)⇧* O ((rrstep P ∪ rstep R) ∩ M)"
shows "SN S"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain f where "⋀i. (f i, f (Suc i)) ∈ S" by (auto simp: SN_defs)
from chain_reshuffling [of f, OF this [unfolded S_def M_def], folded M_def]
consider (ichain) "¬ SN_rel_ext (rrstep P) (rrstep Q) (rstep R) (rstep E) M'" |
(min) "(∃t. M' t ∧ ¬ SN_on (relto (rstep R ∩ M) (rstep E ∩ M)) {t})" by blast
then show False
proof (cases)
case ichain
with strictly_finite_imp_SN_rel_ext [OF assms(1)] show False by (auto simp: M'_def)
next
case min
have "rstep R ∩ M ⊆ rstep R" and "rstep E ∩ M ⊆ rstep E" by auto
from SN_on_mono [OF _ relto_mono [OF this]] and min show ?thesis by (auto simp: M'_def)
qed
qed
context relative_dp
begin
theorem ACDP_transformation:
assumes sp: "size_preserving_trs E" and F: "{f. defined (R ∪ E) f} ⊆ F"
and fin: "strictly_finite (DP_on ♯ F R) (DP_on ♯ F E) R E"
shows "SN (relstep R E)"
proof (rule ccontr)
def M' ≡ "λt. SN_on (relstep R E) {t}"
def M ≡ "{(s::('f, 'v) term, t). M' t}"
def E' ≡ "(rrstep (DP_on ♯ F E) ∪ rstep E)"
def R' ≡ "(rrstep (DP_on ♯ F R) ∪ rstep R)"
interpret sp: size_preserving_trs E using sp.
note readable = M'_def M_def E'_def R'_def
assume "¬ SN (relstep R E)"
then obtain s where "s ∈ Tinf (relstep R E)" by (auto simp: SN_def dest: not_SN_imp_subt_Tinf)
then show False
proof (induct "♯ s" arbitrary: s rule: SN_induct [OF strictly_finite_SN [OF fin],folded readable])
case (1 s)
then have "s ∈ Tinf (relstep R E)" by auto
from Tinf_starts_relchain [OF sp.SN_suptrel F this, unfolded starts_relchain_def]
obtain v and n
where "relchain_part (DP_on ♯ F R) (DP_on ♯ F E) s v n" by blast
from this[unfolded relchain_part_def]
have v: "⋀i. v i ∈ Tinf (relstep R E)"
and sv: "s = v 0"
and E: "⋀i. i < n ⟹ (♯ (v i), ♯ (v (Suc i))) ∈ E'"
and R: "(♯ (v n), ♯ (v (Suc n))) ∈ R'"
unfolding E'_def R'_def by (auto simp: nrrstep_imp_rstep)
from v have *: "⋀i. M' (♯ (v i))" unfolding M'_def using Tinf_sharp_imp_SN by auto
from R * have "(♯ (v n), ♯ (v (Suc n))) ∈ (R' ∩ M)" unfolding M_def by auto
moreover from E and * have "⋀i. i < n ⟹ (♯ (v i), ♯ (v (Suc i))) ∈ E' ∩ M" by (auto simp: M_def)
then have "(♯ s, ♯ (v n)) ∈ (E' ∩ M)⇧*" using sv by (induct n) (auto intro: rtrancl_into_rtrancl)
ultimately have "(♯ s, ♯ (v (Suc n))) ∈ (E' ∩ M)⇧* O (R' ∩ M)" by auto
from "1.hyps" [OF this] and v show False by force
qed
qed
corollary SN_relstep_via_finite_rel_dpp:
assumes "size_preserving_trs E" and F: "{f. defined (R ∪ E) f} ⊆ F"
and fin: "finite_rel_dpp (DP_on ♯ F R, DP_on ♯ F E, R, {}, E)"
shows "SN (relstep R E)"
by (rule ACDP_transformation[OF assms(1-2)], insert fin,
auto simp: strictly_finite_def finite_rel_dpp_def)
end
subsection ‹AC-Extensions›
inductive_set actopstep_sym for f and F :: "'f set" and R :: "('f, 'v) trs"
where
root: "(s, t) ∈ rrstep R ⟹ (s, t) ∈ actopstep_sym f F R"
| Binl: "root s = Some (f, 2) ⟹ (s, t) ∈ actopstep_sym f F R ⟹ f ∈ F ⟹
(Bin f s u, Bin f t u) ∈ actopstep_sym f F R"
| Binr: "root s = Some (f, 2) ⟹ (s, t) ∈ actopstep_sym f F R ⟹ f ∈ F ⟹
(Bin f u s, Bin f u t) ∈ actopstep_sym f F R"
definition "actopstep F R = {(s, t) | s t f. (s, t) ∈ actopstep_sym f F R}"
definition "acnontopstep F R = rstep R - actopstep F R"
lemma acnontopstep_eq_roots:
assumes "(s, t) ∈ acnontopstep F R"
shows "∃f n. root s = Some (f, n) ∧ root t = Some (f, n)"
using assms
apply (auto simp: acnontopstep_def elim!: rstepE)
apply (case_tac C)
apply (auto simp: actopstep_def intro!: actopstep_sym.intros)
done
lemma actop_cases:
assumes "(s, t) ∈ rstep R"
obtains (top) "(s, t) ∈ actopstep F R"
| (nontop) "(s, t) ∉ actopstep F R" and "(s, t) ∈ acnontopstep F R"
using assms by (auto simp: acnontopstep_def)
context
fixes R R⇩e⇩x⇩t :: "('f, 'v) trs" and F⇩A F⇩C :: "'f set"
assumes R_ext: "is_ext_trs R F⇩A F⇩C R⇩e⇩x⇩t" and vc: "∀(l, r)∈R. is_Fun l"
begin
interpretation aoc_rewriting F⇩A F⇩C .
private lemma vc_AC: "f ∈ F⇩A ⟹ (l, r) ∈ R ⟹ root l = Some (f, 2) ⟹ ∃x. x ∉ vars_rule (l, r)"
using R_ext by (fastforce simp: is_ext_trs_def)
private lemma vc_A_only: "f ∈ F⇩A - F⇩C ⟹ (l, r) ∈ R ⟹ root l = Some (f, 2) ⟹
∃x y. x ≠ y ∧ x ∉ vars_rule (l, r) ∧ y ∉ vars_rule (l, r)"
using R_ext by (fastforce simp: is_ext_trs_def)
lemma AC_rrstep_imp_rrstep_ext_trs:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A" and "(s, t) ∈ rrstep R"
shows "(Bin f s u, Bin f t u) ∈ rrstep (ext_trs R)"
proof -
obtain l and r and σ where lr: "(l, r) ∈ R" and [simp]: "s = l ⋅ σ" "t = r ⋅ σ"
using ‹(s, t) ∈ rrstep R› by (auto elim: rrstepE)
with assms and vc and vc_AC [OF ‹f ∈ F⇩A› lr] obtain x where "x ∉ vars_rule (l, r)"
and ext_rule: "(Bin f l (Var x), Bin f r (Var x)) ∈ ext_trs R" (is "(?l, ?r) ∈ _")
apply (cases s; cases l)
apply (auto simp: ext_trs_def ext_AC_trs_def ext_AC_rule_def ext_A_trs_def ext_A_rules_def)
by (metis ‹(l, r) ∈ R› insert_subset order_refl root.simps(2))
moreover def τ ≡ "λy. if y = x then u else σ y"
ultimately have "(?l ⋅ τ, ?r ⋅ τ) ∈ rrstep (ext_trs R)"
and "Bin f s u = ?l ⋅ τ" and "Bin f t u = ?r ⋅ τ"
using rrstepI [OF ext_rule, of "Bin f s u" τ "Bin f t u"]
by (auto simp: term_subst_eq_conv vars_rule_def) force
then show ?thesis by simp
qed
lemma A_only_rrstep_imp_rrstep_ext_trs_right:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A - F⇩C" and "(s, t) ∈ rrstep R"
shows "(Bin f u s, Bin f u t) ∈ rrstep (ext_trs R)"
proof -
have "f ∈ F⇩A" using assms by blast
obtain l and r and σ where lr: "(l, r) ∈ R" and [simp]: "s = l ⋅ σ" "t = r ⋅ σ"
using ‹(s, t) ∈ rrstep R› by (auto elim: rrstepE)
with assms and vc and vc_AC [OF ‹f ∈ F⇩A› lr] obtain x where "x ∉ vars_rule (l, r)"
and ext_rule: "(Bin f (Var x) l, Bin f (Var x) r) ∈ ext_trs R" (is "(?l, ?r) ∈ _")
apply (cases s; cases l)
apply (auto simp: ext_trs_def ext_AC_trs_def ext_AC_rule_def ext_A_trs_def ext_A_rules_def)
by (metis ‹(l, r) ∈ R› insert_subset order_refl root.simps(2))
moreover def τ ≡ "λy. if y = x then u else σ y"
ultimately have "(?l ⋅ τ, ?r ⋅ τ) ∈ rrstep (ext_trs R)"
and "Bin f u s = ?l ⋅ τ" and "Bin f u t = ?r ⋅ τ"
using rrstepI [OF ext_rule, of "Bin f u s" τ "Bin f u t"]
apply (auto simp: term_subst_eq_conv vars_rule_def)
by (metis (no_types, lifting) term_subst_eq)
then show ?thesis by simp
qed
lemma A_only_rrstep_imp_rrstep_ext_trs_middle:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A - F⇩C" and "(s, t) ∈ rrstep R"
shows "(Bin f (Bin f u s) v, Bin f (Bin f u t) v) ∈ rrstep (ext_trs R)"
proof -
obtain l and r and σ where lr: "(l, r) ∈ R" and [simp]: "s = l ⋅ σ" "t = r ⋅ σ"
using ‹(s, t) ∈ rrstep R› by (auto elim: rrstepE)
with assms and vc and vc_A_only [OF ‹f ∈ F⇩A - F⇩C› lr] obtain x and y
where vars: "x ≠ y" "x ∉ vars_rule (l, r)" "y ∉ vars_rule (l, r)"
and ext_rule: "(Bin f (Bin f (Var x) l) (Var y), Bin f (Bin f (Var x) r) (Var y)) ∈ ext_trs R" (is "(?l, ?r) ∈ _")
apply (cases s; cases l)
apply (auto simp: ext_trs_def ext_AC_trs_def ext_AC_rule_def ext_A_trs_def ext_A_rules_def)
by (metis ‹(l, r) ∈ R› insert_subset order_refl root.simps(2))
moreover def τ ≡ "λz. if z = x then u else if z = y then v else σ z"
ultimately have "(?l ⋅ τ, ?r ⋅ τ) ∈ rrstep (ext_trs R)"
and "Bin f (Bin f u s) v = ?l ⋅ τ" and "Bin f (Bin f u t) v = ?r ⋅ τ"
using rrstepI [OF ext_rule, of "Bin f (Bin f u s) v" τ "Bin f (Bin f u t) v"]
apply (auto simp: term_subst_eq_conv vars_rule_def)
by (metis (no_types, lifting) term_subst_eq)
then show ?thesis by simp
qed
lemma rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_AC:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A ∩ F⇩C" and "(s, t) ∈ rrstep (ext_trs R)"
shows "(Bin f s u, Bin f t u) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
proof -
obtain l and r and v and σ where rule: "(l, r) ∈ R"
and "root l = Some (f, 2)"
and "(Bin f l v, Bin f r v) ∈ ext_trs R"
and [simp]: "s = Bin f l v ⋅ σ" "t = Bin f r v ⋅ σ"
using assms
by (auto elim!: rrstepE simp: ext_trs_def ext_AC_rule_def ext_AC_trs_def ext_A_trs_def ext_A_rules_def)
moreover then obtain x where "x ∉ vars_rule (l, r)"
and ext_rule: "(Bin f l (Var x), Bin f r (Var x)) ∈ ext_trs R" (is "(?l, ?r) ∈ _")
using vc and vc_AC [OF _ rule] and ‹f ∈ F⇩A ∩ F⇩C›
by (auto simp: ext_trs_def ext_AC_rule_def ext_AC_trs_def ext_A_trs_def ext_A_rules_def)
moreover def τ ≡ "λy. if y = x then Bin f u (v ⋅ σ) else σ y"
ultimately have "(?l ⋅ τ, ?r ⋅ τ) ∈ rrstep (ext_trs R)"
and "?l ⋅ τ = Bin f (l ⋅ σ) (Bin f u (v ⋅ σ))"
and "?r ⋅ τ = Bin f (r ⋅ σ) (Bin f u (v ⋅ σ))"
using rrstepI [OF ext_rule refl refl, of τ] by (auto simp: term_subst_eq_conv vars_rule_def)
moreover then have "(Bin f s u, ?l ⋅ τ) ∈ AOCEQ" and "(?r ⋅ τ, Bin f t u) ∈ AOCEQ"
using ‹f ∈ F⇩A ∩ F⇩C› by (auto simp: aocconv_iff ac_simps)
ultimately show ?thesis by blast
qed
lemma rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_A_only_left:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A - F⇩C" and "(s, t) ∈ rrstep (ext_trs R)"
shows "(Bin f s u, Bin f t u) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
using assms(3, 1, 2)
proof (cases rule: rrstep_ext_trs_cases)
case ext_A_trs
show ?thesis using ext_A_trs(2) and ‹root s = Some (f, 2)›
proof (cases rule: rrstep_ext_A_trs_cases)
case (left v w x)
with AC_rrstep_imp_rrstep_ext_trs [of v f w]
have "(Bin f v (Bin f x u), Bin f w (Bin f x u)) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by (rule relcomp3_I) (insert left, auto)
next
case [simp]: (right v w x)
from A_only_rrstep_imp_rrstep_ext_trs_middle [OF this(1-3)]
have "(Bin f (Bin f x v) u, Bin f (Bin f x w) u) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by auto
next
case (middle v w x y)
from A_only_rrstep_imp_rrstep_ext_trs_middle [OF this(1-3)]
have "(Bin f (Bin f x v) (Bin f y u), Bin f (Bin f x w) (Bin f y u)) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by (rule relcomp3_I) (insert middle, auto)
qed
qed simp
lemma rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_A_right:
assumes "root s = Some (f, 2)" and "f ∈ F⇩A - F⇩C" and "(s, t) ∈ rrstep (ext_trs R)"
shows "(Bin f u s, Bin f u t) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
using assms(3, 1, 2)
proof (cases rule: rrstep_ext_trs_cases)
case ext_A_trs
show ?thesis using ext_A_trs(2) and ‹root s = Some (f, 2)›
proof (cases rule: rrstep_ext_A_trs_cases)
case (left v w x)
from A_only_rrstep_imp_rrstep_ext_trs_middle [OF this(1-3)]
have "(Bin f (Bin f u v) x, Bin f (Bin f u w) x) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by (rule relcomp3_I) (insert left, auto)
next
case (right v w x)
from A_only_rrstep_imp_rrstep_ext_trs_right [OF this(1-3)]
have "(Bin f (Bin f u x) v, Bin f (Bin f u x) w) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by (rule relcomp3_I) (insert right, auto)
next
case (middle v w x y)
from A_only_rrstep_imp_rrstep_ext_trs_middle [OF this(1-3)]
have "(Bin f (Bin f (Bin f u x) v) y, Bin f (Bin f (Bin f u x) w) y) ∈ rrstep (ext_trs R)" by blast
then show ?thesis by (rule relcomp3_I) (insert middle, auto simp: aocconv_iff)
qed
qed simp
lemma actopstep_sym_rrstep_or_ext_trs:
assumes "(s, t) ∈ actopstep_sym f F⇩A R"
shows "(s, t) ∈ rrstep R ∨ (s, t) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
using assms
proof (induct)
case (root s t)
then show ?case by simp
next
case (Binl s t u)
then consider "(s, t) ∈ rrstep R" | "(s, t) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ" by auto
then show ?case
proof (cases)
case 1
with Binl have "(Bin f s u, Bin f t u) ∈ rrstep (ext_trs R)"
by (auto dest: AC_rrstep_imp_rrstep_ext_trs)
then show ?thesis by auto
next
case 2
then obtain v and w where aoceq: "(s, v) ∈ AOCEQ" "(w, t) ∈ AOCEQ"
and "(v, w) ∈ rrstep (ext_trs R)" by auto
moreover then have "root v = Some (f, 2)"
using ‹root s = Some (f, 2)› by (auto dest: AOCEQ_roots)
moreover have "f ∈ F⇩A ∩ F⇩C ∨ f ∈ F⇩A - F⇩C" using Binl by blast
ultimately have "(Bin f v u, Bin f w u) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
by (blast dest: rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_AC rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_A_only_left)
then show ?thesis
by (rule disjI2 [OF relcomp3_transI [OF conversion_trans]])
(insert aoceq, auto simp: args_acconv_imp_acconv nth_Cons')
qed
next
case (Binr s t u)
then consider "(s, t) ∈ rrstep R" | "(s, t) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ" by auto
then show ?case
proof (cases)
case 1
consider (AC) "f ∈ F⇩A ∩ F⇩C" | (A_only) "f ∈ F⇩A - F⇩C" using Binr by blast
then show ?thesis
proof (cases)
case AC
with 1 and Binr have "(Bin f s u, Bin f t u) ∈ rrstep (ext_trs R)"
by (auto dest: AC_rrstep_imp_rrstep_ext_trs)
moreover have "(Bin f u s, Bin f s u) ∈ AOCEQ" and "(Bin f t u, Bin f u t) ∈ AOCEQ"
using AC by auto
ultimately show ?thesis by blast
next
case A_only
with 1 and Binr have "(Bin f u s, Bin f u t) ∈ rrstep (ext_trs R)"
using A_only_rrstep_imp_rrstep_ext_trs_right by auto
then show ?thesis by auto
qed
next
case 2
then obtain v and w where aoceq: "(s, v) ∈ AOCEQ" "(w, t) ∈ AOCEQ"
and vw: "(v, w) ∈ rrstep (ext_trs R)" by auto
then have root_v: "root v = Some (f, 2)"
using ‹root s = Some (f, 2)› by (auto dest: AOCEQ_roots)
consider (AC) "f ∈ F⇩A ∩ F⇩C" | (A_only) "f ∈ F⇩A - F⇩C" using Binr by blast
then show ?thesis
proof (cases)
case AC
with root_v and vw have rrstep: "(Bin f v u, Bin f w u) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
by (auto dest: rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_AC)
moreover have "(Bin f s u, Bin f v u) ∈ AOCEQ"
and "(Bin f w u, Bin f t u) ∈ AOCEQ"
using ‹(s, v) ∈ AOCEQ› and ‹(w, t) ∈ AOCEQ›
by (auto simp: args_acconv_imp_acconv nth_Cons')
ultimately show ?thesis
by (intro disjI2 [OF relcomp3_transI [OF conversion_trans]])
(insert AC, auto simp: aocconv_iff ac_simps)
next
case A_only
have "(Bin f u v, Bin f u w) ∈ AOCEQ O rrstep (ext_trs R) O AOCEQ"
using rrstep_ext_trs_imp_rrstep_ext_trs_AOCEQ_A_right [OF root_v A_only vw] .
then show ?thesis
by (rule disjI2 [OF relcomp3_transI [OF conversion_trans]])
(insert aoceq, auto simp: args_acconv_imp_acconv nth_Cons')
qed
qed
qed
end
inductive_set top_ctxts for f
where
Hole: "□ ∈ top_ctxts f"
| Binl: "C ∈ top_ctxts f ⟹ More f [] C [t] ∈ top_ctxts f"
| Binr: "C ∈ top_ctxts f ⟹ More f [t] C [] ∈ top_ctxts f"
lemma actopstep_sym_cases:
assumes "(s, t) ∈ actopstep_sym f F R"
shows "(s, t) ∈ rrstep R ∨
(∃u v C. C ∈ top_ctxts f ∧ C ≠ □ ∧
s = C⟨u⟩ ∧ t = C⟨v⟩ ∧
root u = Some (f, 2) ∧ (u, v) ∈ rrstep R)" (is "_ ∨ (∃u v C. ?P s t u v C)")
using assms
proof (induct)
case (root s t)
then show ?case by blast
next
case (Binl s t u)
then consider "(s, t) ∈ rrstep R" | v w C where "?P s t v w C" by blast
then show ?case
proof (cases)
def C ≡ "More f [] □ [u]"
case 1
moreover have "C ≠ □" and "C ∈ top_ctxts f" by (auto simp: C_def intro: top_ctxts.intros)
ultimately show ?thesis using Binl
by (intro disjI2) (rule exI [of _ s], rule exI [of _ t], rule exI [of _ C], auto simp: C_def)
next
case (2 v w C)
moreover def D ≡ "More f [] C [u]"
moreover have "D ≠ □" and "D ∈ top_ctxts f"
using 2 by (auto simp: D_def intro: top_ctxts.intros)
ultimately show ?thesis
by (intro disjI2) (rule exI [of _ v], rule exI [of _ w], rule exI [of _ D], simp)
qed
next
case (Binr s t u)
then consider "(s, t) ∈ rrstep R" | v w C where "?P s t v w C" by blast
then show ?case
proof (cases)
def C ≡ "More f [u] □ []"
case 1
moreover have "C ≠ □" and "C ∈ top_ctxts f" by (auto simp: C_def intro: top_ctxts.intros)
ultimately show ?thesis using Binr
by (intro disjI2) (rule exI [of _ s], rule exI [of _ t], rule exI [of _ C], auto simp: C_def)
next
case (2 v w C)
moreover def D ≡ "More f [u] C []"
moreover have "D ≠ □" and "D ∈ top_ctxts f"
using 2 by (auto simp: D_def intro: top_ctxts.intros)
ultimately show ?thesis
by (intro disjI2) (rule exI [of _ v], rule exI [of _ w], rule exI [of _ D], simp)
qed
qed
lemma top_ctxts_root:
assumes "C ∈ top_ctxts f" and "C ≠ □"
shows "root (C⟨t⟩) = Some (f, 2)"
using assms by (induct) simp_all
lemma top_ctxts_actopstep_symI:
assumes "C ∈ top_ctxts f"
and "C ≠ □" and "s = C⟨u⟩" and "t = C⟨v⟩"
and "f ∈ F"
and "root u = Some (f, 2)"
and "(u, v) ∈ rrstep R"
shows "(s, t) ∈ actopstep_sym f F R"
using assms(1-4)
proof (induct arbitrary: s t)
case (Binl C w)
then show ?case
using assms(5-) by (cases C) (auto dest: top_ctxts_root intro: actopstep_sym.intros)
next
case (Binr C w)
then show ?case
using assms(5-) by (cases C) (auto dest: top_ctxts_root intro: actopstep_sym.intros)
qed simp
lemma actopstep_sym_iff:
"(s, t) ∈ actopstep_sym f F R ⟷ (s, t) ∈ rrstep R ∨ f ∈ F ∧
(∃C u v. C ≠ □ ∧ C ∈ top_ctxts f ∧ s = C⟨u⟩ ∧ t = C⟨v⟩ ∧
root u = Some (f, 2) ∧ (u, v) ∈ rrstep R)"
using actopstep_sym_cases [of s t f F R]
by (auto intro: actopstep_sym.intros top_ctxts_actopstep_symI elim: actopstep_sym.cases)
lemma acnontopstepD:
assumes "(s, t) ∈ acnontopstep F R"
shows "∃C u v. C ≠ □ ∧ s = C⟨u⟩ ∧ t = C⟨v⟩ ∧ (u, v) ∈ rrstep R ∧
(∀f∈F. root u ≠ Some (f, 2) ∨ C ∉ top_ctxts f)"
proof -
obtain C and u and v where [simp]: "s = C⟨u⟩" "t = C⟨v⟩" and "(u, v) ∈ rrstep R"
and *: "⋀f. (s, t) ∉ actopstep_sym f F R"
using assms by (auto simp: acnontopstep_def actopstep_def elim!: rstepE)
moreover then have "C ≠ □" by (auto simp: actopstep_sym.root)
moreover
{ fix f assume "f ∈ F" and "root u = Some (f, 2)" and "C ∈ top_ctxts f"
then have False
using * [of f] and ‹C ≠ □› and ‹(u, v)∈ rrstep R› by (auto simp: actopstep_sym_iff) }
ultimately show ?thesis by blast
qed
lemma actop_not_empty [simp]: "actop f t ≠ {#}"
by (induct f t rule: actop.induct) simp_all
lemma actop_singleton_iff:
"actop f u = {#u#} ⟷ root u ≠ Some (f, 2)"
by (cases "(f, u)" rule: actop.cases) (auto simp: non_empty_plus_non_empty_not_single)
lemma not_top_ctxts_actops:
assumes "C ∉ top_ctxts f" and "s = C⟨u⟩" and "t = C⟨v⟩"
shows "actop f s = {#s#} ∧ actop f t = {#t#} ∨
(∃D M. M ≠ {#} ∧ actop f s = {#D⟨u⟩#} + M ∧ actop f (D⟨u⟩) = {#D⟨u⟩#} ∧
actop f t = {#D⟨v⟩#} + M ∧ actop f (D⟨v⟩) = {#D⟨v⟩#} ∧
s ⊳ D⟨u⟩ ∧ t ⊳ D⟨v⟩)"
using assms
proof (induct C arbitrary: s t)
case Hole
then show ?case by (auto intro: top_ctxts.intros)
next
case (More g ss C ts)
then consider s' where "ss = [s']" and "ts = []" | t' where "ss = []" and "ts = [t']" |
"⋀u v. s ≠ Bin g u v" and "⋀u v. t ≠ Bin g u v"
using Bin_cases [of s] and Bin_cases [of t]
by (metis (no_types, lifting) ctxt.distinct(1) ctxt.inject ctxt_apply_term_Bin_cases)
then show ?case
proof (cases)
case [simp]: 1
show ?thesis
proof (cases "C ∈ top_ctxts f")
case True
with More show ?thesis by (auto intro: top_ctxts.intros)
next
case False
from More(1) [OF this refl refl]
consider (A) "actop f C⟨u⟩ = {#C⟨u⟩#}" and "actop f (C⟨v⟩) = {#C⟨v⟩#}"
| (B) D M where "M ≠ {#}" and "actop f (C⟨u⟩) = {#D⟨u⟩#} + M" and "actop f (D⟨u⟩) = {#D⟨u⟩#}"
and "actop f (C⟨v⟩) = {#D⟨v⟩#} + M" and "actop f (D⟨v⟩) = {#D⟨v⟩#}"
and "C⟨u⟩ ⊳ D⟨u⟩" and "C⟨v⟩ ⊳ D⟨v⟩" by auto
then show ?thesis
proof (cases)
case A then show ?thesis unfolding More actop_singleton_iff
apply (auto simp: A)
apply (rule exI [of _ C], rule exI [of _ "actop f s'"]) apply auto
done
next
case B then show ?thesis unfolding More actop_singleton_iff
apply (auto simp: B)
apply (rule exI [of _ "D"], rule exI [of _ "actop f s' + M"])
using B apply (auto simp: ac_simps)
done
qed
qed
next
case [simp]: 2
show ?thesis
proof (cases "C ∈ top_ctxts f")
case True
with More show ?thesis by (auto intro: top_ctxts.intros)
next
case False
from More(1) [OF this refl refl]
consider (A) "actop f C⟨u⟩ = {#C⟨u⟩#}" and "actop f (C⟨v⟩) = {#C⟨v⟩#}"
| (B) D M where "M ≠ {#}" and "actop f (C⟨u⟩) = {#D⟨u⟩#} + M" and "actop f (D⟨u⟩) = {#D⟨u⟩#}"
and "actop f (C⟨v⟩) = {#D⟨v⟩#} + M" and "actop f (D⟨v⟩) = {#D⟨v⟩#}"
and "C⟨u⟩ ⊳ D⟨u⟩" and "C⟨v⟩ ⊳ D⟨v⟩" by auto
then show ?thesis
proof (cases)
case A then show ?thesis unfolding More actop_singleton_iff
apply (auto simp: A)
apply (rule exI [of _ C], rule exI [of _ "actop f t'"]) apply auto
done
next
case B then show ?thesis unfolding More actop_singleton_iff
apply (auto simp: B)
apply (rule exI [of _ "D"], rule exI [of _ "actop f t' + M"])
using B apply (auto simp: ac_simps)
done
qed
qed
next
case 3
with More show ?thesis by auto
qed
qed
fun actop_ctxt
where
"actop_ctxt f Hole = {#}"
| "actop_ctxt f (More g ss C ts) =
(if f = g ∧ length ss + length ts = 1 then
⋃# (mset (map (actop f) (ss @ ts))) + actop_ctxt f C
else {#})"
lemma top_ctxts_actop_apply_ctxt [simp]:
assumes "C ∈ top_ctxts f"
shows "actop f (C⟨t⟩) = actop_ctxt f C + actop f t"
using assms by (induct C) (auto simp: ac_simps)
lemma not_AC_actop [simp]:
assumes "root t ≠ Some (f, 2)"
shows "actop f t = {#t#}"
using assms by (cases "(f, t)" rule: actop.cases) auto
fun nabla ("∇")
where
"∇ F (Fun f ts) = (if f ∈ F ∧ length ts = 2 then actop f (Fun f ts) else mset ts)"
| "∇ F (Var x) = {#}"
lemma actop_subteq:
assumes "s ∈# actop f t"
shows "s ⊴ t"
using assms by (induct t rule: bterm_induct) (auto split: if_splits)
lemma actop_subt:
assumes "t = Fun f ts" "s ∈# actop f t" "length ts = 2"
shows "s ⊲ t"
proof -
from assms obtain t1 t2 where ts: "ts = [t1,t2]" by (cases ts; cases "tl ts"; auto)
hence "s ∈# actop f t1 ∨ s ∈# actop f t2" using assms by auto
with actop_subteq[of s f _] consider "t1 ⊵ s" | "t2 ⊵ s" by auto
thus ?thesis unfolding assms(1) ts
by (cases, auto intro: set_supteq_into_supt)
qed
lemma nabla_subt:
assumes "s ∈# ∇ F t"
shows "s ⊲ t"
proof (cases t)
case Var thus ?thesis using assms by auto
next case (Fun f ts)
show ?thesis
proof (cases "f ∈ F ∧ length ts = 2")
case True
with actop_subt[OF Fun, of s] assms
show ?thesis unfolding Fun by auto
next case False
with assms show ?thesis unfolding Fun by force
qed
qed
lemma non_ac_term_acnontopstepE:
assumes "(s, t) ∈ acnontopstep F R" and "∀f∈F. root s ≠ Some (f, 2)"
obtains u v M where "(u, v) ∈ rstep R" and "∇ F s = {#u#} + M" and "∇ F t = {#v#} + M"
and "s ⊳ u" and "t ⊳ v"
proof -
obtain f and n where roots: "root s = Some (f, n)" "root t = Some (f, n)"
using assms by (auto dest: acnontopstep_eq_roots)
then have "¬ (f ∈ F ∧ n = 2)" using assms by auto
then have [simp]: "∇ F s = mset (args s) ∧ ∇ F t = mset (args t)"
using roots by (cases s; cases t) auto
have nrrstep: "(s, t) ∈ nrrstep R"
using assms by (auto simp: acnontopstep_def actopstep_def elim!: rstep_cases intro: actopstep_sym.intros)
moreover then obtain i where i: "i < length (args s)" and "(args s ! i, args t ! i) ∈ rstep R"
and args_t: "args s [i := args t ! i] = args t" and "length (args t) = length (args s)"
by (auto simp: nrrstep_iff_arg_rstep)
moreover then have "s ⊳ args s ! i" and "t ⊳ args t ! i"
using nrrstep by (auto dest!: nrrstep_equiv_root)
moreover have "mset (take i (args s) @ args s ! i # drop (Suc i) (args s)) = mset (args s)"
unfolding id_take_nth_drop [OF i, symmetric] ..
moreover have "mset (take i (args s) @ args t ! i # drop (Suc i) (args s)) = mset (args t)"
proof -
have *: "i < length (args s [i := args t ! i])" using i by simp
show ?thesis using id_take_nth_drop[OF *, symmetric] and i by (simp) (metis args_t)
qed
ultimately have "∃u v M. (u, v) ∈ rstep R ∧ ∇ F s = {#u#} + M ∧ ∇ F t = {#v#} + M ∧ s ⊳ u ∧ t ⊳ v"
using assms and roots
apply (subst exI [of _ "args s ! i"], subst exI [of _ "args t ! i"])
apply (rule exI [of _ "mset (take i (args s) @ drop (Suc i) (args s))"])
apply (auto simp: actop_singleton_iff acnontopstep_def actopstep_def ac_simps)
done
then show ?thesis using that by blast
qed
lemma ac_term_acnontopstepE:
assumes st: "(s, t) ∈ acnontopstep F R" and "root s = Some (f, 2)" and "f ∈ F"
obtains
(nonroot) u v M where "(u, v) ∈ rstep R" and "∇ F s = {#u#} + M" and "actop f u = {#u#}"
and "∇ F t = {#v#} + M ∧ actop f v = {#v#} ∨ ∇ F t = actop f v + M"
and "s ⊳ u" and "t ⊳ v"
proof -
have roots: "root s = Some (f, 2)" "root t = Some (f, 2)"
using assms by (auto dest: acnontopstep_eq_roots)
then have [simp]: "f ∈ F" and *: "∇ F s = actop f s" "∇ F t = actop f t"
using assms by (cases s; cases t; simp)+
from acnontopstepD [OF assms(1)] obtain C and u and v
where C: "C ≠ □" and [simp]: "s = C⟨u⟩" "t = C⟨v⟩"
and uv: "(u, v) ∈ rrstep R"
and "root u ≠ Some (f, 2) ∨ C ∉ top_ctxts f"
using assms by blast
then consider "C ∈ top_ctxts f" and "root u ≠ Some (f, 2)" | "C ∉ top_ctxts f" by auto
then have "(∃u v M. (u, v) ∈ rstep R ∧
∇ F s = {#u#} + M ∧ actop f u = {#u#} ∧
(∇ F t = {#v#} + M ∧ actop f v = {#v#} ∨ ∇ F t = actop f v + M) ∧ s ⊳ u ∧ t ⊳ v)"
proof (cases)
case 2
from not_top_ctxts_actops [OF this, of s u t v]
consider (A) "actop f s = {#s#}" and "actop f t = {#t#}"
| (B) D M where "M ≠ {#}" and "actop f s = {#D⟨u⟩#} + M" and "actop f (D⟨u⟩) = {#D⟨u⟩#}"
and "actop f t = {#D⟨v⟩#} + M" and "actop f (D⟨v⟩) = {#D⟨v⟩#}"
and "s ⊳ D⟨u⟩" and "t ⊳ D⟨v⟩" by auto
then show ?thesis
proof (cases)
case A then show ?thesis
using rrstep_imp_rstep [OF uv] and roots by (auto simp: actop_singleton_iff)
next
case B
then show ?thesis
using rrstep_imp_rstep [OF uv] unfolding *
by (subst exI[of _ "D⟨u⟩"], subst exI[of _ "D⟨v⟩"], subst exI[of _ M]) auto
qed
next
case 1
show ?thesis
proof (cases "root v = Some (f, 2)")
case False
with 1 have "actop f s = {#u#} + actop_ctxt f C" and "actop f u = {#u#}"
and "actop f t = {#v#} + actop_ctxt f C" and "actop f v = {#v#}" by auto
then show ?thesis
using rrstep_imp_rstep [OF uv] C unfolding * by auto
next
case True
then have [simp]: "∇ F v = actop f v" by (cases "(f, v)" rule: actop.cases) auto
have "actop f s = {#u#} + actop_ctxt f C" and "actop f u = {#u#}"
and "actop f t = actop f v + actop_ctxt f C" using 1 by (auto simp: ac_simps)
moreover have "∀x∈set_mset (actop f v). x ⊴ v" by (auto simp: actop_subteq)
ultimately show ?thesis
using rrstep_imp_rstep[OF uv] C unfolding * by auto
qed
qed
then show ?thesis using that by blast
qed
lemma acnontopstep_cases [consumes 1]:
assumes "(s, t) ∈ acnontopstep F R"
obtains (nonac) u v M where "∀f∈F. root s ≠ Some (f, 2)"
and "(u, v) ∈ rstep R" and "∇ F s = {#u#} + M" and "∇ F t = {#v#} + M" and "s ⊳ u" and "t ⊳ v"
| (ac) u v M f where "root s = Some (f, 2)" and "f ∈ F" and "(u, v) ∈ rstep R"
and "∇ F s = {#u#} + M" and "actop f u = {#u#}"
and "∇ F t = {#v#} + M ∧ actop f v = {#v#} ∨ ∇ F t = actop f v + M" and "s ⊳ u" and "t ⊳ v"
using non_ac_term_acnontopstepE [OF assms, of thesis]
and ac_term_acnontopstepE [OF assms, of _ thesis] by auto
lemma restrict_Un[simp]: "(R∪S)↾X = R↾X ∪ S↾X" by auto
lemma restrict_id[simp]: "R↾X↾X = R↾X" by auto
lemma restrict_mono: "R' ⊆ R ⟹ R'↾X ⊆ R↾X" by auto
lemma restrict_relpow_Suc[simp]: "((R↾X)^^Suc n)↾X = (R↾X)^^Suc n" by (induct n, auto simp: relpow_Suc)
lemma restrict_trancl_id[simp]: "(R↾X)⇧+↾X = (R↾X)⇧+"
proof(intro equalityI subrelI,force)
fix x y
assume "(x,y) ∈ (R↾X)⇧+"
then obtain n where "n > 0" "(x,y) ∈ (R↾X)^^n" by (unfold trancl_power, auto)
then obtain n' where "(x,y) ∈ (R↾X)^^Suc n'" by (cases n, auto)
then have "(x,y) ∈ ((R↾X)^^Suc n')↾X" unfolding restrict_relpow_Suc.
then show "(x,y) ∈ (R↾X)⇧+↾X" by (rule subsetD[OF restrict_mono[OF pow_Suc_subset_trancl]])
qed
lemma restrict_O_id[simp]: "(R↾X O S↾X)↾X = R↾X O S↾X" by auto
lemma restrict_trancl_O_id[simp]: "((R↾X)⇧+ O S↾X)↾X = (R↾X)⇧+ O S↾X"
by (subst restrict_trancl_id[symmetric], unfold restrict_O_id, simp)
lemma SN_rel_ext_trans:
fixes P Pw R Rw :: "'a rel" and M :: "'a ⇒ bool"
defines A: "A ≡ (P ∪ Pw ∪ R ∪ Rw) ↾ Collect M"
assumes "SN_rel_ext P Pw R Rw M"
shows "SN_rel_ext (A^* O (P ↾ Collect M) O A^*) (A^* O ((P ∪ Pw) ↾ Collect M) O A^*) (A^* O ((P ∪ R) ↾ Collect M) O A^*) (A^*) M" (is "SN_rel_ext ?P ?Pw ?R ?Rw M")
proof (rule ccontr)
let ?relt = "SN_rel_ext_step ?P ?Pw ?R ?Rw"
let ?rel = "SN_rel_ext_step P Pw R Rw"
assume "¬ ?thesis"
from this[unfolded SN_rel_ext_def]
obtain f ty
where steps: "⋀ i. (f i, f (Suc i)) ∈ ?relt (ty i)"
and min: "⋀ i. M (f i)"
and inf1: "INFM i. ty i ∈ {top_s, top_ns}"
and inf2: "INFM i. ty i ∈ {top_s, normal_s}"
by auto
let ?Un = "λ tt. ⋃ (?rel ` tt)"
let ?UnM = "λ tt. (⋃ (?rel ` tt)) ↾ Collect M"
let ?A = "?UnM {top_s,top_ns,normal_s,normal_ns}"
let ?P' = "?UnM {top_s}"
let ?Pw' = "?UnM {top_s,top_ns}"
let ?R' = "?UnM {top_s,normal_s}"
let ?Rw' = "?UnM {top_s,top_ns,normal_s,normal_ns}"
have A: "A = ?A" unfolding A by auto
have P: "(P ↾ Collect M) = ?P'" by auto
have Pw: "(P ∪ Pw) ↾ Collect M = ?Pw'" by auto
have R: "(P ∪ R) ↾ Collect M = ?R'" by auto
have Rw: "A = ?Rw'" unfolding A ..
{
fix s t tt
assume m: "M s" and st: "(s,t) ∈ ?UnM tt"
hence "∃ typ ∈ tt. (s,t) ∈ ?rel typ ∧ M s ∧ M t" by auto
} note one_step = this
let ?seq = "λ s t g n ty. s = g 0 ∧ t = g n ∧ (∀ i < n. (g i, g (Suc i)) ∈ ?rel (ty i)) ∧ (∀ i ≤ n. M (g i))"
{
fix s t
assume m: "M s" and st: "(s,t) ∈ A^*"
from st[unfolded rtrancl_fun_conv]
obtain g n where g0: "g 0 = s" and gn: "g n = t" and steps: "⋀ i. i < n ⟹ (g i, g (Suc i)) ∈ ?A" unfolding A by auto
{
fix i
assume "i ≤ n"
have "M (g i)"
proof (cases i)
case 0
show ?thesis unfolding 0 g0 by (rule m)
next
case (Suc j)
with ‹i ≤ n› have "j < n" by auto
from steps[OF this] show ?thesis unfolding Suc by auto
qed
} note min = this
{
fix i
assume i: "i < n" hence i': "i ≤ n" by auto
from i' one_step[OF min steps[OF i]]
have "∃ ty. (g i, g (Suc i)) ∈ ?rel ty" by blast
}
hence "∀ i. (∃ ty. i < n ⟶ (g i, g (Suc i)) ∈ ?rel ty)" by auto
from choice[OF this]
obtain tt where steps: "⋀ i. i < n ⟹ (g i, g (Suc i)) ∈ ?rel (tt i)" by auto
from g0 gn steps min
have "?seq s t g n tt" by auto
hence "∃ g n tt. ?seq s t g n tt" by blast
} note A_steps = this
let ?seqtt = "λ s t tt g n ty. s = g 0 ∧ t = g n ∧ n > 0 ∧ (∀ i<n. (g i, g (Suc i)) ∈ ?rel (ty i)) ∧ (∀ i ≤ n. M (g i)) ∧ (∃ i < n. ty i ∈ tt)"
{
fix s t tt
assume m: "M s" and st: "(s,t) ∈ A^* O ?UnM tt O A^*"
then obtain u v where su: "(s,u) ∈ A^*" and uv: "(u,v) ∈ ?UnM tt" and vt: "(v,t) ∈ A^*"
by auto
from A_steps[OF m su] obtain g1 n1 ty1 where seq1: "?seq s u g1 n1 ty1" by auto
from uv have "M v" by auto
from A_steps[OF this vt] obtain g2 n2 ty2 where seq2: "?seq v t g2 n2 ty2" by auto
from seq1 have "M u" by auto
from one_step[OF this uv] obtain ty where ty: "ty ∈ tt" and uv: "(u,v) ∈ ?rel ty" by auto
let ?g = "λ i. if i ≤ n1 then g1 i else g2 (i - (Suc n1))"
let ?ty = "λ i. if i < n1 then ty1 i else if i = n1 then ty else ty2 (i - (Suc n1))"
let ?n = "Suc (n1 + n2)"
have ex: "∃ i < ?n. ?ty i ∈ tt"
by (rule exI[of _ n1], simp add: ty)
have steps: "∀ i < ?n. (?g i, ?g (Suc i)) ∈ ?rel (?ty i)"
proof (intro allI impI)
fix i
assume "i < ?n"
show "(?g i, ?g (Suc i)) ∈ ?rel (?ty i)"
proof (cases "i ≤ n1")
case True
with seq1 seq2 uv show ?thesis by auto
next
case False
hence "i = Suc n1 + (i - Suc n1)" by auto
then obtain k where i: "i = Suc n1 + k" by auto
with ‹i < ?n› have "k < n2" by auto
thus ?thesis using seq2 unfolding i by auto
qed
qed
from steps seq1 seq2 ex
have seq: "?seqtt s t tt ?g ?n ?ty" by auto
have "∃ g n ty. ?seqtt s t tt g n ty"
by (intro exI, rule seq)
} note A_tt_A = this
let ?tycon = "λ ty1 ty2 tt ty' n. ty1 = ty2 ⟶ (∃i < n. ty' i ∈ tt)"
let ?seqt = "λ i ty g n ty'. f i = g 0 ∧ f (Suc i) = g n ∧ (∀ j < n. (g j, g (Suc j)) ∈ ?rel (ty' j)) ∧ (∀ j ≤ n. M (g j))
∧ (?tycon (ty i) top_s {top_s} ty' n)
∧ (?tycon (ty i) top_ns {top_s,top_ns} ty' n)
∧ (?tycon (ty i) normal_s {top_s,normal_s} ty' n)"
{
fix i
have "∃ g n ty'. ?seqt i ty g n ty'"
proof (cases "ty i")
case top_s
from steps[of i, unfolded top_s]
have "(f i, f (Suc i)) ∈ ?P" by auto
from A_tt_A[OF min this[unfolded P]]
show ?thesis unfolding top_s by auto
next
case top_ns
from steps[of i, unfolded top_ns]
have "(f i, f (Suc i)) ∈ ?Pw" by auto
from A_tt_A[OF min this[unfolded Pw]]
show ?thesis unfolding top_ns by auto
next
case normal_s
from steps[of i, unfolded normal_s]
have "(f i, f (Suc i)) ∈ ?R" by auto
from A_tt_A[OF min this[unfolded R]]
show ?thesis unfolding normal_s by auto
next
case normal_ns
from steps[of i, unfolded normal_ns]
have "(f i, f (Suc i)) ∈ ?Rw" by auto
from A_steps[OF min this]
show ?thesis unfolding normal_ns by auto
qed
}
hence "∀ i. ∃ g n ty'. ?seqt i ty g n ty'" by auto
from choice[OF this] obtain g where "∀ i. ∃ n ty'. ?seqt i ty (g i) n ty'" by auto
from choice[OF this] obtain n where "∀ i. ∃ ty'. ?seqt i ty (g i) (n i) ty'" by auto
from choice[OF this] obtain ty' where "∀ i. ?seqt i ty (g i) (n i) (ty' i)" by auto
hence partial: "⋀ i. ?seqt i ty (g i) (n i) (ty' i)" ..
let ?ind = "inf_concat n"
let ?g = "λ k. (λ (i,j). g i j) (?ind k)"
let ?ty = "λ k. (λ (i,j). ty' i j) (?ind k)"
have inf: "INFM i. 0 < n i"
unfolding INFM_nat_le
proof (intro allI)
fix m
from inf1[unfolded INFM_nat_le]
obtain k where k: "k ≥ m" and ty: "ty k ∈ {top_s, top_ns}" by auto
show "∃ k ≥ m. 0 < n k"
proof (intro exI conjI, rule k)
from partial[of k] ty show "0 < n k" by (cases "n k", auto)
qed
qed
note bounds = inf_concat_bounds[OF inf]
note inf_Suc = inf_concat_Suc[OF inf]
note inf_mono = inf_concat_mono[OF inf]
have "¬ SN_rel_ext P Pw R Rw M"
unfolding SN_rel_ext_def simp_thms
proof (rule exI[of _ ?g], rule exI[of _ ?ty], intro conjI allI)
fix k
obtain i j where ik: "?ind k = (i,j)" by force
from bounds[OF this] have j: "j < n i" by auto
show "M (?g k)" unfolding ik using partial[of i] j by auto
next
fix k
obtain i j where ik: "?ind k = (i,j)" by force
from bounds[OF this] have j: "j < n i" by auto
from partial[of i] j have step: "(g i j, g i (Suc j)) ∈ ?rel (ty' i j)" by auto
obtain i' j' where isk: "?ind (Suc k) = (i',j')" by force
have i'j': "g i' j' = g i (Suc j)"
proof (rule inf_Suc[OF _ ik isk])
fix i
from partial[of i]
have "g i (n i) = f (Suc i)" by simp
also have "... = g (Suc i) 0" using partial[of "Suc i"] by simp
finally show "g i (n i) = g (Suc i) 0" .
qed
show "(?g k, ?g (Suc k)) ∈ ?rel (?ty k)"
unfolding ik isk split i'j'
by (rule step)
next
show "INFM i. ?ty i ∈ {top_s, top_ns}"
unfolding INFM_nat_le
proof (intro allI)
fix k
obtain i j where ik: "?ind k = (i,j)" by force
from inf1[unfolded INFM_nat] obtain i' where i': "i' > i" and ty: "ty i' ∈ {top_s, top_ns}" by auto
from partial[of i'] ty obtain j' where j': "j' < n i'" and ty': "ty' i' j' ∈ {top_s, top_ns}" by auto
from inf_concat_surj[of _ n, OF j'] obtain k' where ik': "?ind k' = (i',j')" ..
from inf_mono[OF ik ik' i'] have k: "k ≤ k'" by simp
show "∃ k' ≥ k. ?ty k' ∈ {top_s, top_ns}"
by (intro exI conjI, rule k, unfold ik' split, rule ty')
qed
next
show "INFM i. ?ty i ∈ {top_s, normal_s}"
unfolding INFM_nat_le
proof (intro allI)
fix k
obtain i j where ik: "?ind k = (i,j)" by force
from inf2[unfolded INFM_nat] obtain i' where i': "i' > i" and ty: "ty i' ∈ {top_s, normal_s}" by auto
from partial[of i'] ty obtain j' where j': "j' < n i'" and ty': "ty' i' j' ∈ {top_s, normal_s}" by auto
from inf_concat_surj[of _ n, OF j'] obtain k' where ik': "?ind k' = (i',j')" ..
from inf_mono[OF ik ik' i'] have k: "k ≤ k'" by simp
show "∃ k' ≥ k. ?ty k' ∈ {top_s, normal_s}"
by (intro exI conjI, rule k, unfold ik' split, rule ty')
qed
qed
with assms show False by auto
qed
context relative_dp
begin
context
fixes F⇩A F⇩C :: "'f set"
assumes AC_C_E: "AC_C_theory E (F⇩C - F⇩A)"
and EF: "funs_trs E ⊆ F⇩A ∪ F⇩C"
begin
private abbreviation "ST ≡ { s. ∀ s' ⊲ s. SN_on (relstep R E) {s'} }"
private abbreviation "po2s ≡ (relto (rstep R ↾ M ∪ {⊳} ↾ M) (rstep E ↾ M))⇧+"
private abbreviation "po2w ≡ (rstep R ↾ M ∪ {⊳} ↾ M ∪ rstep E ↾ M)⇧*"
interpretation AC_theory E using AC_C_E unfolding AC_C_theory_def ..
interpretation po2: SN_order_pair po2s po2w
proof
let ?T = "{t. SN_on (relstep R E) {t}}"
interpret E_compatible "relstep R E" "(rstep E)⇧*"
by (standard, auto)
have "SN_on (relstep R E ∪ (relto {⊳} (rstep E))) ?T"
by (rule ctxt_closed_imp_SN_on_E_supt[OF _ SN_supt_relto], auto)
hence "SN_on ((rstep E)⇧* O (rstep R ∪ {⊳})) ?T" by (rule SN_on_mono) regexp
hence "SN_on ((rstep E ↾ M)⇧* O ((rstep R ∪ {⊳}) ↾ M)) ?T"
apply (rule SN_on_mono) apply(rule relcomp_mono, rule rtrancl_mono, auto) done
from SN_on_imp_SN_restrict[OF this, unfolded mem_Collect_eq, folded M_def]
have "SN ((rstep E ↾ M)⇧* O (rstep R ↾ M ∪ {⊳} ↾ M))"
apply(rule SN_on_mono)
unfolding rtrancl_trancl_reflcl relcomp_distrib2 Id_O_R restrict_Un by simp
thus "SN po2s"
unfolding SN_on_trancl_SN_on_conv
unfolding SN_on_relto_relcomp.
qed
context
fixes Q :: "('f, 'v) trs"
begin
private definition "M' ≡ λs. SN_on (relstep R E) {s}"
private abbreviation "po3w P ≡ (minstep (P ∪ Q) ∪ rstep (R ∪ E))⇧*"
private abbreviation "po3s P ≡ (relto (minstep P) (minstep Q ∪ rstep (R ∪ E)))⇧+"
lemma minstep_union: "minstep (P ∪ Q) = minstep P ∪ minstep Q"
unfolding rrstep_union by auto
interpretation po3: order_pair "po3s P" "po3w P"
unfolding minstep_union rstep_union
by (standard, unfold trans_O_iff refl_O_iff, regexp+)
private lemma po3: assumes fin: "weakly_finite P Q R E"
shows "SN_order_pair (po3s P) (po3w P)"
proof
let ?R = "relto (minstep P) (minstep Q ∪ rstep (R ∪ E))"
show "SN (po3s P)" unfolding SN_trancl_SN_conv
proof
fix f
assume f: "∀ i. (f i, f (Suc i)) ∈ ?R"
def g ≡ "λ i. f (Suc i)"
have g: "⋀ i. (g i, g (Suc i)) ∈ ?R" using f unfolding g_def by blast
from weakly_finite_imp_SN_rel_ext[OF fin]
have SN: "SN_rel_ext (rrstep P) (rrstep Q) {} (rstep (R ∪ E)) M'" unfolding M'_def by auto
let ?P = "rrstep P" let ?Pw = "rrstep Q" let ?R = "{}" let ?Rw = "rstep (R ∪ E)"
def A ≡ "?P ∪ ?Pw ∪ ?R ∪ ?Rw"
let ?A = "A ↾ M"
from SN_rel_ext_trans[OF SN, unfolded M'_def, folded A_def M_def, folded M'_def]
have SN: "SN_rel_ext (relto (?P↾M) ?A) (relto ((?P ∪ ?Pw)↾M) ?A)
(relto (?P↾M) ?A) (?A⇧*) M'" (is ?SN) by auto
{
fix s t
assume s: "M' s" and st: "(s,t) ∈ (?Pw↾M ∪ ?Rw)⇧*"
from st have "M' t ∧ (s,t) ∈ ?A⇧*"
proof (induct rule: rtrancl_induct)
case (step t u)
from step(2) have u: "M' u"
proof
assume "(t,u) ∈ rstep (R ∪ E)"
hence "(t,u) ∈ (rstep R ∪ rstep E)⇧*" by auto
from steps_preserve_SN_on_relto[OF this] step(3)
show ?thesis unfolding M'_def by auto
qed (auto simp: M_def M'_def)
from step(2,3) u have "(t,u) ∈ ?A" unfolding A_def M_def M'_def rstep_union by auto
with u step(3) show ?case by (meson rtrancl.rtrancl_into_rtrancl)
qed (insert s, auto)
} note SN_steps = this
{
fix i
from f obtain s where "M' s" and "(s,f (Suc i)) ∈ (?Pw ↾ M ∪ ?Rw)⇧*"
unfolding M_def M'_def by auto
from SN_steps[OF this]
have "M' (g i)" unfolding g_def by auto
} note Mg = this
{
fix i
from g[of i] obtain s t where gs: "(g i, s) ∈ (?Pw ↾ M ∪ ?Rw)⇧*" and st: "(s,t) ∈ ?P ↾ M"
and tg: "(t, g (Suc i)) ∈ (?Pw ↾ M ∪ ?Rw)⇧*" by auto
from Mg have g: "M' (g i)" .
from st have t: "M' t" unfolding M_def M'_def by auto
from SN_steps[OF g gs] st SN_steps[OF t tg]
have "(g i, g (Suc i)) ∈ relto (?P ↾ M) ?A" by auto
} note steps = this
have "¬ ?SN" unfolding SN_rel_ext_def not_not
by (rule exI[of _ g], rule exI[of _ "λ _. top_s"], intro conjI allI, auto simp: Mg steps)
with SN show False by simp
qed
qed
lemma acnontopstep_mul_ext:
assumes "s ∈ ST"
shows "(s, t) ∈ acnontopstep F R ⟹ (∇ F s, ∇ F t) ∈ s_mul_ext po2w po2s" (is "_ ⟹ _ ∈ ?S")
and "(s, t) ∈ acnontopstep F E ⟹ (∇ F s, ∇ F t) ∈ ns_mul_ext po2w po2s" (is "_ ⟹ _ ∈ ?NS")
proof -
assume nontop: "(s, t) ∈ acnontopstep F R"
then obtain f and n where roots: "root s = Some (f, n)" "root t = Some (f, n)"
by (auto dest: acnontopstep_eq_roots)
with nontop obtain u v N where rstep: "(u, v) ∈ rstep R" and s: "∇ F s = N + {#u#}"
and "∇ F t = N + {#v#} ∨ ∇ F t = N + actop f v" and "s ⊳ u"
by (cases rule: acnontopstep_cases) (auto simp: ac_simps)
then consider "∇ F t = N + {#v#}" | "∇ F t = N + actop f v" by blast
note * = this
have "SN_on (relstep R E) {v}"
using assms and ‹s ⊳ u› and rstep and step_preserves_SN_on_relto [of u v "rstep R" "rstep E"] by auto
moreover from ‹s ⊳ u› ‹s ∈ ST› have uM: "u ∈ M" by (auto simp: M_def)
ultimately have vM: "v ∈ M" and strict: "(u, v) ∈ po2s"
using rstep by (auto simp: M_def)
have N: "(N, N) ∈ ?NS" by (rule ns_mul_ext_refl_local) (auto simp: locally_refl_def)
show "(∇ F s, ∇ F t) ∈ ?S" using *
proof (cases)
case t: 1
show ?thesis
using strict unfolding s and t by (intro ns_s_mul_ext_union_multiset_l [OF N]) auto
next
case t: 2
{ fix y assume "v ⊳ y"
moreover from subterm_preserves_SN_rel[OF _ this] vM have "y ∈ M" by (auto simp: M_def)
ultimately have "(v, y) ∈ relto (rstep R ↾ M ∪ {⊳} ↾ M) (rstep E ↾ M)" using vM by auto
moreover have "(u, v) ∈ relto (rstep R ↾ M ∪ {⊳} ↾ M) (rstep E ↾ M)" using rstep uM vM by auto
ultimately have "(u, y) ∈ po2s" by (simp add: r_r_into_trancl) }
then have "∀y. y ∈# actop f v ⟶ (∃x. x ∈# {#u#} ∧ (x, y) ∈ po2s)"
using strict by (auto dest!: actop_subteq simp: supteq_supt_conv r_into_trancl')
then show ?thesis
unfolding s and t by (intro ns_s_mul_ext_union_multiset_l [OF N]) auto
qed
next
assume nontop: "(s, t) ∈ acnontopstep F E"
then obtain f and n where roots: "root s = Some (f, n)" "root t = Some (f, n)"
using assms by (auto dest: acnontopstep_eq_roots)
show "(∇ F s, ∇ F t) ∈ ?NS" using nontop
proof (cases rule: acnontopstep_cases)
case (ac u v N f)
then have s: "∇ F s = N + {#u#}"
and "∇ F t = N + {#v#} ∧ actop f u = {#u#} ∨ ∇ F t = N + actop f v" by (auto simp: ac_simps)
then consider "∇ F t = N + {#v#}" | "∇ F t = N + actop f v" by blast
note * = this
have v: "actop f v = {#v#}"
using ac and rstep_root by (simp add: actop_singleton_iff)
have N: "(N, N) ∈ ?NS" by (rule ns_mul_ext_refl_local) (auto simp: locally_refl_def)
from ‹s ∈ ST› ‹s ⊳ u› have uM: "u ∈ M" by (auto simp: M_def)
have vM: "v ∈ M"
using assms and ac and step_preserves_SN_on_relto [of u v "rstep R" "rstep E"] by (auto simp: M_def)
from uM vM have weak: "(u, v) ∈ po2w" using ac by auto
show "(∇ F s, ∇ F t) ∈ ?NS" using *
proof (cases)
case t: 1
show ?thesis
using weak unfolding s and t by (intro ns_ns_mul_ext_union_compat [OF N]) simp
next
case t: 2
show ?thesis
using weak unfolding s and t and v by (intro ns_ns_mul_ext_union_compat [OF N]) simp
qed
next
case (nonac u v N)
then have s: "∇ F s = N + {#u#}" and t: "∇ F t = N + {#v#}" by (auto simp: ac_simps)
have N: "(N, N) ∈ ?NS" by (rule ns_mul_ext_refl_local) (auto simp: locally_refl_def)
have "SN_on (relstep R E) {v}"
using assms and nonac and step_preserves_SN_on_relto [of u v "rstep R" "rstep E"] by auto
then have weak: "(u, v) ∈ po2w" using ‹s ∈ ST› nonac by (auto simp: M_def)
show "(∇ F s, ∇ F t) ∈ ?NS"
using weak unfolding s and t by (intro ns_ns_mul_ext_union_compat [OF N]) simp
qed
qed
lemma sharp_rstep_imp_nrrstep:
assumes "r ⊆ R ∪ E"
assumes st: "(♯ s, ♯ t) ∈ rstep r"
and d: "defined (R ∪ E) (the (root s))"
shows "(s, t) ∈ nrrstep r"
proof -
have wf: "wf_trs r" using wf assms(1) unfolding wf_trs_def by auto
with st have s: "is_Fun (♯ s)" by (simp add: is_Fun_Fun_conv rstep_imp_Fun)
then obtain f ss where s: "s = Fun f ss" by (cases s, auto)
let ?f = "(f,length ss)"
have "(♯ s, ♯ t) ∈ nrrstep r"
proof (rule rstep_imp_nrrstep[OF _ _ _ st])
show "∀(l, r)∈r. is_Fun l" using wf unfolding wf_trs_def by auto
from d have "defined (R ∪ E) ?f" unfolding s by auto
from shp_not_defined[OF this] assms(1) show "¬ defined r (the (root (♯ s)))"
unfolding s defined_def by auto
qed (simp add: s)
thus ?thesis unfolding nrrstep_iff_arg_rstep s by (cases t; insert inj_shp, auto)
qed
lemma actop_subst: "funas_term t ⊆ {(f,2)} ⟹ actop f (t ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms t))"
by (induct t rule: bterm_induct, auto simp: ac_simps)
lemma nabla_subst: "funas_term t ⊆ {(f,2)} ⟹ is_Fun t ⟹ f ∈ F ⟹ ∇ F (t ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms t))"
using actop_subst[of t f σ] by (cases t, auto)
lemma flatten_vars_term_subst:
assumes "(l, r) ∈ E" "the (root l) ∈ F⇩A × UNIV"
shows "∃ f ∈ F⇩A. root l = Some (f,2) ∧ root r = Some (f,2)
∧ ∇ F⇩A (l ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms l))
∧ ∇ F⇩A (r ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms r))"
proof -
from ruleD[OF assms(1)] obtain f l1 l2 r1 r2 where l: "l = Fun f [l1,l2]"
and r: "r = Fun f [r1,r2]" "⋃ (funas_term ` {l1,l2,r1,r2}) ⊆ {(f,2)}" by auto
hence lf: "funas_term l ⊆ {(f,2)}" "is_Fun l" and rf: "funas_term r ⊆ {(f,2)}" "is_Fun r" by auto
from assms[unfolded l] have f: "f ∈ F⇩A" unfolding funs_trs_def funs_rule_def[abs_def] by force
from nabla_subst[OF lf f, of σ] nabla_subst[OF rf f, of σ] l r f show ?thesis by auto
qed
lemma flatten_vars_term_subst_actop:
assumes "(l, r) ∈ E" and "root l = Some (f, n)"
shows "actop f (l ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms l))
∧ actop f (r ⋅ σ) = ⋃# (image_mset (actop f o σ) (vars_term_ms r))"
proof -
from ruleD[OF assms(1)]
have lf: "funas_term l ⊆ {(f,2)}" and rf: "funas_term r ⊆ {(f,2)}" using assms(2) by auto
from actop_subst[OF lf] actop_subst[OF rf] show ?thesis by blast+
qed
lemma nabla_rrstep_E:
assumes "(s,t) ∈ rrstep E"
shows "∇ F⇩A s = ∇ F⇩A t"
proof -
from rrstepE[OF assms] obtain l r σ where lr: "(l, r) ∈ E" and id: "s = l ⋅ σ" "t = r ⋅ σ" .
show ?thesis
proof (cases "the (root l) ∈ F⇩A × UNIV")
case True
from flatten_vars_term_subst[OF lr True, of σ, folded id] ruleD(2)[OF lr] show ?thesis by auto
next
case False
from ruleD[OF lr] obtain f l1 l2 r1 r2 where
id': "l = Fun f [l1,l2]" "r = Fun f [r1,r2]" by auto
from lr id' have "f ∈ funs_trs E" unfolding funs_trs_def funs_rule_def[abs_def] by force
with EF False id' have f: "f ∈ F⇩C - F⇩A" by auto
from AC_C_theory.only_C_D[OF AC_C_E lr _ f] obtain u v where l: "l = Fun f [u,v]"
and r: "r = Fun f [v,u]" unfolding id' by auto
thus ?thesis unfolding id l r using f by simp
qed
qed
lemma actop_rrstepE:
assumes "(s, t) ∈ rrstep E" and "root s = Some (f, n)"
shows "actop f s = actop f t"
proof -
from rrstepE [OF assms(1)] obtain l r σ where lr: "(l, r) ∈ E" and id: "s = l ⋅ σ" "t = r ⋅ σ" .
with assms no_left_var[of _ r] lr
have "root l = Some (f, n)" by (cases l) auto
from flatten_vars_term_subst_actop [OF lr this, of σ, folded id]
and ruleD(2) [OF lr] show ?thesis by auto
qed
lemma ne_top_ctxts_actop_ctxt_ne [simp]:
assumes "C ∈ top_ctxts f" and "C ≠ □"
shows "actop_ctxt f C ≠ {#}"
using assms by (induct) auto
lemma ac_term_top_ctxtsI:
assumes "funas_term t = {(f, 2)}" and "t = C⟨u⟩"
shows "C ∈ top_ctxts f"
using assms
proof (induct C arbitrary: t)
case Hole
show ?case by (auto intro: top_ctxts.intros)
next
case (More g ss C ts)
moreover then have "funas_term (C⟨u⟩) ⊆ funas_term t" by auto
with ‹funas_term t = {(f, 2)}› and More(1) [of "C⟨u⟩"]
have "C ∈ top_ctxts f" by (cases C) (auto intro: top_ctxts.intros)
then show ?case
using More.prems by (cases ss; cases ts; auto intro!: top_ctxts.intros)
qed
lemma subst_top_ctxts:
assumes "C ∈ top_ctxts f"
shows "C ⋅⇩c σ ∈ top_ctxts f"
using assms by (induct C) (auto intro: top_ctxts.intros)
lemma rhs_subt_actop_subset:
fixes s t :: "('f, 'v) term"
assumes rule: "(l, r) ∈ E"
and s: "s = l ⋅ σ" and t: "t = r ⋅ σ" and "r ⊳ u" and rt: "root l = Some (f, n)"
and f: "f ∈ F⇩A"
shows "actop f (u ⋅ σ) ⊂# ∇ F⇩A s"
proof -
have rrstep: "(s, t) ∈ rrstep E" using assms by (auto)
have nabla_s: "∇ F⇩A s = ∇ F⇩A t" by (rule nabla_rrstep_E [OF rrstep])
from rt f have "the (root l) ∈ F⇩A × UNIV" by auto
from flatten_vars_term_subst[OF rule this, of σ] rt s t
have [simp]: "root t = root s"
and *: "root t = Some (f, 2)" "f ∈ F⇩A" by (cases l; cases r; auto)+
then have [simp]: "∇ F⇩A s = actop f t" by (cases t) (auto simp: nabla_s)
from ruleD[OF rule] *
have "funas_term r = {(f, 2)}" unfolding t by auto
with ‹r ⊳ u› obtain C where "C ∈ top_ctxts f" and "C ≠ □" and "r = C⟨u⟩"
by (auto simp: ac_term_top_ctxtsI)
then have "C ⋅⇩c σ ∈ top_ctxts f" and "t = (C ⋅⇩c σ)⟨u ⋅ σ⟩"
using ‹r ⊳ u› by (auto simp: t dest: subst_top_ctxts)
moreover have "C ⋅⇩c σ ≠ □" using ‹C ≠ □› by (cases C) auto
ultimately show ?thesis
by auto (metis add.left_neutral subset_mset.zero_less_iff_neq_zero ne_top_ctxts_actop_ctxt_ne subset_mset.add_less_cancel_right)
qed
lemma nabla_actop_suptmulexeq:
fixes ts
assumes "f ∈ F⇩A"
defines "s ≡ Fun f ts"
shows "actop f s ⊵⇩# ∇ F⇩A s"
using assms and args_in_suptmulex [of f ts]
by (auto simp: locally_refl_def s_ns_mul_ext intro: ns_mul_ext_refl)
lemma nabla_of_subt_suptmulex:
assumes "s ⊳ t"
shows "{#s#} ⊳⇩# ∇ F⇩A t"
using assms by (intro all_s_s_mul_ext) (auto dest!: nabla_subt intro: supt_trans)
lemma actop_suptmulexeq:
"{#t#} ⊵⇩# actop f t"
using Bin_cases_with_length [of t]
apply (auto)
apply (intro s_ns_mul_ext all_s_s_mul_ext)
by (auto dest: actop_subteq intro: set_supteq_into_supt)
lemma nabla_not_actop_suptmulex:
assumes "¬ (f ∈ F⇩A ∧ length ts = 2)"
defines "s ≡ Fun f ts"
assumes "s ⊳ t"
shows "∇ F⇩A s ⊳⇩# ∇ F⇩A t"
proof -
have "mset ts ⊳⇩# ∇ F⇩A t"
using ‹s ⊳ t›
by (intro all_s_s_mul_ext)
(auto simp: s_def in_multiset_in_set supteq_supt_trans dest!: nabla_subt supt_Fun_imp_arg_supteq)
then show ?thesis using assms by auto
qed
lemma not_top_ctxts_supt:
assumes "C ∉ top_ctxts f"
shows "∃u. u ∈# actop f (C⟨t⟩) ∧ u ⊳ t"
using assms
proof (induct C arbitrary: t)
case Hole then show ?case by (auto simp: top_ctxts.intros)
next
case (More g ss C ts)
let ?C = "More g ss C ts"
consider s' where "ss = [s']" and "ts = []" | t' where "ss = []" and "ts = [t']" |
"⋀u v. ?C⟨t⟩ ≠ Bin g u v"
using More and Bin_cases [of "?C⟨t⟩"]
by (metis (no_types, lifting) ctxt.distinct(1) ctxt.inject ctxt_apply_term_Bin_cases)
then show ?case
proof (cases)
case [simp]: 1
show ?thesis
proof (cases "C ∈ top_ctxts f")
case True
with More show ?thesis
apply (auto intro: top_ctxts.intros)
by (metis Cons_eq_append_conv ctxt.distinct(1) ctxt_apply_term.simps(2) ctxt_supt)
next
case False
from More(1) [OF this] show ?thesis apply auto
by (metis Cons_eq_append_conv ctxt.distinct(1) ctxt_apply_term.simps(2) ctxt_supt)
qed
next
case [simp]: 2
show ?thesis
proof (cases "C ∈ top_ctxts f")
case True
with More show ?thesis
apply (auto intro: top_ctxts.intros)
by (metis Cons_eq_append_conv ctxt.distinct(1) ctxt_apply_term.simps(2) ctxt_supt)
next
case False
from More(1) [OF this] show ?thesis apply auto
by (metis Cons_eq_append_conv ctxt.distinct(1) ctxt_apply_term.simps(2) ctxt_supt)
qed
next
case 3
with More show ?thesis by auto
qed
qed
lemma not_top_ctxts_actop_mul_ext_supt:
assumes "C ∉ top_ctxts f"
shows "actop f (C⟨t⟩) ⊳⇩# {#t#}"
using assms by (intro all_s_s_mul_ext) (auto dest: not_top_ctxts_supt)
lemma supt_impl_nabla_mul_supt:
fixes s t :: "('f, 'v) term"
assumes "s ⊳ t"
shows "∇ F⇩A s ⊳⇩# ∇ F⇩A t"
proof (cases t)
case (Var x)
moreover have "∇ F⇩A s ≠ {#}" using assms by (cases s) auto
ultimately show ?thesis using assms by (auto dest: s_mul_ext_bottom)
next
case t: (Fun g ts)
show ?thesis
proof (cases s)
case [simp]: (Fun f ss)
show ?thesis
proof (cases "f ∈ F⇩A ∧ length ss = 2")
case False
from nabla_not_actop_suptmulex [OF this, of t] show ?thesis using assms by simp
next
case F: True
obtain C where [simp]: "C ≠ □" and s: "Fun f ss = C⟨t⟩" using assms by auto
show ?thesis
proof (cases "C ∈ top_ctxts f")
case True
{
assume "f ∈ F⇩A" "length ss = 2"
from True this have "actop f C⟨t⟩ ⊳⇩# ∇ F⇩A t"
apply (auto simp: t)
apply (cases "f = g")
apply auto
apply (rule s_mul_ext_self_extend_left)
apply force
apply (force simp: locally_refl_def)
apply (subst add_mset_add_single)
apply (rule s_mul_ext_ne_extend_left)
apply force
apply (rule actop_suptmulexeq)
apply (subst add_mset_add_single)
apply (rule s_mul_ext_extend_left)
apply (simp add: args_in_suptmulex)
apply (subst add_mset_add_single)
apply (rule s_mul_ext_extend_left)
apply (simp add: args_in_suptmulex)
done
} note main = this
show ?thesis using F unfolding Fun by (auto, unfold s, insert main, auto)
next
case False
then show ?thesis using F unfolding Fun apply auto
unfolding s
apply (auto simp: t)
apply (rule s_ns_mul_ext_trans [of _ _ _ "{#Fun g ts#}"])
apply (auto simp: trans_def compatible_l_def compatible_r_def refl_on_def dest: supt_trans)
apply (rule all_s_s_mul_ext)
apply (auto dest: not_top_ctxts_supt intro: actop_suptmulexeq)
apply (rule s_mul_ext_trans [of _ _ _ "{#Fun g ts#}"])
apply (auto simp: trans_def compatible_l_def compatible_r_def refl_on_def dest: supt_trans)
apply (rule s_ns_mul_ext_trans [of _ _ _ "{#Fun g ts#}"])
apply (auto simp: trans_def compatible_l_def compatible_r_def refl_on_def dest: supt_trans)
apply (rule all_s_s_mul_ext)
apply (auto dest: not_top_ctxts_supt intro: actop_suptmulexeq args_in_suptmulex)
apply (rule s_mul_ext_trans [of _ _ _ "{#Fun g ts#}"])
apply (auto simp: trans_def compatible_l_def compatible_r_def refl_on_def dest: supt_trans)
apply (rule s_ns_mul_ext_trans [of _ _ _ "{#Fun g ts#}"])
apply (auto simp: trans_def compatible_l_def compatible_r_def refl_on_def dest: supt_trans)
apply (rule all_s_s_mul_ext)
apply (auto dest: not_top_ctxts_supt intro: actop_suptmulexeq args_in_suptmulex)
done
qed
qed
next
case (Var x)
with assms show ?thesis by auto
qed
qed
lemma rrstep_E_imp_nabla_mul_supt:
assumes "(s, t) ∈ rrstep E" and "t ⊳ u"
shows "∇ F⇩A s ⊳⇩# ∇ F⇩A u"
using nabla_rrstep_E[OF assms(1)] supt_impl_nabla_mul_supt[OF assms(2)]
by auto
lemma actopstep_E_preserves_actop:
assumes "(s, t) ∈ actopstep F E" and "root s = Some (f, n)"
shows "actop f s = actop f t"
using assms apply (auto simp: actopstep_def dest!: actopstep_sym_cases)
using actop_rrstepE apply blast
by (auto dest!: actop_rrstepE simp: top_ctxts_root)
lemma nabla_actop_conv:
assumes "C ∈ top_ctxts f" and "C ≠ □" and "f ∈ F⇩A"
shows "∇ F⇩A (C⟨t⟩) = actop f (C⟨t⟩)"
using assms by (cases) auto
lemma actopstep_E_preserves_nabla:
assumes "(s, t) ∈ actopstep F E" and "root s = Some (f, n)" and "f ∈ F⇩A"
shows "∇ F⇩A s = ∇ F⇩A t"
using assms apply (auto simp: actopstep_def dest!: actopstep_sym_cases)
using nabla_rrstep_E apply blast
by (auto dest!: actop_rrstepE simp: nabla_actop_conv top_ctxts_root)
lemma Q_preserves_nabla:
assumes "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ D E)"
shows "∇ F⇩A s ⊇# ∇ F⇩A t" (is ?goal1)
and "(s,t) ∈ rstep E O {⊳} ⟹ ∇ F⇩A s ⊃# ∇ F⇩A t" (is "?prem2 ⟹ ?goal2")
proof(atomize(full))
have "wf_trs E" using wf by (auto simp: wf_trs_def)
obtain l and r and f and us and σ
where rule: "(l, r) ∈ E" and "♯ s = ♯ l ⋅ σ" and "♯ t = ♯ (Fun f us) ⋅ σ"
and "r ⊵ Fun f us" (is "r ⊵ ?u") and lu: "¬ l ⊳ Fun f us" and "(f, length us) ∈ D"
using assms by (auto simp: DP_on_def elim!: rrstepE)
then have s: "s = l ⋅ σ" and t: "t = ?u ⋅ σ"
using wf_trs_imp_lhs_Fun [OF ‹wf_trs E› rule]
by (cases s; cases t; auto dest!: inj_shp)+
show "?goal1 ∧ (?prem2 ⟶ ?goal2)" (is ?thesis)
proof (cases "r = ?u")
case True
then have rrstep: "(s, t) ∈ rrstep E" using rule and s and t by (auto)
then have "∇ F⇩A s = ∇ F⇩A t" by (rule nabla_rrstep_E)
moreover {
assume "?prem2"
then obtain u where "(s,u) ∈ rstep E" "(u,t) ∈ {⊳}" by auto
from rstep_num_symbs_eq[OF this(1)] supt_num_symbs[OF this(2)]
rstep_num_symbs_eq[OF rrstep_imp_rstep[OF rrstep]]
have False by auto
}
ultimately show ?thesis using rrstep by auto
next
case False
then have ru: "r ⊳ ?u" using ‹r ⊵ ?u› by auto
from ru ruleD [OF rule] and EF
have root: "root l = Some (f, 2)" and len: "length us = 2"
using supt_imp_funas_term_subset [OF ‹r ⊳ ?u›] and rule
by (auto simp: funs_defs)
from root rule have fE: "f ∈ funs_trs E" by (cases l; force simp: funs_defs)
with EF have f: "f ∈ F⇩A ∪ F⇩C" by auto
show ?thesis
proof (cases "f ∈ F⇩A")
case True
with len root rhs_subt_actop_subset [OF ‹(l, r) ∈ E› s refl ‹r ⊳ ?u› root True] True
show ?thesis by (auto simp: t)
next
case False
with f have "f ∈ F⇩C - F⇩A" by auto
from AC_C_theory.only_C_D[OF AC_C_E rule root this] obtain v w where
l: "l = Fun f [v,w]" and r: "r = Fun f [w,v]" by auto
def u ≡ ?u
from supt_Fun_imp_arg_supteq[OF ru[unfolded r]] lu[unfolded l] have False
unfolding u_def[symmetric] using set_supteq_into_supt[of _ "[v,w]" u f] by auto
thus ?thesis ..
qed
qed
qed
private lemma QE_preserve_nabla:
assumes "(♯ s, ♯ t) ∈ rstep E ∪ rrstep (DP_on ♯ D E)"
and s: "s ∈ ST"
and d: "defined (R ∪ E) (the (root s))"
shows "(∇ F⇩A s, ∇ F⇩A t) ∈ ns_mul_ext po2w po2s"
using assms(1)
proof
assume "(♯ s, ♯ t) ∈ rstep E"
hence st: "(s,t) ∈ nrrstep E" using sharp_rstep_imp_nrrstep[OF _ _ d] by auto
show ?thesis
proof (cases "(s,t) ∈ actopstep F⇩A E")
case True
with ‹(s, t) ∈ nrrstep E› have eq: "∇ F⇩A s = ∇ F⇩A t"
apply (auto simp: actopstep_def actopstep_sym_iff top_ctxts_root nabla_rrstep_E)
using True actopstep_E_preserves_nabla top_ctxts_root by fastforce
show ?thesis unfolding eq
apply(rule ns_mul_ext_refl_local) unfolding locally_refl_def by auto
next case False
with nrrstep_imp_rstep[OF st]
have "(s,t) ∈ acnontopstep F⇩A E" unfolding acnontopstep_def by auto
from acnontopstep_mul_ext(2)[OF s this] show ?thesis.
qed
next
assume "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ D E)"
then have "∇ F⇩A s ⊇# ∇ F⇩A t" using Q_preserves_nabla by blast
from supseteq_imp_ns_mul_ext [OF refl_rtrancl this]
show ?thesis .
qed
lemma not_SN_on_pred: "(s,t) ∈ r ⟹ ¬ SN_on r {t} ⟹ ¬ SN_on r {s}"
by (meson step_preserves_SN_on)
lemma not_SN_on_rel_pred: "(s,t) ∈ r ∪ e ⟹ ¬ SN_on (relto r e) {t} ⟹ ¬ SN_on (relto r e) {s}"
by (meson step_preserves_SN_on_relto)
lemma not_SN_on_rel_preds:
assumes tr: "(s,t) ∈ (r ∪ e)⇧*"
and SN: "¬ SN_on (relto r e) {t}"
shows "¬ SN_on (relto r e) {s}"
using tr unfolding rtrancl_power
proof (elim exE)
fix n assume "(s, t) ∈ (r ∪ e) ^^ n"
with SN show ?thesis
proof(induct n arbitrary: s)
case 0 thus ?case using SN by auto
next case (Suc n)
obtain s' where ss': "(s,s') ∈ r ∪ e" and s't: "(s',t) ∈ (r ∪ e) ^^ n" using relpow_Suc_E2[OF Suc(3)].
from not_SN_on_rel_pred[OF ss' Suc(1)[OF SN s't]] show ?case.
qed
qed
lemma Tinf_imp_not_SN_on:
"s ∈ Tinf r ⟹ ¬ SN_on r {s}"
by (auto simp: Tinf_def)
lemma AC_is_size_preserving:
assumes "rrstep E = rrstep (AC_trs F F)"
shows "size_preserving_trs E"
proof -
have "E ⊆ rstep E" by auto
also have "… ⊆ acrstep F F"
proof (rule rstep_subset[OF ctxt_closed_rstep subst_closed_rstep])
have "E ⊆ rrstep E" by auto
also have "… ⊆ acrstep F F" unfolding assms(1) by (simp add: rstep_iff_rrstep_or_nrrstep)
finally show "E ⊆ acrstep F F" .
qed
finally have E: "E ⊆ acrstep F F" .
interpret size_preserving_trs "AC_trs F F" by (rule size_preserving_AC_trs)
show ?thesis
proof (standard, clarify)
fix l r
assume "(l,r) ∈ E"
with E have "(l,r) ∈ acrstep F F" by auto
from rstep_num_symbs_eq[OF this] rstep_vars_terms_ms_eq[OF this]
show "num_symbs l = num_symbs r ∧ vars_term_ms l = vars_term_ms r" by auto
qed
qed
lemma Tinf_relstep_defined_root':
assumes "wf_trs (R ∪ E)" and "t ∈ Tinf (relstep R E)"
shows "∃f. defined (R ∪ E) f ∧ root t = Some f"
using assms(1)
and Tinf_imp_SN_nr_first_root_step_rel[of _ False "{}" _ "{}", unfolded qrstep_rstep_conv nrqrstep_nrrstep rqrstep_rrstep_conv, OF assms(2)]
and nrrsteps_imp_eq_root_arg_rsteps [of t _ "R ∪ E"]
and assms
by (auto simp: nrrstep_union wf_trs_def defined_def elim!: rrstepE) (case_tac l; auto)+
lemma rrstep_Tinfs_imp_rrstep_R_DP_on:
assumes "(s, t) ∈ rrstep R" and "s ∈ Tinf (relstep R E)" and "t ∈ Tinf (relstep R E)"
shows "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ {f. defined (R ∪ E) f} R)"
proof -
from Tinf_relstep_defined_root' [OF wf assms(3)] obtain f and n
where "root t = Some (f, n)" and *: "defined (R ∪ E) (f, n)" by force
moreover obtain l and r and σ where rule: "(l, r) ∈ R" and s: "s = l ⋅ σ" and t: "t = r ⋅ σ"
using assms by (auto elim: rrstepE)
moreover have "is_Fun r"
proof
assume "is_Var r"
then obtain x where "r = Var x" and "x ∈ vars_term l"
using wf and rule by (cases r; force simp: wf_trs_def)
then have "l ⊳ r" using wf and rule by (cases l) (auto simp: wf_trs_def)
then show False using assms(2, 3) by (auto simp: s t Tinf_def dest: supt_subst)
qed
ultimately obtain us where r: "r = Fun f us" (is "_ = ?u") and [simp]: "length us = n" by auto
then have "r ⊵ ?u" by simp
then have "(♯ l, ♯ ?u) ∈ DP_on ♯ {f. defined (R ∪ E) f} R"
using * and rule apply (auto simp: DP_on_def)
apply (rule exI [of _ l]) apply auto
apply (rule exI [of _ r], rule exI [of _ f]) apply (auto simp: r [symmetric])
using s and t and assms(2, 3) by (auto simp: Tinf_def dest: supt_subst)
from rrstepI [OF this, of "♯ s" σ "♯ t"]
show "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ {f. defined (R ∪ E) f} R)"
using wf and rule by (cases l) (auto simp: s t r wf_trs_def)
qed
lemma rrstep_Tinfs_imp_rrstep_E_DP_on:
assumes "(s, t) ∈ rrstep E" and "s ∈ Tinf (relstep R E)"
shows "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ {f. defined (R ∪ E) f} E)"
proof -
obtain l and r and σ where rule: "(l, r) ∈ E" and s: "s = l ⋅ σ" and t: "t = r ⋅ σ"
using assms by (auto elim: rrstepE)
from ruleD[OF rule] obtain f ls rs where l: "l = Fun f ls" and r: "r = Fun f rs" (is "_ = ?u")
and [simp]: "length ls = length rs" by auto
from rule l have *: "defined (R ∪ E) (f,length rs)" unfolding defined_def by auto
interpret AC_C_theory E "F⇩C - F⇩A" by (rule AC_C_E)
from supt_num_symbs[of l r] same_size rule
have supt: "¬ l ⊳ r" by auto
have "(♯ l, ♯ r) ∈ DP_on ♯ {f. defined (R ∪ E) f} E"
using * and rule apply (auto simp: DP_on_def r)
apply (rule exI [of _ l]) apply auto
apply (rule exI [of _ r], rule exI [of _ f]) by (insert supt, auto simp: r)
from rrstepI [OF this, of "♯ s" σ "♯ t"]
show "(♯ s, ♯ t) ∈ rrstep (DP_on ♯ {f. defined (R ∪ E) f} E)"
using wf and rule by (auto simp: l r s t)
qed
interpretation aoc_rewriting F⇩A F⇩C .
theorem main_sound:
defines "D ≡ {f. defined (R ∪ E) f}"
defines "P ≡ DP_on ♯ D R"
assumes R_ext: "is_ext_trs R F⇩A F⇩C R⇩e⇩x⇩t"
and E_is_AC: "(rstep E)⇧* = AOCEQ"
and Q: "Q = DP_on ♯ D E"
and finP: "weakly_finite P Q R E"
and finP': "weakly_finite (♯ R⇩e⇩x⇩t) Q R E"
shows "SN (relstep R E)"
proof (rule ccontr)
from po3[OF finP] interpret po3P: SN_order_pair "po3s P" "po3w P".
from po3[OF finP'] interpret po3P': SN_order_pair "po3s (♯ R⇩e⇩x⇩t)" "po3w (♯ R⇩e⇩x⇩t)".
def po2ms ≡ "s_mul_ext po2w po2s"
def po2mw ≡ "ns_mul_ext po2w po2s"
interpret AC_C_theory E "F⇩C - F⇩A" by (rule AC_C_E)
interpret po2m: SN_order_pair po2ms po2mw
unfolding po2ms_def po2mw_def using po2.mul_ext_SN_order_pair.
def indos ≡ "lex_two (po3s P) (po3w P) (lex_two (po3s (♯ R⇩e⇩x⇩t)) (po3w (♯ R⇩e⇩x⇩t)) po2ms)"
def indow ≡ "lex_two (po3s P) (po3w P) (lex_two (po3s (♯ R⇩e⇩x⇩t)) (po3w (♯ R⇩e⇩x⇩t)) po2mw)"
interpret indo: SN_order_pair indos indow
unfolding indos_def indow_def by(intro lex_two_SN_order_pair;fact)
def msr ≡ "λs :: ('f,'v) term. (♯ s, ♯ s, ∇ F⇩A s )"
{ fix s assume "s ∈ Tinf (relstep R E)"
hence False
proof (induct "msr s" arbitrary: s rule: SN_induct[OF indo.SN])
case (1 s)
from Tinf_starts_relchain [OF SN_suptrel subset_refl 1(2), unfolded starts_relchain_def]
obtain w and m
where "relchain_part P Q s w m" unfolding P_def Q D_def by blast
from this[unfolded relchain_part_def]
have w: "⋀i. w i ∈ Tinf (relstep R E)"
and sw0: "s = w 0"
and QE: "⋀i. i < m ⟹ (♯ (w i), ♯ (w (Suc i))) ∈ rstep E ∪ minstep Q"
and PR: "(♯ (w m), ♯ (w (Suc m))) ∈ rstep R ∪ minstep P"
by (auto simp: nrrstep_imp_rstep)
from Tinf_relstep_defined_root[OF wf w]
have d: "⋀ i. defined (R ∪ E) (the (root (w i)))" .
def u ≡ "w (Suc m)"
with PR w
have tu: "(♯ (w m), ♯ u) ∈ rstep R ∪ minstep P" and u: "u ∈ Tinf (relstep R E)" by auto
have "⋀P''. (♯ s, ♯ (w m)) ∈ po3w P''"
proof -
fix P''
have "(♯ s, ♯ (w m)) ∈ (rstep E ∪ minstep Q)⇧*"
unfolding rtrancl_fun_conv
apply (intro exI[of _ "λi. ♯ (w i)"] exI[of _ m]) using QE sw0 by auto
also have "... ⊆ po3w P''" unfolding rstep_union minstep_union by regexp
ultimately show "(♯ s, ♯ (w m)) ∈ ..." by auto
qed
moreover have "(∇ F⇩A s, ∇ F⇩A (w m)) ∈ po2mw"
proof -
{ fix i assume "i ≤ m" hence "(∇ F⇩A s, ∇ F⇩A (w i)) ∈ po2mw"
proof (induct i)
case 0 show ?case unfolding sw0 using "po2m.refl_NS_point" by auto
next case (Suc i)
hence i: "i < m"
and st: "(∇ F⇩A s, ∇ F⇩A (w i)) ∈ po2mw" by auto
have "(∇ F⇩A (w i), ∇ F⇩A (w (Suc i))) ∈ po2mw"
unfolding po2mw_def
apply(rule QE_preserve_nabla[OF _ _ d])
using Suc w[unfolded Tinf_def] QE[unfolded Q, of i] by auto
from po2m.trans_NS_point[OF st this]
show ?case.
qed
}
thus ?thesis by auto
qed
ultimately have swm_indow: "(msr s, msr (w m)) ∈ indow" unfolding indow_def msr_def by auto
show ?case
proof(cases "(♯ (w m), ♯ u) ∈ minstep P")
case True
hence "(♯ (w m), ♯ u) ∈ po3s P" by auto
hence "(msr (w m), msr u) ∈ indos" unfolding indos_def msr_def by auto
with indo.compat_NS_S_point[OF swm_indow this] 1 u show ?thesis by auto
next case False
hence Rsh: "(♯ (w m), ♯ u) ∈ rstep R" using tu by auto
note R = sharp_rstep_imp_nrrstep[OF _ Rsh d]
have wmu_po3w: "⋀P''. (♯ (w m), ♯ u) ∈ po3w P''"
apply(rule subsetD[OF _ Rsh]) unfolding minstep_union rstep_union by regexp
show ?thesis
proof (cases "(w m, u) ∈ actopstep F⇩A R")
case False
with R have "(w m, u) ∈ acnontopstep F⇩A R"
using nrrstep_imp_rstep unfolding acnontopstep_def by auto
from acnontopstep_mul_ext(1)[OF _ this] w[unfolded Tinf_def]
have "(∇ F⇩A (w m), ∇ F⇩A u) ∈ po2ms" unfolding po2ms_def by auto
with wmu_po3w
have "(msr (w m), msr u) ∈ indos" unfolding indos_def msr_def by auto
with indo.compat_NS_S_point[OF swm_indow this] 1 u show ?thesis by auto
next
case True
then obtain f where topstep: "(w m, u) ∈ actopstep_sym f F⇩A R" by (auto simp: actopstep_def)
have "∀(l, r)∈R. is_Fun l" using wf by (auto simp: wf_trs_def')
from actopstep_sym_rrstep_or_ext_trs[OF R_ext this topstep, folded E_is_AC]
show ?thesis
proof
assume "(w m, u) ∈ rrstep R"
from rrstep_Tinfs_imp_rrstep_R_DP_on [OF this w]
have "(♯ (w m), ♯ u) ∈ minstep P"
using u w by (auto dest: Tinf_sharp_imp_SN simp: P_def D_def M_def)
with False show False by auto
next
assume "(w m, u) ∈ relto (rrstep (ext_trs R)) (rstep E)"
then obtain t' v
where wt': "(w m, t') ∈ (rstep E)⇧*"
and t'v: "(t',v) ∈ rrstep (ext_trs R)"
and vu: "(v,u) ∈ (rstep E)⇧*"
by force
from t'v have t'vR: "(t',v) ∈ nrrstep R"
by (auto dest: rrstep_imp_rstep rstep_ext_trs_imp_nrrstep)
from nrrstep_imp_rstep[OF this] vu u
have t': "¬ SN_on (relstep R E) {t'}"
unfolding Tinf_def by (subst not_SN_on_pred, auto)
from wt' obtain t n
where wt: "t 0 = w m"
and E: "⋀i. i < n ⟹ (t i, t (Suc i)) ∈ rstep E"
and tt': "t n = t'"
unfolding rtrancl_fun_conv by auto
have t_t': "⋀i. i ≤ n ⟹ (t i, t') ∈ (rstep E)⇧*"
proof -
fix i assume i_n: "i ≤ n"
thus "(t i, t') ∈ (rstep E)⇧*"
proof (induct "n - i" arbitrary: i)
case (Suc ni i)
with E[of "i"]
have "(t i, t (Suc i)) ∈ rstep E" and "(t (Suc i), t') ∈ (rstep E)⇧*" by auto
thus ?case by auto
qed (auto simp: tt')
qed
have t: "⋀i. i ≤ n ⟹ ¬ SN_on (relstep R E) {t i}"
proof -
fix i assume i: "i ≤ n"
show "¬ SN_on (relstep R E) {t i}"
by (rule not_SN_on_rel_preds[OF _ t'], rule set_mp[OF _ t_t'[OF i]], regexp)
qed
have "⋀i. i ≤ n ⟹ t i ∈ Tinf (relstep R E) ∧ (msr s, msr (t i)) ∈ indow"
proof -
fix i assume "i ≤ n"
thus "t i ∈ Tinf (relstep R E) ∧ (msr s, msr (t i)) ∈ indow"
proof (induct i)
case 0 thus ?case using wt w[of m] swm_indow by auto
next case (Suc i)
hence i: "i < n"
and ti: "t i ∈ Tinf (relstep R E)"
and sti_indow: "(msr s, msr (t i)) ∈ indow" by auto
from E[OF i] consider (root) "(t i, t (Suc i)) ∈ rrstep E"
| (nroot) "(t i, t (Suc i)) ∈ nrrstep E" unfolding rstep_iff_rrstep_or_nrrstep by auto
then have QE: "(♯ (t i), ♯ (t (Suc i))) ∈ rstep E ∪ rrstep Q"
proof (cases)
case nroot
from nrrstep_imp_sharp_rstep[OF this]
have "(♯ (t i), ♯ (t (Suc i))) ∈ rstep E" by auto
thus ?thesis by auto
next
case root
from rrstep_Tinfs_imp_rrstep_E_DP_on[OF this ti]
have "(♯ (t i), ♯ (t (Suc i))) ∈ rrstep Q" unfolding Q D_def .
thus ?thesis by auto
qed
have titSi_po2mw: "(∇ F⇩A (t i), ∇ F⇩A (t (Suc i))) ∈ po2mw"
using ti unfolding po2mw_def Tinf_def
apply (intro QE_preserve_nabla[OF QE [unfolded Q] _ Tinf_relstep_defined_root [OF wf ti]])
by auto
have tSi: "t (Suc i) ∈ Tinf (relstep R E)"
proof (rule ccontr)
have nSN: "¬ SN_on (relstep R E) {t (Suc i)}" using t Suc by auto
assume notTinf: "t (Suc i) ∉ Tinf (relstep R E)"
with E[OF i, unfolded rstep_iff_rrstep_or_nrrstep] Tinf_nrrstep[OF ti _ nSN]
have "(t i, t (Suc i)) ∈ rrstep E" unfolding nrrstep_union by auto
from rrstep_imp_minstep(2)[OF _ wf ti nSN this]
obtain t''
where "t'' ⊴ t (Suc i)"
and t'': "t'' ∈ Tinf (relstep R E)"
and tit'': "(♯ (t i), ♯ t'') ∈ minstep Q" unfolding Q D_def by auto
hence tSit'': "t (Suc i) ⊳ t''" using notTinf by auto
have "(♯ (t i), ♯ t'') ∈ po3w P" "(♯ (t i), ♯ t'') ∈ po3w (♯ R⇩e⇩x⇩t)"
using tit'' unfolding minstep_union by auto
moreover
from tit'' Q_preserves_nabla(2)[OF _ relcompI[OF E[OF i] tSit'']]
have "∇ F⇩A (t i) ⊃# ∇ F⇩A t''" by (auto simp: Q)
then have "(∇ F⇩A (t i), ∇ F⇩A t'') ∈ po2ms"
by (unfold po2ms_def, auto intro!: supset_imp_s_mul_ext refl_onI)
ultimately have "(msr (t i), msr t'') ∈ indos"
unfolding indos_def msr_def by auto
with sti_indow have "(msr s, msr t'') ∈ indos"
using indo.compat_NS_S by auto
from 1(1)[OF this t''] show False.
qed
with ti Tinf_sharp_imp_SN have "♯ (t i) ∈ M" "♯ (t (Suc i)) ∈ M" by (auto simp: M_def)
moreover then have "⋀P''. (♯ (t i), ♯ (t (Suc i))) ∈ po3w P''"
using QE by (auto simp: minstep_union rstep_union)
then have "(msr (t i), msr (t (Suc i))) ∈ indow"
unfolding indow_def msr_def using titSi_po2mw by auto
ultimately show ?case using indo.trans_NS_point[OF sti_indow] tSi
by (auto simp: M'_def)
qed
qed
with tt'
have t': "t' ∈ Tinf (relstep R E)" and st'_indow: "(msr s, msr t') ∈ indow" by auto
have v: "v ∈ Tinf (relstep R E)"
apply (rule Tinf_nrrstep[OF t']) using t'vR unfolding nrrstep_union apply simp
apply (rule not_SN_on_rel_preds[OF _ Tinf_imp_not_SN_on[OF u]])
apply (rule subsetD[OF _ vu]) by regexp
with t' have "♯t' ∈ M" "♯ v ∈ M" using Tinf_sharp_imp_SN by (auto simp: M_def)
moreover from is_ext_trs_rrstep[OF R_ext t'v]
have "(♯ t', ♯ v) ∈ rrstep (♯ R⇩e⇩x⇩t)" .
ultimately have "(♯ t', ♯ v) ∈ minstep (♯ R⇩e⇩x⇩t)" unfolding M_def by auto
hence "(♯ t', ♯ v) ∈ po3s (♯ R⇩e⇩x⇩t)" unfolding minstep_union by auto
moreover have "(♯ t', ♯ v) ∈ po3w P"
unfolding rstep_union
using nrrstep_imp_sharp_nrrstep[OF t'vR] nrrstep_imp_rstep by fast
hence "(♯ t', ♯ v) ∈ po3w P" using t' unfolding M_def Tinf_def by auto
ultimately have "(msr t', msr v) ∈ indos" unfolding indos_def msr_def by auto
with st'_indow have "(msr s, msr v) ∈ indos" using "indo.compat_NS_S" by auto
from 1(1)[OF this v] show False.
qed
qed
qed
qed
} note main = this
assume "¬ ?thesis"
then obtain s where "s ∈ Tinf (relstep R E)" using not_SN_imp_Tinf by auto
from main[OF this]
show False.
qed
end
end
context
fixes F⇩A F⇩C :: "'f set"
begin
interpretation aoc_rewriting F⇩A F⇩C .
corollary SN_relstep_via_finite_rel_dpps:
defines "D ≡ {f. defined (R ∪ E) f}"
assumes R_ext: "is_ext_trs R F⇩A F⇩C R⇩e⇩x⇩t"
and E_is_AC: "(rstep E)⇧* = AOCEQ"
and AC: "AC_C_theory E (F⇩C - F⇩A)"
and EF⇩A: "funs_trs E ⊆ F⇩A ∪ F⇩C"
and finP: "finite_rel_dpp (DP_on ♯ D R, DP_on ♯ D E, {}, R, E)"
and finP': "finite_rel_dpp (♯ R⇩e⇩x⇩t, DP_on ♯ D E, {}, R, E)"
shows "SN (relstep R E)"
by (rule main_sound [OF AC EF⇩A R_ext E_is_AC refl])
(insert finP finP', auto simp: D_def finite_rel_dpp_def weakly_finite_def)
corollary SN_relstep_via_finite_rel_dpps_defined_R:
defines "D ≡ {f. defined R f}"
assumes R_ext: "is_ext_trs R F⇩A F⇩C R⇩e⇩x⇩t"
and E_is_AC: "(rstep E)⇧* = AOCEQ"
and AC: "AC_C_theory E (F⇩C - F⇩A)"
and EF⇩A: "funs_trs E ⊆ F⇩A ∪ F⇩C"
and finP: "finite_rel_dpp (DP_on ♯ D R, DP_on ♯ D E, {}, R, E)"
and finP': "finite_rel_dpp (♯ R⇩e⇩x⇩t, DP_on ♯ D E, {}, R, E)"
shows "SN (relstep R E)"
proof -
def RR ≡ "{(l,r). root l ≠ None ∧ root r ≠ None ∧ the (root l) ∈ D ∧ the (root r) ∈ D} :: ('f,'v)trs"
let ?Rext = "R⇩e⇩x⇩t ∩ RR"
have finP': "finite_rel_dpp (♯ ?Rext, DP_on ♯ D E, {}, R, E)"
by (rule finite_rel_dpp_pairs_mono[OF finP'], auto simp: dir_image_def)
have R_ext: "is_ext_trs R F⇩A F⇩C ?Rext" unfolding is_ext_trs_def
proof (intro allI impI conjI)
fix l r f
assume lr: "(l,r) ∈ R" "f ∈ F⇩A" "root l = Some (f,2)"
note R_ext = R_ext[unfolded is_ext_trs_def, rule_format, OF this]
from lr(1,3) have f: "(f,2) ∈ D" "(f,Suc (Suc 0)) ∈ D" unfolding defined_def D_def by auto
from R_ext obtain x where x: "x ∉ vars_rule (l,r)" and lr: "ext_AC_rule f (l,r) (Var x) ∈ R⇩e⇩x⇩t" by auto
from lr f have "ext_AC_rule f (l,r) (Var x) ∈ ?Rext" unfolding RR_def ext_AC_rule_def by auto
with x show "∃x. x ∉ vars_rule (l, r) ∧ ext_AC_rule f (l, r) (Var x) ∈ R⇩e⇩x⇩t ∩ RR" by blast
assume "f ∉ F⇩C"
with R_ext show "∃x y z. x ∉ vars_rule (l, r) ∧
y ∉ vars_rule (l, r) ∧
z ∉ vars_rule (l, r) ∧
x ≠ y ∧
(Fun f [Var z, l], Fun f [Var z, r]) ∈ R⇩e⇩x⇩t ∩ RR ∧
(Fun f [Fun f [Var x, l], Var y], Fun f [Fun f [Var x, r], Var y]) ∈ R⇩e⇩x⇩t ∩ RR"
unfolding RR_def using f by auto
qed
let ?DRE = "{f. defined (R ∪ E) f}"
def DD ≡ "{(shp f,n) | f n. defined R (f,n)}"
def C ≡ "{(shp f,n) | f n. defined (R ∪ E) (f,n)} - DD"
have C: "⋀f. f ∈ C ⟹ ¬ defined (R ∪ E) f"
unfolding C_def using shp_not_defined by auto
have CD: "C ∩ DD = {}" unfolding C_def by auto
interpret AC_C_theory E "F⇩C - F⇩A" by fact
{
fix D E and s t :: "('f,'v)term"
assume "(s,t) ∈ DP_on ♯ D E"
hence "root t ∈ Some ` {(shp f,n) | f n. (f,n) ∈ D}"
unfolding DP_on_def by force
} note root_t = this
{
fix D and s t :: "('f,'v)term"
assume st: "(s,t) ∈ DP_on ♯ D E"
then obtain l r h where lr: "(l,r) ∈ E" and s: "s = ♯ l" and rh: "r ⊵ h" and t: "t = ♯ h"
and h: "is_Fun h" unfolding DP_on_def by auto
from ac_ruleD[OF lr] obtain f where l: "funas_term l = {(f,2)}" and r: "funas_term r = {(f,2)}" by auto
hence rs: "root s = Some (shp f,2)" unfolding s by (cases l, auto)
from supteq_imp_funas_term_subset[OF rh] r have "funas_term h ⊆ {(f,2)}" by simp
with h have rt: "root t = Some (shp f,2)" unfolding t by (cases h, auto)
from root_t[OF st, unfolded rt, folded rs] rs[folded rt]
have "root s ∈ Some ` {(♯ f, n) |f n. (f, n) ∈ D}" "root t = root s" by auto
} note root_s_E = this
{
fix s t
assume "(s, t) ∈ DP_on ♯ D E"
from root_t[OF this] root_s_E[OF this]
have "root s ∈ Some ` DD ∧ root t ∈ Some ` DD" unfolding DD_def D_def by auto
} note DP_D_E = this
{
fix s t D
assume st: "(s, t) ∈ DP_on ♯ D R"
then obtain l r where lr: "(l,r) ∈ R" and s: "s = ♯ l" unfolding DP_on_def by auto
from wf lr obtain f ls where l: "l = Fun f ls" unfolding wf_trs_def by (cases l, auto)
from l lr have "defined R (f,length ls)" unfolding defined_def by auto
hence "root s ∈ Some ` DD" unfolding DD_def s l by auto
} note root_s_R = this
note fin_step = defined_symbol_finite_rel_dpp[OF _ _ _ DP_D_E _ CD C wf]
show ?thesis
proof (rule SN_relstep_via_finite_rel_dpps[OF R_ext E_is_AC AC EF⇩A
fin_step[OF finP]
fin_step[OF finP']])
fix s t
assume st: "(s, t) ∈ DP_on ♯ ?DRE R - DP_on ♯ D R"
then obtain l r h where lr: "(l,r) ∈ R" and s: "s = ♯ l" and rh: "r ⊵ h"
and lh: "¬ (l ⊳ h)" and t: "t = ♯ h"
and h: "is_Fun h" "root h ∈ Some ` ?DRE" unfolding DP_on_def by auto
from st have st': "(s, t) ∈ DP_on ♯ ?DRE R" by auto
note root_t = root_t[OF this]
note root_s = root_s_R[OF st']
{
assume "root t ∈ Some ` DD"
hence "root h ∈ Some ` D" unfolding t DD_def D_def using inj_shp h by (cases h, auto)
with lr s rh lh h(1) t have "(s,t) ∈ DP_on ♯ D R" unfolding DP_on_def
by (cases h, auto)
with st have False by auto
}
with root_t have "root t ∈ Some ` C" unfolding C_def by auto
with root_s show "root s ∈ Some ` DD ∧ root t ∈ Some ` C" by auto
next
fix s t
assume "(s, t) ∈ DP_on ♯ D R"
with root_t[OF this] root_s_R[OF this]
show "root s ∈ Some ` DD ∧ root t ∈ Some ` DD" unfolding DD_def D_def by auto
next
fix s t
assume st: "(s, t) ∈ DP_on ♯ ?DRE E - DP_on ♯ D E"
hence "(s,t) ∈ DP_on ♯ ?DRE E" by auto
from root_s_E[OF this] have s_t: "root s = root t" "root s ∈ Some ` {(♯ f, n) |f n. (f, n) ∈ ?DRE}"
by auto
{
assume "root s ∈ Some ` DD"
with s_t have rt: "root t ∈ Some ` DD" by auto
from st obtain l r h where lr: "(l,r) ∈ E" and s: "s = ♯ l" and rh: "r ⊵ h"
and lh: "¬ (l ⊳ h)" and t: "t = ♯ h"
and h: "is_Fun h" "root h ∈ Some ` ?DRE" unfolding DP_on_def by auto
from rt[unfolded t DD_def] have "root h ∈ Some ` D" unfolding D_def using inj_shp h by (cases h, auto)
with lr s rh lh h(1) t have "(s,t) ∈ DP_on ♯ D E" unfolding DP_on_def
by (cases h, auto)
with st have False by auto
}
with s_t(2) have "root s ∈ Some ` C" unfolding C_def by auto
with s_t(1)
show "root s ∈ Some ` C ∧ root t ∈ Some ` C" by auto
thus "root s ∈ Some ` C ∧ root t ∈ Some ` C" .
next
fix s t
assume st: "(s, t) ∈ dir_image ?Rext ♯"
then obtain l r where lr: "(l,r) ∈ RR" and s: "s = ♯ l" and t: "t = ♯ r"
unfolding dir_image_def by auto
thus "root s ∈ Some ` DD ∧ root t ∈ Some ` DD" unfolding s t DD_def RR_def D_def
by (cases l; cases r, auto)
qed auto
qed
end
end
end