theory
Critical_Pair_Closing_Systems
imports
Parallel_Closed
begin
definition
"critical_pair_closing' C R = ((∀ (b, p, q) ∈ critical_pairs R R. (p, q) ∈ (rstep C)⇧↓) ∧
C ⊆ { (l ⋅ σ, r ⋅ σ) | σ l r. (l, r) ∈ R ∧ (∀ x. σ x ≠ Var x ⟶ (σ x) ∈ NF R ∧ ground (σ x))})"
definition
"critical_pair_closing C R = ((∀ (b, p, q) ∈ critical_pairs R R. (p, q) ∈ (rstep C)⇧↓) ∧ C ⊆ R)"
lemma cpcs_sn_cr:
assumes "critical_pair_closing S R"
and "SN (rstep S)"
shows "CR (rstep S)"
proof -
from assms have "∀ (b, p, q) ∈ critical_pairs S S. (p, q) ∈ (rstep S)⇧↓"
using critical_pairs_mono unfolding critical_pair_closing_def by blast
with critical_pair_lemma have "WCR (rstep S)" by auto
with Newman assms show ?thesis by auto
qed
lemma cpcs_sn:
assumes "critical_pair_closing S R"
and "SN (rstep S)"
and left_lin: "left_linear_trs R"
and closed:"⋀p q. (False, p, q) ∈ critical_pairs R R ⟹ ∃v. (q, v) ∈ par_rstep S ∧ (p, v) ∈ (rstep S)⇧*"
shows "CR (rstep R)"
proof -
have SR: "S ⊆ R" using assms(1)[unfolded critical_pair_closing_def] by auto
with left_lin have left_lin :"left_linear_trs R" "left_linear_trs S" unfolding left_linear_trs_def by auto
have overlay_closed: "⋀p q. (True, p, q) ∈ critical_pairs R R ⟹ ∃w. (p, w) ∈ (rstep S)⇧* ∧ (q, w) ∈ (rstep S)⇧*"
using assms(1)[unfolded critical_pair_closing_def, THEN conjunct1] by auto
let ?pR = "par_rstep R"
let ?pS = "par_rstep S"
{ fix s t u
assume "(s, t) ∈ ?pR" and "(s, u) ∈ ?pR"
with par_rstep_par_rstep_mctxt_conv obtain C ss ts and D us vs
where "(s, t) ∈ par_rstep_mctxt R C ss ts" and "(s, u) ∈ par_rstep_mctxt R D vs us"
by metis
then have "∃v w c. (t, v) ∈ (rstep S)⇧* ∧ (v, c) ∈ ?pR ∧ (u, w) ∈ (rstep S)⇧* ∧ (w, c) ∈ ?pR"
proof (induct "overlap' (C, ss) (D, vs)" arbitrary: C D ss vs s t us ts u rule: wf_induct_rule[OF wf_mult[OF SN_imp_wf[OF SN_supt]]])
case 1
then show ?case
proof (induct s arbitrary: C D ss vs t ts u us)
case (Var x)
from par_rstep_mctxt_Var_diamond[OF Var(2) Var(3)] left_lin show ?case by blast
next
case (Fun f ss')
then have s: "Fun f ss' =⇩f (C, ss)" and t: "t =⇩f (C ,ts)"
and s2: "Fun f ss' =⇩f (D, vs)" and u:"u =⇩f (D, us)"
and len1: "length ss = length ts" and len2 : "length vs = length us"
and steps1: "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R"
and steps2: "∀i<length vs. (vs ! i, us ! i) ∈ rrstep R"
unfolding par_rstep_mctxt_def by (auto dest!: eqfE)
show ?case
proof (cases C)
case MHole
then have ss:"ss = [Fun f ss']" using s by (auto elim: eqf_MHoleE)
moreover have "ts = [t]" using t MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', t) ∈ rrstep R" using steps1 by auto
then obtain l r σ where lr: "(l, r) ∈ R" and l:"Fun f ss' = l ⋅ σ" and r:" t = r ⋅ σ "
using rrstep_imp_rule_subst by fastforce
from lr left_lin have linl:"linear_term l" by (auto simp: left_linear_trs_def)
show ?thesis
proof (cases D)
case (MFun g Ds)
then have [simp]: "g = f" using s2 by (auto dest: eqfE)
obtain vss where lDs:"length ss' = length Ds" and lvss:"length vss = length Ds"
and vss:"vs = concat vss" and vs'iD:"⋀ i. i < length Ds ⟹ ss' ! i =⇩f (Ds ! i, vss ! i)"
using MFun s2 by (auto elim: eqf_MFunE)
from u MFun obtain us' where [simp]: "u = Fun f us'" by (auto elim: eqf_MFunE)
obtain uss where lDs2:"length us' = length Ds" and luss:"length uss = length Ds"
and uss:"us = concat uss" and us'iD:"⋀ i. i < length Ds ⟹ us' ! i =⇩f (Ds ! i, uss ! i)"
using MFun u by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length vss"
then have "ss' ! i =⇩f (Ds ! i, vss ! i)" using lvss vs'iD by auto
moreover have "us' ! i =⇩f (Ds ! i, uss ! i)" using luss us'iD i lvss by auto
ultimately have "length (vss ! i) = length (uss ! i)" by (auto dest!: eqfE)
} note lvssuss = this
from par_rstep_mctxt_linear_subst[OF linl Fun(4)[unfolded l]]
obtain τ where τ:"u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR) ∨
(∃E s' l' r' j D'. l = E⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos E ∈ hole_poss D ∧ j < length vs
∧ (E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs) ∧ u =⇩f (D', remove_nth j us))"
by blast
then show ?thesis
proof
assume "u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR)"
with step_in_subst_imp_par_diamond r lr show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃E s' l' r' j D'. l = E⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos E ∈ hole_poss D ∧ j < length vs
∧ (E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs) ∧ u =⇩f (D', remove_nth j us)"
then obtain E l'' l' r' j D' where E:"l = E⟨l''⟩" and l'':"is_Fun l''" and lr':"(l', r') ∈ R"
and unifiable:"l'' ⋅ σ = l' ⋅ τ" and hpos:"hole_pos E ∈ hole_poss D" and j:"j < length vs"
and Eσr:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs)"
and uD:"u =⇩f (D', remove_nth j us)"
by auto
obtain μ1 μ2 δ where mgu:"mgu_var_disjoint_string l'' l' = Some (μ1, μ2)"
and σ:"σ = μ1 ∘⇩s δ" and τ:"τ = μ2 ∘⇩s δ" and μ:"l'' ⋅ μ1 = l' ⋅ μ2"
using mgu_var_disjoint_string_complete[OF unifiable] by auto
have inner:"hole_pos E ≠ ε" using hpos MFun by auto
have "(False, r ⋅ μ1, (E ⋅⇩c μ1)⟨r' ⋅ μ2⟩) ∈ critical_pairs R R"
using lr lr' E l'' mgu inner by (force intro: critical_pairsI)
from closed[rule_format,OF this] obtain v
where v:"((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, v) ∈ par_rstep S" "(r ⋅ μ1, v) ∈ (rstep S)⇧*" by auto
then have closed1:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep S" unfolding σ τ
using subst_closed_par_rstep by fastforce
from v have closed2: "(r ⋅ σ, v ⋅ δ) ∈ (rstep S)⇧*" unfolding σ τ using rsteps_closed_subst by auto
from par_rstep_mctxtE[OF closed1] obtain F cs ds where EF:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (F, cs)" and "v ⋅ δ =⇩f (F, ds)"
and "length ds = length cs" and "∀i < length cs. (cs ! i, ds ! i) ∈ rrstep S" by metis
then have Er: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt S F cs ds"
unfolding par_rstep_mctxt_def by auto
then have ErR: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt R F cs ds"
using SR unfolding par_rstep_mctxt_def rrstep_def rstep_r_p_s_def by fastforce
let ?ol' = "overlap' (F, cs) (D', remove_nth j vs)"
have "(?ol', mset (remove_nth j vs)) ∈ (mult {⊲})⇧="
using overlap'_bounded[OF Eσr EF] overlap'_symmetric[OF EF Eσr] by auto
moreover have "(mset (remove_nth j vs), mset vs) ∈ mult {⊲}"
using remove_nth_mult j by auto
moreover have "overlap' (C, ss) (D, vs) = mset vs" using MFun MHole ss by auto
ultimately have ol:"(?ol', overlap' (C, ss) (D, vs)) ∈ mult {⊲}"
unfolding mult_def by simp
from len2 have lenrem:"length (remove_nth j us) = length (remove_nth j vs)"
by (simp add: remove_nth_def)
have stepsrem:"∀i<length (remove_nth j vs). (remove_nth j vs ! i, remove_nth j us ! i) ∈ rrstep R"
using steps2 len2 j by (metis adjust_idx_length adjust_idx_nth)
from Eσr uD lenrem stepsrem have Eu:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, u) ∈ par_rstep_mctxt R D' (remove_nth j vs) (remove_nth j us)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol ErR Eu] closed2 show ?thesis using r rtrancl_trans by metis
qed
next
case MHole
then have "vs = [Fun f ss']" using s2 by (auto elim: eqf_MHoleE)
moreover have "us = [u]" using u MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', u) ∈ rrstep R" using steps2 by auto
then obtain l' r' σ' where lr': "(l', r') ∈ R" and l':"Fun f ss' = l' ⋅ σ'"
and r':" u = r' ⋅ σ'"
using rrstep_imp_rule_subst by fastforce
with l have eq:"l' ⋅ σ' = l ⋅ σ" by auto
from lr' left_lin have "linear_term l'" by (auto simp: left_linear_trs_def)
from par_rstep_mctxt_linear_subst[OF this Fun(3)[unfolded l']]
obtain τ where τ:"t = l' ⋅ τ ∧ (∀x∈vars_term l'. (σ' x, τ x) ∈ par_rstep R) ∨
(∃E s'. l' = E⟨s'⟩ ∧ is_Fun s' ∧ hole_pos E ∈ hole_poss C)"
by blast
then show ?thesis
proof
assume "t = l' ⋅ τ ∧ (∀x∈vars_term l'. (σ' x, τ x) ∈ par_rstep R)"
with step_in_subst_imp_par_diamond r' lr' show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃E s'. l' = E⟨s'⟩ ∧ is_Fun s' ∧ hole_pos E ∈ hole_poss C"
then obtain E s' where "l' = E⟨s'⟩" and "is_Fun s'" and "hole_pos E ∈ hole_poss C" by blast
with ‹C = MHole› have isFun:"is_Fun l'" by (cases E) auto
from mgu_var_disjoint_string_complete[OF eq] obtain μ1 μ2 δ
where unif:"mgu_var_disjoint_string l' l = Some (μ1, μ2)"
and σ:"σ' = μ1 ∘⇩s δ" and σ':"σ = μ2 ∘⇩s δ"
by auto
from critical_pairsI[OF lr' lr _ _ unif] isFun
have "(True, r' ⋅ μ1, r ⋅ μ2) ∈ critical_pairs R R" by force
with overlay_closed obtain w
where "(r ⋅ μ2, w) ∈ (rstep S)⇧*" and "(r' ⋅ μ1, w) ∈ (rstep S)⇧*" by auto
with σ σ' have "(r ⋅ σ, w ⋅ δ) ∈ (rstep S)⇧*" "(r' ⋅ σ', w ⋅ δ) ∈ (rstep S)⇧*"
by (auto simp: rsteps_closed_subst)
with r r' show ?thesis using par_rsteps_rsteps by auto
qed
qed (insert s2, auto dest: eqfE)
next
case (MFun g Cs)
note C = this
then have [simp]: "g = f" using s by (auto dest: eqfE)
obtain sss where lCs:"length ss' = length Cs" and lsss:"length sss = length Cs"
and sss:"ss = concat sss" and ss'iC:"⋀ i. i < length Cs ⟹ ss' ! i =⇩f (Cs ! i, sss ! i)"
using C s by (auto elim: eqf_MFunE)
from s have "Fun f ss' = fill_holes C ss" "num_holes C = length ss" by (auto dest: eqfE)
from t C obtain ts' where [simp]: "t = Fun f ts'" by (auto elim: eqf_MFunE)
obtain tss where lCs2:"length ts' = length Cs" and ltss:"length tss = length Cs"
and tss:"ts = concat tss" and ts'iC:"⋀ i. i < length Cs ⟹ ts' ! i =⇩f (Cs ! i, tss ! i)"
using MFun t by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length sss"
then have "ss' ! i =⇩f (Cs ! i, sss ! i)" using lsss ss'iC by auto
moreover have "ts' ! i =⇩f (Cs ! i, tss ! i)" using ltss ts'iC i lsss by auto
ultimately have "length (sss ! i) = length (tss ! i)" by (auto dest!: eqfE)
} note lssstss = this
show ?thesis
proof (cases D)
case MHole
then have vs:"vs = [Fun f ss']" using s2 by (auto elim: eqf_MHoleE)
moreover have "us = [u]" using u MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', u) ∈ rrstep R" using steps2 by auto
then obtain l r σ where lr: "(l, r) ∈ R" and l:"Fun f ss' = l ⋅ σ" and r: "u = r ⋅ σ"
using rrstep_imp_rule_subst by fastforce
from lr left_lin have "linear_term l" by (auto simp: left_linear_trs_def)
from par_rstep_mctxt_linear_subst[OF this Fun(3)[unfolded l]]
obtain τ where τ:"t = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR) ∨
(∃D s' l' r' j C'. l = D⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos D ∈ hole_poss C ∧ j < length ss
∧ (D ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss) ∧ t =⇩f (C', remove_nth j ts))"
by blast
then show ?thesis
proof
assume *:"t = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR)"
with step_in_subst_imp_par_diamond r lr show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃D s' l' r' j C'. l = D⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos D ∈ hole_poss C ∧ j < length ss
∧ (D ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss) ∧ t =⇩f (C', remove_nth j ts)"
then obtain E l'' l' r' j C' where E:"l = E⟨l''⟩" and l'':"is_Fun l''" and lr':"(l', r') ∈ R"
and unifiable:"l'' ⋅ σ = l' ⋅ τ" and hpos:"hole_pos E ∈ hole_poss C" and j:"j < length ss"
and Eσr:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss)" and tCtsj:"t =⇩f (C', remove_nth j ts)"
by auto
obtain μ1 μ2 δ where mgu:"mgu_var_disjoint_string l'' l' = Some (μ1, μ2)"
and σ:"σ = μ1 ∘⇩s δ" and τ:"τ = μ2 ∘⇩s δ" and μ:"l'' ⋅ μ1 = l' ⋅ μ2"
using mgu_var_disjoint_string_complete[OF unifiable] by auto
have inner:"hole_pos E ≠ ε" using hpos C by auto
have "(False, r ⋅ μ1, (E ⋅⇩c μ1)⟨r' ⋅ μ2⟩) ∈ critical_pairs R R"
using lr lr' E l'' mgu inner by (force intro: critical_pairsI)
from closed[rule_format,OF this] obtain v
where v: "((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, v) ∈ par_rstep S" "(r ⋅ μ1, v) ∈ (rstep S)⇧*" by auto
then have closed1: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep S" unfolding σ τ
using subst_closed_par_rstep by fastforce
from v have closed2: "(r ⋅ σ, v ⋅ δ) ∈ (rstep S)⇧*" unfolding σ τ using rsteps_closed_subst by auto
from par_rstep_mctxtE[OF closed1] obtain F cs ds where EF:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (F, cs)" and "v ⋅ δ =⇩f (F, ds)"
and "length ds = length cs" and "∀i < length cs. (cs ! i, ds ! i) ∈ rrstep S" by metis
then have Ev:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt S F cs ds"
unfolding par_rstep_mctxt_def by auto
then have EvR: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt R F cs ds"
using SR unfolding par_rstep_mctxt_def rrstep_def rstep_r_p_s_def by fastforce
let ?ol' = "overlap' (C', remove_nth j ss) (F, cs)"
have "(?ol', mset (remove_nth j ss)) ∈ (mult {⊲})⇧=" using overlap'_bounded[OF Eσr EF] by auto
moreover have "(mset (remove_nth j ss), mset ss) ∈ mult {⊲}" using remove_nth_mult j by auto
moreover have "overlap' (C, ss) (D, vs) = mset ss" using C MHole vs by auto
ultimately have ol:"(?ol', overlap' (C, ss) (D, vs)) ∈ mult {⊲}" unfolding mult_def by simp
from len1 have lenrem:"length (remove_nth j ts) = length (remove_nth j ss)"
by (simp add: remove_nth_def)
have stepsrem:"∀i<length (remove_nth j ss). (remove_nth j ss ! i, remove_nth j ts ! i) ∈ rrstep R"
using len1 steps1 adjust_idx_length adjust_idx_nth j by metis
from Eσr tCtsj lenrem stepsrem
have Et:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, t) ∈ par_rstep_mctxt R C' (remove_nth j ss) (remove_nth j ts)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol Et EvR] show ?thesis by (metis closed2 r rtrancl_trans)
qed
next
case (MFun h Ds)
then have [simp]: "h = f" using s2 by (auto dest: eqfE)
obtain vss where lDs:"length ss' = length Ds" and lvss:"length vss = length Ds"
and vss:"vs = concat vss" and vs'iD:"⋀ i. i < length Ds ⟹ ss' ! i =⇩f (Ds ! i, vss ! i)"
using MFun s2 by (auto elim: eqf_MFunE)
from u MFun obtain us' where [simp]: "u = Fun f us'" by (auto elim: eqf_MFunE)
obtain uss where lDs2:"length us' = length Ds" and luss:"length uss = length Ds"
and uss:"us = concat uss" and us'iD:"⋀ i. i < length Ds ⟹ us' ! i =⇩f (Ds ! i, uss ! i)"
using MFun u by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length vss"
then have "ss' ! i =⇩f (Ds ! i, vss ! i)" using lvss vs'iD by auto
moreover have "us' ! i =⇩f (Ds ! i, uss ! i)" using luss us'iD i lvss by auto
ultimately have "length (vss ! i) = length (uss ! i)" by (auto dest!: eqfE)
} note lvssuss = this
{ fix i
assume i:"i < length ss'"
then have s: "ss' ! i ∈ set ss'" using nth_mem by blast
from i ts'iC lCs lCs2 have ts'i:"ts' ! i =⇩f (Cs ! i, tss ! i)" by auto
from i us'iD lDs lDs2 have us'i:"us' ! i =⇩f (Ds ! i, uss ! i)" by auto
have "sss ! i = partition_holes ss Cs ! i"
by (metis eqfE(2) lsss partition_holes_concat_id ss'iC sss)
moreover have " vss ! i = partition_holes vs Ds ! i"
by (metis eqfE(2) lvss partition_holes_concat_id vs'iD vss)
ultimately have "overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i) ∈#
mset (map (λi. overlap' (Cs ! i, partition_holes ss Cs ! i) (Ds ! i, partition_holes vs Ds ! i)) [0..<length Cs])"
unfolding sss vss using i lCs by fastforce
then have ol:"overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i) ⊆# overlap' (C, ss) (D, vs)"
unfolding C MFun by (simp add: in_mset_subset_Union)
{ fix C' D' ss' vs' s' t' ts' u' us'
assume 1:"(overlap' (C', ss') (D', vs'), overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i)) ∈ mult {⊲}"
and 2: "(s', t') ∈ par_rstep_mctxt R C' ss' ts'" "(s', u') ∈ par_rstep_mctxt R D' vs' us'"
have "trans {⊲}" unfolding trans_def using supt_trans by auto
with mult_subset_mult ol 1 have "(overlap' (C', ss') (D', vs'), overlap' (C, ss) (D, vs)) ∈ mult {⊲}" by blast
from Fun(2)[OF this 2] have "∃v w c. (t', v) ∈ (rstep S)⇧* ∧ (v, c) ∈ ?pR ∧ (u', w) ∈ (rstep S)⇧* ∧ (w, c) ∈ ?pR" .
} note m = this
{ fix j
assume j:"j < length (sss ! i)"
let ?k = "sum_list (map length (take i sss)) + j"
from lssstss have *:"map length (take i tss) = map length (take i sss)"
by (simp add: lsss ltss nth_map_conv)
from concat_nth_length have "?k < length ss"
using sss i j lCs lsss by metis
moreover have "ss ! ?k = sss ! i ! j" using sss concat_nth[OF _ j] i lsss lCs by auto
moreover have "ts ! ?k = tss ! i ! j" using tss concat_nth[of i tss j ?k]
j i ltss lsss lCs * lssstss by simp
ultimately have "(sss ! i ! j, tss ! i ! j) ∈ rrstep R" using steps1 by auto
}
then have "∀j<length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ rrstep R" by blast
with ss'iC i lCs ts'i
have ssts:"(ss' ! i, ts' ! i) ∈ par_rstep_mctxt R (Cs ! i) (sss ! i) (tss ! i)"
unfolding par_rstep_mctxt_def by auto
{ fix j
assume j:"j < length (vss ! i)"
let ?k = "sum_list (map length (take i vss)) + j"
from lvssuss have *:"map length (take i uss) = map length (take i vss)"
by (simp add: luss lvss nth_map_conv)
from concat_nth_length have "?k < length vs"
using i j lDs lvss vss by metis
moreover have "vs ! ?k = vss ! i ! j" using vss concat_nth[OF _ j] i lvss lDs
by auto
moreover have "us ! ?k = uss ! i ! j" using uss concat_nth[of i uss j ?k]
j i luss lvss lDs * lvssuss by simp
ultimately have "(vss ! i ! j, uss ! i ! j) ∈ rrstep R" using steps2 by auto
}
then have "∀j<length (vss ! i). (vss ! i ! j, uss ! i ! j) ∈ rrstep R" by blast
with vs'iD i lDs us'i
have "(ss' ! i, us' ! i) ∈ par_rstep_mctxt R (Ds ! i) (vss ! i) (uss ! i)"
unfolding par_rstep_mctxt_def by auto
from Fun(1)[OF s m ssts this]
have "∃v w c. (ts' ! i, v) ∈ (rstep S)⇧* ∧ (v, c) ∈ ?pR ∧
(us' ! i, w) ∈ (rstep S)⇧* ∧ (w, c) ∈ ?pR" by auto
}
then obtain v w c
where vwc: "⋀i. i < length ts' ⟹ (ts' ! i, v i) ∈ (rstep S)⇧* ∧ (v i, c i) ∈ ?pR ∧
(us' ! i, w i) ∈ (rstep S)⇧* ∧ (w i, c i) ∈ ?pR"
using lCs lCs2 by metis
let ?vs' = "map v [0..<length ts']"
let ?ws' = "map w [0..<length us']"
let ?cs' = "map c [0..<length ts']"
from vwc have *:"⋀i. i < length ts' ⟹ (ts' ! i, v i) ∈ (rstep S)⇧*" by auto
have "length ts' = length ?vs'" by auto
from * args_rsteps_imp_rsteps[OF this] have v:"(Fun f ts', Fun f ?vs') ∈ (rstep S)⇧*" by auto
from vwc have *:"⋀i. i < length us' ⟹ (us' ! i, w i) ∈ (rstep S)⇧*"
using par_rsteps_rsteps lCs lCs2 lDs lDs2 by auto
have "length us' = length ?ws'" by auto
from * args_rsteps_imp_rsteps[OF this] have w:"(Fun f us', Fun f ?ws') ∈ (rstep S)⇧*"
by auto
from vwc have c1:"(Fun f ?vs', Fun f ?cs') ∈ ?pR" by auto
have "length ?ws' = length ?cs'" using lCs lCs2 lDs lDs2 by auto
with vwc have c2:"(Fun f ?ws', Fun f ?cs') ∈ ?pR" by auto
from v w c1 c2 show ?thesis by auto
qed (insert s2, auto dest: eqfE)
qed (insert s, auto dest: eqfE)
qed
qed
} note b = this
{ fix s t u
assume "(s, t) ∈ rstep S"
and "(s, u) ∈ par_rstep R"
then have "(s, t) ∈ ?pS" and "(s, u) ∈ ?pR" using rstep_par_rstep by auto
with par_rstep_par_rstep_mctxt_conv obtain C ss ts and D us vs
where "(s, t) ∈ par_rstep_mctxt S C ss ts" and "(s, u) ∈ par_rstep_mctxt R D vs us"
by metis
then have "∃v w. (t, v) ∈ (rstep S)⇧* ∧ (v, w) ∈ par_rstep R ∧ (u, w) ∈ (rstep S)⇧*"
proof (induct "overlap' (C, ss) (D, vs)" arbitrary: C D ss vs s t us ts u rule: wf_induct_rule[OF wf_mult[OF SN_imp_wf[OF SN_supt]]])
case 1
then show ?case
proof (induct s arbitrary: C D ss vs t ts u us)
case (Var x)
from par_rstep_mctxt_Var_diamond[OF Var(2) Var(3)] left_lin par_rstep_rsteps show ?case by blast
next
case (Fun f ss')
then have s: "Fun f ss' =⇩f (C, ss)" and t: "t =⇩f (C ,ts)"
and s2: "Fun f ss' =⇩f (D, vs)" and u:"u =⇩f (D, us)"
and len1: "length ss = length ts" and len2 : "length vs = length us"
and steps1: "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep S"
and steps2: "∀i<length vs. (vs ! i, us ! i) ∈ rrstep R"
unfolding par_rstep_mctxt_def by (auto dest!: eqfE)
show ?case
proof (cases C)
case MHole
then have ss:"ss = [Fun f ss']" using s by (auto elim: eqf_MHoleE)
moreover have "ts = [t]" using t MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', t) ∈ rrstep S" using steps1 by auto
then obtain l r σ where lr: "(l, r) ∈ S" and l:"Fun f ss' = l ⋅ σ" and r:" t = r ⋅ σ "
using rrstep_imp_rule_subst by fastforce
from lr left_lin have linl:"linear_term l" by (auto simp: left_linear_trs_def)
show ?thesis
proof (cases D)
case (MFun g Ds)
then have [simp]: "g = f" using s2 by (auto dest: eqfE)
obtain vss where lDs:"length ss' = length Ds" and lvss:"length vss = length Ds"
and vss:"vs = concat vss" and vs'iD:"⋀ i. i < length Ds ⟹ ss' ! i =⇩f (Ds ! i, vss ! i)"
using MFun s2 by (auto elim: eqf_MFunE)
from u MFun obtain us' where [simp]: "u = Fun f us'" by (auto elim: eqf_MFunE)
obtain uss where lDs2:"length us' = length Ds" and luss:"length uss = length Ds"
and uss:"us = concat uss" and us'iD:"⋀ i. i < length Ds ⟹ us' ! i =⇩f (Ds ! i, uss ! i)"
using MFun u by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length vss"
then have "ss' ! i =⇩f (Ds ! i, vss ! i)" using lvss vs'iD by auto
moreover have "us' ! i =⇩f (Ds ! i, uss ! i)" using luss us'iD i lvss by auto
ultimately have "length (vss ! i) = length (uss ! i)" by (auto dest!: eqfE)
} note lvssuss = this
from par_rstep_mctxt_linear_subst[OF linl Fun(4)[unfolded l]]
obtain τ where τ:"u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR) ∨
(∃E s' l' r' j D'. l = E⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos E ∈ hole_poss D ∧ j < length vs
∧ (E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs) ∧ u =⇩f (D', remove_nth j us))"
by blast
then show ?thesis
proof
assume "u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pR)"
with step_in_subst_imp_par_diamond r lr show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃E s' l' r' j D'. l = E⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos E ∈ hole_poss D ∧ j < length vs
∧ (E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs) ∧ u =⇩f (D', remove_nth j us)"
then obtain E l'' l' r' j D' where E:"l = E⟨l''⟩" and l'':"is_Fun l''" and lr':"(l', r') ∈ R"
and unifiable:"l'' ⋅ σ = l' ⋅ τ" and hpos:"hole_pos E ∈ hole_poss D" and j:"j < length vs"
and Eσr:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (D', remove_nth j vs)"
and uD:"u =⇩f (D', remove_nth j us)"
by auto
obtain μ1 μ2 δ where mgu:"mgu_var_disjoint_string l'' l' = Some (μ1, μ2)"
and σ:"σ = μ1 ∘⇩s δ" and τ:"τ = μ2 ∘⇩s δ" and μ:"l'' ⋅ μ1 = l' ⋅ μ2"
using mgu_var_disjoint_string_complete[OF unifiable] by auto
have inner:"hole_pos E ≠ ε" using hpos MFun by auto
have "(False, r ⋅ μ1, (E ⋅⇩c μ1)⟨r' ⋅ μ2⟩) ∈ critical_pairs R R"
using lr lr' E l'' mgu inner SR by (force intro: critical_pairsI)
from closed[rule_format,OF this] obtain v
where v:"((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, v) ∈ par_rstep S" "(r ⋅ μ1, v) ∈ (rstep S)⇧*" by auto
then have closed1:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep S" unfolding σ τ
using subst_closed_par_rstep by fastforce
from v have closed2: "(r ⋅ σ, v ⋅ δ) ∈ (rstep S)⇧*" unfolding σ τ using rsteps_closed_subst by auto
from par_rstep_mctxtE[OF closed1] obtain F cs ds where EF:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (F, cs)" and "v ⋅ δ =⇩f (F, ds)"
and "length ds = length cs" and "∀i < length cs. (cs ! i, ds ! i) ∈ rrstep S" by metis
then have Er: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt S F cs ds"
unfolding par_rstep_mctxt_def by auto
let ?ol' = "overlap' (F, cs) (D', remove_nth j vs)"
have "(?ol', mset (remove_nth j vs)) ∈ (mult {⊲})⇧="
using overlap'_bounded[OF Eσr EF] overlap'_symmetric[OF EF Eσr] by auto
moreover have "(mset (remove_nth j vs), mset vs) ∈ mult {⊲}"
using remove_nth_mult j by auto
moreover have "overlap' (C, ss) (D, vs) = mset vs" using MFun MHole ss by auto
ultimately have ol:"(?ol', overlap' (C, ss) (D, vs)) ∈ mult {⊲}"
unfolding mult_def by simp
from len2 have lenrem:"length (remove_nth j us) = length (remove_nth j vs)"
by (simp add: remove_nth_def)
have stepsrem:"∀i<length (remove_nth j vs). (remove_nth j vs ! i, remove_nth j us ! i) ∈ rrstep R"
using steps2 len2 j by (metis adjust_idx_length adjust_idx_nth)
from Eσr uD lenrem stepsrem have Eu:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, u) ∈ par_rstep_mctxt R D' (remove_nth j vs) (remove_nth j us)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol Er Eu] closed2 show ?thesis using r rtrancl_trans by metis
qed
next
case MHole
then have "vs = [Fun f ss']" using s2 by (auto elim: eqf_MHoleE)
moreover have "us = [u]" using u MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', u) ∈ rrstep R" using steps2 by auto
then obtain l' r' σ' where lr': "(l', r') ∈ R" and l':"Fun f ss' = l' ⋅ σ'"
and r':" u = r' ⋅ σ'"
using rrstep_imp_rule_subst by fastforce
with l have eq:"l' ⋅ σ' = l ⋅ σ" by auto
from lr' left_lin have "linear_term l'" by (auto simp: left_linear_trs_def)
from par_rstep_mctxt_linear_subst[OF this Fun(3)[unfolded l']]
obtain τ where τ:"t = l' ⋅ τ ∧ (∀x∈vars_term l'. (σ' x, τ x) ∈ par_rstep S) ∨
(∃E s'. l' = E⟨s'⟩ ∧ is_Fun s' ∧ hole_pos E ∈ hole_poss C)"
by blast
then show ?thesis
proof
assume "t = l' ⋅ τ ∧ (∀x∈vars_term l'. (σ' x, τ x) ∈ par_rstep S)"
with step_in_subst_imp_par_diamond r' lr' show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃E s'. l' = E⟨s'⟩ ∧ is_Fun s' ∧ hole_pos E ∈ hole_poss C"
then obtain E s' where "l' = E⟨s'⟩" and "is_Fun s'" and "hole_pos E ∈ hole_poss C" by blast
with ‹C = MHole› have isFun:"is_Fun l'" by (cases E) auto
from mgu_var_disjoint_string_complete[OF eq] obtain μ1 μ2 δ
where unif:"mgu_var_disjoint_string l' l = Some (μ1, μ2)"
and σ:"σ' = μ1 ∘⇩s δ" and σ':"σ = μ2 ∘⇩s δ"
by auto
from critical_pairsI[OF lr' lr _ _ unif] isFun
have "(True, r' ⋅ μ1, r ⋅ μ2) ∈ critical_pairs R R"
using critical_pairs_mono[OF subset_refl[of R] SR] by force
with overlay_closed obtain w
where "(r ⋅ μ2, w) ∈ (rstep S)⇧*" and "(r' ⋅ μ1, w) ∈ (rstep S)⇧*" by auto
with σ σ' have "(r ⋅ σ, w ⋅ δ) ∈ (rstep S)⇧*" "(r' ⋅ σ', w ⋅ δ) ∈ (rstep S)⇧*"
by (auto simp: rsteps_closed_subst)
with r r' show ?thesis using par_rsteps_rsteps by auto
qed
qed (insert s2, auto dest: eqfE)
next
case (MFun g Cs)
note C = this
then have [simp]: "g = f" using s by (auto dest: eqfE)
obtain sss where lCs:"length ss' = length Cs" and lsss:"length sss = length Cs"
and sss:"ss = concat sss" and ss'iC:"⋀ i. i < length Cs ⟹ ss' ! i =⇩f (Cs ! i, sss ! i)"
using C s by (auto elim: eqf_MFunE)
from s have "Fun f ss' = fill_holes C ss" "num_holes C = length ss" by (auto dest: eqfE)
from t C obtain ts' where [simp]: "t = Fun f ts'" by (auto elim: eqf_MFunE)
obtain tss where lCs2:"length ts' = length Cs" and ltss:"length tss = length Cs"
and tss:"ts = concat tss" and ts'iC:"⋀ i. i < length Cs ⟹ ts' ! i =⇩f (Cs ! i, tss ! i)"
using MFun t by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length sss"
then have "ss' ! i =⇩f (Cs ! i, sss ! i)" using lsss ss'iC by auto
moreover have "ts' ! i =⇩f (Cs ! i, tss ! i)" using ltss ts'iC i lsss by auto
ultimately have "length (sss ! i) = length (tss ! i)" by (auto dest!: eqfE)
} note lssstss = this
show ?thesis
proof (cases D)
case MHole
then have vs:"vs = [Fun f ss']" using s2 by (auto elim: eqf_MHoleE)
moreover have "us = [u]" using u MHole by (auto elim: eqf_MHoleE)
ultimately have "(Fun f ss', u) ∈ rrstep R" using steps2 by auto
then obtain l r σ where lr: "(l, r) ∈ R" and l:"Fun f ss' = l ⋅ σ" and r: "u = r ⋅ σ"
using rrstep_imp_rule_subst by fastforce
from lr left_lin have "linear_term l" by (auto simp: left_linear_trs_def)
from par_rstep_mctxt_linear_subst[OF this Fun(3)[unfolded l]]
obtain τ where τ:"t = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pS) ∨
(∃D s' l' r' j C'. l = D⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ S ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos D ∈ hole_poss C ∧ j < length ss
∧ (D ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss) ∧ t =⇩f (C', remove_nth j ts))"
by blast
then show ?thesis
proof
assume *:"t = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ ?pS)"
with step_in_subst_imp_par_diamond r lr show ?thesis using par_rstep_rsteps by fastforce
next
assume "∃D s' l' r' j C'. l = D⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ S ∧ s' ⋅ σ = l' ⋅ τ
∧ hole_pos D ∈ hole_poss C ∧ j < length ss
∧ (D ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss) ∧ t =⇩f (C', remove_nth j ts)"
then obtain E l'' l' r' j C' where E:"l = E⟨l''⟩" and l'':"is_Fun l''" and lr':"(l', r') ∈ S"
and unifiable:"l'' ⋅ σ = l' ⋅ τ" and hpos:"hole_pos E ∈ hole_poss C" and j:"j < length ss"
and Eσr:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (C', remove_nth j ss)" and tCtsj:"t =⇩f (C', remove_nth j ts)"
by auto
obtain μ1 μ2 δ where mgu:"mgu_var_disjoint_string l'' l' = Some (μ1, μ2)"
and σ:"σ = μ1 ∘⇩s δ" and τ:"τ = μ2 ∘⇩s δ" and μ:"l'' ⋅ μ1 = l' ⋅ μ2"
using mgu_var_disjoint_string_complete[OF unifiable] by auto
have inner:"hole_pos E ≠ ε" using hpos C by auto
have "(False, r ⋅ μ1, (E ⋅⇩c μ1)⟨r' ⋅ μ2⟩) ∈ critical_pairs R R"
using lr lr' E l'' mgu inner SR by (force intro: critical_pairsI)
from closed[rule_format,OF this] obtain v
where v: "((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, v) ∈ par_rstep S" "(r ⋅ μ1, v) ∈ (rstep S)⇧*" by auto
then have closed1: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep S" unfolding σ τ
using subst_closed_par_rstep by fastforce
from v have closed2: "(r ⋅ σ, v ⋅ δ) ∈ (rstep S)⇧*" unfolding σ τ using rsteps_closed_subst by auto
from par_rstep_mctxtE[OF closed1] obtain F cs ds where EF:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (F, cs)" and "v ⋅ δ =⇩f (F, ds)"
and "length ds = length cs" and "∀i < length cs. (cs ! i, ds ! i) ∈ rrstep S" by metis
then have Ev:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt S F cs ds"
unfolding par_rstep_mctxt_def by auto
then have EvR: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt R F cs ds"
using SR unfolding par_rstep_mctxt_def rrstep_def rstep_r_p_s_def by fastforce
let ?ol' = "overlap' (C', remove_nth j ss) (F, cs)"
have "(?ol', mset (remove_nth j ss)) ∈ (mult {⊲})⇧=" using overlap'_bounded[OF Eσr EF] by auto
moreover have "(mset (remove_nth j ss), mset ss) ∈ mult {⊲}" using remove_nth_mult j by auto
moreover have "overlap' (C, ss) (D, vs) = mset ss" using C MHole vs by auto
ultimately have ol:"(?ol', overlap' (C, ss) (D, vs)) ∈ mult {⊲}" unfolding mult_def by simp
from len1 have lenrem:"length (remove_nth j ts) = length (remove_nth j ss)"
by (simp add: remove_nth_def)
have stepsrem:"∀i<length (remove_nth j ss). (remove_nth j ss ! i, remove_nth j ts ! i) ∈ rrstep S"
using len1 steps1 adjust_idx_length adjust_idx_nth j by metis
from Eσr tCtsj lenrem stepsrem
have Et:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, t) ∈ par_rstep_mctxt S C' (remove_nth j ss) (remove_nth j ts)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol Et EvR] show ?thesis by (metis closed2 r rtrancl_trans)
qed
next
case (MFun h Ds)
then have [simp]: "h = f" using s2 by (auto dest: eqfE)
obtain vss where lDs:"length ss' = length Ds" and lvss:"length vss = length Ds"
and vss:"vs = concat vss" and vs'iD:"⋀ i. i < length Ds ⟹ ss' ! i =⇩f (Ds ! i, vss ! i)"
using MFun s2 by (auto elim: eqf_MFunE)
from u MFun obtain us' where [simp]: "u = Fun f us'" by (auto elim: eqf_MFunE)
obtain uss where lDs2:"length us' = length Ds" and luss:"length uss = length Ds"
and uss:"us = concat uss" and us'iD:"⋀ i. i < length Ds ⟹ us' ! i =⇩f (Ds ! i, uss ! i)"
using MFun u by (auto elim: eqf_MFunE)
{ fix i
assume i:"i < length vss"
then have "ss' ! i =⇩f (Ds ! i, vss ! i)" using lvss vs'iD by auto
moreover have "us' ! i =⇩f (Ds ! i, uss ! i)" using luss us'iD i lvss by auto
ultimately have "length (vss ! i) = length (uss ! i)" by (auto dest!: eqfE)
} note lvssuss = this
{ fix i
assume i:"i < length ss'"
then have s: "ss' ! i ∈ set ss'" using nth_mem by blast
from i ts'iC lCs lCs2 have ts'i:"ts' ! i =⇩f (Cs ! i, tss ! i)" by auto
from i us'iD lDs lDs2 have us'i:"us' ! i =⇩f (Ds ! i, uss ! i)" by auto
have "sss ! i = partition_holes ss Cs ! i"
by (metis eqfE(2) lsss partition_holes_concat_id ss'iC sss)
moreover have " vss ! i = partition_holes vs Ds ! i"
by (metis eqfE(2) lvss partition_holes_concat_id vs'iD vss)
ultimately have "overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i) ∈#
mset (map (λi. overlap' (Cs ! i, partition_holes ss Cs ! i) (Ds ! i, partition_holes vs Ds ! i)) [0..<length Cs])"
unfolding sss vss using i lCs by fastforce
then have ol:"overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i) ⊆# overlap' (C, ss) (D, vs)"
unfolding C MFun by (simp add: in_mset_subset_Union)
{ fix C' D' ss' vs' s' t' ts' u' us'
assume 1:"(overlap' (C', ss') (D', vs'), overlap' (Cs ! i, sss ! i) (Ds ! i, vss ! i)) ∈ mult {⊲}"
and 2: "(s', t') ∈ par_rstep_mctxt S C' ss' ts'" "(s', u') ∈ par_rstep_mctxt R D' vs' us'"
have "trans {⊲}" unfolding trans_def using supt_trans by auto
with mult_subset_mult ol 1 have "(overlap' (C', ss') (D', vs'), overlap' (C, ss) (D, vs)) ∈ mult {⊲}" by blast
from Fun(2)[OF this 2] have "∃v w. (t', v) ∈ (rstep S)⇧* ∧ (v, w) ∈ ?pR ∧ (u', w) ∈ (rstep S)⇧*" .
} note m = this
{ fix j
assume j:"j < length (sss ! i)"
let ?k = "sum_list (map length (take i sss)) + j"
from lssstss have *:"map length (take i tss) = map length (take i sss)"
by (simp add: lsss ltss nth_map_conv)
from concat_nth_length have "?k < length ss"
using sss i j lCs lsss by metis
moreover have "ss ! ?k = sss ! i ! j" using sss concat_nth[OF _ j] i lsss lCs by auto
moreover have "ts ! ?k = tss ! i ! j" using tss concat_nth[of i tss j ?k]
j i ltss lsss lCs * lssstss by simp
ultimately have "(sss ! i ! j, tss ! i ! j) ∈ rrstep S" using steps1 by auto
}
then have "∀j<length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ rrstep S" by blast
with ss'iC i lCs ts'i
have ssts:"(ss' ! i, ts' ! i) ∈ par_rstep_mctxt S (Cs ! i) (sss ! i) (tss ! i)"
unfolding par_rstep_mctxt_def by auto
{ fix j
assume j:"j < length (vss ! i)"
let ?k = "sum_list (map length (take i vss)) + j"
from lvssuss have *:"map length (take i uss) = map length (take i vss)"
by (simp add: luss lvss nth_map_conv)
from concat_nth_length have "?k < length vs"
using i j lDs lvss vss by metis
moreover have "vs ! ?k = vss ! i ! j" using vss concat_nth[OF _ j] i lvss lDs
by auto
moreover have "us ! ?k = uss ! i ! j" using uss concat_nth[of i uss j ?k]
j i luss lvss lDs * lvssuss by simp
ultimately have "(vss ! i ! j, uss ! i ! j) ∈ rrstep R" using steps2 by auto
}
then have "∀j<length (vss ! i). (vss ! i ! j, uss ! i ! j) ∈ rrstep R" by blast
with vs'iD i lDs us'i
have "(ss' ! i, us' ! i) ∈ par_rstep_mctxt R (Ds ! i) (vss ! i) (uss ! i)"
unfolding par_rstep_mctxt_def by auto
from Fun(1)[OF s m ssts this]
have "∃v w. (ts' ! i, v) ∈ (rstep S)⇧* ∧ (v, w) ∈ ?pR ∧ (us' ! i, w) ∈ (rstep S)⇧*" by auto
}
then obtain v w
where vw: "⋀i. i < length ts' ⟹ (ts' ! i, v i) ∈ (rstep S)⇧* ∧ (v i, w i) ∈ ?pR ∧
(us' ! i, w i) ∈ (rstep S)⇧*"
using lCs lCs2 by metis
let ?vs' = "map v [0..<length ts']"
let ?ws' = "map w [0..<length us']"
from vw have *:"⋀i. i < length ts' ⟹ (ts' ! i, v i) ∈ (rstep S)⇧*" by auto
have "length ts' = length ?vs'" by auto
from * args_rsteps_imp_rsteps[OF this] have v:"(Fun f ts', Fun f ?vs') ∈ (rstep S)⇧*" by auto
from vw have *:"⋀i. i < length us' ⟹ (us' ! i, w i) ∈ (rstep S)⇧*"
using par_rsteps_rsteps lCs lCs2 lDs lDs2 by auto
have "length us' = length ?ws'" by auto
from * args_rsteps_imp_rsteps[OF this] have w:"(Fun f us', Fun f ?ws') ∈ (rstep S)⇧*"
by auto
from vw have "(Fun f ?vs', Fun f ?ws') ∈ ?pR" using lCs lCs2 lDs lDs2 by auto
with v w show ?thesis by auto
qed (insert s2, auto dest: eqfE)
qed (insert s, auto dest: eqfE)
qed
qed
} note a = this
from assms(2) have sn:"SN ((rstep S)⇧+)" using SN_imp_SN_trancl by blast
have "a*": "∃v w. (t, v) ∈ (rstep S)⇧* ∧ (v, w) ∈ par_rstep R ∧ (u, w) ∈ (rstep S)⇧*"
if st:"(s, t) ∈ (rstep S)⇧*" and su:"(s, u) ∈ par_rstep R" for s t u
using st su
proof (induct s arbitrary: t u rule: SN_induct[OF sn])
case (1 s) note IH = 1(1)
from 1(2) show ?case
proof (cases rule: converse_rtranclE)
case (step s')
from a step(1) 1(3) obtain v w
where sv:"(s', v) ∈ (rstep S)⇧*" and vw:"(v, w) ∈ par_rstep R" and uw:"(u, w) ∈ (rstep S)⇧*"
by blast
from sv step(2) cpcs_sn_cr[OF assms(1,2)] obtain t'
where tt:"(t, t') ∈ (rstep S)⇧*" and vt:"(v, t') ∈ (rstep S)⇧*" by auto
from sv step(1) have "(s, v) ∈ (rstep S)⇧+" by simp
from IH[OF this vt vw] obtain v' w'
where "(t', v') ∈ (rstep S)⇧*" and "(v', w') ∈ par_rstep R" and "(w, w') ∈ (rstep S)⇧*"
by auto
then have "(t, v') ∈ (rstep S)⇧* ∧ (v', w') ∈ par_rstep R ∧ (u, w') ∈ (rstep S)⇧*"
using tt uw by auto
then show ?thesis by blast
qed (insert 1, blast)
qed
have "∃v w x. (t', v) ∈ (rstep S)⇧* ∧ (v, x) ∈ par_rstep R ∧ (u', w) ∈ (rstep S)⇧* ∧ (w, x) ∈ par_rstep R"
if st:"(s, t) ∈ (rstep S)⇧*" and tt:"(t, t') ∈ par_rstep R"
and su:"(s, u) ∈ (rstep S)⇧*" and uu:"(u, u') ∈ par_rstep R" for s t t' u u'
using st tt su uu
proof (induct s arbitrary: t u t' u' rule: SN_induct[OF sn])
case (1 s)
then consider (empty) "s = t ∧ t = u" | (nonempty) "(s, t) ∈ (rstep S)⇧+ ∨ (s, u) ∈ (rstep S)⇧+" by (metis rtranclD)
then show ?case
proof (cases)
case empty
then show ?thesis using b 1 by auto
next
case nonempty
from 1 cpcs_sn_cr[OF assms(1,2)] obtain v where
tv:"(t , v) ∈ (rstep S)⇧*" and uv:"(u, v) ∈ (rstep S)⇧*" by blast
with nonempty have sv:"(s, v) ∈ (rstep S)⇧+" by auto
from "a*"[OF tv 1(3)] obtain v⇩1 w⇩1 where
vv⇩1:"(v, v⇩1) ∈ (rstep S)⇧*" and v⇩1w⇩1: "(v⇩1, w⇩1) ∈ par_rstep R" and tw⇩1:"(t', w⇩1) ∈ (rstep S)⇧*"
by auto
from "a*"[OF uv 1(5)] obtain v⇩2 w⇩2 where
vv⇩2:"(v, v⇩2) ∈ (rstep S)⇧*" and v⇩2w⇩2: "(v⇩2, w⇩2) ∈ par_rstep R" and uw⇩2:"(u', w⇩2) ∈ (rstep S)⇧*"
by auto
from 1(1)[OF sv vv⇩1 v⇩1w⇩1 vv⇩2 v⇩2w⇩2] tw⇩1 uw⇩2 show ?thesis by (meson rtrancl_trans)
qed
qed
then have "◇ ((rstep S)⇧* O par_rstep R)" by (intro diamond_I') blast
moreover have "rstep R ⊆ (rstep S)⇧* O par_rstep R" using rstep_par_rstep by fastforce
moreover have "(rstep S)⇧* O par_rstep R ⊆ (rstep R)⇧*" using SR
by (metis par_rstep_rsteps relcomp_mono rstep_mono rtrancl_idemp_self_comp rtrancl_mono)
ultimately show ?thesis using diamond_imp_CR' by auto
qed
end