Theory Ground_Reduction_on_LV
section ‹Reducing Rewrite Properties to Properties on Ground Terms over Linear Variable-Separated Systems›
theory Ground_Reduction_on_LV
imports
Rewriting_Properties
Rewriting_LLRG_LV_Mondaic
begin
lemma lv_linear_sys: "lv ℛ ⟹ linear_sys ℛ"
by (auto simp: lv_def)
lemma comp_rrstep_rel'_sig_mono:
"ℱ ⊆ 𝒢 ⟹ comp_rrstep_rel' ℱ ℛ 𝒮 ⊆ comp_rrstep_rel' 𝒢 ℛ 𝒮"
by (meson Un_mono relcomp_mono srsteps_monp srsteps_with_root_step_sig_mono)
lemma srsteps_eqD: "(s, t) ∈ (srstep ℱ ℛ)⇧* ⟹ (s, t) ∈ (rstep ℛ)⇧*"
by (metis rtrancl_eq_or_trancl srstepsD)
section ‹Linear-variable separated results›
locale open_terms_two_const_lv =
fixes ℛ :: "('f, 'v) term rel" and ℱ c d
assumes lv: "lv ℛ" and sig: "funas_rel ℛ ⊆ ℱ"
and fresh: "(c, 0) ∉ ℱ" "(d, 0) ∉ ℱ"
and diff: "c ≠ d"
begin
abbreviation "ℋ ≡ insert (c, 0) (insert (d,0) ℱ)"
abbreviation "σ⇩c ≡ const_subst c"
abbreviation "σ⇩d ≡ const_subst d"
lemma sig_mono: "ℱ ⊆ ℋ" by auto
lemma fresh_sym_c: "(c, 0) ∉ funas_rel ℛ" using sig fresh
by (auto simp: funas_rel_def)
lemma fresh_sym_d: "(d, 0) ∉ funas_rel ℛ" using sig fresh
by (auto simp: funas_rel_def)
lemma fresh_sym_c_inv: "(c, 0) ∉ funas_rel (ℛ¯)" using sig fresh
by (auto simp: funas_rel_def)
lemma fresh_sym_d_inv: "(d, 0) ∉ funas_rel (ℛ¯)" using sig fresh
by (auto simp: funas_rel_def)
lemmas all_fresh = fresh_sym_c fresh_sym_d fresh_sym_c_inv fresh_sym_d_inv
lemma sig_inv: "funas_rel (ℛ¯) ⊆ ℱ" using sig unfolding funas_rel_def by auto
lemma lv_inv: "lv (ℛ¯)" using lv unfolding lv_def by auto
lemma well_subst:
"⋀x. funas_term ((const_subst c) x) ⊆ ℋ"
"⋀x. funas_term ((const_subst d) x) ⊆ ℋ"
by auto
lemma srsteps_with_root_step_to_grsteps:
assumes "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
shows "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧*"
proof -
from assms have lift: "(s, t) ∈ srsteps_with_root_step ℋ ℛ"
using srsteps_with_root_step_sig_mono[OF sig_mono]
by blast
note [dest!] = lv_srsteps_with_root_step_idep_subst[OF lv _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (srstep ℋ ℛ)⇧*" using lift
using srsteps_eq_subst_closed[OF _ well_subst(1)]
using srsteps_eq_subst_closed[OF _ well_subst(2)]
by (auto dest: trancl_into_rtrancl)
then show ?thesis
by (intro ground_srsteps_eq_gsrsteps_eq) auto
qed
lemma comp_rrstep_rel'_to_grsteps:
assumes "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
shows "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ ℛ)⇧*"
proof -
from assms have lift: "(s, t) ∈ comp_rrstep_rel' ℋ (ℛ¯) ℛ" using sig_mono
by (meson in_mono relcomp_mono srsteps_monp srsteps_with_root_step_sig_mono sup_mono)
note [dest!] = lv_srsteps_with_root_step_idep_subst[OF lv _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
note [dest!] = lv_srsteps_with_root_step_idep_subst[OF lv_inv _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (srstep ℋ (ℛ¯))⇧* O (srstep ℋ ℛ)⇧*" using lift
using srsteps_eq_subst_closed[OF _ well_subst(1)]
using srsteps_eq_subst_closed[OF _ well_subst(2)]
by (auto dest!: trancl_into_rtrancl) blast
then show ?thesis
by (intro srsteps_eq_relcomp_gsrsteps_relcomp) auto
qed
lemma gsrsteps_eq_to_srsteps:
assumes "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧*"
and funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
shows "(s, t) ∈ (srstep ℱ ℛ)⇧*"
proof -
from funas have d: "(d, 0) ∉ funas_term s" and c: "(c, 0) ∉ funas_term (t ⋅ σ⇩d)"
using fresh diff by (auto simp: funas_term_subst)
have "(s, t) ∈ (rstep ℛ)⇧*" using c gsrsteps_eq_to_rsteps_eq[OF assms(1)]
using remove_const_subst_steps_eq_lhs[OF lv_linear_sys[OF lv] fresh_sym_c,
THEN remove_const_subst_steps_eq_rhs[OF lv_linear_sys[OF lv] fresh_sym_d d]]
by auto
then show ?thesis using funas sig by blast
qed
lemma convert_NF_to_GNF:
"funas_term t ⊆ ℱ ⟹ t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ σ⇩c ∈ NF (gsrstep ℋ ℛ)"
"funas_term t ⊆ ℱ ⟹ t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ)"
using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv] fresh_sym_c sig]
using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv] fresh_sym_d sig]
by blast+
lemma convert_GNF_to_NF:
"funas_term t ⊆ ℱ ⟹ t ⋅ σ⇩c ∈ NF (gsrstep ℋ ℛ) ⟹ t ∈ NF (srstep ℱ ℛ)"
"funas_term t ⊆ ℱ ⟹ t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ) ⟹ t ∈ NF (srstep ℱ ℛ)"
using fresh_const_subst_NF_pres[OF fresh_sym_c sig]
using fresh_const_subst_NF_pres[OF fresh_sym_d sig]
using sig_mono by blast+
lemma lv_CR:
assumes cr: "CR (gsrstep ℋ ℛ)"
shows "CR (srstep ℱ ℛ)"
proof -
{fix s t assume ass: "(s, t) ∈ (srstep ℱ (ℛ¯))⇧+ O srsteps_with_root_step ℱ ℛ"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Pair_inject ass relcompE srstepsD srsteps_with_root_step_srstepsD)+
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ ℛ)⇧*"
using ass comp_rrstep_rel'_to_grsteps by auto
then have s: "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧* O (gsrstep ℋ (ℛ¯))⇧*"
using cr unfolding CR_on_def
by (auto simp: join_def rew_converse_outwards)
from gsrsteps_eq_relcomp_to_rsteps_relcomp[OF this]
have "commute_redp ℱ ℛ ℛ s t" unfolding commute_redp_def using funas fresh
using remove_const_subst_relcomp[OF lv_linear_sys[OF lv] lv_linear_sys[OF lv_inv]
all_fresh diff, THEN rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig sig_inv funas]]
by (metis srstep_converse_dist subsetD)}
then show ?thesis by (intro CR_rrstep_intro) simp
qed
lemma lv_WCR:
assumes wcr: "WCR (gsrstep ℋ ℛ)"
shows "WCR (srstep ℱ ℛ)"
proof -
note sig_trans_root = subsetD[OF srrstep_monp[OF sig_mono]]
note sig_trans = subsetD[OF srstep_monp[OF sig_mono]]
{fix s t u assume ass: "(s, t) ∈ sig_step ℱ (rrstep ℛ)" "(s, u) ∈ srstep ℱ ℛ"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ" by blast+
then have free: "(d, 0) ∉ funas_term u" "(c, 0) ∉ funas_term t" using fresh by blast+
have *: "ground (s ⋅ σ⇩c)" "ground (t ⋅ σ⇩d)" "ground (u ⋅ σ⇩c)" by auto
moreover have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ srstep ℋ ℛ" using lv sig_trans_root[OF ass(1)]
by (intro lv_root_step_idep_subst[THEN srrstep_to_srestep]) auto
moreover have "(s ⋅ σ⇩c, u ⋅ σ⇩c) ∈ srstep ℋ ℛ"
using srstep_subst_closed[OF sig_trans[OF ass(2)], of σ⇩c]
by auto
ultimately have w: "(t ⋅ σ⇩d, u ⋅ σ⇩c) ∈ (gsrstep ℋ ℛ)⇧↓" using wcr unfolding WCR_on_def
by auto (metis (no_types, lifting) * )
note join_unfolded = w[unfolded join_def rew_converse_inwards]
have "(t, u) ∈ (srstep ℱ ℛ)⇧↓" unfolding join_def
using remove_const_subst_relcomp[OF lv_linear_sys[OF lv] lv_linear_sys[OF lv_inv]
fresh_sym_d fresh_sym_c fresh_sym_d_inv fresh_sym_c_inv diff[symmetric] free
gsrsteps_eq_relcomp_to_rsteps_relcomp[OF join_unfolded],
THEN rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig sig_inv funas(2-)]]
by (metis (no_types, lifting) srstep_converse_dist)}
then show ?thesis by (intro WCR_rrstep_intro) simp
qed
lemma lv_NFP:
assumes nfp: "NFP (gsrstep ℋ ℛ)"
shows "NFP (srstep ℱ ℛ)"
proof -
{fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Un_iff ass relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
from comp_rrstep_rel'_to_grsteps[OF ass]
have " (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ ℛ)⇧*" by simp
then have "t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ) ⟹ (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧*" using NFP_stepD[OF nfp]
by (auto simp: rew_converse_outwards)
from gsrsteps_eq_to_srsteps[OF this funas]
have "NFP_redp ℱ ℛ s t" unfolding NFP_redp_def
using convert_NF_to_GNF(2)[OF funas(2)]
by simp}
then show ?thesis by (intro NFP_rrstep_intro) simp
qed
lemma lv_UNF:
assumes unf: "UNF (gsrstep ℋ ℛ)"
shows "UNF (srstep ℱ ℛ)"
proof -
{fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Un_iff ass relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
from comp_rrstep_rel'_to_grsteps[OF ass]
have " (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ ℛ)⇧*" by simp
then have "s ⋅ σ⇩c ∈ NF (gsrstep ℋ ℛ) ⟹ t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ) ⟹ s ⋅ σ⇩c = t ⋅ σ⇩d"
using unf unfolding UNF_on_def
by (auto simp: normalizability_def rew_converse_outwards)
then have "UN_redp ℱ ℛ s t" unfolding UN_redp_def
using convert_NF_to_GNF(1)[OF funas(1)]
using convert_NF_to_GNF(2)[OF funas(2)]
by (metis NF_not_suc funas gsrsteps_eq_to_srsteps rtrancl_eq_or_trancl)}
then show ?thesis by (intro UNF_rrstep_intro) simp
qed
lemma lv_UNC:
assumes unc: "UNC (gsrstep ℋ ℛ)"
shows "UNC (srstep ℱ ℛ)"
proof -
have lv_conv: "lv (ℛ⇧↔)" using lv by (auto simp: lv_def)
{fix s t assume ass: "(s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔)"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Un_iff ass relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧↔⇧*"
using lv_srsteps_with_root_step_idep_subst[OF lv_conv srsteps_with_root_step_sig_mono[OF sig_mono, THEN subsetD, OF ass]
well_subst,THEN srsteps_with_root_step_sresteps_eqD]
unfolding conversion_def Restr_smycl_dist srstep_symcl_dist
by (intro ground_srsteps_eq_gsrsteps_eq) auto
then have "s ⋅ σ⇩c ∈ NF (gsrstep ℋ ℛ) ⟹ t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ) ⟹ s ⋅ σ⇩c = t ⋅ σ⇩d"
using unc unfolding UNC_def
by (auto simp: normalizability_def sig_step_converse_rstep rtrancl_converse Restr_converse)
then have "UN_redp ℱ ℛ s t" unfolding UN_redp_def
using convert_NF_to_GNF(1)[OF funas(1)]
using convert_NF_to_GNF(2)[OF funas(2)]
by (metis NF_not_suc funas gsrsteps_eq_to_srsteps rtrancl_eq_or_trancl)}
then show ?thesis by (intro UNC_rrstep_intro) simp
qed
lemma lv_SCR:
assumes scr: "SCR (gsrstep ℋ ℛ)"
shows "SCR (srstep ℱ ℛ)"
proof -
note sig_trans_root = subsetD[OF srrstep_monp[OF sig_mono]]
note sig_trans = subsetD[OF srstep_monp[OF sig_mono]]
note cl_on_c = lin_fresh_rstep_const_replace_closed[OF lv_linear_sys[OF lv] fresh_sym_c]
lin_fresh_rstep_const_replace_closed[OF lv_linear_sys[OF lv_inv] fresh_sym_c_inv]
note cl_on_d = lin_fresh_rstep_const_replace_closed[OF lv_linear_sys[OF lv] fresh_sym_d]
lin_fresh_rstep_const_replace_closed[OF lv_linear_sys[OF lv_inv] fresh_sym_d_inv]
{fix s t u assume ass: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
and root: "(s, t) ∈ sig_step ℱ (rrstep ℛ) ∨ (s, u) ∈ sig_step ℱ (rrstep ℛ)"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
by (force dest: sig_stepE)+
then have fresh_c_t:"(c, 0) ∉ funas_term (t ⋅ σ⇩d)" and fresh_d_u:"(d, 0) ∉ funas_term u" using fresh diff
by (auto simp: funas_term_subst)
have *: "(s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ gsrstep ℋ ℛ ∧ (s ⋅ σ⇩c, u ⋅ σ⇩c) ∈ gsrstep ℋ ℛ"
"(s, u) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s ⋅ σ⇩d, t ⋅ σ⇩d) ∈ gsrstep ℋ ℛ ∧ (s ⋅ σ⇩d, u ⋅ σ⇩c) ∈ gsrstep ℋ ℛ"
using srstep_subst_closed[OF sig_trans[OF ass(2)] well_subst(1)]
using srstep_subst_closed[OF sig_trans[OF ass(2)] well_subst(2)]
using lv_root_step_idep_subst[OF lv] sig_trans_root[of "(s, t)" ℛ] sig_trans_root[of "(s, u)" ℛ]
by (simp_all add: ass(1) sig_trans srstep_subst_closed srrstep_to_srestep)
from this scr have "(u ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧* O ((gsrstep ℋ ℛ)⇧=)¯"
using root unfolding SCR_on_def by (meson UNIV_I converse_iff relcomp.simps)
then have v: "(u ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (srstep ℋ ℛ)⇧* O ((srstep ℋ ℛ)⇧=)¯"
by (auto dest: gsrsteps_eq_to_srsteps_eq)
have [simp]: "funas_term v ⊆ ℱ ⟹ term_to_sig ℱ x v = v" for x v
by (simp add: subset_insertI2)
have "(u, t) ∈ (srstep ℱ ℛ)⇧* O ((srstep ℱ ℛ)⇧=)¯"
proof -
from v have "(u, t ⋅ σ⇩d) ∈ (rstep ℛ)⇧* O (rstep (ℛ¯))⇧="
using const_replace_closed_relcomp[THEN const_replace_closed_remove_subst_lhs, OF
const_replace_closed_rtrancl[OF cl_on_c(1)]
const_replace_closed_symcl[OF cl_on_c(2)] fresh_c_t, of u]
by (auto simp: relcomp.relcompI srstepD simp flip: rstep_converse_dist dest: srsteps_eqD)
then have "(u, t) ∈ (rstep ℛ)⇧* O (rstep (ℛ¯))⇧="
using const_replace_closed_relcomp[THEN const_replace_closed_remove_subst_lhs, OF
const_replace_closed_symcl[OF cl_on_d(1)]
const_replace_closed_rtrancl[OF cl_on_d(2)] fresh_d_u, of t]
using converse_relcomp[where ?s = "(rstep (ℛ¯))⇧=" and ?r = "(rstep ℛ)⇧*"]
by (metis (no_types, lifting) converseD converse_Id converse_Un converse_converse rstep_converse_dist rtrancl_converse)
then obtain v where "(u, v) ∈ (rstep ℛ)⇧*" "(v, t) ∈ (rstep (ℛ¯))⇧=" by auto
then have "(u, term_to_sig ℱ x v) ∈ (srstep ℱ ℛ)⇧*" "(term_to_sig ℱ x v, t) ∈ (srstep ℱ (ℛ¯))⇧="
using funas(2, 3) sig fresh
by (auto simp: rtrancl_eq_or_trancl rstep_trancl_sig_step_r subset_insertI2
rew_converse_outwards dest: fuans_term_term_to_sig[THEN subsetD]
intro!: rstep_term_to_sig_r rstep_srstepI rsteps_eq_srsteps_eqI)
then show ?thesis
by (metis converse_Id converse_Un relcomp.relcompI srstep_converse_dist)
qed
then have "SCRp ℱ ℛ t u"
by auto}
then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+
qed
end
locale open_terms_two_const_lv_two_sys =
open_terms_two_const_lv ℛ
for ℛ :: "('f, 'v) term rel" +
fixes 𝒮 :: "('f, 'v) term rel"
assumes lv_S: "lv 𝒮" and sig_S: "funas_rel 𝒮 ⊆ ℱ"
begin
lemma fresh_sym_c_S: "(c, 0) ∉ funas_rel 𝒮" using sig_S fresh
by (auto simp: funas_rel_def)
lemma fresh_sym_d_S: "(d, 0) ∉ funas_rel 𝒮" using sig_S fresh
by (auto simp: funas_rel_def)
lemma lv_commute:
assumes com: "commute (gsrstep ℋ ℛ) (gsrstep ℋ 𝒮)"
shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
have linear: "linear_sys 𝒮" "linear_sys (ℛ¯)" using lv lv_S unfolding lv_def by auto
{fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮"
from ass have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Un_iff ass relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ (ℛ¯))⇧* O (gsrstep ℋ 𝒮)⇧*"
using comp_rrstep_rel'_sig_mono[OF sig_mono, THEN subsetD, OF ass]
using srsteps_eq_subst_closed[OF _ well_subst(1)] srsteps_eq_subst_closed[OF _ well_subst(2)]
by (auto simp: rew_converse_inwards dest!: trancl_into_rtrancl
lv_srsteps_with_root_step_idep_subst[OF lv_inv _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
lv_srsteps_with_root_step_idep_subst[OF lv_S _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
intro!: srsteps_eq_relcomp_gsrsteps_relcomp) blast
then have w: "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ 𝒮)⇧* O (gsrstep ℋ (ℛ¯))⇧*" using com
unfolding commute_def Restr_converse srstep_converse_dist
by blast
have "(s, t) ∈ (srstep ℱ 𝒮)⇧* O (srstep ℱ (ℛ¯))⇧*" using funas sig_S sig_inv fresh
using remove_const_subst_relcomp[OF linear fresh_sym_c_S fresh_sym_d_S fresh_sym_c_inv fresh_sym_d_inv diff _ _
gsrsteps_eq_relcomp_to_rsteps_relcomp[OF w]]
by (intro rsteps_eq_relcomp_srsteps_eq_relcompI) auto
then have "commute_redp ℱ ℛ 𝒮 s t" unfolding commute_redp_def
by (simp add: rew_converse_inwards)}
then show ?thesis by (intro commute_rrstep_intro) simp
qed
lemma lv_NE:
assumes ne: "NE (gsrstep ℋ ℛ) (gsrstep ℋ 𝒮)"
shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
from NE_NF_eq[OF ne] have ne_eq: "NF (srstep ℱ ℛ) = NF (srstep ℱ 𝒮)"
using lv lv_S sig sig_S fresh_sym_c fresh_sym_c_S
by (intro linear_sys_gNF_eq_NF_eq) (auto dest: lv_linear_sys)
{fix s t assume step: "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
then have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis Un_iff step relcompEpair srstepsD srsteps_with_root_step_srstepsD)+
then have fresh: "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s" using fresh by auto
from srsteps_with_root_step_sig_mono[OF sig_mono, THEN subsetD, OF step]
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧*"
using lv_srsteps_with_root_step_idep_subst[OF lv _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
by (intro ground_srsteps_eq_gsrsteps_eq) auto
then have "t ⋅ σ⇩d ∈ NF (gsrstep ℋ 𝒮) ⟹ (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ 𝒮)⇧*"
using ne NE_NF_eq[OF ne] unfolding NE_on_def
by (auto simp: normalizability_def)
from this[THEN gsrsteps_eq_to_rsteps_eq, THEN remove_const_subst_steps[OF lv_linear_sys[OF lv_S] fresh_sym_c_S fresh_sym_d_S diff fresh]]
have "NE_redp ℱ ℛ 𝒮 s t" using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv_S] fresh_sym_d_S sig_S funas(2)]
using funas sig_S unfolding NE_redp_def ne_eq
by (auto intro: rsteps_eq_srsteps_eqI)}
moreover
{fix s t assume step: "(s, t) ∈ srsteps_with_root_step ℱ 𝒮"
then have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (metis sig_S sig_stepE sig_step_rsteps_dist srsteps_with_root_step_srstepsD)+
then have fresh: "(c, 0) ∉ funas_term t" "(d, 0) ∉ funas_term s" using fresh by auto
from srsteps_with_root_step_sig_mono[OF sig_mono, THEN subsetD, OF step]
have "(s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ 𝒮)⇧*"
using lv_srsteps_with_root_step_idep_subst[OF lv_S _ well_subst, THEN srsteps_with_root_step_sresteps_eqD]
by (intro ground_srsteps_eq_gsrsteps_eq) auto
then have "t ⋅ σ⇩d ∈ NF (gsrstep ℋ ℛ) ⟹ (s ⋅ σ⇩c, t ⋅ σ⇩d) ∈ (gsrstep ℋ ℛ)⇧*"
using ne NE_NF_eq[OF ne] unfolding NE_on_def
by (auto simp: normalizability_def)
from this[THEN gsrsteps_eq_to_rsteps_eq, THEN remove_const_subst_steps[OF lv_linear_sys[OF lv] fresh_sym_c fresh_sym_d diff fresh]]
have "NE_redp ℱ 𝒮 ℛ s t" using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv] fresh_sym_d sig funas(2), of ℋ]
using funas sig unfolding NE_redp_def ne_eq
by (auto intro: rsteps_eq_srsteps_eqI)}
ultimately show ?thesis using ne_eq
by (intro NE_rrstep_intro) auto
qed
end
lemma lv_CE_aux:
assumes "(s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔)"
and sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and fresh: "(c, 0) ∉ ℱ" and const: "(a, 0) ∈ ℱ"
and lv: "lv ℛ" "lv 𝒮"
and ce: "CE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "(s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
proof -
let ?ℋ = "insert (c, 0) ℱ" have mono: "ℱ ⊆ ?ℋ" by auto
have lv_conv: "lv (ℛ⇧↔)" "lv (𝒮⇧↔)" using lv by (auto simp: lv_def)
have sig_conv: "funas_rel (𝒮⇧↔) ⊆ ℱ" using sig(2) by (auto simp: funas_rel_def)
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮" "(c, 0) ∉ funas_rel (𝒮⇧↔)"
using sig by (auto simp: funas_rel_def)
from assms(1) have lift: "(s, t) ∈ srsteps_with_root_step ?ℋ (ℛ⇧↔)"
unfolding srsteps_with_root_step_def
by (meson in_mono mono relcomp_mono rtrancl_mono srrstep_monp srstep_monp)
from assms(1) have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (meson srstepsD srsteps_with_root_step_srstepsD)+
from srsteps_with_root_step_sresteps_eqD[OF assms(1), THEN subsetD[OF srsteps_eq_monp[OF mono]]]
have "(s ⋅ const_subst c, t ⋅ const_subst c) ∈ (srstep ?ℋ ℛ)⇧↔⇧*"
by (auto simp: sig_step_conversion_dist intro: srsteps_eq_subst_closed)
moreover have "(s ⋅ const_subst c, t ⋅ const_subst a) ∈ (srstep ?ℋ ℛ)⇧↔⇧*"
unfolding sig_step_conversion_dist using const
by (intro lv_srsteps_with_root_step_idep_subst[OF lv_conv(1) lift, THEN srsteps_with_root_step_sresteps_eqD]) auto
moreover have "ground (s ⋅ const_subst c)" "ground (t ⋅ const_subst a)" "ground (t ⋅ const_subst a)"
by auto
ultimately have toS:"(s ⋅ const_subst c, t ⋅ const_subst c) ∈ (gsrstep ?ℋ 𝒮)⇧↔⇧*"
"(s ⋅ const_subst c, t ⋅ const_subst a) ∈ (gsrstep ?ℋ 𝒮)⇧↔⇧*"
using ground_srsteps_eq_gsrsteps_eq[where ?ℱ = ?ℋ and ?ℛ = "ℛ⇧↔"]
using ce unfolding CE_on_def
by (auto simp: Restr_smycl_dist conversion_def srstep_symcl_dist)
then have *: "(t ⋅ const_subst a, t ⋅ const_subst c) ∈ (gsrstep ?ℋ 𝒮)⇧↔⇧*"
by (metis (no_types, lifting) conversion_inv conversion_rtrancl rtrancl.rtrancl_into_rtrancl)
have "(t ⋅ const_subst a, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*" using const
using funas(2) fresh
using remove_const_subst_steps_eq_rhs[OF lv_linear_sys[OF lv_conv(2)] fresh_sys(3) _
gsrsteps_eq_to_rsteps_eq[OF *[unfolded gsrstep_conversion_dist]]]
by (cases "vars_term t = {}")
(auto simp: funas_term_subst sig_step_conversion_dist split: if_splits intro!: rsteps_eq_srsteps_eqI[OF sig_conv])
moreover have "(s, t ⋅ const_subst a) ∈ (srstep ℱ 𝒮)⇧↔⇧*" using const
using funas fresh
using remove_const_subst_steps_eq_lhs[OF lv_linear_sys[OF lv_conv(2)] fresh_sys(3) _
gsrsteps_eq_to_rsteps_eq[OF toS(2)[unfolded gsrstep_conversion_dist]]]
by (cases "vars_term t = {}")
(auto simp: sig_step_conversion_dist funas_term_subst split: if_splits intro!: rsteps_eq_srsteps_eqI[OF sig_conv])
ultimately show "(s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
by (meson conversionE conversionI rtrancl_trans)
qed
lemma lv_CE:
assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and fresh: "(c, 0) ∉ ℱ" and const: "(a, 0) ∈ ℱ"
and lv: "lv ℛ" "lv 𝒮"
and ce: "CE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "CE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
{fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔)"
from lv_CE_aux[OF this assms] have "(s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*" by simp}
moreover
{fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ (𝒮⇧↔)"
from lv_CE_aux[OF this sig(2, 1) fresh const lv(2, 1) CE_symmetric[OF ce]]
have "(s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*" by simp}
ultimately show ?thesis
by (intro CE_rrstep_intro) auto
qed
subsection ‹Specialized for monadic signature›
lemma lv_NE_aux:
assumes "(s, t) ∈ srsteps_with_root_step ℱ ℛ" and fresh: "(c, 0) ∉ ℱ"
and sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and lv: "lv ℛ" "lv 𝒮"
and mon: "monadic ℱ"
and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "NE_redp ℱ ℛ 𝒮 s t"
proof -
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
have mono: "ℱ ⊆ ?ℋ" by auto
from mon have mh: "monadic ?ℋ" by (auto simp: monadic_def)
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮" using sig
by (auto simp: funas_rel_def)
from assms have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
by (meson srstepsD srsteps_with_root_step_srstepsD)+
from funas have fresh_t: "(c, 0) ∉ funas_term t" using fresh by auto
from srsteps_subst_closed[OF srsteps_monp[OF mono, THEN subsetD, OF srsteps_with_root_step_srstepsD[OF assms(1)]], of ?σ]
have gstep: "(s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep (insert (c, 0) ℱ) ℛ)⇧+"
by (auto simp: ground_subst_apply intro!: ground_srsteps_gsrsteps)
then have neq: "t ∈ NF (srstep ℱ ℛ) ⟹ s ⋅ ?σ ≠ t ⋅ ?σ"
using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv(1)] fresh_sys(1) sig(1) funas(2), of ?ℋ]
by (metis NF_no_trancl_step)
then have "t ∈ NF (srstep ℱ ℛ) ⟹ (s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep (insert (c, 0) ℱ) 𝒮)⇧+" using gstep
using NF_to_fresh_const_subst_NF[OF lv_linear_sys[OF lv(1)] fresh_sys(1) sig(1) funas(2), of ?ℋ]
using NE_NF_eq[OF ne, symmetric] ne unfolding NE_on_def
by (auto simp: normalizability_def ground_subst_apply) (meson rtrancl_eq_or_trancl)
then show ?thesis unfolding NE_redp_def
using remove_const_lv_mondaic_steps[OF lv(2) fresh_sys(2) mh, THEN srstepsD[THEN conjunct1],
THEN rsteps_srstepsI[OF sig(2) funas]]
by (auto dest!: gsrsteps_to_srsteps)
qed
lemma lv_NE:
assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and mon: "monadic ℱ" and fresh: "(c, 0) ∉ ℱ"
and lv: "lv ℛ" "lv 𝒮"
and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮"
using sig by (auto simp: funas_rel_def)
from NE_NF_eq[OF ne] have ne_eq: "NF (srstep ℱ ℛ) = NF (srstep ℱ 𝒮)" using lv sig fresh_sys
by (intro linear_sys_gNF_eq_NF_eq) (auto dest: lv_linear_sys)
{fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
from lv_NE_aux[OF this fresh sig lv mon ne] have "NE_redp ℱ ℛ 𝒮 s t" by simp}
moreover
{fix s t assume ass: "(s, t) ∈ srsteps_with_root_step ℱ 𝒮"
from lv_NE_aux[OF this fresh sig(2, 1) lv(2, 1) mon NE_symmetric[OF ne]] have "NE_redp ℱ 𝒮 ℛ s t" by simp}
ultimately show ?thesis using ne_eq
by (intro NE_rrstep_intro) auto
qed
end