theory Parallel_Closed
imports
"Check-NT.Critical_Pairs"
TA.Multihole_Context
begin
subsection ‹Measuring Overlap›
fun overlap' :: "('f, 'v) mctxt × ('f, 'v) term list ⇒ ('f, 'v) mctxt × ('f, 'v) term list ⇒ ('f, 'v) term multiset"
where
"overlap' (MHole, [l]) (C, ls) = mset ls"
| "overlap' (C, ls) (MHole, [l]) = mset ls"
| "overlap' (MFun f Cs, ls) (MFun g Ds, ls') =
⋃# {# overlap' (Cs ! i, partition_holes ls Cs ! i) (Ds ! i, partition_holes ls' Ds ! i). i ∈# mset [0..<length Cs] #}"
| "overlap' (MVar x, []) (C, ls) = {#}"
| "overlap' (C, ls) (MVar x, []) = {#}"
| "overlap' _ _ = undefined"
lemma overlap'_symmetric:
assumes "s =⇩f (C, ls)" and "s =⇩f (D, ls')"
shows "overlap' (C, ls) (D, ls') = overlap' (D, ls') (C, ls)"
using assms
proof (induct C arbitrary: D s ls ls')
case (MVar x) note C = this
then have [simp]: "ls = []" by (auto dest!: eqfE)
show ?case
proof (cases D)
case (MVar y) with C show ?thesis by (auto dest!: eqfE)
next
case MHole with C show ?thesis by (auto dest!: eqf_MHoleE)
qed auto
next
case MHole note C = this
then obtain l where [simp]: "ls = [l]" by (auto dest!: eqf_MHoleE)
show ?case
proof (cases D)
case (MVar y) with C show ?thesis by (auto dest!: eqfE)
next
case MHole with C show ?thesis by (auto dest!: eqf_MHoleE)
qed auto
next
case (MFun f cs) note C = this
then obtain ss lss where s:"s = Fun f ss"
and lcs:"length ss = length cs" and llss:"length lss = length cs"
and lss:"ls = concat lss" and lsics:"⋀ i. i < length cs ⟹ ss ! i =⇩f (cs ! i, lss ! i)"
using C by (auto elim: eqf_MFunE)
show ?case
proof (cases D)
case (MVar x) with C show ?thesis by (auto dest!: eqfE)
next
case MHole with C show ?thesis by (auto dest!: eqf_MHoleE)
next
case (MFun g ds)
with C obtain ts lss' where "s = Fun g ts"
and lds:"length ts = length ds" and llss':"length lss' = length ds"
and lss':"ls' = concat lss'" and ls'ids:"⋀ i. i < length ds ⟹ ts ! i =⇩f (ds ! i, lss' ! i)"
using C by (auto elim: eqf_MFunE)
with s have [simp]: "g = f" "ts = ss" by auto
have [simp]: "partition_holes ls cs = lss" by (metis eqfE(2) llss lsics lss partition_holes_concat_id)
have [simp]: "partition_holes ls' ds = lss'" by (metis eqfE(2) llss' ls'ids lss' partition_holes_concat_id)
{ fix i
assume i:"i < length cs"
then have "cs ! i ∈ set cs" by auto
from C(1)[OF this lsics[OF i], of "ds ! i" "lss' ! i"] ls'ids i
have "overlap' (cs ! i, lss ! i) (ds ! i, lss' ! i) = overlap' (ds ! i, lss' ! i) (cs ! i, lss ! i)"
using lds lcs by auto
} note ieq = this
then have "(map (λi. overlap' (cs ! i, lss ! i) (ds ! i, lss' ! i)) [0..<length cs]) =
(map (λi. overlap' (ds ! i, lss' ! i) (cs ! i, lss ! i)) [0..<length ds])"
using nth_equalityI lcs lds by auto
then have "{#overlap' (cs ! i, lss ! i) (ds ! i, lss' ! i). i ∈# mset [0..<length cs]#} =
{#overlap' (ds ! i, lss' ! i) (cs ! i, lss ! i). i ∈# mset [0..<length ds]#}"
using mset_map by (metis (no_types))
with MFun show ?thesis by auto
qed
qed
lemma overlap'_bounded:
assumes "s =⇩f (C, ls)" and "s =⇩f (D, ls')"
shows "(overlap' (C, ls) (D, ls'), mset ls) ∈ (mult {⊲})⇧="
proof -
have trans: "trans {⊲}" unfolding trans_def using supt_trans by auto
show ?thesis
using assms
proof (induct C arbitrary: D ls ls' s)
case (MVar x) note C = this
then have [simp]: "ls = []" by (auto dest!: eqfE)
show ?case
proof (cases D)
case (MVar y) with C show ?thesis by (auto dest!: eqfE)
next
case MHole with C show ?thesis by (auto dest!: eqf_MHoleE)
qed auto
next
case MHole note C = this
then obtain l where [simp]: "ls = [l]" "s = l" by (auto dest!: eqf_MHoleE)
show ?case
proof (cases D)
case (MVar y) with C show ?thesis by (auto dest!: eqfE simp: mult_def)
next
case MHole with C show ?thesis by (auto dest!: eqf_MHoleE)
next
case (MFun g ds)
from eqf_MFun_imp_strict_subt[OF C(2)[unfolded MFun]] have "⋀t. t ∈ set ls' ⟹ l ⊳ t"
by auto
then have "(mset ls', {#l#}) ∈ mult {⊲}"
using one_step_implies_mult [of "{#l#}" "mset ls'" "{⊲}" "{#}"] by auto
with MFun show ?thesis by simp
qed
next
case (MFun f cs) note C = this
then obtain ss lss where s:"s = Fun f ss"
and lcs:"length ss = length cs" and llss:"length lss = length cs"
and lss:"ls = concat lss" and lsics:"⋀ i. i < length cs ⟹ ss ! i =⇩f (cs ! i, lss ! i)"
using C by (auto elim: eqf_MFunE)
show ?case
proof (cases D)
case (MVar y)
with C show ?thesis using non_empty_empty_mult[of "mset ls"] by (auto dest!: eqfE)
next
case MHole
with C obtain l' where [simp]: "ls' = [l']" "s = l'" by (auto dest!: eqf_MHoleE)
from eqf_MFun_imp_strict_subt[OF C(2)] have "⋀t. t ∈ set ls ⟹ l' ⊳ t"
by auto
then have "(mset ls, {#l'#}) ∈ mult {⊲}"
using one_step_implies_mult[of "{#l'#}" "mset ls" "{⊲}" "{#}"] by auto
with MHole show ?thesis by simp
next
case (MFun g ds)
with C obtain ts lss' where "s = Fun g ts"
and lds:"length ts = length ds" and llss':"length lss' = length ds"
and lss':"ls' = concat lss'" and ls'ids:"⋀ i. i < length ds ⟹ ts ! i =⇩f (ds ! i, lss' ! i)"
using C by (auto elim: eqf_MFunE)
with s have [simp]: "g = f" "ts = ss" by auto
have partlscs: "partition_holes ls cs = lss"
by (metis eqfE(2) llss lsics lss partition_holes_concat_id)
have partlsds:"partition_holes ls' ds = lss'"
by (metis eqfE(2) llss' ls'ids lss' partition_holes_concat_id)
let ?ol = "λi. overlap' (cs ! i, lss ! i) (ds ! i, lss' ! i)"
{ fix i
assume i:"i < length cs"
then have "cs ! i ∈ set cs" by auto
from C(1)[OF this lsics[OF i]] ls'ids i lds lcs
have "(?ol i, mset (lss ! i)) ∈ (mult {⊲})⇧=" by auto
} note IH = this
then have "∀i < length cs. (map ?ol [0..<length cs] ! i , map mset lss ! i) ∈ (mult {⊲})⇧="
using llss by auto
with pointwise_mult_imp_mult[OF _ _ trans]
have "(⋃# mset (map ?ol [0..<length cs]), ⋃# mset (map mset lss)) ∈ (mult {⊲})⇧="
using length_map llss map_upt_len_conv by (metis (lifting))
then show ?thesis unfolding lss mset_concat_union MFun overlap'.simps
using lss mset_map partlscs partlsds by metis
qed
qed
qed
subsection ‹Parallel Rewriting using Multihole Contexts›
lemma par_rstep_mctxtE:
assumes "(s, t) ∈ par_rstep R"
obtains C ss ts where "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "length ss = length ts"
and "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R"
proof -
have "∃ C ss ts. s =⇩f (C, ss) ∧ t =⇩f (C, ts) ∧ length ss = length ts ∧
(∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R)" (is "∃C ss ts. ?P s t C ss ts")
using assms
proof (induct)
case (root_step s t σ)
then have "(s ⋅ σ, t ⋅ σ) ∈ rrstep R" by auto
moreover have "s ⋅ σ =⇩f (MHole, [s ⋅ σ])" and "t ⋅ σ =⇩f (MHole, [t ⋅ σ])" by auto
ultimately show ?case by force
next
case (par_step_var x)
have "Var x =⇩f (MVar x, [])" by auto
then show ?case by force
next
case (par_step_fun ts ss f)
then have "∀i<length ts. ∃x. ?P (ss ! i) (ts ! i) (fst x) (fst (snd x)) (snd (snd x))" by force
then obtain g where "∀i<length ts. ?P (ss ! i) (ts ! i) (fst (g i)) (fst (snd (g i))) (snd (snd (g i)))"
unfolding choice_iff' by blast
moreover
define Cs us vs where "Cs = map (λi. fst (g i)) [0 ..< length ts]"
and "us = map (λi. fst (snd (g i))) [0 ..< length ts]"
and "vs = map (λi. snd (snd (g i))) [0 ..< length ts]"
ultimately have [simp]: "length Cs = length ts"
"length us = length ts" "length vs = length ts"
and *: "∀i<length us. ss ! i =⇩f (Cs ! i, us ! i) ∧ ts ! i =⇩f (Cs ! i, vs ! i) ∧
(∀j<length (us ! i). (us ! i ! j, vs ! i ! j) ∈ rrstep R)"
by simp_all
define C where "C = MFun f Cs"
have "Fun f ss =⇩f (C, concat us)" and "Fun f ts =⇩f (C, concat vs)"
using * by (auto simp: C_def ‹length ss = length ts› intro: eqf_MFunI)
moreover have "∀i<length (concat us). (concat us ! i, concat vs ! i) ∈ rrstep R"
using * by (intro concat_all_nth) (auto dest!: eqfE)
moreover have "length (concat us) = length (concat vs)" by (metis calculation(1) calculation(2) eqfE(2))
ultimately show ?case by blast
qed
with that show ?thesis by blast
qed
lemma par_rstep_mctxt_rrstepI :
assumes "s =⇩f (C, ss)" and "t =⇩f (C, ts)"
and "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R"
shows "(s, t) ∈ par_rstep R"
by (meson assms contra_subsetD par_rstep_mctxt rrstep_imp_rstep rstep_par_rstep)
definition "par_rstep_mctxt R C ss ts =
{(s, t). s =⇩f (C, ss) ∧ t =⇩f (C, ts) ∧ (∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R)}"
lemma par_rstep_par_rstep_mctxt_conv:
"(s, t) ∈ par_rstep R ⟷ (∃C ss ts. (s, t) ∈ par_rstep_mctxt R C ss ts)"
proof
assume "(s, t) ∈ par_rstep R"
from par_rstep_mctxtE[OF this] obtain C ss ts
where " s =⇩f (C, ss)" and "t =⇩f (C, ts)" and "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R"
by metis
then show "∃C ss ts. (s, t) ∈ par_rstep_mctxt R C ss ts" by (auto simp: par_rstep_mctxt_def)
next
assume "∃C ss ts. (s, t) ∈ par_rstep_mctxt R C ss ts"
then show "(s, t) ∈ par_rstep R"
by (auto simp: par_rstep_mctxt_def intro: par_rstep_mctxt_rrstepI)
qed
text ‹lemma which tells us, that a parallel rewrite step of s ⋅ σ is either inside s i.e., we
can split of a critical pair, or we can do the step completely inside σ›
lemma par_rstep_mctxt_linear_subst:
assumes "linear_term s"
and "(s ⋅ σ, t) ∈ par_rstep_mctxt R C ss ts"
shows "(∃ τ. t = s ⋅ τ ∧ (∀ x ∈ vars_term s. (σ x, τ x) ∈ par_rstep R) ∨
(∃ D s' l r j C'. s = D⟨s'⟩ ∧ is_Fun s' ∧ (l, r) ∈ R ∧ (s' ⋅ σ = l ⋅ τ)
∧ j < length ss ∧ hole_pos D ∈ hole_poss C
∧ (D ⋅⇩c σ)⟨r ⋅ τ⟩ =⇩f (C', remove_nth j ss) ∧ t =⇩f (C', remove_nth j ts)))"
using assms
proof (induction s arbitrary: t C ss ts)
case (Var x)
then show ?case
unfolding par_rstep_mctxt_def by (auto intro: exI[of _ "λy. t"] par_rstep_mctxt_rrstepI)
next
case (Fun f ss')
then have s:"Fun f ss' ⋅ σ =⇩f (C, ss)" and t: "t =⇩f (C, ts)"
and steps : "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R"
and length: "length ss = length ts"
unfolding par_rstep_mctxt_def by (auto dest!: eqfE)
let ?ss = "map (λ s. s ⋅ σ) ss'"
show ?case
proof (cases C)
case (MHole)
with t have t:"ts = [t]" by (auto elim: eqf_MHoleE)
from s MHole have ss: "ss = [Fun f ?ss]" by (auto elim: eqf_MHoleE)
with steps obtain τ l r where l:"Fun f ?ss = l ⋅ τ" and r:"ts ! 0 = r ⋅ τ" and lr:"(l, r) ∈ R"
unfolding rrstep_def' by auto
show ?thesis
proof (rule exI, rule disjI2, intro exI conjI)
show "Fun f ss' = □⟨Fun f ss'⟩" by simp
show "is_Fun (Fun f ss')" by auto
from l show " Fun f ss' ⋅ σ = l ⋅ τ" by auto
from lr show "(l, r) ∈ R" .
from ss show "0 < length ss" by auto
show "(□ ⋅⇩c σ)⟨r ⋅ τ⟩ =⇩f (mctxt_of_term (r ⋅ τ), remove_nth 0 ss)"
using ss unfolding remove_nth_def by auto
show "t =⇩f (mctxt_of_term (r ⋅ τ), remove_nth 0 ts)"
using r t unfolding remove_nth_def by auto
show "hole_pos □ ∈ hole_poss C" using MHole by auto
qed
next
case (MFun g Cs)
then have gf [simp]: "g = f" using s by (auto dest: eqfE)
from s have "Fun f ?ss =⇩f (C, ss)" by auto
with MFun 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)"
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 MFun obtain ts' where t2 [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
let ?p1 = "λ τ i. ts' ! i = ss' ! i ⋅ τ ∧ (∀ x ∈ vars_term (ss' ! i). (σ x, τ x) ∈ par_rstep R)"
let ?p2 = "λ τ i. (∃ D s' l r j C'. ss' ! i = D⟨s'⟩ ∧ is_Fun s' ∧ (l, r) ∈ R ∧ s' ⋅ σ = l ⋅ τ ∧
j < length (sss ! i) ∧ hole_pos D ∈ hole_poss (Cs ! i) ∧
(D ⋅⇩c σ)⟨r ⋅ τ⟩ =⇩f (C', remove_nth j (sss ! i)) ∧
ts' ! i =⇩f (C', remove_nth j (tss ! i)))"
let ?p = "λ τ i. ?p1 τ i ∨ ?p2 τ i"
{
fix i
assume i: "i < length ss'"
then have i2: "i < length Cs" using lCs by auto
from ss'iC[OF i2] i have eqf:"ss' ! i ⋅ σ =⇩f (Cs ! i, sss ! i)" by simp
from ts'iC[OF i2] i have eqf2:"ts' ! i =⇩f (Cs ! i, tss ! i)" by simp
from i have mem: "ss' ! i ∈ set ss'" by auto
from Fun(2) i have lin:"linear_term (ss' ! i)" by auto
from lssstss i lCs lsss ltss have len: "length (tss ! i) = length (sss ! i)" by auto
{ 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)
have "?k < length ss" by (simp add: concat_nth_length i2 j lsss sss)
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 steps by auto
}
then have rrstep: "∀j<length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ rrstep R" by blast
from eqf eqf2 rrstep have "(ss' ! i ⋅ σ, ts' ! i) ∈ par_rstep_mctxt R (Cs ! i) (sss ! i) (tss ! i)"
unfolding par_rstep_mctxt_def by auto
from Fun.IH[OF mem lin this] have "∃ τ. ?p τ i" .
}
hence "∀i. ∃τ. i < length ss' ⟶ ?p τ i" by blast
from choice[OF this] obtain τs where τs: "⋀ i. i < length ss' ⟹ ?p (τs i) i" by blast
show ?thesis
proof (cases "∃ i. i < length ss' ∧ ?p2 (τs i) i")
case True
then obtain i where iss': "i < length ss'" and p2: "?p2 (τs i) i" by blast+
from iss' have its': "i < length ts'" using lCs lCs2 by auto
from p2 obtain D s' l r j C' where ssi: "ss' ! i = D⟨s'⟩" and "is_Fun s'" "(l, r) ∈ R"
and s':"s' ⋅ σ = l ⋅ τs i" and j:"j < length (sss ! i)" and hpos: "hole_pos D ∈ hole_poss (Cs ! i)"
and Dσr:"(D ⋅⇩c σ)⟨r ⋅ τs i⟩ =⇩f (C', remove_nth j (sss ! i))"
and ts'i:"ts' ! i =⇩f (C', remove_nth j (tss ! i))"
by blast
define bef where "bef = take i ss'"
define aft where "aft = drop (Suc i) ss'"
from id_take_nth_drop[OF iss', unfolded ssi] have ss':"ss' = bef @ D ⟨s'⟩ # aft"
using aft_def bef_def by blast
let ?D = "More f bef D aft"
let ?r = "(D ⋅⇩c σ)⟨r ⋅ τs i⟩"
let ?σ = "map (λ s. s ⋅ σ)"
let ?Cs = "take i Cs @ C' # drop (Suc i) Cs"
have D: "(?D ⋅⇩c σ)⟨r ⋅ τs i⟩ = Fun f (?σ bef @ ?r # ?σ aft)" by simp
have D2: "(?D ⋅⇩c σ)⟨l ⋅ τs i⟩ = Fun f ?ss" by (simp add: ss' s')
show ?thesis unfolding ss'
proof (rule exI[of _ "τs i"], rule disjI2, rule exI[of _ ?D], intro exI conjI)
show "is_Fun s'" by fact
show "(l, r) ∈ R" by fact
show "s' ⋅ σ = l ⋅ τs i" by fact
show "Fun f (bef @ D⟨s'⟩ # aft) = (More f bef D aft)⟨s'⟩" by auto
have "min (length Cs) i = i" using iss' lCs by auto
then show "hole_pos (More f bef D aft) ∈ hole_poss C" using hpos MFun bef_def iss' lCs by auto
from bef_def iss' have "length bef = i" by auto
have iCs: "i < length Cs" using lCs iss' by auto
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)
show k:"?k < length ss" by (simp add: concat_nth_length iCs j lsss sss)
have ssk:"ss ! ?k = sss ! i ! j" using sss concat_nth[OF _ j] iss' lsss lCs by auto
have tsk:"ts ! ?k = tss ! i ! j" using tss concat_nth[of i tss j ?k] j iss' ltss lsss lCs * lssstss by simp
from iss' lCs lsss have isss:"i < length sss" by auto
let ?sssk = "take i sss @ remove_nth j (sss ! i) # drop (Suc i) sss"
have sssk:"concat ?sssk = remove_nth ?k ss" using concat_remove_nth[OF isss j] sss by auto
have "length ?sssk = length ?Cs" using lsss by auto
moreover have "length (?σ bef @ ?r # ?σ aft) = length ?Cs"
using lCs ss' iss' by auto
moreover {
fix l
assume "l < length ?Cs"
then have l:"l < length Cs" using iCs by auto
consider (le) "l < i" | (eq) "l = i" | (gt) "l > i" by fastforce
then have "(?σ bef @ ?r # ?σ aft) ! l =⇩f (?Cs ! l, ?sssk ! l)"
proof (cases)
case le
have "ss' ! l ⋅ σ =⇩f (Cs ! l, sss ! l)" using ss'iC[OF l] nth_map lCs l by force
with le show ?thesis using l lCs lsss by (auto simp: nth_append bef_def aft_def)
next
case eq
then show ?thesis using l lCs lsss Dσr by (auto simp: nth_append bef_def aft_def)
next
case gt
have "ss' ! l ⋅ σ =⇩f (Cs ! l, sss ! l)" using ss'iC[OF l] nth_map lCs l by force
moreover have "min (length Cs) i = i" using iCs by auto
ultimately show ?thesis using l lCs lsss gt by (auto simp: nth_append bef_def aft_def)
qed
}
ultimately have "Fun f (?σ bef @ ?r # ?σ aft) =⇩f (MFun f ?Cs, concat ?sssk)"
using eqf_MFunI by fast
then show "(?D ⋅⇩c σ)⟨r ⋅ τs i⟩ =⇩f (MFun f ?Cs, remove_nth ?k ss)" unfolding D sssk .
let ?tssk = "take i tss @ remove_nth j (tss ! i) # drop (Suc i) tss"
have "?k = sum_list (map length (take i tss)) + j" using * by auto
then have tssk:"concat ?tssk = remove_nth ?k ts" unfolding tss
using concat_remove_nth[OF _ j[unfolded lssstss[OF isss]]] isss lsss ltss by auto
have "length ?tssk = length ?Cs" using ltss by auto
moreover have "length ts' = length ?Cs" using lCs2 lCs iss' by auto
moreover {
fix l
assume "l < length ?Cs"
then have l:"l < length Cs" using iCs by auto
consider (le) "l < i" | (eq) "l = i" | (gt) "l > i" by fastforce
then have "ts' ! l =⇩f (?Cs ! l, ?tssk ! l)"
proof (cases)
case le
with ts'iC[OF l] show ?thesis using l lCs2 ltss by (auto simp: nth_append)
next
case eq
then show ?thesis using l lCs ltss ts'i by (auto simp: nth_append)
next
case gt
moreover have "min (length Cs) i = i" using iCs by auto
ultimately show ?thesis using l lCs ltss gt ts'iC[OF l] by (auto simp: nth_append)
qed
}
ultimately have "Fun f ts' =⇩f (MFun f ?Cs, concat ?tssk)"
using eqf_MFunI by fast
then show "t =⇩f (MFun f ?Cs, remove_nth ?k ts)" unfolding tssk t2 .
qed
next
case False
with τs have τs: "⋀ i. i < length ss' ⟹ ?p1 (τs i) i" by blast
from Fun(2) have "is_partition (map vars_term ss')" by simp
from subst_merge[OF this, of τs] obtain τ
where τ: "⋀i x. i < length ss' ⟹ x ∈ vars_term (ss' ! i) ⟹ τ x = τs i x" by auto
{ fix i
assume i: "i < length ss'"
then have mem: "ss' ! i ∈ set ss'" by auto
from τs[OF i] have p1: "?p1 (τs i) i" .
have id: "ss' ! i ⋅ (τs i) = ss' ! i ⋅ τ" by (rule term_subst_eq, rule τ[OF i, symmetric])
have "?p1 τ i"
proof (rule conjI[OF _ ballI])
fix x
assume x: "x ∈ vars_term (ss' ! i)"
with p1 have step: "(σ x, τs i x) ∈ par_rstep R" by auto
with τ[OF i x] show "(σ x, τ x) ∈ par_rstep R" by simp
qed (insert p1[unfolded id], auto)
} note p1 = this
have p1: "⋀ i. i < length ss' ⟹ ?p1 τ i" by (rule p1)
let ?ss = "map (λ s. s ⋅ τ) ss'"
show ?thesis
proof (rule exI[of _ τ], rule disjI1, rule conjI[OF _ ballI])
have "ts' = map (λ i. ts' ! i) [0 ..< (length ts')]" by (rule map_nth[symmetric])
also have "... = map (λ i. ?ss ! i) [0 ..< length ?ss]" using p1 lCs2 lCs by auto
also have "... = ?ss" by (rule map_nth)
finally have ts: "ts' = ?ss" .
then show "t = Fun f ss' ⋅ τ" by auto
next
fix x
assume "x ∈ vars_term (Fun f ss')"
then obtain s where s: "s ∈ set ss'" and x: "x ∈ vars_term s" by auto
from s[unfolded set_conv_nth] obtain i where i: "i < length ss'" and s: "s = ss' ! i" by auto
from p1[OF i] x[unfolded s]
show "(σ x, τ x) ∈ par_rstep R" by blast
qed
qed
qed (insert s t, auto dest: eqfE)
qed
lemma step_in_subst_imp_par_diamond:
assumes "t = r ⋅ σ"
and "u = l ⋅ τ"
and "∀x∈vars_term l. (σ x, τ x) ∈ par_rstep R2"
and "(l, r) ∈ R1"
shows "∃v. (t, v) ∈ par_rstep R2 ∧ (u, v) ∈ par_rstep R1"
proof -
define δ where "δ = (λx. if x ∈ vars_term l then τ x else σ x)"
have "∀x∈vars_term l. τ x = δ x" by (auto simp: δ_def)
then have "l ⋅ τ = l ⋅ δ" using term_subst_eq_conv by auto
moreover have "(l ⋅ δ, r ⋅ δ) ∈ par_rstep R1" using assms rstep_par_rstep by blast
ultimately have "(l ⋅ τ, r ⋅ δ) ∈ par_rstep R1" by auto
moreover have "(r ⋅ σ, r ⋅ δ) ∈ par_rstep R2"
proof (rule all_ctxt_closed_subst_step)
fix x
assume "x ∈ vars_term r"
show "(σ x, δ x) ∈ par_rstep R2" using assms by (cases "x ∈ vars_term l") (auto simp: δ_def)
qed auto
ultimately show ?thesis using assms par_rstep_rsteps by auto
qed
lemma ctxt_subst_eq:
assumes "⋀x. x ∈ vars_ctxt C ⟹ σ x = τ x"
shows "C ⋅⇩c σ = C ⋅⇩c τ"
using assms
proof (induct C)
case (More f bef C aft)
{ fix t
assume t:"t ∈ set bef"
have "t ⋅ σ = t ⋅ τ" using t More(2) by (auto intro: term_subst_eq)
}
moreover
{ fix t
assume t:"t ∈ set aft"
have "t ⋅ σ = t ⋅ τ" using t More(2) by (auto intro: term_subst_eq)
}
moreover have "C ⋅⇩c σ = C ⋅⇩c τ" using More by auto
ultimately show ?case by auto
qed auto
lemma par_rstep_mctxt_Var_diamond:
fixes u t :: "('f, 'v) term"
assumes "(Var x, t) ∈ par_rstep_mctxt R⇩1 C ss ts"
and "(Var x, u) ∈ par_rstep_mctxt R⇩2 D vs us"
and left_lin: "left_linear_trs R⇩1" "left_linear_trs R⇩2"
shows "∃v. (t, v) ∈ par_rstep R⇩2 ∧ (u, v) ∈ par_rstep R⇩1"
proof -
from assms have s: "Var x =⇩f (C, ss)" and t: "t =⇩f (C ,ts)"
and s2: "Var x =⇩f (D, vs)" and u:"u =⇩f (D, us)"
and steps1: "∀i<length ss. (ss ! i, ts ! i) ∈ rrstep R⇩1"
unfolding par_rstep_mctxt_def by (auto dest!: eqfE)
then have "Var x = fill_holes C ss" and "length ss = num_holes C" and "Var x = fill_holes D vs"
by (auto dest: eqfE)
then consider (MVar1) "C = MVar x" | (MVar2) "D = MVar x"
| (MHole) "C = MHole" and "ss = [Var x]" and "D = MHole"
by (cases C, auto) (cases D, auto, cases ss, auto)
then show ?thesis
proof (cases)
case MVar1
with assms t have "(t, u) ∈ par_rstep_mctxt R⇩2 D vs us" by (auto dest: eqfE)
then show ?thesis using par_rstep_par_rstep_mctxt_conv by blast
next
case MVar2
with assms u have "(u, t) ∈ par_rstep_mctxt R⇩1 C ss ts" by (auto dest: eqfE)
then show ?thesis using par_rstep_par_rstep_mctxt_conv by blast
next
case MHole
moreover have "ts = [t]" using t MHole by (auto elim: eqf_MHoleE)
ultimately obtain l r σ where lr: "(l, r) ∈ R⇩1" and l:"Var x = l ⋅ σ" and r:"t = r ⋅ σ"
using rrstep_imp_rule_subst steps1 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 assms(2)[unfolded l]]
obtain τ where τ:"u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ par_rstep R⇩2) ∨
(∃E s'. l = E⟨s'⟩ ∧ is_Fun s' ∧ hole_pos E ∈ hole_poss D)"
by blast
then show ?thesis
proof
assume "u = l ⋅ τ ∧ (∀x∈vars_term l. (σ x, τ x) ∈ par_rstep R⇩2)"
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 D"
then obtain E l'' where E:"l = E⟨l''⟩" and l'':"is_Fun l''" and "hole_pos E ∈ hole_poss D" by auto
with MHole have "E = □" by (cases E) auto
with E l'' l show ?thesis by auto
qed
qed
qed
lemma parallel_closed_strongly_commute:
assumes closed_1:"⋀p q b. (b, p, q) ∈ critical_pairs R2 R1 ⟹ ∃v. (q, v) ∈ par_rstep R2 ∧ (p, v) ∈ (rstep R1)⇧*"
and closed_2: "⋀p q. (False, p, q) ∈ critical_pairs R1 R2 ⟹ (q, p) ∈ par_rstep R1"
and left_lin: "left_linear_trs R1" "left_linear_trs R2"
shows "strongly_commute (par_rstep R1) (par_rstep R2)"
proof (rule strongly_commuteI)
fix s t u
let ?pR1 = "par_rstep R1"
let ?pR2 = "par_rstep R2"
assume "(s, t) ∈ ?pR1" and "(s, u) ∈ ?pR2"
with par_rstep_par_rstep_mctxt_conv obtain C ss ts and D us vs
where "(s, t) ∈ par_rstep_mctxt R1 C ss ts" and "(s, u) ∈ par_rstep_mctxt R2 D vs us"
by metis
then have "∃v. (t, v) ∈ ?pR2 ∧ (u, v) ∈ (rstep R1)⇧*"
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)
with par_rstep_mctxt_Var_diamond left_lin par_rstep_rsteps show ?case by fast
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 R1"
and steps2: "∀i<length vs. (vs ! i, us ! i) ∈ rrstep R2"
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 R1" using steps1 by auto
then obtain l r σ where lr: "(l, r) ∈ R1" 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) ∈ ?pR2) ∨
(∃E s' l' r' j D'. l = E⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R2 ∧ 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) ∈ ?pR2)"
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') ∈ R2 ∧ 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') ∈ R2"
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 R1 R2"
using lr lr' E l'' mgu inner by (force intro: critical_pairsI)
from closed_2[OF this] have closed:"((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, r ⋅ μ1) ∈ par_rstep R1" by auto
from closed have "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, r ⋅ σ) ∈ par_rstep R1" unfolding σ τ
using subst_closed_par_rstep by fastforce
from par_rstep_mctxtE[OF this] obtain F cs ds where EF:"(E ⋅⇩c σ)⟨r' ⋅ τ⟩ =⇩f (F, cs)" and "r ⋅ σ =⇩f (F, ds)"
and "length ds = length cs" and "∀i < length cs. (cs ! i, ds ! i) ∈ rrstep R1" by metis
then have Er: "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, r ⋅ σ) ∈ par_rstep_mctxt R1 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 R2"
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 R2 D' (remove_nth j vs) (remove_nth j us)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol Er Eu] show ?thesis using r by auto
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 R2" using steps2 by auto
then obtain l' r' σ' where lr': "(l', r') ∈ R2" 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 R1) ∨
(∃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 R1)"
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 R2 R1" by force
from closed_1[OF this] obtain w
where "(r ⋅ μ2, w) ∈ par_rstep R2" and "(r' ⋅ μ1, w) ∈ (rstep R1)⇧*" by auto
with σ σ' have "(r ⋅ σ, w ⋅ δ) ∈ par_rstep R2" "(r' ⋅ σ', w ⋅ δ) ∈ (rstep R1)⇧*"
by (auto simp: subst_closed_par_rstep 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 R2" using steps2 by auto
then obtain l r σ where lr: "(l, r) ∈ R2" 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) ∈ ?pR1) ∨
(∃D s' l' r' j C'. l = D⟨s'⟩ ∧ is_Fun s' ∧ (l', r') ∈ R1 ∧ 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) ∈ ?pR1)"
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') ∈ R1 ∧ 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') ∈ R1"
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 R2 R1"
using lr lr' E l'' mgu inner by (force intro: critical_pairsI)
with closed_1[OF this] obtain v where closed1:"((E ⋅⇩c μ1)⟨r' ⋅ μ2⟩, v) ∈ ?pR2"
and closed2:"(r ⋅ μ1, v) ∈ (rstep R1)⇧*" by auto
from closed1 have "((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep R2" unfolding σ τ
using subst_closed_par_rstep by fastforce
from par_rstep_mctxtE[OF this] 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 R2" by metis
then have Ev:"((E ⋅⇩c σ)⟨r' ⋅ τ⟩, v ⋅ δ) ∈ par_rstep_mctxt R2 F cs ds"
unfolding par_rstep_mctxt_def by auto
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 R1"
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 R1 C' (remove_nth j ss) (remove_nth j ts)"
unfolding par_rstep_mctxt_def by auto
from Fun(2)[OF ol Et Ev]
show ?thesis using r rsteps_closed_subst[OF closed2, of δ] unfolding σ by auto
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 R1 C' ss' ts'" "(s', u') ∈ par_rstep_mctxt R2 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. (t', v) ∈ ?pR2 ∧ (u', v) ∈ (rstep R1)⇧*" .
} 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 R1" using steps1 by auto
}
then have "∀j<length (sss ! i). (sss ! i ! j, tss ! i ! j) ∈ rrstep R1" by blast
with ss'iC i lCs ts'i
have ssts:"(ss' ! i, ts' ! i) ∈ par_rstep_mctxt R1 (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 R2" using steps2 by auto
}
then have "∀j<length (vss ! i). (vss ! i ! j, uss ! i ! j) ∈ rrstep R2" by blast
with vs'iD i lDs us'i
have "(ss' ! i, us' ! i) ∈ par_rstep_mctxt R2 (Ds ! i) (vss ! i) (uss ! i)"
unfolding par_rstep_mctxt_def by auto
from Fun(1)[OF s m ssts this]
have "∃v. (ts' ! i, v) ∈ ?pR2 ∧ (us' ! i, v) ∈ (rstep R1)⇧*" by auto
}
then obtain v
where v: "⋀i. i < length ts' ⟹ (ts' ! i, v i) ∈ ?pR2 ∧ (us' ! i, v i) ∈ (rstep R1)⇧*"
using lCs lCs2 by metis
let ?vs' = "map v [0..<length ts']"
from v have v1:"(Fun f ts', Fun f ?vs') ∈ ?pR2" by auto
from v have *:"⋀i. i < length us' ⟹ (us' ! i, v i) ∈ (rstep R1)⇧*"
using par_rsteps_rsteps lCs lCs2 lDs lDs2 by auto
have "length us' = length ?vs'" using lCs lCs2 lDs lDs2 by auto
with * args_rsteps_imp_rsteps[OF this] have v2:"(Fun f us', Fun f ?vs') ∈ (rstep R1)⇧*"
by auto
from v1 v2 show ?thesis by auto
qed (insert s2, auto dest: eqfE)
qed (insert s, auto dest: eqfE)
qed
qed
then show "∃v. (t, v) ∈ ?pR2⇧= ∧ (u, v) ∈ ?pR1⇧*" by (auto simp: par_rsteps_rsteps)
qed
corollary parallel_closed_commute:
assumes closed_1:"⋀p q b. (b, p, q) ∈ critical_pairs R2 R1 ⟹ ∃v. (q, v) ∈ par_rstep R2 ∧ (p, v) ∈ (rstep R1)⇧*"
and closed_2: "⋀p q. (False, p, q) ∈ critical_pairs R1 R2 ⟹ (q, p) ∈ par_rstep R1"
and left_lin: "left_linear_trs R1" "left_linear_trs R2"
shows "commute (rstep R1) (rstep R2)"
proof
fix x y⇩1 y⇩2
assume "(x, y⇩1) ∈ (rstep R1)⇧*" and "(x, y⇩2) ∈ (rstep R2)⇧*"
then have "(x, y⇩1) ∈ (par_rstep R1)⇧*" and "(x, y⇩2) ∈ (par_rstep R2)⇧*"
using rtrancl_mono[OF rstep_par_rstep] by auto
from commuteE[OF strongly_commute_imp_commute[OF parallel_closed_strongly_commute[OF assms]] this]
obtain z where "(y⇩1, z) ∈ (par_rstep R2)⇧* ∧ (y⇩2, z) ∈ (par_rstep R1)⇧*" by fast
then show "∃z. (y⇩1, z) ∈ (rstep R2)⇧* ∧ (y⇩2, z) ∈ (rstep R1)⇧*"
using rtrancl_mono[OF par_rstep_rsteps] rtrancl_idemp by auto
qed
corollary parallel_closed_imp_CR:
assumes "⋀p q. (False, p, q) ∈ critical_pairs R R ⟹ (q, p) ∈ par_rstep R"
and "⋀p q. (True, p, q) ∈ critical_pairs R R ⟹ ∃v. (q, v) ∈ par_rstep R ∧ (p, v) ∈ (rstep R)⇧*"
and "left_linear_trs R"
shows "CR (rstep R)"
proof -
{ fix p q b
assume "(b, p, q) ∈ critical_pairs R R"
then have "∃v. (q, v) ∈ par_rstep R ∧ (p, v) ∈ (rstep R)⇧*"
using assms(1,2) by (cases b) auto
} moreover
{ fix p q
assume "(False, p, q) ∈ critical_pairs R R"
with assms(1) have "(q, p) ∈ par_rstep R" by auto
}
ultimately have "commute (rstep R) (rstep R)"
using parallel_closed_commute assms(3) by blast
then show ?thesis using CR_iff_self_commute by auto
qed
end