Theory Rewriting_LLRG_LV_Mondaic
theory Rewriting_LLRG_LV_Mondaic
imports Rewriting
Replace_Constant
begin
subsection ‹Specific results about rewriting under a linear variable-separated system›
lemma card_varposs_ground:
"card (varposs s) = 0 ⟷ ground s"
by (simp add: finite_varposs varposs_empty_gound)
lemma poss_of_term_subst_apply_varposs:
assumes "p ∈ poss_of_term (constT c) (s ⋅ σ)" "(c, 0) ∉ funas_term s"
shows "∃ q. q ∈ varposs s ∧ q ≤⇩p p" using assms
proof (induct p arbitrary: s)
case Nil
then show ?case by (cases s) (auto simp: poss_of_term_def)
next
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"] Cons(2-)
apply (cases s)
apply (auto simp: poss_of_term_def)
apply (metis position_less_eq_Cons)+
done
qed
lemma poss_of_term_hole_poss:
assumes "p ∈ poss_of_term t C⟨s⟩" and "hole_pos C ≤⇩p p"
shows "p -⇩p hole_pos C ∈ poss_of_term t s" using assms
proof (induct C arbitrary: p)
case (More f ss C ts)
from More(3) obtain ps where [simp]: "p = length ss # ps" and h: "hole_pos C ≤⇩p ps"
by (metis append_Cons hole_pos.simps(2) less_eq_poss_append_itself pos_les_eq_append_diff)
show ?case using More(1)[OF _ h] More(2)
by (auto simp: poss_of_term_def)
qed auto
lemma remove_const_subst_from_match:
assumes "s ⋅ const_subst c = C⟨l ⋅ σ⟩" "(c, 0) ∉ funas_term l" "linear_term l"
shows "∃ D τ. s = D⟨l ⋅ τ⟩" using assms
proof (induct "card (varposs s)" arbitrary: s)
case (Suc x)
from Suc(2) obtain p ps where varposs: "varposs s = insert p ps" "p ∉ ps"
by (metis card_Suc_eq)
let ?s = "s[p ← Fun c []]" have vp: "p ∈ varposs s" using varposs by auto
then have *: "?s ⋅ const_subst c = s ⋅ const_subst c"
by (induct s arbitrary: p) (auto simp: nth_list_update map_update intro!: nth_equalityI)
have "varposs ?s = ps" using varposs varposs_ground_replace_at[of p s "constT c"]
by auto
from Suc(1)[of ?s] Suc(2-) varposs obtain D τ where split: "s[p ← constT c] = D⟨l ⋅ τ⟩"
by (metis "*" ‹varposs s[p ← constT c] = ps› card_insert_if diff_Suc_1 finite_varposs)
have wit: "s = D⟨l ⋅ τ⟩[p ← s |_ p]" unfolding arg_cong[OF split, of "λ t. t[p ← s |_ p]", symmetric]
using vp by simp
from vp split have cases: "p ⊥ hole_pos D ∨ hole_pos D ≤⇩p p"
by auto (metis poss_of_term_const_ctxt_apply poss_of_term_replace_term_at varposs_imp_poss)
show ?case
proof (cases "p ⊥ hole_pos D")
case True then show ?thesis using wit
by (auto simp: par_hole_pos_replace_term_context_at)
next
case False
then have hole: "hole_pos D ≤⇩p p" using cases by auto
from vp split have "p ∈ poss_of_term (constT c) s[p ← constT c]"
using poss_of_term_replace_term_at varposs_imp_poss by blast
from poss_of_term_hole_poss[OF this[unfolded split] hole]
have "p -⇩p hole_pos D ∈ poss_of_term (constT c) (l ⋅ τ)"
by simp
from poss_of_term_subst_apply_varposs[OF this Suc(4)] obtain q where
q: "q ∈ varposs l" "q ≤⇩p (p -⇩p (hole_pos D))" by blast
show ?thesis using wit Suc(5) hole
using linear_term_varposs_subst_replace_term[OF Suc(5) q, of τ "s |_ p"]
by auto
qed
qed (auto simp: card_varposs_ground ground_subst_apply)
definition "llrg ℛ ⟷ (∀ (l, r) ∈ ℛ. linear_term l ∧ ground r)"
definition "lv ℛ ⟷ (∀ (l, r) ∈ ℛ. linear_term l ∧ linear_term r ∧ vars_term l ∩ vars_term r = {})"
definition "monadic ℱ ⟷ (∀ (f, n) ∈ ℱ. n ≤ Suc 0)"
lemma ground_NF_srstep_gsrstep:
"ground s ⟹ s ∈ NF (srstep ℱ ℛ) ⟹ s ∈ NF (gsrstep ℱ ℛ)"
by blast
lemma NF_to_fresh_const_subst_NF:
assumes lin: "linear_sys ℛ" and fresh_const: "(c, 0) ∉ funas_rel ℛ" "funas_rel ℛ ⊆ ℱ"
and nf_f: "funas_term s ⊆ ℱ" "s ∈ NF (srstep ℱ ℛ)"
shows "s ⋅ const_subst c ∈ NF (gsrstep ℋ ℛ)"
proof (rule ccontr)
assume "s ⋅ const_subst c ∉ NF (Restr (srstep ℋ ℛ) (Collect ground))"
then obtain C l r σ where step: "(l, r) ∈ ℛ" "s ⋅ const_subst c = C⟨l ⋅ σ⟩" by fastforce
from step(1) have l: "(c, 0) ∉ funas_term l" "linear_term l" using lin fresh_const
by (auto simp: funas_rel_def)
obtain D τ where "s = D⟨l ⋅ τ⟩" using remove_const_subst_from_match[OF step(2) l] by blast
then show False using step(1) nf_f
by (meson NF_no_trancl_step fresh_const(2) r_into_trancl' rstepI rstep_trancl_sig_step_r)
qed
lemma fresh_const_subst_NF_pres:
assumes fresh_const: "(c, 0) ∉ funas_rel ℛ" "funas_rel ℛ ⊆ ℱ"
and nf_f: "funas_term s ⊆ ℱ" "ℱ ⊆ ℋ" "(c, 0) ∈ ℋ" "s ⋅ const_subst c ∈ NF (gsrstep ℋ ℛ)"
shows "s ∈ NF (srstep ℱ ℛ)"
proof (rule ccontr)
assume "s ∉ NF (srstep ℱ ℛ)"
then obtain C l r σ where step: "(l, r) ∈ ℛ" "s = C⟨l ⋅ σ⟩" by fastforce
let ?τ = "λ x. if x ∈ vars_term l then (σ x) ⋅ const_subst c else Fun c []"
define D where "D = (C ⋅⇩c const_subst c)"
have s: "s ⋅ const_subst c = D⟨l ⋅ ?τ⟩" unfolding D_def step(2)
by (auto simp: subst_compose simp flip: subst_subst_compose intro!: term_subst_eq)
have funas: "funas_ctxt D ⊆ ℋ" "funas_term (l ⋅ ?τ) ⊆ ℋ" "funas_term (r ⋅ ?τ) ⊆ ℋ"
using step nf_f(1 - 3) fresh_const(2) unfolding D_def
by (auto simp: funas_ctxt_subst_apply_ctxt funas_term_subst funas_rel_def split: if_splits)
moreover have "ground_ctxt D" "ground (l ⋅ ?τ)" "ground (r ⋅ ?τ)" using arg_cong[OF s, of ground] unfolding D_def
by (auto intro!: ground_substI)
ultimately have "(D⟨l ⋅ ?τ⟩, D⟨r ⋅ ?τ⟩) ∈ gsrstep ℋ ℛ" using step(1)
by (simp add: rstepI sig_stepI)
then show False using nf_f(4) unfolding s[symmetric]
by blast
qed
lemma linear_sys_gNF_eq_NF_eq:
assumes lin: "linear_sys ℛ" "linear_sys 𝒮"
and well: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and fresh: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮"
and lift: "ℱ ⊆ ℋ" "(c, 0) ∈ ℋ"
and nf: "NF (gsrstep ℋ ℛ) = NF (gsrstep ℋ 𝒮)"
shows "NF (srstep ℱ ℛ) = NF (srstep ℱ 𝒮)"
proof -
have [simp]: "¬ funas_term s ⊆ ℱ ⟹ s ∈ NF (srstep ℱ 𝒰)" for s 𝒰 by (meson NF_I sig_stepE(1))
have d1: "s ∈ NF (gsrstep ℋ ℛ) ⟹ s ∈ NF (gsrstep ℋ 𝒮)" for s using nf by auto
have d2: "s ∈ NF (gsrstep ℋ 𝒮) ⟹ s ∈ NF (gsrstep ℋ ℛ)" for s using nf by auto
{fix s assume n: "s ∈ NF (srstep ℱ ℛ)" then have "s ∈ NF (srstep ℱ 𝒮)"
using NF_to_fresh_const_subst_NF[OF lin(1) fresh(1) well(1) _ n, THEN d1]
using fresh_const_subst_NF_pres[OF fresh(2) well(2) _ lift, of s]
by (cases "funas_term s ⊆ ℱ") simp_all}
moreover
{fix s assume n: "s ∈ NF (srstep ℱ 𝒮)" then have "s ∈ NF (srstep ℱ ℛ)"
using NF_to_fresh_const_subst_NF[OF lin(2) fresh(2) well(2) _ n, THEN d2]
using fresh_const_subst_NF_pres[OF fresh(1) well(1) _ lift, of s]
by (cases "funas_term s ⊆ ℱ") simp_all}
ultimately show ?thesis by blast
qed
lemma gsrsteps_to_srsteps:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧+ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧+"
by (meson inf_le1 trancl_mono)
lemma gsrsteps_eq_to_srsteps_eq:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*"
by (metis gsrsteps_to_srsteps rtrancl_eq_or_trancl)
lemma gsrsteps_to_rsteps:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧+ ⟹ (s, t) ∈ (rstep ℛ)⇧+"
using gsrsteps_to_srsteps srstepsD by blast
lemma gsrsteps_eq_to_rsteps_eq:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧* ⟹ (s, t) ∈ (rstep ℛ)⇧*"
by (metis gsrsteps_eq_to_srsteps_eq rtrancl_eq_or_trancl srstepsD)
lemma gsrsteps_eq_relcomp_srsteps_relcompD:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧* O (gsrstep ℱ 𝒮)⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
using gsrsteps_eq_to_srsteps_eq by blast
lemma gsrsteps_eq_relcomp_to_rsteps_relcomp:
"(s, t) ∈ (gsrstep ℱ ℛ)⇧* O (gsrstep ℱ 𝒮)⇧* ⟹ (s, t) ∈ (rstep ℛ)⇧* O (rstep 𝒮)⇧*"
using gsrsteps_eq_relcomp_srsteps_relcompD
using gsrsteps_eq_to_rsteps_eq by blast
lemma ground_srsteps_gsrsteps:
assumes "ground s" "ground t"
and "(s, t) ∈ (srstep ℱ ℛ)⇧+"
shows "(s, t) ∈ (gsrstep ℱ ℛ)⇧+"
proof -
let ?σ = "λ _. s"
from assms(3) have f: "funas_term s ⊆ ℱ" using srstepsD by blast
have "(s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep ℱ ℛ)⇧+" using assms(3, 1) f
proof (induct)
case (base t)
then have "(s ⋅ ?σ, t ⋅ ?σ) ∈ gsrstep ℱ ℛ"
by (auto intro: srstep_subst_closed)
then show ?case by auto
next
case (step t u)
from step(2, 4, 5) have "(t ⋅ ?σ, u ⋅ ?σ) ∈ gsrstep ℱ ℛ"
by (auto intro: srstep_subst_closed)
then show ?case using step(3 - 5)
by (meson Transitive_Closure.trancl_into_trancl)
qed
then show ?thesis using assms(1, 2)
by (simp add: ground_subst_apply)
qed
lemma ground_srsteps_eq_gsrsteps_eq:
assumes "ground s" "ground t"
and "(s, t) ∈ (srstep ℱ ℛ)⇧*"
shows "(s, t) ∈ (gsrstep ℱ ℛ)⇧*"
using ground_srsteps_gsrsteps
by (metis assms rtrancl_eq_or_trancl)
lemma srsteps_eq_relcomp_gsrsteps_relcomp:
assumes "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
and "ground s" "ground t"
shows "(s, t) ∈ (gsrstep ℱ ℛ)⇧* O (gsrstep ℱ 𝒮)⇧*"
proof -
from assms(1) obtain u where steps: "(s, u) ∈ (srstep ℱ ℛ)⇧*" "(u, t) ∈ (srstep ℱ 𝒮)⇧*"
by blast
let ?σ = "λ x. s"
have "(s ⋅ ?σ, u ⋅ ?σ) ∈ (srstep ℱ ℛ)⇧*" "(u ⋅ ?σ, t ⋅ ?σ) ∈ (srstep ℱ 𝒮)⇧*" using steps
using srsteps_eq_subst_closed[OF steps(1), of ?σ]
using srsteps_eq_subst_closed[OF steps(2), of ?σ]
by (metis rtrancl_eq_or_trancl srstepsD)+
then have "(s ⋅ ?σ, u ⋅ ?σ) ∈ (gsrstep ℱ ℛ)⇧*" "(u ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep ℱ 𝒮)⇧*"
using assms(2)
by (auto intro: ground_srsteps_eq_gsrsteps_eq)
then show ?thesis using assms(2, 3)
by (auto simp: ground_subst_apply)
qed
lemma llrg_ground_rhs:
"llrg ℛ ⟹ (l, r) ∈ ℛ ⟹ ground r"
unfolding llrg_def by auto
lemma llrg_rrsteps_groundness:
assumes "llrg ℛ" and "(s, t) ∈ (srrstep ℱ ℛ)"
shows "ground t" using assms(2) ground_vars_term_empty
by (fastforce simp: llrg_def sig_step_def dest!: llrg_ground_rhs[OF assms(1)] split: prod.splits)
lemma llrg_rsteps_pres_groundness:
assumes "llrg ℛ" "ground s"
and "(s, t) ∈ (srstep ℱ ℛ)⇧*"
shows "ground t" using assms(3, 2)
proof (induct rule: rtrancl.induct)
case (rtrancl_into_rtrancl s t u)
then have "ground t" by auto
then show ?case using rtrancl_into_rtrancl(3)
by (auto simp: sig_step_def vars_term_ctxt_apply ground_vars_term_empty ground_subst_apply
dest!: llrg_ground_rhs[OF assms(1)] rstep_imp_C_s_r split: prod.splits)
qed simp
lemma llrg_srsteps_with_root_step_ground:
assumes "llrg ℛ" and "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
shows "ground t" using assms llrg_rrsteps_groundness llrg_rsteps_pres_groundness
unfolding srsteps_with_root_step_def
by blast
lemma llrg_srsteps_with_root_step_inv_ground:
assumes "llrg ℛ" and "(s, t) ∈ srsteps_with_root_step ℱ (ℛ¯)"
shows "ground s" using assms llrg_rrsteps_groundness llrg_rsteps_pres_groundness
unfolding srsteps_with_root_step_def
by (metis (no_types, lifting) converseD relcomp.cases rtrancl_converseD srrstep_converse_dist srstep_converse_dist)
lemma llrg_funas_term_step_pres:
assumes "llrg ℛ" and "(s, t) ∈ (rstep ℛ)"
shows "funas_term t ⊆ funas_rel ℛ ∪ funas_term s"
proof -
have [simp]: "(l, r) ∈ ℛ ⟹ r ⋅ σ = r" for l r σ using assms(1) unfolding llrg_def
by(auto split: prod.splits intro: ground_subst_apply)
show ?thesis using assms
by (auto simp: llrg_def funas_rel_def dest!: rstep_imp_C_s_r)
qed
lemma llrg_funas_term_steps_pres:
assumes "llrg ℛ" and "(s, t) ∈ (rstep ℛ)⇧*"
shows "funas_term t ⊆ funas_rel ℛ ∪ funas_term s"
using assms(2) llrg_funas_term_step_pres[OF assms(1)]
by (induct) auto
lemma monadic_ground_ctxt_apply:
"monadic ℱ ⟹ funas_ctxt C ⊆ ℱ ⟹ ground r ⟹ ground C⟨r⟩"
by (induct C) (auto simp: monadic_def)
lemma llrg_monadic_rstep_pres_groundness:
assumes "llrg ℛ" "monadic ℱ"
and "(s, t) ∈ srstep ℱ ℛ"
shows "ground t" using assms(3)
proof -
from assms(3) obtain C l r σ where r: "(l, r) ∈ ℛ" and t:"t = C⟨r ⋅ σ⟩"
using rstep_imp_C_s_r unfolding sig_step_def by blast
from assms(1, 3) have funas: "funas_term t ⊆ ℱ" "ground r"
by (auto simp: llrg_ground_rhs[OF assms(1) r(1)] dest: srstepD)
then have *: "r ⋅ σ = r" by (simp add: ground_subst_apply)
show ?thesis using funas assms(2) unfolding t *
by (intro monadic_ground_ctxt_apply) auto
qed
lemma llrg_monadic_rsteps_groundness:
assumes "llrg ℛ" "monadic ℱ"
and "(s, t) ∈ (srstep ℱ ℛ)⇧+"
shows "ground t" using assms(3)
using llrg_monadic_rstep_pres_groundness[OF assms(1 ,2)]
by (induct rule: trancl.induct) auto
fun monadic_term where
"monadic_term (Var x) = True"
| "monadic_term (Fun f []) = True"
| "monadic_term (Fun f ts) = (length ts = Suc 0 ∧ monadic_term (hd ts))"
fun monadic_get_leave where
"monadic_get_leave (Var x) = (Var x)"
| "monadic_get_leave (Fun f []) = Fun f []"
| "monadic_get_leave (Fun f ts) = monadic_get_leave (hd ts)"
fun monadic_replace_leave where
"monadic_replace_leave t (Var x) = t"
| "monadic_replace_leave t (Fun f []) = t"
| "monadic_replace_leave t (Fun f ts) = Fun f [monadic_replace_leave t (hd ts)]"
lemma monadic_replace_leave_undo_const_subst:
assumes "monadic_term s"
shows "monadic_replace_leave (monadic_get_leave s) (s ⋅ const_subst c) = s" using assms
proof (induct s)
case (Fun f ts) then show ?case
by (cases ts) auto
qed auto
lemma monadic_replace_leave_context:
assumes "monadic_term C⟨s⟩"
shows "monadic_replace_leave t C⟨s⟩ = C⟨monadic_replace_leave t s⟩" using assms
proof (induct C)
case (More f ss C ts) then show ?case
by (cases ss; cases ts) auto
qed simp
lemma monadic_replace_leave_subst:
assumes "monadic_term (s ⋅ σ)" "¬ ground s"
shows "monadic_replace_leave t (s ⋅ σ) = s ⋅ (λ x. monadic_replace_leave t (σ x))" using assms
proof (induct s)
case (Fun f ts) then show ?case
by (cases ts) auto
qed auto
lemma monadic_sig:
"monadic ℱ ⟹ (f, length ts) ∈ ℱ ⟹ length ts ≤ Suc 0"
by (auto simp: monadic_def)
lemma monadic_sig_funas_term_mt:
"monadic ℱ ⟹ funas_term s ⊆ ℱ ⟹ monadic_term s"
proof (induct s)
case (Fun f ts) then show ?case unfolding monadic_def
by (cases ts) auto
qed simp
lemma monadic_term_const_pres [intro]:
"monadic_term s ⟹ monadic_term (s ⋅ const_subst c)"
proof (induct s)
case (Fun f ts) then show ?case
by (cases ts) auto
qed simp
lemma remove_const_lv_mondaic_step_lhs:
assumes lv: "lv ℛ" and fresh: "(c, 0) ∉ funas_rel ℛ"
and mon: "monadic ℱ"
and step: "(s ⋅ const_subst c, t) ∈ (srstep ℱ ℛ)"
shows "(s, t) ∈ (srstep ℱ ℛ)"
proof -
from step obtain C l r σ where s: "(l, r) ∈ ℛ" "s ⋅ const_subst c = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
by fastforce
have lv: "x ∈ vars_term l ⟹ x ∉ vars_term r" for x using s(1) lv
by (auto simp: lv_def)
from s(1) fresh have cl: "(c, 0) ∉ funas_term l" by (auto simp: funas_rel_def)
have funas: "funas_term s ⊆ ℱ" "(c, 0) ∉ funas_term l" "funas_term t ⊆ ℱ" using s(1) fresh
using step mon funas_term_subst unfolding funas_rel_def
by (auto dest!: srstepD) blast
then have mt: "monadic_term s" "monadic_term (s ⋅ const_subst c)"
using monadic_sig_funas_term_mt[OF mon] by auto
then have ml: "monadic_term (l ⋅ σ)" unfolding s(2)
by (metis funas_ctxt_apply le_sup_iff step mon monadic_sig_funas_term_mt s(2) sig_stepE(1))
show ?thesis
proof (cases "ground s")
case True then show ?thesis using step
by (auto simp: ground_subst_apply)
next
case False note ng = this
then have cs: "(c, 0) ∈ funas_term (s ⋅ const_subst c)"
by (auto simp: funas_term_subst vars_term_empty_ground)
have ngrl: "¬ ground l" using s(2) cs mt ng
proof (induct s arbitrary: C)
case (Var x) then show ?case using cl cs
by (cases C) (auto simp: funas_rel_def ground_subst_apply)
next
case (Fun f ts)
from Fun(5-) obtain t where [simp]: "ts = [t]" by (cases ts) auto
show ?case
proof (cases "C = Hole")
case True then show ?thesis using Fun(2, 3) cl
by (auto simp: ground_subst_apply)
next
case False
from this Fun(2, 3) obtain D where [simp]: "C = More f [] D []"
by (cases C) (auto simp: Cons_eq_append_conv)
show ?thesis using Fun(1)[of t D] Fun(2-)
by simp
qed
qed
let ?τ = "λ x. if x ∈ vars_term l then monadic_replace_leave (monadic_get_leave s) (σ x) else (σ x)"
have "C⟨l ⋅ (λ x. monadic_replace_leave (monadic_get_leave s) (σ x))⟩ = C⟨l ⋅ ?τ⟩"
by (auto intro: term_subst_eq)
then have "s = C⟨l ⋅ ?τ⟩" using arg_cong[OF s(2), of "monadic_replace_leave (monadic_get_leave s)",
unfolded monadic_replace_leave_undo_const_subst[OF mt(1), of c],
unfolded monadic_replace_leave_context[OF mt(2)[unfolded s(2)]],
unfolded monadic_replace_leave_subst[OF ml ngrl]]
by presburger
moreover have "t = C⟨r ⋅ ?τ⟩" using lv unfolding s(3)
by (auto intro!: term_subst_eq)
ultimately show ?thesis using s(1) funas(1, 3)
by blast
qed
qed
lemma remove_const_lv_mondaic_step_rhs:
assumes lv: "lv ℛ" and fresh: "(c, 0) ∉ funas_rel ℛ"
and mon: "monadic ℱ"
and step: "(s, t ⋅ const_subst c) ∈ (srstep ℱ ℛ)"
shows "(s, t) ∈ (srstep ℱ ℛ)"
proof -
have inv_v: "lv (ℛ¯)""(c, 0) ∉ funas_rel (ℛ¯)" using fresh lv
by (auto simp: funas_rel_def lv_def)
have "(t ⋅ const_subst c, s) ∈ (srstep ℱ (ℛ¯))" using step
by (auto simp: rew_converse_outwards)
from remove_const_lv_mondaic_step_lhs[OF inv_v mon this]
have "(t, s) ∈ (srstep ℱ (ℛ¯))" by simp
then show ?thesis by (auto simp: rew_converse_outwards)
qed
lemma remove_const_lv_mondaic_steps_lhs:
assumes lv: "lv ℛ" and fresh: "(c, 0) ∉ funas_rel ℛ"
and mon: "monadic ℱ"
and steps: "(s ⋅ const_subst c, t) ∈ (srstep ℱ ℛ)⇧+"
shows "(s, t) ∈ (srstep ℱ ℛ)⇧+"
using remove_const_lv_mondaic_step_lhs[OF lv fresh mon] steps
by (meson converse_tranclE r_into_trancl trancl_into_trancl2)
lemma remove_const_lv_mondaic_steps_rhs:
assumes lv: "lv ℛ" and fresh: "(c, 0) ∉ funas_rel ℛ"
and mon: "monadic ℱ"
and steps: "(s, t ⋅ const_subst c) ∈ (srstep ℱ ℛ)⇧+"
shows "(s, t) ∈ (srstep ℱ ℛ)⇧+"
using remove_const_lv_mondaic_step_rhs[OF lv fresh mon] steps
by (meson trancl.simps)
lemma remove_const_lv_mondaic_steps:
assumes lv: "lv ℛ" and fresh: "(c, 0) ∉ funas_rel ℛ"
and mon: "monadic ℱ"
and steps: "(s ⋅ const_subst c, t ⋅ const_subst c) ∈ (srstep ℱ ℛ)⇧+"
shows "(s, t) ∈ (srstep ℱ ℛ)⇧+"
using remove_const_lv_mondaic_steps_rhs[OF lv fresh mon remove_const_lv_mondaic_steps_lhs[OF assms]]
by simp
lemma lv_root_step_idep_subst:
assumes "lv ℛ"
and "(s, t) ∈ srrstep ℱ ℛ"
and well: "⋀ x. funas_term (σ x) ⊆ ℱ" "⋀ x. funas_term (τ x) ⊆ ℱ"
shows "(s ⋅ σ, t ⋅ τ) ∈ srrstep ℱ ℛ"
proof -
from assms(2) obtain l r γ where mid: "s = l ⋅ γ" "t = r ⋅ γ" "(l, r) ∈ ℛ"
by (auto simp: sig_step_def)
from mid(3) assms(1) have vs: "x ∈ vars_term l ⟹ x ∉ vars_term r" for x
by (auto simp: lv_def)
let ?σ = "λ x. if x ∈ vars_term l then (γ x) ⋅ σ else (γ x) ⋅ τ"
have subst: "s ⋅ σ = l ⋅ ?σ" "t ⋅ τ = r ⋅ ?σ"
unfolding mid subst_subst_compose[symmetric]
unfolding term_subst_eq_conv
by (auto simp: subst_compose_def vs)
then show ?thesis unfolding subst
using assms(2) mid(3) well unfolding mid(1, 2)
by (auto simp: sig_step_def funas_term_subst)
qed
lemma lv_srsteps_with_root_step_idep_subst:
assumes "lv ℛ"
and "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
and well: "⋀ x. funas_term (σ x) ⊆ ℱ" "⋀ x. funas_term (τ x) ⊆ ℱ"
shows "(s ⋅ σ, t ⋅ τ) ∈ srsteps_with_root_step ℱ ℛ" using assms(2)
using lv_root_step_idep_subst[OF assms(1) _ well, where ?x1 = id and ?x2 = id]
using srsteps_eq_subst_closed[OF _ well(1), where ?x1 = id and ?ℛ = ℛ]
using srsteps_eq_subst_closed[OF _ well(2), where ?x1 = id and ?ℛ = ℛ]
by (auto simp: srsteps_with_root_step_def) (metis (full_types) relcomp3_I)
end