Theory ParRed
section ‹Parallel reduction›
theory ParRed imports "HOL-Proofs-Lambda.Commutation" Sigma begin
subsection ‹Parallel reduction›
inductive par_beta :: "[sterm,sterm] ⇒ bool" (infixl "⇒⇩β" 50)
where
pbeta_Fvar[simp,intro!]: "Fvar x ⇒⇩β Fvar x"
| pbeta_Obj[simp,intro!] :
"⟦ dom f' = dom f; finite L;
∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(f' l) = σ[s,p] t);
∀l∈dom f. body (the(f l)) ⟧ ⟹ Obj f T ⇒⇩β Obj f' T"
| pbeta_Upd[simp,intro!] :
"⟦ t ⇒⇩β t'; lc t; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t'' ∧ u' = σ[s,p] t'');
body u ⟧ ⟹ Upd t l u ⇒⇩β Upd t' l u'"
| pbeta_Upd'[simp,intro!]:
"⟦ Obj f T ⇒⇩β Obj f' T; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (t⇗[Fvar s, Fvar p]⇖) ⇒⇩β t'' ∧ t' = σ[s,p] t''); l ∈ dom f;
lc (Obj f T); body t ⟧ ⟹ (Upd (Obj f T) l t) ⇒⇩β (Obj (f'(l ↦ t')) T)"
| pbeta_Call[simp,intro!]:
"⟦ t ⇒⇩β t'; u ⇒⇩β u'; lc t; lc u ⟧
⟹ Call t l u ⇒⇩β Call t' l u'"
| pbeta_beta[simp,intro!]:
"⟦ Obj f T ⇒⇩β Obj f' T; l ∈ dom f; p ⇒⇩β p'; lc (Obj f T); lc p ⟧
⟹ Call (Obj f T) l p ⇒⇩β (the(f' l)⇗[(Obj f' T), p']⇖)"
inductive_cases par_beta_cases [elim!]:
"Fvar x ⇒⇩β t"
"Obj f T ⇒⇩β t"
"Call f l p ⇒⇩β t"
"Upd f l t ⇒⇩β u"
abbreviation
par_beta_ascii :: "[sterm, sterm] => bool" (infixl "=>" 50) where
"t => u == par_beta t u"
lemma Obj_par_red[consumes 1, case_names obj]:
"⟦ Obj f T ⇒⇩β z;
⋀lz. ⟦ dom lz = dom f; z = Obj lz T⟧ ⟹ Q ⟧ ⟹ Q"
by (rule par_beta_cases(2), assumption, auto)
lemma Upd_par_red[consumes 1, case_names upd obj]:
fixes t l u z
assumes
"Upd t l u ⇒⇩β z" and
"⋀t' u' L. ⟦ t ⇒⇩β t'; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t''
∧ u' = σ[s,p]t'');
z = Upd t' l u' ⟧ ⟹ Q" and
"⋀f f' T u' L. ⟦ l ∈ dom f; Obj f T = t; Obj f T ⇒⇩β Obj f' T;
finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t''
∧ u' = σ[s,p]t'');
z = Obj (f'(l ↦ u')) T ⟧ ⟹ Q"
shows Q
using assms
proof (cases rule: par_beta.cases)
case pbeta_Upd thus ?thesis using assms(2) by force
next
case pbeta_Upd'
from this(1-2) this(5-6) assms(3)[OF _ _ this(3-4)]
show ?thesis by force
qed
lemma Call_par_red[consumes 1, case_names call beta]:
fixes s l u z
assumes
"Call s l u ⇒⇩β z" and
"⋀t u'. ⟦ s ⇒⇩β t; u ⇒⇩β u'; z = Call t l u' ⟧
⟹ Q"
"⋀f f' T u'. ⟦ Obj f T = s; Obj f T ⇒⇩β Obj f' T;
l ∈ dom f'; u ⇒⇩β u';
z = (the (f' l)⇗[Obj f' T, u']⇖) ⟧ ⟹ Q"
shows Q
using assms
proof (cases rule: par_beta.cases)
case pbeta_Call thus ?thesis using assms(2) by force
next
case pbeta_beta
from this(1-5) assms(3)[OF _ this(3)]
show ?thesis by force
qed
lemma pbeta_induct[consumes 1, case_names Fvar Call Upd Upd' Obj beta Bnd]:
fixes
t :: sterm and t' :: sterm and
P1 :: "sterm ⇒ sterm ⇒ bool" and P2 :: "sterm ⇒ sterm ⇒ bool"
assumes
"t ⇒⇩β t'" and
"⋀x. P1 (Fvar x) (Fvar x)" and
"⋀t t' l u u'. ⟦ t ⇒⇩β t'; P1 t t'; lc t; u ⇒⇩β u'; P1 u u'; lc u ⟧
⟹ P1 (Call t l u) (Call t' l u')" and
"⋀t t' l u u'. ⟦ t ⇒⇩β t'; P1 t t'; lc t; P2 u u'; body u ⟧
⟹ P1 (Upd t l u) (Upd t' l u')" and
"⋀f f' T t t' l. ⟦ Obj f T ⇒⇩β Obj f' T; P1 (Obj f T) (Obj f' T);
P2 t t'; l ∈ dom f; lc (Obj f T); body t ⟧
⟹ P1 (Upd (Obj f T) l t) (Obj (f'(l ↦ t')) T)" and
"⋀f f' T. ⟦ dom f' = dom f; ∀l∈dom f. body (the(f l));
∀l∈dom f. P2 (the(f l)) (the(f' l)) ⟧
⟹ P1 (Obj f T) (Obj f' T)" and
"⋀f f' T l p p'. ⟦ Obj f T ⇒⇩β Obj f' T; P1 (Obj f T) (Obj f' T); lc (Obj f T);
l ∈ dom f; p ⇒⇩β p'; P1 p p'; lc p ⟧
⟹ P1 (Call (Obj f T) l p) (the(f' l)⇗[Obj f' T, p']⇖)" and
"⋀L t t'.
⟦ finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''
∧ P1 (t⇗[Fvar s,Fvar p]⇖) t'' ∧ t' = σ[s,p] t'') ⟧
⟹ P2 t t'"
shows "P1 t t'"
by (induct rule: par_beta.induct[OF assms(1)], auto simp: assms)
subsection ‹Preservation›
lemma par_beta_lc[simp]:
fixes t t'
assumes "t ⇒⇩β t'"
shows "lc t ∧ lc t'"
using assms
proof
(induct
taking: "λt t'. body t'"
rule: pbeta_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case Upd thus ?case by (simp add: lc_upd)
next
case Upd' thus ?case by (simp add: lc_upd lc_obj)
next
case Obj thus ?case by (simp add: lc_obj)
next
case (beta f f' T l p p') thus ?case
by (clarify, simp add: lc_obj body_lc[of "the(f' l)" "Obj f' T" p'])
next
case (Bnd L t t') note cof = this(2)
from exFresh_s_p_cof[OF ‹finite L›]
obtain s p where sp: "s ∉ L ∧ p ∉ L ∧ s ≠ p" by auto
with cof obtain t'' where "lc t''" and "t' = σ[s,p] t''" by blast
with lc_body[of t'' s p] sp show "body t'" by force
qed
lemma par_beta_preserves_FV[simp, rule_format]:
fixes t t' x
assumes "t ⇒⇩β t'"
shows "x ∉ FV t ⟶ x ∉ FV t'"
using assms
proof
(induct
taking: "λt t'. x ∉ FV t ⟶ x ∉ FV t'"
rule: pbeta_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case Upd thus ?case by simp
next
case Upd' thus ?case by simp
next
case Obj thus ?case by (simp add: FV_option_lem)
next
case (beta f f' T l p p') thus ?case
proof (intro strip)
assume "x ∉ FV (Call (Obj f T) l p)"
with
‹x ∉ FV (Obj f T) ⟶ x ∉ FV (Obj f' T)›
‹x ∉ FV p ⟶ x ∉ FV p'›
have obj': "x ∉ FV (Obj f' T)" and p': "x ∉ FV p'"
by auto
from ‹l ∈ dom f› ‹Obj f T ⇒⇩β Obj f' T› have "l ∈ dom f'"
by auto
with
obj' p' FV_option_lem[of f']
contra_subsetD[OF sopen_FV[of 0 "Obj f' T" p' "the(f' l)"]]
show "x ∉ FV (the (f' l)⇗[Obj f' T,p']⇖)" by (auto simp: openz_def)
qed
next
case (Bnd L t t') note cof = this(2)
from ‹finite L› exFresh_s_p_cof[of "L ∪ {x}"]
obtain s p where
"s ∉ L"and "p ∉ L" and "s ≠ p" and
"x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)"
by auto
with cof obtain t'' where
tt'': "x ∉ FV (t⇗[Fvar s, Fvar p]⇖) ⟶ x ∉ FV t''" and
"t' = σ[s,p] t''"
by auto
show ?case
proof (intro strip)
assume "x ∉ FV t"
with
tt'' ‹x ∉ FV (Fvar s)› ‹x ∉ FV (Fvar p)›
contra_subsetD[OF sopen_FV[of 0 "Fvar s" "Fvar p" t]]
sclose_subset_FV[of 0 s p t''] ‹t' = σ[s,p] t''›
show "x ∉ FV t'" by (auto simp: openz_def closez_def)
qed
qed
lemma par_beta_body[simp]:
"⟦ finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'' ∧ t' = σ[s,p] t'') ⟧
⟹ body t ∧ body t'"
proof (intro conjI)
fix L :: "fVariable set" and t :: sterm and t' :: sterm
assume "finite L" hence "finite (L ∪ FV t)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where sp: "s ∉ L ∪ FV t ∧ p ∉ L ∪ FV t ∧ s ≠ p" by auto
hence "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" by auto
assume
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ => t'' ∧ t' = σ[s,p] t'')"
with sp obtain t'' where "t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''" and "t' = σ[s,p] t''"
by blast
from par_beta_lc[OF this(1)] have "lc (t⇗[Fvar s,Fvar p]⇖)" and "lc t''"
by auto
from
lc_body[OF this(1) ‹s ≠ p›]
sclose_sopen_eq_t[OF ‹s ∉ FV t› ‹p ∉ FV t› ‹s ≠ p›]
show "body t"
by (simp add: closez_def openz_def)
from lc_body[OF ‹lc t''› ‹s ≠ p›] ‹t' = σ[s,p] t''› show "body t'" by simp
qed
subsection ‹Miscellaneous properties of par\_beta›
lemma Fvar_pbeta [simp]: "(Fvar x ⇒⇩β t) = (t = Fvar x)" by auto
lemma Obj_pbeta: "Obj f T ⇒⇩β Obj f' T
⟹ dom f' = dom f
∧ (∃L. finite L
∧ (∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(f' l) = σ[s,p]t)))
∧ (∀l∈dom f. body (the(f l)))"
by (rule par_beta_cases(2), assumption, auto)
lemma Obj_pbeta_subst:
"⟦ finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (t⇗[Fvar s, Fvar p]⇖) ⇒⇩β t'' ∧ t' = σ[s,p] t'');
Obj f T ⇒⇩β Obj f' T; lc (Obj f T); body t ⟧
⟹ Obj (f(l ↦ t)) T ⇒⇩β Obj (f'(l ↦ t')) T"
proof -
fix L f f' T l t t'
assume "Obj f T ⇒⇩β Obj f' T" from Obj_pbeta[OF this]
have
dom: "dom (f'(l ↦ t')) = dom (f(l ↦ t))" and
exL: "∃L. finite L
∧ (∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t. the (f l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (f' l) = σ[s,p] t))" and
bodyf: "∀l∈dom f. body (the (f l))"
by auto
assume "body t" with bodyf
have body: "∀l'∈dom (f(l ↦ t)). body (the ((f(l ↦ t)) l'))"
by auto
assume
"finite L" and
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'' ∧ t' = σ[s,p] t'')"
with exL
obtain L' where
"finite (L' ∪ L)" and
"∀l'∈dom (f(l ↦ t)). ∀s p. s ∉ L' ∪ L ∧ p ∉ L' ∪ L ∧ s ≠ p
⟶ (∃t''. the ((f(l ↦ t)) l')⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''
∧ the ((f'(l ↦ t')) l') = σ[s,p] t'')"
by auto
from par_beta.pbeta_Obj[OF dom this body]
show "Obj (f(l ↦ t)) T ⇒⇩β Obj (f'(l ↦ t')) T"
by assumption
qed
lemma Upd_pbeta: "Upd t l u ⇒⇩β Upd t' l u'
⟹ t ⇒⇩β t'
∧ (∃L. finite L
∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t'' ∧ u' = σ[s,p]t'')))
∧ lc t ∧ body u"
by (rule par_beta_cases(4), assumption, auto)
lemma par_beta_refl:
fixes t
assumes "lc t"
shows "t ⇒⇩β t"
using assms
proof -
define pred_cof
where "pred_cof L t ⟷
(∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t'. (t⇗[Fvar s, Fvar p]⇖) ⇒⇩β t' ∧ t = σ[s,p] t'))"
for L t
from assms show ?thesis
proof
(induct
taking: "λt. body t ∧ (∃L. finite L ∧ pred_cof L t)"
rule: lc_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case Upd thus ?case
unfolding pred_cof_def
by auto
next
case (Obj f T) note pred = this
define pred_fl where "pred_fl s p b l ⟷ (∃t'. (the b⇗[Fvar s, Fvar p]⇖) ⇒⇩β t' ∧ the b = σ[s,p]t')"
for s p b and l :: Label
from fmap_ex_cof[of f pred_fl] pred
obtain L where
"finite L" and "∀l∈dom f. body (the(f l))
∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ pred_fl s p (f l) l)"
unfolding pred_cof_def pred_fl_def
by auto
thus "Obj f T ⇒⇩β Obj f T"
unfolding pred_fl_def
by auto
next
case (Bnd L t) note pred = this(2)
with ‹finite L› show ?case
proof
(auto simp: body_def, unfold pred_cof_def,
rule_tac x = "L ∪ FV t" in exI, simp, clarify)
fix s p assume
"s ∉ L" and "p ∉ L" and "s ≠ p" and
"s ∉ FV t" and "p ∉ FV t"
from
this(1-3) pred
sclose_sopen_eq_t[OF this(4-5) this(3)]
show "∃t'. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t' ∧ t = σ[s,p] t'"
by (rule_tac x = "t⇗[Fvar s,Fvar p]⇖" in exI, simp add: openz_def closez_def)
qed
qed
qed
lemma par_beta_body_refl:
fixes u
assumes "body u"
shows "∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t'. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t' ∧ u = σ[s,p] t'))"
proof (rule_tac x = "FV u" in exI, simp, clarify)
fix s p assume "s ∉ FV u" and "p ∉ FV u" and "s ≠ p"
from
par_beta_refl[OF body_lc[OF assms lc_Fvar[of s] lc_Fvar[of p]]]
sclose_sopen_eq_t[OF this]
show "∃t'. (u⇗[Fvar s, Fvar p]⇖) ⇒⇩β t' ∧ u = σ[s,p] t'"
by (rule_tac x = "u⇗[Fvar s, Fvar p]⇖" in exI, simp add: openz_def closez_def)
qed
lemma par_beta_ssubst[rule_format]:
fixes t t'
assumes "t ⇒⇩β t'"
shows "∀x v v'. v ⇒⇩β v' ⟶ [x → v] t ⇒⇩β [x → v'] t'"
proof -
define pred_cof
where "pred_cof L t t' ⟷
(∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. t⇗[Fvar s, Fvar p]⇖ ⇒⇩β t'' ∧ t' = σ[s,p] t''))"
for L t t'
{
fix x v v' t t'
assume
"v ⇒⇩β v'" and
"∀x v v'. v ⇒⇩β v' ⟶ (∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v'] t'))"
hence
"∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v'] t')"
by auto
}note Lex = this
{
fix x v l and f :: "Label ⇒ sterm option"
assume "l ∈ dom f" hence "l ∈ dom (λl. ssubst_option x v (f l))"
by simp
}note domssubst = this
{
fix x v l T and f :: "Label ⇒ sterm option"
assume "lc (Obj f T)" and "lc v" from ssubst_preserves_lc[OF this]
have obj: "lc (Obj (λl. ssubst_option x v (f l)) T)" by simp
}note lcobj = this
from assms show ?thesis
proof
(induct
taking: "λt t'. ∀x v v'. v ⇒⇩β v'
⟶ (∃L. finite L
∧ pred_cof L ([x → v] t) ([x → v'] t'))"
rule: pbeta_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case (Upd t t' l u u') note pred_t = this(2) and pred_u = this(4)
show ?case
proof (intro strip)
fix x v v' assume "v ⇒⇩β v'"
from Lex[OF this pred_u]
obtain L where
"finite L" and "pred_cof L ([x → v] u) ([x → v'] u')"
by auto
with
ssubst_preserves_lc[of t v x]
ssubst_preserves_body[of u v x]
‹lc t› par_beta_lc[OF ‹v ⇒⇩β v'›] ‹body u›
‹v ⇒⇩β v'› pred_t
show "[x → v] Upd t l u ⇒⇩β [x → v'] Upd t' l u'"
unfolding pred_cof_def
by auto
qed
next
case (Upd' f f' T t t' l)
note pred_obj = this(2) and pred_t = this(3)
show ?case
proof (intro strip)
from ‹Obj f T ⇒⇩β Obj f' T› ‹l ∈ dom f› have "l ∈ dom f'" by auto
fix x v v' assume "v ⇒⇩β v'"
with
domssubst[OF ‹l ∈ dom f›]
ssubst_preserves_lc[of "Obj f T" v x]
ssubst_preserves_body[of t v x]
‹lc (Obj f T)› par_beta_lc[OF ‹v ⇒⇩β v'›] ‹body t›
pred_obj
have
"[x → v] Obj f T ⇒⇩β [x → v'] Obj f' T" and
"lc ([x → v] Obj f T)" and "body ([x → v] t)"
by auto
note lem =
pbeta_Upd'[OF this(1)[simplified] _ _
domssubst[OF ‹l ∈ dom f›]
this(2)[simplified] this(3)]
from Lex[OF ‹v ⇒⇩β v'› pred_t]
obtain L where
"finite L" and "pred_cof L ([x → v] t) ([x → v'] t')"
by auto
with lem[of L "[x → v'] t'"] ssubstoption_insert[OF ‹l ∈ dom f'›]
show "[x → v] Upd (Obj f T) l t ⇒⇩β [x → v'] Obj (f'(l ↦ t')) T"
unfolding pred_cof_def
by auto
qed
next
case (beta f f' T l p p')
note pred_obj = this(2) and pred_p = this(6)
show ?case
proof (intro strip)
fix x v v' assume "v ⇒⇩β v'"
from
par_beta_lc[OF this]
ssubst_preserves_lc[OF ‹lc p›]
have "lc v" and "lc v'" and "lc ([x → v] p)" by auto
note lem =
pbeta_beta[OF _ domssubst[OF ‹l ∈ dom f›] _
lcobj[OF ‹lc (Obj f T)› this(1)] this(3)]
from ‹Obj f T ⇒⇩β Obj f' T› have "dom f = dom f'" by auto
with ‹l ∈ dom f› have "the (ssubst_option x v' (f' l)) = [x → v'] the (f' l)"
by auto
with
lem[of x "λl. ssubst_option x v' (f' l)" "[x → v'] p'"]
‹v ⇒⇩β v'› pred_obj pred_p
ssubst_openz_distrib[OF ‹lc v'›]
show
"[x → v] Call (Obj f T) l p ⇒⇩β [x → v'] (the (f' l)⇗[Obj f' T, p']⇖)"
by simp
qed
next
case (Obj f f' T) note pred = fmap_ball_all3[OF this(1) this(3)]
show ?case
proof (intro strip)
fix x v v'
define pred_bnd
where "pred_bnd s p b b' l ⟷
(∃t''. [x → v] the b⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'' ∧ [x → v'] the b' = σ[s,p] t'')"
for s p b b' and l::Label
assume "v ⇒⇩β v'"
with pred ‹dom f' = dom f› fmap_ex_cof2[of f' f pred_bnd]
obtain L where
"finite L" and
predf: "∀l∈dom f. pred_cof L ([x → v] the (f l)) ([x → v'] the (f' l))"
unfolding pred_cof_def pred_bnd_def
by auto
have "∀l∈dom (λl. ssubst_option x v (f l)). body (the (ssubst_option x v (f l)))"
proof (intro strip, simp)
fix l' :: Label assume "l' ∈ dom f"
with ‹∀l∈dom f. body (the(f l))› have "body (the (f l'))" by blast
note ssubst_preserves_body[OF this]
from
this[of v x] par_beta_lc[OF ‹v ⇒⇩β v'›]
‹l' ∈ dom f› ssubst_option_lem[of f x v]
show "body (the (ssubst_option x v (f l')))" by auto
qed
note intro = pbeta_Obj[OF _ ‹finite L› _ this]
from
predf
ssubst_option_lem[of f x v]
ssubst_option_lem[of f' x v'] ‹dom f' = dom f›
dom_ssubstoption_lem[of x v f]
dom_ssubstoption_lem[of x v' f']
show "[x → v] Obj f T ⇒⇩β [x → v'] Obj f' T"
unfolding pred_cof_def
by (simp, intro intro[of "(λl. ssubst_option x v' (f' l))" T], auto)
qed
next
case (Bnd L t t') note pred = this(2)
show ?case
proof (intro strip)
fix x v v' assume "v ⇒⇩β v'"
from ‹finite L›
show "∃L. finite L ∧ pred_cof L ([x → v] t) ([x → v'] t')"
proof (rule_tac x = "L ∪ {x} ∪ FV v'" in exI,
unfold pred_cof_def, auto)
fix s p assume "s ∉ L" and "p ∉ L" and "s ≠ p"
with pred
obtain t'' where
"t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''" and
"∀x v v'. v ⇒⇩β v' ⟶ [x → v] (t⇗[Fvar s,Fvar p]⇖) ⇒⇩β [x → v'] t''" and
"t' = σ[s,p] t''"
by blast
from this(2) ‹v ⇒⇩β v'›
have ssubst_pbeta: "[x → v] (t⇗[Fvar s,Fvar p]⇖) ⇒⇩β [x → v'] t''" by blast
assume "s ≠ x" and "p ≠ x"
hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" by auto
from
ssubst_pbeta
par_beta_lc[OF ‹v ⇒⇩β v'›] ssubst_sopen_commute[OF _ this]
have "[x → v] t⇗[Fvar s,Fvar p]⇖ ⇒⇩β [x → v'] t''" by (simp add: openz_def)
moreover
assume "s ∉ FV v'" and "p ∉ FV v'"
from
ssubst_sclose_commute[OF this not_sym[OF ‹s ≠ x›]
not_sym[OF ‹p ≠ x›]]
‹t' = σ[s,p] t''›
have "[x → v'] t' = σ[s,p] [x → v'] t''" by (simp add: closez_def)
ultimately
show "∃t''. [x → v] t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'' ∧ [x → v'] t' = σ[s,p] t''"
by (rule_tac x = "[x → v'] t''" in exI, simp)
qed
qed
qed
qed
lemma renaming_par_beta: "t ⇒⇩β t' ⟹ [s → Fvar sa] t ⇒⇩β [s → Fvar sa] t'"
by (erule par_beta_ssubst, simp+)
lemma par_beta_beta:
fixes l f f' u u'
assumes
"l ∈ dom f" and "Obj f T ⇒⇩β Obj f' T" and "u ⇒⇩β u'" and "lc (Obj f T)" and "lc u"
shows "(the(f l)⇗[Obj f T, u]⇖) ⇒⇩β (the(f' l)⇗[Obj f' T, u']⇖)"
proof -
from Obj_pbeta[OF ‹Obj f T ⇒⇩β Obj f' T›]
obtain L where
"dom f = dom f'" and
"finite L" and
pred_sp: "∀l∈dom f.∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t''. the (f l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''
∧ the (f' l) = σ[s,p] t'')" and
"∀l∈dom f. body (the (f l))"
by auto
from this(2) finite_FV[of "Obj f T"] have fin: "finite (L ∪ FV (Obj f T) ∪ FV u)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where
sp: "s ∉ L ∪ FV (Obj f T) ∪ FV u ∧ p ∉ L ∪ FV (Obj f T) ∪ FV u ∧ s ≠ p"
by auto
with ‹l ∈ dom f› obtain t'' where
"the (f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t''" and "the (f' l) = σ[s,p] t''"
using pred_sp by blast
from par_beta_lc[OF this(1)] have "lc t''" by simp
from
sopen_sclose_eq_t[OF this]
‹the (f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t''› ‹the(f' l) = σ[s,p] t''›
have "the (f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β (the (f' l)⇗[Fvar s, Fvar p]⇖)"
by (simp add: openz_def closez_def)
from par_beta_ssubst[OF this] ‹u ⇒⇩β u'›
have "[p → u] (the (f l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β [p → u'] (the (f' l)⇗[Fvar s, Fvar p]⇖)"
by simp
note par_beta_ssubst[OF this ‹Obj f T ⇒⇩β Obj f' T›]
moreover
from ‹l ∈ dom f› sp
have "s ∉ FV (the(f l))" and "p ∉ FV (the(f l))" and "s ≠ p" and "s ∉ FV u"
by force+
note ssubst_intro[OF this]
moreover
from ‹l ∈ dom f› ‹dom f = dom f'› have "l ∈ dom f'" by force
with
par_beta_preserves_FV[OF ‹Obj f T ⇒⇩β Obj f' T›]
par_beta_preserves_FV[OF ‹u ⇒⇩β u'›] sp FV_option_lem[of f']
have "s ∉ FV (the (f' l))" and "p ∉ FV (the (f' l))" and "s ≠ p" and "s ∉ FV u'"
by auto
note ssubst_intro[OF this]
ultimately
show "the (f l)⇗[Obj f T, u]⇖ ⇒⇩β (the (f' l)⇗[Obj f' T, u']⇖)"
by (simp add: openz_def closez_def)
qed
subsection ‹Inclusions›
text ‹‹beta ⊆ par_beta ⊆ beta^*› \medskip›
lemma beta_subset_par_beta: "beta ≤ par_beta"
proof (clarify)
define pred_cof
where "pred_cof L t t' ⟷
(∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. (t⇗[Fvar s, Fvar p]⇖) ⇒⇩β t'' ∧ t' = σ[s,p] t''))"
for L t t'
fix t t' assume "t →⇩β t'" thus "t ⇒⇩β t'"
proof
(induct
taking: "λt t'. body t ∧ body t' ∧ (∃L. finite L ∧ pred_cof L t t')"
rule: beta_induct)
case CallL thus ?case by (simp add: par_beta_refl)
next
case CallR thus ?case by (simp add: par_beta_refl)
next
case beta thus ?case by (simp add: par_beta_refl)
next
case UpdL
from
par_beta_lc[OF this(2)] this(2)
par_beta_body_refl[OF this(3)] this(3)
show ?case by auto
next
case (UpdR t t' u l)
from this(1) obtain L where
"finite L" and "pred_cof L t t'" and "body t"
by auto
from
this(2) pbeta_Upd[OF par_beta_refl[OF ‹lc u›] ‹lc u› this(1) _ this(3)]
show ?case
unfolding pred_cof_def
by auto
next
case (Upd l f T t)
from par_beta_body_refl[OF ‹body t›]
obtain L where
"finite L" and
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ (∃t'. t⇗[Fvar s, Fvar p]⇖ ⇒⇩β t' ∧ t = σ[s,p] t')"
by auto
from
pbeta_Upd'[OF par_beta_refl[OF ‹lc (Obj f T)›] this
‹l ∈ dom f› ‹lc (Obj f T)› ‹body t›]
show ?case by assumption
next
case (Obj l f t t' T) note cof = this(2) and body = this(3)
from cof obtain L where
"body t" and "finite L" and "pred_cof L t t'"
by auto
from body have "lc (Obj f T)" by (simp add: lc_obj)
from
Obj_pbeta_subst[OF ‹finite L› _ par_beta_refl[OF this] this ‹body t›]
‹pred_cof L t t'›
show ?case
unfolding pred_cof_def
by auto
next
case (Bnd L t t') note pred = this(2)
from ‹finite L› exFresh_s_p_cof[of "L ∪ FV t"]
obtain s p where
"s ∉ L" and "p ∉ L" and "s ≠ p" and
"s ∉ FV t" and "p ∉ FV t"
by auto
with pred obtain t'' where
"t⇗[Fvar s, Fvar p]⇖ ⇒⇩β t''" and "t' = σ[s,p] t''"
by blast
from
par_beta_lc[OF this(1)] this(2) lc_body[OF _ ‹s ≠ p›]
have "body σ[s,p](t⇗[Fvar s, Fvar p]⇖)" and "body t'" by auto
from this(1) sclose_sopen_eq_t[OF ‹s ∉ FV t› ‹p ∉ FV t› ‹s ≠ p›]
have "body t" by (simp add: openz_def closez_def)
with ‹body t'› ‹finite L› pred show ?case
unfolding pred_cof_def
by (simp, rule_tac x = L in exI, auto)
qed
qed
lemma par_beta_subset_beta: "par_beta ≤ beta^**"
proof (rule predicate2I)
define pred_cof
where "pred_cof L t t' ⟷
(∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ (∃t''. (t⇗[Fvar s, Fvar p]⇖) →⇩β⇧* t'' ∧ t' = σ[s,p] t''))"
for L t t'
fix x y assume "x ⇒⇩β y" thus "x →⇩β⇧* y"
proof (induct
taking: "λt t'. body t' ∧ (∃L. finite L ∧ pred_cof L t t')"
rule: pbeta_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by auto
next
case (Upd t t' l u u')
from this(4) obtain L where
"finite L" and "pred_cof L u u'" by auto
from
this(2)
rtrancl_beta_Upd[OF ‹t →⇩β⇧* t'› this(1) _ ‹lc t› ‹body u›]
show ?case
unfolding pred_cof_def
by simp
next
case (Upd' f f' T t t' l)
from this(3) obtain L where
"body t'" and "finite L" and "pred_cof L t t'" by auto
from
this(3)
rtrancl_beta_Upd[OF ‹Obj f T →⇩β⇧* Obj f' T› ‹finite L› _
‹lc (Obj f T)› ‹body t›]
have rtranclp: "Upd (Obj f T) l t →⇩β⇧* Upd (Obj f' T) l t'"
unfolding pred_cof_def
by simp
from
Obj_pbeta[OF ‹Obj f T ⇒⇩β Obj f' T›] ‹l ∈ dom f›
par_beta_lc[OF ‹Obj f T ⇒⇩β Obj f' T›]
have "l ∈ dom f'" and "lc (Obj f' T)" by auto
from beta_Upd[OF this ‹body t'›] rtranclp
show ?case by simp
next
case (Obj f f' T) note body = this(2) and pred = this(3)
define pred_bnd
where "pred_bnd s p b b' l ⟷ (∃t''. the b⇗[Fvar s,Fvar p]⇖ →⇩β⇧* t'' ∧ the b' = σ[s,p] t'')"
for s p b b' and l::Label
from
pred ‹dom f' = dom f› fmap_ex_cof2[of f' f pred_bnd]
obtain L where
"finite L" and
"∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ pred_bnd s p (f l) (f' l) l"
unfolding pred_cof_def pred_bnd_def
by auto
from
this(2)
rtrancl_beta_obj_n[OF ‹finite L› _ sym[OF ‹dom f' = dom f›] body]
show ?case
unfolding pred_bnd_def
by simp
next
case (beta f f' T l p p')
note
rtrancl_beta_Call[OF ‹Obj f T →⇩β⇧* Obj f' T› ‹lc (Obj f T)›
‹p →⇩β⇧* p'› ‹lc p›]
moreover
from
Obj_pbeta[OF ‹Obj f T ⇒⇩β Obj f' T›] ‹l ∈ dom f›
par_beta_lc[OF ‹Obj f T ⇒⇩β Obj f' T›]
par_beta_lc[OF ‹p ⇒⇩β p'›]
have "l ∈ dom f'" and "lc (Obj f' T)" and "lc p'" by auto
note beta.beta[OF this]
ultimately
show ?case
by (auto simp: rtranclp.rtrancl_into_rtrancl[of _ _ "Call (Obj f' T) l p'"])
next
case (Bnd L t t') note pred = this(2)
hence "pred_cof L t t'"
unfolding pred_cof_def
by blast
moreover
from pred ‹finite L› par_beta_body[of L t t']
have "body t'" by blast
ultimately
show ?case
using ‹finite L›
by auto
qed
qed
subsection ‹Confluence (directly)›
lemma diamond_binder:
fixes L1 L2 t ta tb
assumes
"finite L1" and
pred_L1: "∀s p. s ∉ L1 ∧ p ∉ L1 ∧ s ≠ p
⟶ (∃t'. (t⇗[Fvar s, Fvar p]⇖ ⇒⇩β t'
∧ (∀z. (t⇗[Fvar s, Fvar p]⇖ ⇒⇩β z) ⟶ (∃u. t' ⇒⇩β u ∧ z ⇒⇩β u)))
∧ ta = σ[s,p]t')" and
"finite L2" and
pred_L2: "∀s p. s ∉ L2 ∧ p ∉ L2 ∧ s ≠ p
⟶ (∃t'. t⇗[Fvar s, Fvar p]⇖ ⇒⇩β t' ∧ tb = σ[s,p]t')"
shows
"∃L'. finite L'
∧ (∃t''. (∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃u. ta⇗[Fvar s, Fvar p]⇖ ⇒⇩β u ∧ t'' = σ[s,p]u))
∧ (∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃u. tb⇗[Fvar s, Fvar p]⇖ ⇒⇩β u ∧ t'' = σ[s,p]u)))"
proof -
from ‹finite L1› ‹finite L2› have "finite (L1 ∪ L2)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where sp: "s ∉ L1 ∪ L2 ∧ p ∉ L1 ∪ L2 ∧ s ≠ p" by auto
with pred_L1
obtain t' where
"t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'" and
"∀z. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β z ⟶ (∃u. t' ⇒⇩β u ∧ z ⇒⇩β u)" and
"ta = σ[s,p] t'"
by blast
from sp pred_L2 obtain t'' where "t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''" and "tb = σ[s,p] t''"
by blast
from ‹∀z. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β z ⟶ (∃u. t' ⇒⇩β u ∧ z ⇒⇩β u)› this(1)
obtain u where "t' ⇒⇩β u" and "t'' ⇒⇩β u" by blast
from ‹finite L1› ‹finite L2› have "finite (L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p})" by simp
moreover
{
fix x :: sterm and y :: sterm
assume "t⇗[Fvar s, Fvar p]⇖ ⇒⇩β y" and "x = σ[s,p] y" and "y ⇒⇩β u"
hence
"∀sa pa. sa ∉ L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p}
∧ pa ∉ L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
⟶ (∃t. x⇗[Fvar sa,Fvar pa]⇖ ⇒⇩β t ∧ σ[s,p] u = σ[sa,pa] t)"
proof (intro strip)
fix sa :: fVariable and pa :: fVariable
assume
sapa: "sa ∉ L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p}
∧ pa ∉ L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
with sp par_beta_lc[OF ‹y ⇒⇩β u›]
have "s ≠ p" and "s ∉ FV (Fvar pa)" and "lc y" and "lc u" by auto
from
sopen_sclose_eq_ssubst[OF this(1-3)]
sopen_sclose_eq_ssubst[OF this(1-2) this(4)]
renaming_par_beta ‹x = σ[s,p] y› ‹y ⇒⇩β u›
have "x⇗[Fvar sa, Fvar pa]⇖ ⇒⇩β (σ[s,p] u⇗[Fvar sa, Fvar pa]⇖)"
by (auto simp: openz_def closez_def)
moreover
from
sapa par_beta_preserves_FV[OF ‹t ⇗[Fvar s,Fvar p]⇖ ⇒⇩β y›]
sopen_FV[of 0 "Fvar s" "Fvar p" t]
par_beta_preserves_FV[OF ‹y ⇒⇩β u›]
sclose_subset_FV[of 0 s p u]
have "sa ∉ FV (σ[s,p] u)" and "pa ∉ FV (σ[s,p] u)" and "sa ≠ pa"
by (auto simp: openz_def closez_def)
from sym[OF sclose_sopen_eq_t[OF this]]
have "σ[s,p] u = σ[sa,pa] (σ[s,p] u⇗[Fvar sa, Fvar pa]⇖)"
by (simp add: openz_def closez_def)
ultimately show "∃t. x⇗[Fvar sa,Fvar pa]⇖ ⇒⇩β t ∧ σ[s,p] u = σ[sa,pa] t"
by blast
qed
}note
this[OF ‹t ⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'› ‹ta = σ[s,p] t'› ‹t' ⇒⇩β u›]
this[OF ‹t ⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''› ‹tb = σ[s,p] t''› ‹t'' ⇒⇩β u›]
ultimately
show
"∃L'. finite L'
∧ (∃t''. (∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t'. ta⇗[Fvar s,Fvar p]⇖ ⇒⇩β t' ∧ t'' = σ[s,p] t'))
∧ (∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t'. tb⇗[Fvar s,Fvar p]⇖ ⇒⇩β t' ∧ t'' = σ[s,p] t')))"
by (rule_tac x = "L1 ∪ L2 ∪ FV t ∪ {s} ∪ {p}" in exI, simp, blast)
qed
lemma exL_exMap_lem:
fixes
f :: "Label -~> sterm" and
lz :: "Label -~> sterm" and f' :: "Label -~> sterm"
assumes "dom f = dom lz" and "dom f' = dom f"
shows
"∀L1 L2. finite L1
⟶ (∀l∈dom f. ∀s p. s ∉ L1 ∧ p ∉ L1 ∧ s ≠ p
⟶ (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t
∧ (∀z. (the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β z)
⟶ (∃u. t ⇒⇩β u ∧ z ⇒⇩β u)))
∧ the(f' l) = σ[s,p]t))
⟶ finite L2
⟶ (∀l∈dom f. ∀s p. s ∉ L2 ∧ p ∉ L2 ∧ s ≠ p
⟶ (∃t. the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t ∧ the(lz l) = σ[s,p]t))
⟶ (∃L'. finite L'
∧ (∃lu. dom lu = dom f
∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. (the(f' l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(lu l) = σ[s,p]t))
∧ (∀l∈dom f. body (the (f' l)))
∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. (the(lz l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(lu l) = σ[s,p]t))
∧ (∀l∈dom f. body (the (lz l)))))"
using assms
proof (induct rule: fmap_induct3)
case empty thus ?case by force
next
case (insert x a b c F1 F2 F3) thus ?case
proof (intro strip)
fix L1 :: "fVariable set" and L2 :: "fVariable set"
{
fix
L :: "fVariable set" and
t :: sterm and F :: "Label -~> sterm" and
P :: "sterm ⇒ sterm ⇒ fVariable ⇒ fVariable ⇒ bool"
assume
"dom F1 = dom F" and
*: "∀l∈dom (F1(x ↦ a)).
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ P (the ((F1(x ↦ a)) l)) (the ((F(x ↦ t)) l)) s p"
hence
F: "∀l∈dom F1. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
⟶ P (the(F1 l)) (the(F l)) s p"
proof (intro strip)
fix l :: Label and s :: fVariable and p :: fVariable
assume "l ∈ dom F1" hence "l ∈ dom (F1(x ↦ a))" by simp
moreover assume "s ∉ L ∧ p ∉ L ∧ s ≠ p"
ultimately
have "P (the((F1(x ↦ a)) l)) (the((F(x ↦ t)) l)) s p"
using * by blast
moreover from ‹x ∉ dom F1› ‹l ∈ dom F1› have "l ≠ x" by auto
ultimately show "P (the(F1 l)) (the(F l)) s p" by force
qed
from * have "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p ⟶ P a t s p" by auto
note this F
}
note pred = this
note
tmp =
pred[of _ L1 "(λt t' s p.
∃t''. (t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t''
∧ (∀z. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β z ⟶ (∃u. t'' ⇒⇩β u ∧ z ⇒⇩β u)))
∧ t' = σ[s,p] t'')"]
note predc = tmp(1) note predF3 = tmp(2)
note tmp = pred[of _ L2
"(λt t' s p. ∃t''. t⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'' ∧ t' = σ[s,p] t'')"]
note predb = tmp(1) note predF2 = tmp(2)
assume
a: "∀l∈dom (F1(x ↦ a)). ∀s p. s ∉ L1 ∧ p ∉ L1 ∧ s ≠ p
⟶ (∃t. (the ((F1(x ↦ a)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ (∀z. the ((F1(x ↦ a)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β z
⟶ (∃u. t ⇒⇩β u ∧ z ⇒⇩β u)))
∧ the ((F3(x ↦ c)) l) = σ[s,p] t)" and
b: "∀l∈dom (F1(x ↦ a)). ∀s p. s ∉ L2 ∧ p ∉ L2 ∧ s ≠ p
⟶ (∃t. the ((F1(x ↦ a)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the ((F2(x ↦ b)) l) = σ[s,p] t)" and
"finite L1" and "finite L2"
from
diamond_binder[OF this(3) predc[OF sym[OF ‹dom F3 = dom F1›] this(1)]
this(4) predb[OF ‹dom F1 = dom F2› this(2)]]
obtain La t where
"finite La" and
pred_c: "∀s p. s ∉ La ∧ p ∉ La ∧ s ≠ p
⟶ (∃u. c⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ t = σ[s,p] u)" and
pred_b: "∀s p. s ∉ La ∧ p ∉ La ∧ s ≠ p
⟶ (∃u. b⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ t = σ[s,p] u)"
by blast
{
from this(1) have "finite (La ∪ FV c ∪ FV b)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where
sp: "s ∉ La ∪ FV c ∪ FV b ∧ p ∉ La ∪ FV c ∪ FV b ∧ s ≠ p"
by auto
with pred_c obtain u where "c⇗[Fvar s,Fvar p]⇖ ⇒⇩β u" by blast
from par_beta_lc[OF this] have "lc (c⇗[Fvar s,Fvar p]⇖)" by simp
with lc_body[of "c⇗[Fvar s,Fvar p]⇖" s p] sp sclose_sopen_eq_t[of s c p 0]
have c: "body c" by (auto simp: closez_def openz_def)
from sp pred_b obtain u where "b⇗[Fvar s,Fvar p]⇖ ⇒⇩β u" by blast
from par_beta_lc[OF this] have "lc (b⇗[Fvar s,Fvar p]⇖)" by simp
with lc_body[of "b⇗[Fvar s,Fvar p]⇖" s p] sp sclose_sopen_eq_t[of s b p 0]
have "body b" by (auto simp: closez_def openz_def)
note c this
}note bodycb = this
from
predF3[OF sym[OF ‹dom F3 = dom F1›] a]
predF2[OF ‹dom F1 = dom F2› b]
‹finite L1› ‹finite L2›
have
"∃L'. finite L'
∧ (∃lu. dom lu = dom F1
∧ (∀l∈dom F1. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. the (F3 l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (lu l) = σ[s,p] t))
∧ (∀l∈dom F1. body (the (F3 l)))
∧ (∀l∈dom F1. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. the (F2 l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (lu l) = σ[s,p] t))
∧ (∀l∈dom F1. body (the (F2 l))))"
by (rule_tac x = L1 in allE[OF insert(1)], simp)
then obtain Lb f where
"finite Lb" and "dom f = dom F1" and
pred_F3: "∀l∈dom F1. ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p
⟶ (∃t. the (F3 l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (f l) = σ[s,p] t)" and
body_F3: "∀l∈dom F1. body (the (F3 l))" and
pred_F2: "∀l∈dom F1. ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p
⟶ (∃t. the (F2 l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (f l) = σ[s,p] t)" and
body_F2: "∀l∈dom F1. body (the (F2 l))"
by auto
from ‹finite La› ‹finite Lb› have "finite (La ∪ Lb)" by simp
moreover
from ‹dom f = dom F1› have "dom (f(x ↦ t)) = dom (F1(x ↦ a))" by simp
moreover
from pred_c pred_F3
have
"∀l∈dom (F1(x ↦ a)). ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p
⟶ (∃t'. the ((F3(x ↦ c)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'
∧ the ((f(x ↦ t)) l) = σ[s,p] t')"
by auto
moreover
from bodycb(1) body_F3
have "∀l∈dom (F1(x ↦ a)). body (the ((F3(x ↦ c)) l))"
by simp
moreover
from pred_b pred_F2
have
"∀l∈dom (F1(x ↦ a)). ∀s p. s ∉ La ∪ Lb ∧ p ∉ La ∪ Lb ∧ s ≠ p
⟶ (∃t'. the ((F2(x ↦ b)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'
∧ the ((f(x ↦ t)) l) = σ[s,p] t')"
by auto
moreover
from bodycb(2) body_F2
have "∀l∈dom (F1(x ↦ a)). body (the ((F2(x ↦ b)) l))"
by simp
ultimately
show
"∃L'. finite L'
∧ (∃lu. dom lu = dom (F1(x ↦ a))
∧ (∀l∈dom (F1(x ↦ a)).
∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t'. the ((F3(x ↦ c)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'
∧ the (lu l) = σ[s,p] t'))
∧ (∀l∈dom (F1(x ↦ a)). body (the ((F3(x ↦ c)) l)))
∧ (∀l∈dom (F1(x ↦ a)).
∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t'. the ((F2(x ↦ b)) l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t'
∧ the (lu l) = σ[s,p] t'))
∧ (∀l∈dom (F1(x ↦ a)). body (the ((F2(x ↦ b)) l))))"
by (rule_tac x = "La ∪ Lb" in exI,
simp (no_asm_simp) only: conjI simp_thms(22),
rule_tac x = "(f(x ↦ t))" in exI, simp)
qed
qed
lemma exL_exMap:
"⟦ dom (f::Label -~> sterm) = dom (lz::Label -~> sterm);
dom (f'::Label -~> sterm) = dom f;
finite L1;
∀l∈dom f. ∀s p. s ∉ L1 ∧ p ∉ L1 ∧ s ≠ p
⟶ (∃t. (the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t
∧ (∀z. (the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β z) ⟶ (∃u. t ⇒⇩β u ∧ z ⇒⇩β u)))
∧ the(f' l) = σ[s,p]t);
finite L2;
∀l∈dom lz. ∀s p. s ∉ L2 ∧ p ∉ L2 ∧ s ≠ p
⟶ (∃t. the(f l)⇗[Fvar s, Fvar p]⇖ ⇒⇩β t ∧ the(lz l) = σ[s,p]t) ⟧
⟹ ∃L'. finite L'
∧ (∃lu. dom lu = dom f
∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. (the(f' l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(lu l) = σ[s,p]t))
∧ (∀l∈dom f. body (the (f' l)))
∧ (∀l∈dom f. ∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃t. (the(lz l)⇗[Fvar s, Fvar p]⇖) ⇒⇩β t
∧ the(lu l) = σ[s,p]t))
∧ (∀l∈dom f. body (the (lz l))))"
using exL_exMap_lem[of f lz f'] by simp
lemma diamond_par_beta: "diamond par_beta"
unfolding diamond_def commute_def square_def
proof (rule impI [THEN allI [THEN allI]])
fix x y assume "x ⇒⇩β y"
thus "∀z. x ⇒⇩β z ⟶ (∃u. y ⇒⇩β u ∧ z ⇒⇩β u)"
proof (induct rule: par_beta.induct)
case pbeta_Fvar thus ?case by simp
next
case (pbeta_Upd t t' L u u' l)
note pred_t = this(2) and pred_u = this(5)
show ?case
proof (intro strip)
fix z assume "Upd t l u ⇒⇩β z"
thus "∃u. Upd t' l u' ⇒⇩β u ∧ z ⇒⇩β u"
proof (induct rule: Upd_par_red)
case (upd ta ua La)
from
diamond_binder[OF ‹finite L› pred_u this(2-3)]
this(1) pred_t
par_beta_lc[OF this(1)] par_beta_lc[OF ‹t ⇒⇩β t'›]
obtain L' ub tb where
"t' ⇒⇩β tb" and "lc t'" and "ta ⇒⇩β tb" and
"lc ta" and "finite L'" and
"∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃u. u'⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ ub = σ[s,p] u)" and
"∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
⟶ (∃u. ua⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ ub = σ[s,p] u)"
by auto
from
par_beta.pbeta_Upd[OF this(1-2) this(5-6)]
par_beta.pbeta_Upd[OF this(3-5) this(7)]
par_beta_body[OF this(5-6)]
par_beta_body[OF this(5) this(7)] ‹z = Upd ta l ua›
show ?case by (force simp: exI[of _ "Upd tb l ub"])
next
case (obj f fa T ua La)
from diamond_binder[OF ‹finite L› pred_u this(4-5)]
obtain Lb ub where
"finite Lb" and
ub1: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. ua⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ ub = σ[s,p] u)" and
ub2: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. u'⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ ub = σ[s,p] u)"
by auto
from ‹Obj f T = t› ‹Obj f T ⇒⇩β Obj fa T›
have "t ⇒⇩β Obj fa T" by simp
with pred_t obtain a where "t' ⇒⇩β a" "Obj fa T ⇒⇩β a"
by auto
with
par_beta_lc[OF this(2)]
par_beta_body[OF ‹finite Lb› ub1]
obtain fb where
"t' ⇒⇩β Obj fb T" and "Obj fa T ⇒⇩β Obj fb T" and
"lc (Obj fa T)" and "body ua"
by auto
from Obj_pbeta_subst[OF ‹finite Lb› ub1 this(2-4)]
have "Obj (fa(l ↦ ua)) T ⇒⇩β Obj (fb(l ↦ ub)) T" by assumption
moreover
from
‹t ⇒⇩β t'› ‹Obj f T = t›
par_beta_lc[OF ‹t ⇒⇩β t'›] ‹t' ⇒⇩β Obj fb T›
par_beta_body[OF ‹finite Lb› ub2]
obtain f' where
"t' = Obj f' T" and "Obj f' T ⇒⇩β Obj fb T" and
"lc (Obj f' T)" and "body u'"
by auto
note par_beta.pbeta_Upd'[OF this(2) ‹finite Lb› ub2 _ this(3-4)]
moreover
from
‹t ⇒⇩β t'› ‹Obj f T = t› ‹t' = Obj f' T›
‹l ∈ dom f› Obj_pbeta[of f T f']
have "l ∈ dom f'" by simp
ultimately
show ?case
using ‹z = Obj (fa(l ↦ ua)) T› ‹t' = Obj f' T›
by (rule_tac x = "Obj (fb(l ↦ ub)) T" in exI, simp)
qed
qed
next
case (pbeta_Obj f' f L T) note pred = this(3)
show ?case
proof (clarify)
fix fa La
assume
"dom fa = dom f" and "finite La" and
"∀l∈dom f. ∀s p. s ∉ La ∧ p ∉ La ∧ s ≠ p
⟶ (∃t. the (f l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (fa l) = σ[s,p] t)"
from
exL_exMap[OF sym[OF this(1)] ‹dom f' = dom f›
‹finite L› pred this(2)]
this(1) this(3) ‹dom f' = dom f›
obtain Lb fb where
"dom fb = dom f'" and "dom fb = dom fa" and "finite Lb" and
"∀l∈dom f'. ∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃t. the (f' l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (fb l) = σ[s,p] t)" and
"∀l∈dom f'. body (the (f' l))" and
"∀l∈dom fa. ∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃t. the (fa l)⇗[Fvar s,Fvar p]⇖ ⇒⇩β t
∧ the (fb l) = σ[s,p] t)" and
"∀l∈dom fa. body (the (fa l))"
by auto
from
par_beta.pbeta_Obj[OF this(1) this(3-5)]
par_beta.pbeta_Obj[OF this(2) this(3) this(6-7)]
show "∃u. Obj f' T ⇒⇩β u ∧ Obj fa T ⇒⇩β u"
by (rule_tac x = "Obj fb T" in exI, simp)
qed
next
case (pbeta_Upd' f T f' L t t' l)
note pred_obj = this(2) and pred_bnd = this(4)
show ?case
proof (clarify)
fix z assume "Upd (Obj f T) l t ⇒⇩β z"
thus "∃u. Obj (f'(l ↦ t')) T ⇒⇩β u ∧ z ⇒⇩β u"
proof (induct rule: Upd_par_red)
case (upd a ta La) note pred_ta = this(3)
from ‹Obj f T ⇒⇩β a› ‹z = Upd a l ta›
obtain fa where
"Obj f T ⇒⇩β Obj fa T" and "z = Upd (Obj fa T) l ta"
by auto
from this(1) pred_obj
obtain b where "Obj f' T ⇒⇩β b" and "Obj fa T ⇒⇩β b"
by (elim allE impE exE conjE, simp)
with
par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
obtain fb where
"Obj f' T ⇒⇩β Obj fb T" and "lc (Obj f' T)" and
"Obj fa T ⇒⇩β Obj fb T" and "lc (Obj fa T)"
by auto
from diamond_binder[OF ‹finite L› pbeta_Upd'(4) ‹finite La› pred_ta]
obtain Lb tb where
"finite Lb" and
cb1: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. t'⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ tb = σ[s,p] u)" and
cb2: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. ta⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ tb = σ[s,p] u)"
by auto
from
par_beta_body[OF this(1-2)]
Obj_pbeta_subst[OF ‹finite Lb› cb1 ‹Obj f' T ⇒⇩β Obj fb T›
‹lc (Obj f' T)›]
have "Obj (f'(l ↦ t')) T ⇒⇩β Obj (fb(l ↦ tb)) T"
by simp
moreover
from Obj_pbeta[OF ‹Obj f T ⇒⇩β Obj fa T›] ‹l ∈ dom f›
have "l ∈ dom fa" by simp
from
par_beta_body[OF ‹finite Lb› cb2]
par_beta.pbeta_Upd'[OF ‹Obj fa T ⇒⇩β Obj fb T› ‹finite Lb›
cb2 this ‹lc (Obj fa T)›]
have "Upd (Obj fa T) l ta ⇒⇩β Obj (fb(l ↦ tb)) T" by simp
ultimately
show ?case
using ‹z = Upd (Obj fa T) l ta›
by (rule_tac x = "Obj (fb(l ↦ tb)) T" in exI, simp)
next
case (obj f'' fa T' ta La)
note pred_ta = this(5) and this
hence
"l ∈ dom f" and "Obj f T ⇒⇩β Obj fa T" and
"z = Obj (fa(l ↦ ta)) T"
by auto
from diamond_binder[OF ‹finite L› pred_bnd ‹finite La› pred_ta]
obtain Lb tb where
"finite Lb" and
tb1: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. t'⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ tb = σ[s,p] u)" and
tb2: "∀s p. s ∉ Lb ∧ p ∉ Lb ∧ s ≠ p
⟶ (∃u. ta⇗[Fvar s,Fvar p]⇖ ⇒⇩β u ∧ tb = σ[s,p] u)"
by auto
from ‹Obj f T ⇒⇩β Obj fa T› pred_obj
obtain b where "Obj f' T ⇒⇩β b" and "Obj fa T ⇒⇩β b"
by (elim allE impE exE conjE, simp)
with par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
obtain fb where
"Obj f' T ⇒⇩β Obj fb T" "lc (Obj f' T)" and
"Obj fa T ⇒⇩β Obj fb T" "lc (Obj fa T)"
by auto
from
par_beta_body[OF ‹finite Lb› tb1]
Obj_pbeta_subst[OF ‹finite Lb› tb1 this(1-2)]
par_beta_body[OF ‹finite Lb› tb2]
Obj_pbeta_subst[OF ‹finite Lb› tb2 this(3-4)]
have
"Obj (f'(l ↦ t')) T ⇒⇩β Obj (fb(l ↦ tb)) T" and
"Obj (fa(l ↦ ta)) T ⇒⇩β Obj (fb(l ↦ tb)) T"
by simp+
with ‹z = Obj (fa(l ↦ ta)) T› show ?case
by (rule_tac x = "Obj (fb(l ↦ tb)) T" in exI, simp)
qed
qed
next
case (pbeta_Call t t' u u' l)
note pred_t = this(2) and pred_u = this(4)
show ?case
proof (intro strip)
fix z assume "Call t l u ⇒⇩β z"
thus "∃u. Call t' l u' ⇒⇩β u ∧ z ⇒⇩β u"
proof (induct rule: Call_par_red)
case (call ta ua)
from
this(1-2) pred_t pred_u
obtain tb ub where "t' ⇒⇩β tb" "u' ⇒⇩β ub" "ta ⇒⇩β tb" "ua ⇒⇩β ub"
by (elim allE impE exE conjE, simp)
from
par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
par_beta.pbeta_Call[OF this(1-2)]
par_beta_lc[OF this(3)] par_beta_lc[OF this(4)]
par_beta.pbeta_Call[OF this(3-4)]
‹z = Call ta l ua›
show ?case
by (rule_tac x = "Call tb l ub" in exI, simp)
next
case (beta f fa T ua)
from this(1-2) have "t ⇒⇩β Obj fa T" by simp
with ‹u ⇒⇩β ua› pred_t pred_u
obtain b ub where
"t' ⇒⇩β b" and "Obj fa T ⇒⇩β b" and "u' ⇒⇩β ub" and "ua ⇒⇩β ub"
by (elim allE impE exE conjE, simp)
from this(1-2) par_beta_lc[OF this(2)]
obtain fb where
"t' ⇒⇩β Obj fb T" and
"Obj fa T ⇒⇩β Obj fb T" and "lc (Obj fa T)"
by auto
from
par_beta_beta[OF ‹l ∈ dom fa› this(2) ‹ua ⇒⇩β ub› this(3)]
par_beta_lc[OF ‹ua ⇒⇩β ub›]
have "the (fa l)⇗[Obj fa T,ua]⇖ ⇒⇩β (the (fb l)⇗[Obj fb T,ub]⇖)" by simp
moreover
from ‹l ∈ dom fa› Obj_pbeta[OF ‹Obj fa T ⇒⇩β Obj fb T›]
have "l ∈ dom fb" by simp
from
‹t ⇒⇩β t'› sym[OF ‹Obj f T = t›]
par_beta_lc[OF ‹t ⇒⇩β t'›] ‹t' ⇒⇩β Obj fb T›
obtain f' where
"t' = Obj f' T" and "Obj f' T ⇒⇩β Obj fb T" and
"lc (Obj f' T)"
by auto
from
Obj_pbeta[OF this(2)] ‹l ∈ dom fb›
par_beta.pbeta_beta[OF this(2) _ ‹u' ⇒⇩β ub› this(3)]
par_beta_lc[OF ‹u' ⇒⇩β ub›]
have "Call (Obj f' T) l u' ⇒⇩β (the (fb l)⇗[Obj fb T,ub]⇖)" by auto
ultimately
show ?case
using ‹t' = Obj f' T› ‹z = (the (fa l)⇗[Obj fa T,ua]⇖)›
by (rule_tac x = "(the (fb l)⇗[Obj fb T,ub]⇖)" in exI, simp)
qed
qed
next
case (pbeta_beta f T f' l p p')
note pred_obj = this(2) and pred_p = this(5)
show ?case
proof (intro strip)
fix z assume "Call (Obj f T) l p ⇒⇩β z"
thus "∃u. the (f' l)⇗[Obj f' T,p']⇖ ⇒⇩β u ∧ z ⇒⇩β u"
proof (induct rule: Call_par_red)
case (call a pa)
then obtain fa where
"Obj f T ⇒⇩β Obj fa T" and "z = Call (Obj fa T) l pa"
by auto
from
this(1) ‹p ⇒⇩β pa› pred_obj pred_p
obtain b pb where
"Obj f' T ⇒⇩β b" and "Obj fa T ⇒⇩β b" and
"p' ⇒⇩β pb" and "pa ⇒⇩β pb"
by (elim allE impE exE conjE, simp)
with par_beta_lc[OF this(1)] par_beta_lc[OF this(2)]
obtain fb where
"Obj f' T ⇒⇩β Obj fb T" and "lc (Obj f' T)" and
"Obj fa T ⇒⇩β Obj fb T" and "lc (Obj fa T)"
by auto
from this(1) ‹l ∈ dom f› ‹Obj f T ⇒⇩β Obj f' T› ‹Obj f T ⇒⇩β Obj fa T›
have "l ∈ dom f'" and "l ∈ dom fa" by auto
from ‹p' ⇒⇩β pb› ‹pa ⇒⇩β pb› par_beta_lc
have "p' ⇒⇩β pb" and "lc p'" and "pa ⇒⇩β pb" and "lc pa" by auto
from
par_beta.pbeta_beta[OF ‹Obj fa T ⇒⇩β Obj fb T› ‹l ∈ dom fa›
this(3) ‹lc (Obj fa T)› this(4)]
par_beta_beta[OF ‹l ∈ dom f'› ‹Obj f' T ⇒⇩β Obj fb T›
this(1) ‹lc (Obj f' T)› this(2)]
‹z = Call (Obj fa T) l pa›
show ?case
by (rule_tac x = "(the (fb l)⇗[Obj fb T,pb]⇖)" in exI, simp)
next
case (beta f'' fa Ta pa)
hence "Obj f T ⇒⇩β Obj fa T" and "z = (the (fa l)⇗[Obj fa T,pa]⇖)"
by auto
with ‹p ⇒⇩β pa› pred_obj pred_p
obtain b pb where
"Obj f' T ⇒⇩β b" and "Obj fa T ⇒⇩β b" and
"p' ⇒⇩β pb" and "pa ⇒⇩β pb"
by (elim allE impE exE conjE, simp)
with par_beta_lc
obtain fb where
"Obj f' T ⇒⇩β Obj fb T" and "lc (Obj f' T)" and "lc p'" and
"Obj fa T ⇒⇩β Obj fb T" and "lc (Obj fa T)" and "lc pa"
by auto
from ‹l ∈ dom f› ‹Obj f T ⇒⇩β Obj f' T› ‹Obj f T ⇒⇩β Obj fa T›
have "l ∈ dom f'" and "l ∈ dom fa" by auto
from
par_beta_beta[OF ‹l ∈ dom f'› ‹Obj f' T ⇒⇩β Obj fb T›
‹p' ⇒⇩β pb› ‹lc (Obj f' T)› ‹lc p'›]
par_beta_beta[OF ‹l ∈ dom fa› ‹Obj fa T ⇒⇩β Obj fb T›
‹pa ⇒⇩β pb› ‹lc (Obj fa T)› ‹lc pa›]
‹z = (the (fa l)⇗[Obj fa T,pa]⇖)›
show ?case
by (rule_tac x = "(the (fb l)⇗[Obj fb T,pb]⇖)" in exI, simp)
qed
qed
qed
qed
subsection ‹Confluence (classical not via complete developments)›
theorem beta_confluent: "confluent beta"
by (rule diamond_par_beta diamond_to_confluence
par_beta_subset_beta beta_subset_par_beta)+
end