Theory Ground_Reduction_on_LLRG
section ‹Reducing Rewrite Properties to Properties on Ground Terms over Left-Linear Right-Ground Systems›
theory Ground_Reduction_on_LLRG
imports
Rewriting_Properties
Rewriting_LLRG_LV_Mondaic
begin
lemma llrg_linear_sys:
"llrg ℛ ⟹ linear_sys ℛ"
by (auto simp: llrg_def)
section ‹LLRG results›
lemma llrg_commute:
assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ"
and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ" "llrg 𝒮"
and com: "commute (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
let ?σ = "λ _. Fun c []" let ?ℋ = "insert (c, 0) ℱ"
from fresh have fresh_sys: "(c, 0) ∉ funas_rel 𝒮" "(c, 0) ∉ funas_rel (ℛ¯)" using sig
by (auto simp: funas_rel_def)
have linear: "linear_sys 𝒮" "linear_sys (ℛ¯)" using llrg unfolding llrg_def by auto
have sig': "funas_rel 𝒮 ⊆ ℱ" "funas_rel (ℛ¯) ⊆ ℱ" using sig by (auto simp: funas_rel_def)
have mono: "ℱ ⊆ ?ℋ" 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 relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ 𝒮)⇧*"
using rtrancl_mono[OF sig_step_mono[OF mono]]
by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
have gr: "ground s ∨ ground t" using ass llrg
unfolding srstep_converse_dist trancl_converse
by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
have gstep: "(s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep ?ℋ 𝒮)⇧* O (gsrstep ?ℋ (ℛ¯))⇧*"
using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ,
THEN subsetD[OF com[unfolded commute_def], unfolded rew_converse_inwards]]
by (auto simp: ground_substI)
have [simp]: "ground s ⟹ (c, 0) ∉ funas_term s" "ground t ⟹ (c, 0) ∉ funas_term t"
using funas fresh by auto
have "(s, t) ∈ (rstep 𝒮)⇧* O (rstep (ℛ¯))⇧*"
using remove_const_subst_relcomp_lhs[OF linear fresh_sys, of t s]
using gsrsteps_eq_relcomp_to_rsteps_relcomp[OF gstep] gr
using remove_const_subst_relcomp_lhs[OF linear fresh_sys, of t s]
using remove_const_subst_relcomp_rhs[OF linear fresh_sys, of s t]
by (cases "ground s") (simp_all add: ground_subst_apply)
from rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig' funas this]
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 llrg_CR:
assumes sig: "funas_rel ℛ ⊆ ℱ"
and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ"
and com: "CR (gsrstep (insert (c, 0) ℱ) ℛ)"
shows "CR (srstep ℱ ℛ)"
using assms llrg_commute unfolding CR_iff_self_commute
by metis
lemma llrg_SCR:
assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ"
and scr: "SCR (gsrstep (insert (c, 0) ℱ) ℛ)"
shows "SCR (srstep ℱ ℛ)"
proof -
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" using sig
by (auto simp: funas_rel_def)
have mono: "ℱ ⊆ ?ℋ" by auto note sig_trans = subsetD[OF srstep_monp[OF mono]]
{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)+
from root have gr: "ground t ∨ ground u" using ass llrg llrg_rrsteps_groundness
unfolding srstep_converse_dist trancl_converse by blast
have *: "ground (s ⋅ ?σ)" "ground (t ⋅ ?σ)" "ground (u ⋅ ?σ)" by auto
from this scr obtain v where v: "(t ⋅ ?σ, v) ∈ (gsrstep ?ℋ ℛ)⇧= ∧ (u ⋅ ?σ, v) ∈ (gsrstep ?ℋ ℛ)⇧*"
using srstep_subst_closed[OF sig_trans[OF ass(1)], of ?σ]
using srstep_subst_closed[OF sig_trans[OF ass(2)], of ?σ]
using ass unfolding SCR_on_def
by auto (metis (no_types, lifting) * )
then have fv: "funas_term v ⊆ ℱ" using gr llrg_funas_term_step_pres[OF llrg, of _ v]
using llrg_funas_term_steps_pres[OF llrg, of _ v] funas sig
by (auto simp: ground_subst_apply elim!: sig_stepE dest!: gsrsteps_eq_to_rsteps_eq) blast+
then have c_free: "(c, 0) ∉ funas_term v" using fresh by blast
then have "v = t ⋅ const_subst c ⟹ ground t" using arg_cong[of v "t ⋅ ?σ" funas_term]
by (auto simp: funas_term_subst vars_term_empty_ground split: if_splits)
from this v have "(t, v) ∈ (srstep ℱ ℛ)⇧=" "(u, v) ∈ (srstep ℱ ℛ)⇧*"
using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg] fresh_sys c_free, of u,
THEN rsteps_eq_srsteps_eqI[OF sig funas(3) fv]]
using remove_const_subst_step_lhs[OF llrg_linear_sys[OF llrg] fresh_sys c_free, of t,
THEN sig_stepI[OF funas(2) fv]]
by (auto simp: ground_subst_apply dest: srstepD gsrsteps_eq_to_rsteps_eq)
then have "SCRp ℱ ℛ t u" by blast}
then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+
qed
lemma llrg_WCR:
assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ"
and wcr: "WCR (gsrstep (insert (c, 0) ℱ) ℛ)"
shows "WCR (srstep ℱ ℛ)"
proof -
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel (ℛ¯)" using sig
by (auto simp: funas_rel_def)
have lin: "linear_sys ℛ" "linear_sys (ℛ¯)" using llrg unfolding llrg_def by auto
have mono: "ℱ ⊆ ?ℋ" by auto note sig_trans = subsetD[OF srstep_monp[OF 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 c_free: "(c, 0) ∉ funas_term t" using fresh by blast
from ass have gr: "ground t" using ass llrg llrg_rrsteps_groundness by blast
have *: "ground (s ⋅ ?σ)" "ground (u ⋅ ?σ)" by auto
from this wcr have w: "(t, u ⋅ ?σ) ∈ (gsrstep ?ℋ ℛ)⇧↓"
using srstep_subst_closed[OF sig_trans[OF srrstep_to_srestep[OF ass(1)]], of ?σ]
using srstep_subst_closed[OF sig_trans[OF ass(2)], of ?σ]
using ass unfolding WCR_on_def
by auto (metis * gr ground_subst_apply)
have "(t, u) ∈ (srstep ℱ ℛ)⇧↓" unfolding join_def
using remove_const_subst_relcomp_rhs[OF lin fresh_sys c_free
gsrsteps_eq_relcomp_to_rsteps_relcomp[OF w[unfolded join_def rew_converse_inwards]],
THEN rsteps_eq_relcomp_srsteps_eq_relcompI[OF sig funas_rel_converse[OF sig] funas(2-)]]
by (metis (no_types, lifting) srstep_converse_dist)}
then show ?thesis by (intro WCR_rrstep_intro) simp
qed
lemma llrg_UNF:
assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ"
and unf: "UNF (gsrstep (insert (c, 0) ℱ) ℛ)"
shows "UNF (srstep ℱ ℛ)"
proof -
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" using sig
by (auto simp: funas_rel_def)
have mono: "ℱ ⊆ ?ℋ" 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 relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ ℛ)⇧*"
using rtrancl_mono[OF sig_step_mono[OF mono]]
by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
have gr: "ground s ∨ ground t" using ass llrg
unfolding srstep_converse_dist trancl_converse
by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
have wit: "s ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ s ⋅ ?σ = t ⋅ ?σ" using unf
using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ]
by (auto simp: UNF_on_def rew_converse_outwards normalizability_def)
from funas NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg] fresh_sys sig(1)]
have "s ∈ NF (srstep ℱ ℛ) ⟹ s ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)" "t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)"
by auto
moreover have "s ⋅ ?σ = t ⋅ ?σ ⟹ s = t" using gr funas fresh
by (cases "ground s") (auto simp: ground_subst_apply funas_term_subst vars_term_empty_ground split: if_splits)
ultimately have "UN_redp ℱ ℛ s t" using wit unfolding UN_redp_def
by auto}
then show ?thesis by (intro UNF_rrstep_intro) simp
qed
lemma llrg_NFP:
assumes sig: "funas_rel ℛ ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ"
and nfp: "NFP (gsrstep (insert (c, 0) ℱ) ℛ)"
shows "NFP (srstep ℱ ℛ)"
proof -
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ"
using sig by (auto simp: funas_rel_def)
have mono: "ℱ ⊆ ?ℋ" 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 relcomp.cases srstepsD srsteps_with_root_step_srstepsD)+
from ass have m: "(s, t) ∈ (srstep ?ℋ (ℛ¯))⇧* O (srstep ?ℋ ℛ)⇧*"
using rtrancl_mono[OF sig_step_mono[OF mono]]
by (auto dest!: srsteps_with_root_step_sresteps_eqD trancl_into_rtrancl)
have gr: "ground s ∨ ground t" using ass llrg
unfolding srstep_converse_dist trancl_converse
by (auto simp: llrg_srsteps_with_root_step_inv_ground llrg_srsteps_with_root_step_ground)
have wit: "t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ) ⟹ (s ⋅ ?σ, t ⋅ ?σ) ∈ (gsrstep (insert (c, 0) ℱ) ℛ)⇧*"
using NFP_stepD[OF nfp]
using srsteps_eq_subst_relcomp_closed[OF m, THEN srsteps_eq_relcomp_gsrsteps_relcomp, of ?σ]
by (auto simp: rew_converse_outwards)
from funas NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg] fresh_sys(1) sig(1)]
have "t ∈ NF (srstep ℱ ℛ) ⟹ t ⋅ ?σ ∈ NF (gsrstep ?ℋ ℛ)" by auto
moreover have "(s ⋅ ?σ, t ⋅ ?σ) ∈ (rstep ℛ)⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*" using gr funas fresh
using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg] fresh_sys, THEN rsteps_eq_srsteps_eqI[OF sig funas]]
using remove_const_subst_steps_eq_rhs[OF llrg_linear_sys[OF llrg] fresh_sys, THEN rsteps_eq_srsteps_eqI[OF sig funas]]
by (cases "ground s") (auto simp: ground_subst_apply)
ultimately have "NFP_redp ℱ ℛ s t" using wit unfolding NFP_redp_def
by (auto dest: gsrsteps_eq_to_rsteps_eq)}
then show ?thesis by (intro NFP_rrstep_intro) simp
qed
lemma llrg_NE_aux:
assumes "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
and sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ" "llrg 𝒮"
and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "NE_redp ℱ ℛ 𝒮 s t"
proof -
from fresh have fresh_sys: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮"
using sig by (auto simp: funas_rel_def)
let ?σ = "const_subst c" let ?ℋ = "insert (c, 0) ℱ"
let ?ℋ = "insert (c, 0) ℱ" have mono: "ℱ ⊆ ?ℋ" by auto
from assms(1) have gr: "ground t" and funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
using llrg_srsteps_with_root_step_ground[OF llrg(1)]
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 "(s ⋅ ?σ, t) ∈ (gsrstep?ℋ ℛ)⇧+" using gr
by (auto simp: ground_subst_apply intro!: ground_srsteps_gsrsteps)
then have "t ∈ NF (srstep ℱ ℛ) ⟹ (s ⋅ ?σ, t) ∈ (gsrstep (insert (c, 0) ℱ) 𝒮)⇧*"
using NF_to_fresh_const_subst_NF[OF llrg_linear_sys[OF llrg(1)] fresh_sys(1) sig(1) funas(2), of ?ℋ]
using gr NE_NF_eq[OF ne, symmetric] ne unfolding NE_on_def
by (auto simp: normalizability_def ground_subst_apply dest!: trancl_into_rtrancl)
then show "NE_redp ℱ ℛ 𝒮 s t" unfolding NE_redp_def
using remove_const_subst_steps_eq_lhs[OF llrg_linear_sys[OF llrg(2)] fresh_sys(2) fresh_t,
THEN rsteps_eq_srsteps_eqI[OF sig(2) funas]]
by (auto dest: gsrsteps_eq_to_rsteps_eq)
qed
lemma llrg_NE:
assumes sig: "funas_rel ℛ ⊆ ℱ" "funas_rel 𝒮 ⊆ ℱ" and fresh: "(c, 0) ∉ ℱ"
and llrg: "llrg ℛ" "llrg 𝒮"
and ne: "NE (gsrstep (insert (c, 0) ℱ) ℛ) (gsrstep (insert (c, 0) ℱ) 𝒮)"
shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
have f: "(c, 0) ∉ funas_rel ℛ" "(c, 0) ∉ funas_rel 𝒮" using fresh sig
by (auto simp: funas_rel_def)
{fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ ℛ"
from llrg_NE_aux[OF this sig fresh llrg ne] have "NE_redp ℱ ℛ 𝒮 s t"
by simp}
moreover
{fix s t assume "(s, t) ∈ srsteps_with_root_step ℱ 𝒮"
from llrg_NE_aux[OF this sig(2, 1) fresh llrg(2, 1) NE_symmetric[OF ne]]
have "NE_redp ℱ 𝒮 ℛ s t" by simp}
ultimately show ?thesis using linear_sys_gNF_eq_NF_eq[OF llrg_linear_sys[OF llrg(1)]
llrg_linear_sys[OF llrg(2)] sig f _ _ NE_NF_eq[OF ne]]
by (intro NE_rrstep_intro) auto
qed
subsection ‹Specialized for monadic signature›
lemma monadic_commute:
assumes "llrg ℛ" "llrg 𝒮" "monadic ℱ"
and com: "commute (gsrstep ℱ ℛ) (gsrstep ℱ 𝒮)"
shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
{fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮"
then obtain u where steps: "(s, u) ∈ (srstep ℱ (ℛ¯))⇧+" "(u, t) ∈ (srstep ℱ 𝒮)⇧+"
by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
have gr: "ground s" "ground t" using steps assms(1 - 3)
unfolding rew_converse_outwards
by (auto simp: llrg_srsteps_with_root_step_ground llrg_monadic_rsteps_groundness)
from steps(1) have f: "funas_term s ⊆ ℱ" using srstepsD by blast
let ?σ = "λ _. s"
from steps gr have "(s, u ⋅ ?σ) ∈ (gsrstep ℱ (ℛ¯))⇧+" "(u ⋅ ?σ, t) ∈ (gsrstep ℱ 𝒮)⇧+"
unfolding rew_converse_outwards
using srsteps_subst_closed[where ?σ = ?σ and ?s = u, of _ ℱ] f
by (force simp: ground_subst_apply intro: ground_srsteps_gsrsteps)+
then have "(s, t) ∈ (gsrstep ℱ 𝒮)⇧* O (gsrstep ℱ (ℛ¯))⇧*" using com
unfolding commute_def rew_converse_inwards
by (meson relcomp.relcompI subsetD trancl_into_rtrancl)
from gsrsteps_eq_relcomp_srsteps_relcompD[OF this]
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 monadic_CR:
assumes "llrg ℛ" "monadic ℱ"
and "CR (gsrstep ℱ ℛ)"
shows "CR (srstep ℱ ℛ)" using monadic_commute assms
unfolding CR_iff_self_commute
by blast
lemma monadic_SCR:
assumes sig: "funas_rel ℛ ⊆ ℱ" "monadic ℱ"
and llrg: "llrg ℛ"
and scr: "SCR (gsrstep ℱ ℛ)"
shows "SCR (srstep ℱ ℛ)"
proof -
{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 blast+
from root have gr: "ground t" "ground u" using ass sig(2) llrg
by (metis llrg_monadic_rstep_pres_groundness)+
let ?σ = "λ _. t" have grs: "ground (s ⋅ ?σ)" using gr by auto
from this scr obtain v where v: "(t, v) ∈ (gsrstep ℱ ℛ)⇧= ∧ (u, v) ∈ (gsrstep ℱ ℛ)⇧*"
using srstep_subst_closed[OF ass(1), of ?σ]
using srstep_subst_closed[OF ass(2), of ?σ]
using gr unfolding SCR_on_def
by (metis Int_iff UNIV_I funas(2) ground_subst_apply mem_Collect_eq mem_Sigma_iff)
then have "SCRp ℱ ℛ t u"
by (metis Int_iff Un_iff gsrsteps_eq_to_srsteps_eq)}
then show ?thesis by (intro SCR_rrstep_intro) (metis srrstep_to_srestep)+
qed
lemma monadic_WCR:
assumes sig: "funas_rel ℛ ⊆ ℱ" "monadic ℱ"
and llrg: "llrg ℛ"
and wcr: "WCR (gsrstep ℱ ℛ)"
shows "WCR (srstep ℱ ℛ)"
proof -
{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+
from srrstep_to_srestep ass have gr: "ground t" "ground u"using ass sig(2) llrg
by (metis llrg_monadic_rstep_pres_groundness)+
let ?σ = "λ _. t" have grs: "ground (s ⋅ ?σ)" using gr by auto
from this wcr have w: "(t, u) ∈ (gsrstep ℱ ℛ)⇧↓" using gr ass(2) funas
using srstep_subst_closed[OF srrstep_to_srestep[OF ass(1)], of ?σ]
using srstep_subst_closed[OF ass(2), of ?σ]
unfolding WCR_on_def
by (metis IntI SigmaI UNIV_I ground_subst_apply mem_Collect_eq)
then have "(t, u) ∈ (srstep ℱ ℛ)⇧↓" unfolding join_def
by (metis gsrsteps_eq_to_srsteps_eq joinD joinI join_def)}
then show ?thesis by (intro WCR_rrstep_intro) simp
qed
lemma monadic_UNF:
assumes "llrg ℛ" "monadic ℱ"
and unf: "UNF (gsrstep ℱ ℛ)"
shows "UNF (srstep ℱ ℛ)"
proof -
{fix s t assume ass: "(s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ"
then obtain u where steps: "(s, u) ∈ (srstep ℱ (ℛ¯))⇧+" "(u, t) ∈ (srstep ℱ ℛ)⇧+"
by (auto simp: sig_step_converse_rstep dest: srsteps_with_root_step_srstepsD)
have gr: "ground s" "ground t" using steps assms(1, 2)
unfolding rew_converse_outwards
by (auto simp: llrg_srsteps_with_root_step_ground llrg_monadic_rsteps_groundness)
from steps(1) have f: "funas_term s ⊆ ℱ" using srstepsD by blast
let ?σ = "λ _. s"
from steps gr have "(s, u ⋅ ?σ) ∈ (gsrstep ℱ (ℛ¯))⇧+" "(u ⋅ ?σ, t) ∈ (gsrstep ℱ ℛ)⇧+"
unfolding rew_converse_outwards
using srsteps_subst_closed[where ?σ = ?σ and ?s = u, of _ ℱ] f
by (force simp: ground_subst_apply intro: ground_srsteps_gsrsteps)+
then have "UN_redp ℱ ℛ s t" using unf ground_NF_srstep_gsrstep[OF gr(1), of ℱ ℛ]
using ground_NF_srstep_gsrstep[OF gr(2), of ℱ ℛ]
by (auto simp: UNF_on_def UN_redp_def normalizability_def rew_converse_outwards)
(meson trancl_into_rtrancl)}
then show ?thesis by (intro UNF_rrstep_intro) simp
qed
lemma monadic_UNC:
assumes "llrg ℛ" "monadic ℱ"
and well: "funas_rel ℛ ⊆ ℱ"
and unc: "UNC (gsrstep ℱ ℛ)"
shows "UNC (srstep ℱ ℛ)"
proof -
{fix s t assume ass: "(s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*" "s ∈ NF (srstep ℱ ℛ)" "t ∈ NF (srstep ℱ ℛ)"
then have "s = t"
proof (cases "s = t")
case False
then have "∃ s' t'. (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧* ∧ (s', s) ∈ (srstep ℱ ℛ) ∧ (t', t) ∈ (srstep ℱ ℛ)"
using ass by (auto simp: conversion_def rtrancl_eq_or_trancl dest: tranclD tranclD2)
then obtain s' t' where split: "(s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*" "(s', s) ∈ (srstep ℱ ℛ)" "(t', t) ∈ (srstep ℱ ℛ)" by blast
from split(2, 3) have gr: "ground s" "ground t" using llrg_monadic_rstep_pres_groundness[OF assms(1, 2)]
by blast+
from ground_srsteps_eq_gsrsteps_eq[OF this ass(1)[unfolded sig_step_conversion_dist]]
have "(s, t) ∈ (gsrstep ℱ ℛ)⇧↔⇧*"
unfolding conversion_def Restr_smycl_dist
by (simp add: rstep_converse_dist srstep_symcl_dist)
then show ?thesis using ass(2-) unc gr
by (auto simp: UNC_def ground_NF_srstep_gsrstep)
qed auto}
then show ?thesis by (auto simp: UNC_def UN_redp_def)
qed
lemma monadic_NFP:
assumes "llrg ℛ" "monadic ℱ"
and nfp: "NFP (gsrstep ℱ ℛ)"
shows "NFP (srstep ℱ ℛ)"
proof -
{fix s t u assume ass: "(s, t) ∈ (srstep ℱ ℛ)⇧*" "(s, u) ∈ (srstep ℱ ℛ)⇧*" "u ∈ NF (srstep ℱ ℛ)"
have "(t, u) ∈ (srstep ℱ ℛ)⇧*"
proof (cases "s = u ∨ s = t")
case [simp]: True show ?thesis using ass
by (metis NF_not_suc True rtrancl.rtrancl_refl)
next
case False
then have steps:"(s, t) ∈ (srstep ℱ ℛ)⇧+" "(s, u) ∈ (srstep ℱ ℛ)⇧+" using ass(1, 2)
by (auto simp add: rtrancl_eq_or_trancl)
then have gr: "ground t" "ground u" using assms(1, 2) llrg_monadic_rsteps_groundness
by blast+
let ?σ = "λ _. t" from steps gr have "(s ⋅ ?σ, t) ∈ (gsrstep ℱ ℛ)⇧+" "(s ⋅ ?σ, u) ∈ (gsrstep ℱ ℛ)⇧+"
by (auto intro!: ground_srsteps_gsrsteps)
(metis ground_subst_apply srstepsD srsteps_subst_closed)+
then have "(t, u) ∈ (gsrstep ℱ ℛ)⇧*" using nfp ass(3) gr
by (auto simp: NFP_on_def) (metis ground_NF_srstep_gsrstep normalizability_I trancl_into_rtrancl)
then show ?thesis by (auto dest: gsrsteps_eq_to_srsteps_eq)
qed}
then show ?thesis unfolding NFP_on_def
by auto
qed
end