header {* Locally Nameless representation of basic Sigma calculus enriched with formal parameter *}
theory Sigma
imports "../preliminary/FMap"
begin
subsection {* Infrastructure for the finite maps *}
axiomatization max_label :: nat where
LabelAvail: "max_label > 10"
definition "Label = {n :: nat. n ≤ max_label}"
typedef Label = Label
unfolding Label_def by auto
lemmas finite_Label_set = Finite_Set.finite_Collect_le_nat[of max_label]
lemma Univ_abs_label:
"(UNIV :: (Label set)) = Abs_Label ` {n :: nat. n ≤ max_label}"
proof -
have "∀x :: Label. x : Abs_Label ` {n :: nat. n ≤ max_label}"
proof
fix x :: Label
have "Rep_Label x ∈ {n. n ≤ max_label}"
by (fold Label_def, rule Rep_Label)
hence "Abs_Label (Rep_Label x) ∈ Abs_Label ` {n. n ≤ max_label}"
by (rule imageI)
thus "x ∈ Abs_Label ` {n. n ≤ max_label}"
by (simp add: Rep_Label_inverse)
qed
thus ?thesis by force
qed
lemma finite_Label: "finite (UNIV :: (Label set))"
by (simp add: Univ_abs_label finite_Label_set)
instance Label :: finite
proof
show "finite (UNIV :: (Label set))" by (rule finite_Label)
qed
consts
Lsuc :: "(Label set) => Label => Label"
Lmin :: "(Label set) => Label"
Lmax :: "(Label set) => Label"
definition Llt :: "[Label, Label] => bool" (infixl "<" 50) where
"Llt a b == Rep_Label a < Rep_Label b"
definition Lle :: "[Label, Label] => bool" (infixl "≤" 50) where
"Lle a b == Rep_Label a ≤ Rep_Label b"
definition Ltake_eq :: "[Label set, (Label ~=> 'a), (Label ~=> 'a)] => bool"
where "Ltake_eq L f g == ∀l∈L. f l = g l"
lemma Ltake_eq_all:
fixes f g
assumes "dom f = dom g" and "Ltake_eq (dom f) f g"
shows "f = g"
proof
fix x from assms show "f x = g x"
unfolding Ltake_eq_def
by (cases "x ∈ dom f", auto)
qed
lemma Ltake_eq_dom:
fixes L :: "Label set" and f :: "Label -~> 'a"
assumes "L ⊆ dom f" and "card L = card (dom f)"
shows "L = (dom f)"
proof (auto)
fix x :: Label assume "x ∈ L"
with in_mono[OF assms(1)] show "∃y. f x = Some y" by blast
next
fix x y assume "f x = Some y"
from card_seteq[OF finite_dom_fmap[of f] `L ⊆ dom f`] `card L = card (dom f)`
have "L = dom f" by simp
with `f x = Some y` show "x ∈ L" by force
qed
subsection {* Object-terms in Locally Nameless representation notation, beta-reduction and substitution *}
datatype type = Object "Label -~> (type × type)"
datatype bVariable = Self nat | Param nat
type_synonym fVariable = string
subsubsection {* Enriched Sigma datatype of objects *}
datatype sterm =
Bvar bVariable
| Fvar fVariable
| Obj "Label -~> sterm" type
| Call sterm Label sterm
| Upd sterm Label sterm
primrec applyPropOnOption:: "(sterm => bool) => sterm option => bool" where
f1: "applyPropOnOption P None = True" |
f2: "applyPropOnOption P (Some t) = P t"
lemma sterm_induct[case_names Bvar Fvar Obj Call Upd empty insert]:
fixes
t :: sterm and P1 :: "sterm => bool" and
f :: "Label -~> sterm" and P3 :: "(Label -~> sterm) => bool"
assumes
"!!b. P1 (Bvar b)" and
"!!x. P1 (Fvar x)" and
a_obj: "!!f T. P3 f ==> P1 (Obj f T)" and
"!!t1 l t2. [| P1 t1; P1 t2 |] ==> P1 (Call t1 l t2)" and
"!!t1 l t2. [| P1 t1; P1 t2 |] ==> P1 (Upd t1 l t2)" and
"P3 empty" and
a_f: "!!t1 f l . [| l ∉ dom f; P1 t1; P3 f |] ==> (P3 (f(l \<mapsto> t1)))"
shows "P1 t ∧ P3 f"
proof -
have "∀t (f::Label -~> sterm) l. P1 t ∧ (applyPropOnOption P1) (f l)"
proof (intro strip)
fix t :: sterm and f' :: "Label -~> sterm" and l :: Label
def foobar ≡ "f' l"
from assms show "P1 t ∧ applyPropOnOption P1 foobar"
proof (induct_tac t and foobar, auto)
fix f :: "Label -~> sterm" and T :: type
assume "!!x. applyPropOnOption P1 (f x)"
with a_f `P3 empty` have "P3 f"
proof (induct f rule: fmap_induct, simp)
case (insert F x z)
note
P1F' = `!!xa. applyPropOnOption P1 ((F(x \<mapsto> z)) xa)` and
predP3 = `[| !!l f t1. [|l ∉ dom f; P1 t1; P3 f|] ==> P3 (f(l \<mapsto> t1));
P3 Map.empty; !!x. applyPropOnOption P1 (F x)|]
==> P3 F` and
P3F' = `!!l f t f. [| l ∉ dom f; P1 t; P3 f |] ==> P3 (f(l \<mapsto> t))`
have "!!xa. applyPropOnOption P1 (F xa)"
proof -
fix xa :: Label show "applyPropOnOption P1 (F xa)"
proof (cases "xa = x")
case True with P1F' `x ∉ dom F` have "F xa = None" by force
thus ?thesis by simp
next
case False hence eq: "F xa = (F(x \<mapsto> z)) xa" by auto
from P1F'[of xa] show "applyPropOnOption P1 (F xa)"
by (simp only: ssubst[OF eq])
qed
qed
from a_f predP3[OF _ `P3 empty` this] have P3F: "P3 F" by simp
from P1F'[of x]
have "applyPropOnOption P1 (Some z)" by auto
hence "P1 z" by simp
from a_f[OF `x ∉ dom F` this P3F] show ?case by assumption
qed
with a_obj show "P1 (Obj f T)" by simp
qed
qed
with assms show ?thesis
proof (auto)
assume "!!l f t1. [|l ∉ dom f; P3 f|] ==> P3 (f(l \<mapsto> t1))"
with `P3 empty` show "P3 f" by (rule fmap_induct)
qed
qed
lemma ball_tsp_P3:
fixes
P1 :: "sterm => bool" and
P2 :: "sterm => fVariable => fVariable => bool" and
P3 :: "sterm => bool" and f :: "Label -~> sterm"
assumes
"!!t. [| P1 t; ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 t s p |] ==> P3 t" and
"∀l∈dom f. P1 (the(f l))" and
"∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 (the(f l)) s p"
shows "∀l∈dom f. P3 (the(f l))"
proof (intro strip)
fix l assume "l ∈ dom f" with assms(2) have "P1 (the(f l))" by blast
moreover
from assms(3) `l ∈ dom f` have "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 (the(f l)) s p"
by blast
ultimately
show "P3 (the(f l))" using assms(1) by simp
qed
lemma ball_tt'sp_P3:
fixes
P1 :: "sterm => sterm => bool" and
P2 :: "sterm => sterm => fVariable => fVariable => bool" and
P3 :: "sterm => sterm => bool" and
f :: "Label -~> sterm" and f' :: "Label -~> sterm"
assumes
"!!t t'. [| P1 t t'; ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 t t' s p |] ==> P3 t t'" and
"dom f = dom f'" and
"∀l∈dom f. P1 (the(f l)) (the(f' l))" and
"∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 (the(f l)) (the(f' l)) s p"
shows "∀l∈dom f'. P3 (the(f l)) (the(f' l))"
proof (intro strip)
fix l assume "l ∈ dom f'" with assms(2-3) have "P1 (the(f l)) (the(f' l))"
by blast
moreover
from assms(2,4) `l ∈ dom f'`
have "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> P2 (the (f l)) (the(f' l)) s p" by blast
ultimately
show "P3 (the(f l)) (the(f' l))" using assms(1)[of "the(f l)" "the(f' l)"]
by simp
qed
subsubsection {* Free variables *}
primrec
FV :: "sterm => fVariable set"
and
FVoption :: "sterm option => fVariable set"
where
FV_Bvar : "FV(Bvar b) = {}"
| FV_Fvar : "FV(Fvar x) = {x}"
| FV_Call : "FV(Call t l a) = FV t ∪ FV a"
| FV_Upd : "FV(Upd t l s) = FV t ∪ FV s"
| FV_Obj : "FV(Obj f T) = (\<Union> l ∈ dom f. FVoption(f l))"
| FV_None : "FVoption None = {}"
| FV_Some : "FVoption (Some t) = FV t"
definition closed :: "sterm => bool" where
"closed t <-> FV t = {}"
lemma finite_FV_FVoption: "finite (FV t) ∧ finite (FVoption s)"
by(induct _ t _ s rule: sterm.induct, simp_all)
lemma finite_FV[simp]: "finite (FV t)"
by (simp add: finite_FV_FVoption)
lemma FV_and_cofinite: "[| ∀x. x ∉ L --> P x; finite L |]
==> ∃L'. (finite L' ∧ FV t ⊆ L' ∧ (∀ x. x ∉ L' --> P x))"
by (rule_tac x = "L ∪ FV t" in exI, auto)
lemma exFresh_s_p_cof:
fixes L :: "fVariable set"
assumes "finite L"
shows "∃s p. s ∉ L ∧ p ∉ L ∧ s ≠ p"
proof -
from assms have "∃s. s ∉ L" by (simp only: ex_new_if_finite[OF infinite_UNIV_listI])
then obtain s where "s ∉ L" ..
moreover
from `finite L` have "finite (L ∪ {s})" by simp
hence "∃p. p ∉ L ∪ {s}" by (simp only: ex_new_if_finite[OF infinite_UNIV_listI])
then obtain p where "p ∉ L ∪ {s}" ..
ultimately show ?thesis by blast
qed
lemma FV_option_lem: "∀l∈dom f. FV (the(f l)) = FVoption (f l)"
by auto
subsubsection {* Term opening *}
primrec
sopen :: "[nat, sterm, sterm, sterm] => sterm"
("{_ -> [_,_]} _" [0, 0, 0, 300] 300)
and
sopen_option :: "[nat, sterm, sterm, sterm option] => sterm option"
where
sopen_Bvar:
"{k -> [s,p]}(Bvar b) = (case b of (Self i) => (if (k = i) then s else (Bvar b))
| (Param i) => (if (k = i) then p else (Bvar b)))"
| sopen_Fvar: "{k -> [s,p]}(Fvar x) = Fvar x"
| sopen_Call: "{k -> [s,p]}(Call t l a) = Call ({k -> [s,p]}t) l ({k -> [s,p]}a)"
| sopen_Upd : "{k -> [s,p]}(Upd t l u) = Upd ({k -> [s,p]}t) l ({(Suc k) -> [s,p]}u)"
| sopen_Obj : "{k -> [s,p]}(Obj f T) = Obj (λl. sopen_option (Suc k) s p (f l)) T"
| sopen_None: "sopen_option k s p None = None"
| sopen_Some: "sopen_option k s p (Some t) = Some ({k -> [s,p]}t)"
definition openz :: "[sterm, sterm, sterm] => sterm" ("(_)⇗[_,_]⇖" [50, 0, 0] 50) where
"t⇗[s,p]⇖ = {0 -> [s,p]}t"
lemma sopen_eq_Fvar:
fixes n s p t x
assumes "{n -> [Fvar s,Fvar p]} t = Fvar x"
shows
"(t = Fvar x) ∨ (x = s ∧ t = (Bvar (Self n)))
∨ (x = p ∧ t = (Bvar (Param n)))"
proof (cases t)
case Obj with assms show ?thesis by simp
next
case Call with assms show ?thesis by simp
next
case Upd with assms show ?thesis by simp
next
case (Fvar y) with assms show ?thesis
by (cases "y = x", simp_all)
next
case (Bvar b) thus ?thesis
proof (cases b)
case (Self k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
next
case (Param k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
qed
qed
lemma sopen_eq_Fvar':
assumes "{n -> [Fvar s,Fvar p]} t = Fvar x" and "x ≠ s" and "x ≠ p"
shows "t = Fvar x"
proof -
from sopen_eq_Fvar[OF assms(1)] `x ≠ s` `x ≠ p` show ?thesis
by auto
qed
lemma sopen_eq_Bvar:
fixes n s p t b
assumes "{n -> [Fvar s,Fvar p]} t = Bvar b"
shows "t = Bvar b"
proof (cases t)
case Fvar with assms show ?thesis by (simp add: openz_def)
next
case Obj with assms show ?thesis by (simp add: openz_def)
next
case Call with assms show ?thesis by (simp add: openz_def)
next
case Upd with assms show ?thesis by (simp add: openz_def)
next
case (Bvar b') show ?thesis
proof (cases b')
case (Self k) with assms Bvar show ?thesis
by (cases "k = n") (simp_all add: openz_def)
next
case (Param k) with assms Bvar show ?thesis
by (cases "k = n") (simp_all add: openz_def)
qed
qed
lemma sopen_eq_Obj:
fixes n s p t f T
assumes "{n -> [Fvar s,Fvar p]} t = Obj f T"
shows
"∃f'. {n -> [Fvar s, Fvar p]} Obj f' T = Obj f T
∧ t = Obj f' T"
proof (cases t)
case Fvar with assms show ?thesis by simp
next
case Obj with assms show ?thesis by simp
next
case Call with assms show ?thesis by simp
next
case Upd with assms show ?thesis by simp
next
case (Bvar b) thus ?thesis
proof (cases b)
case (Self k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
next
case (Param k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
qed
qed
lemma sopen_eq_Upd:
fixes n s p t t1 l t2
assumes "{n -> [Fvar s,Fvar p]} t = Upd t1 l t2"
shows
"∃t1' t2'. {n -> [Fvar s,Fvar p]} t1' = t1
∧ {(Suc n) -> [Fvar s,Fvar p]} t2' = t2 ∧ t = Upd t1' l t2'"
proof (cases t)
case Fvar with assms show ?thesis by simp
next
case Obj with assms show ?thesis by simp
next
case Call with assms show ?thesis by simp
next
case Upd with assms show ?thesis by simp
next
case (Bvar b) thus ?thesis
proof (cases b)
case (Self k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
next
case (Param k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
qed
qed
lemma sopen_eq_Call:
fixes n s p t t1 l t2
assumes "{n -> [Fvar s,Fvar p]} t = Call t1 l t2"
shows
"∃t1' t2'. {n -> [Fvar s,Fvar p]} t1' = t1
∧ {n -> [Fvar s,Fvar p]} t2' = t2 ∧ t = Call t1' l t2'"
proof (cases t)
case Fvar with assms show ?thesis by simp
next
case Obj with assms show ?thesis by simp
next
case Call with assms show ?thesis by simp
next
case Upd with assms show ?thesis by simp
next
case (Bvar b) thus ?thesis
proof (cases b)
case (Self k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
next
case (Param k) with assms Bvar show ?thesis
by (cases "k = n") simp_all
qed
qed
lemma dom_sopenoption_lem[simp]: "dom (λl. sopen_option k s t (f l)) = dom f"
by (auto, case_tac "x ∈ dom f", auto)
lemma sopen_option_lem:
"∀l∈dom f. {n -> [s,p]} the(f l) = the (sopen_option n s p (f l))"
by auto
lemma pred_sopenoption_lem:
"(∀l∈dom (λl. sopen_option n s p (f l)).
(P::sterm => bool) (the (sopen_option n s p (f l)))) =
(∀l∈dom f. (P::sterm => bool) ({n -> [s,p]} the (f l)))"
by (simp, force)
lemma sopen_FV[rule_format]:
"∀n s p. FV ({n -> [s,p]} t) ⊆ FV t ∪ FV s ∪ FV p"
proof -
have
"(∀n s p. FV ({n -> [s,p]} t) ⊆ FV t ∪ FV s ∪ FV p)
&(∀n s p. FVoption (sopen_option n s p u) ⊆ FVoption u ∪ FV s ∪ FV p)"
by (rule sterm.induct, simp_all split: bVariable.split, blast+)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sopen_commute[rule_format]:
"∀n k s p s' p'. n ≠ k
--> {n -> [Fvar s', Fvar p']} {k -> [Fvar s, Fvar p]} t
= {k -> [Fvar s, Fvar p]} {n -> [Fvar s', Fvar p']} t"
proof -
have
"(∀n k s p s' p'. n ≠ k
--> {n -> [Fvar s', Fvar p']} {k -> [Fvar s, Fvar p]} t
= {k -> [Fvar s, Fvar p]} {n -> [Fvar s', Fvar p']} t)
&(∀n k s p s' p'. n ≠ k
--> sopen_option n (Fvar s') (Fvar p') (sopen_option k (Fvar s) (Fvar p) u)
= sopen_option k (Fvar s) (Fvar p)
(sopen_option n (Fvar s') (Fvar p') u))"
by (rule sterm.induct, simp_all split: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sopen_fresh_inj[rule_format]:
"∀n s p t'. {n -> [Fvar s, Fvar p]} t = {n -> [Fvar s, Fvar p]} t'
--> s ∉ FV t --> s ∉ FV t' --> p ∉ FV t --> p ∉ FV t' --> s ≠ p
--> t = t'"
proof -
{
fix
b s p n t
assume
"(case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b) = t"
hence "Fvar s = t ∨ Fvar p = t ∨ Bvar b = t"
by (cases b, auto, (case_tac "n = nat", auto)+)
}
note cT = this
have
"(∀n s p t'. {n -> [Fvar s, Fvar p]} t = {n -> [Fvar s, Fvar p]} t'
--> s ∉ FV t --> s ∉ FV t' --> p ∉ FV t --> p ∉ FV t' --> s ≠ p
--> t = t')
&(∀n s p u'. sopen_option n (Fvar s) (Fvar p) u
= sopen_option n (Fvar s) (Fvar p) u'
--> s ∉ FVoption u --> s ∉ FVoption u'
--> p ∉ FVoption u --> p ∉ FVoption u' --> s ≠ p
--> u = u')"
proof (induct _ t _ u rule: sterm.induct)
case (Bvar b) thus ?case
proof (auto)
fix s p n t
assume
a: "(case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b)
= {n -> [Fvar s,Fvar p]} t"
note cT[OF this]
moreover assume "s ∉ FV t" and "p ∉ FV t" and "s ≠ p"
ultimately show "Bvar b = t"
proof (auto)
{
fix b'
assume
"(case b' of Self i => if n = i then Fvar s else Bvar b'
| Param i => if n = i then Fvar p else Bvar b') = Fvar s"
with `s ≠ p` have "b' = Self n"
by (cases b', auto, (case_tac "n = nat", auto)+)
}note fvS = this
assume eq_s: "Fvar s = {n -> [Fvar s,Fvar p]} t"
with sym[OF this] `s ∉ FV t` `s ≠ p` fvS
have "t = Bvar (Self n)" by (cases t, auto)
moreover
from a sym[OF eq_s] `s ≠ p` fvS[of b]
have "Self n = b" by simp
ultimately show "Bvar b = t" by simp
next
{
fix b'
assume
"(case b' of Self i => if n = i then Fvar s else Bvar b'
| Param i => if n = i then Fvar p else Bvar b') = Fvar p"
with `s ≠ p` have "b' = Param n"
by (cases b', auto, (case_tac "n = nat", auto)+)
}note fvP = this
assume eq_p: "Fvar p = {n -> [Fvar s,Fvar p]} t"
with sym[OF this] `p ∉ FV t` `s ≠ p` fvP
have "t = Bvar (Param n)" by (cases t, auto)
moreover
from a sym[OF eq_p] `s ≠ p` fvP[of b]
have "Param n = b" by simp
ultimately show "Bvar b = t" by simp
next
assume "Bvar b = {n -> [Fvar s, Fvar p]} t"
from sym[OF this] show "{n -> [Fvar s,Fvar p]} t = t"
proof (cases t, auto)
fix b'
assume
"(case b' of Self i => if n = i then Fvar s else Bvar b'
| Param i => if n = i then Fvar p else Bvar b') = Bvar b"
from cT[OF this] have "Bvar b = Bvar b'" by simp
thus "b = b'" by simp
qed
qed
qed
next
case (Fvar x) thus ?case
proof (auto)
fix n s p t
assume
a: "Fvar x = {n -> [Fvar s,Fvar p]} t" and
"s ∉ FV ({n -> [Fvar s,Fvar p]} t)"
hence "s ≠ x" by force
moreover
assume "p ∉ FV ({n -> [Fvar s,Fvar p]} t)"
with a have "p ≠ x" by force
ultimately
show "{n -> [Fvar s,Fvar p]} t = t"
using a
proof (cases t, auto)
fix b
assume
"Fvar x = (case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b)"
from cT[OF sym[OF this]] `s ≠ x` `p ≠ x`
have False by simp
then show
"(case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b) = Bvar b" ..
qed
qed
next
case (Obj f T) thus ?case
proof (auto)
fix n s p t
assume
"Obj (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) T
= {n -> [Fvar s,Fvar p]} t" and
"∀l∈dom f. s ∉ FVoption (f l)" and
"∀l∈dom f. p ∉ FVoption (f l)" and
"s ∉ FV t" and "p ∉ FV t" and "s ≠ p"
thus "Obj f T = t" using Obj
proof (cases t, auto)
fix b
assume
"Obj (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) T
= (case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b)"
from cT[OF sym[OF this]] show False by auto
next
fix f'
assume
nin_s: "∀l∈dom f'. s ∉ FVoption (f' l)" and
nin_p: "∀l∈dom f'. p ∉ FVoption (f' l)" and
ff': "(λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l))
= (λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f' l))"
have "!!l. f l = f' l"
proof -
fix l
from ff'
have
"sopen_option (Suc n) (Fvar s) (Fvar p) (f l)
= sopen_option (Suc n) (Fvar s) (Fvar p) (f' l)"
by (rule cong, simp)
moreover
from
`∀l∈dom f. s ∉ FVoption (f l)`
`∀l∈dom f. p ∉ FVoption (f l)`
have "s ∉ FVoption (f l)" and "p ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)+
moreover
from nin_s nin_p have "s ∉ FVoption (f' l)" and "p ∉ FVoption (f' l)"
by (case_tac "l ∈ dom f'", auto)+
ultimately show "f l = f' l" using Obj[of l] `s ≠ p`
by simp
qed
thus "f = f'" by (rule ext)
qed
qed
next
case (Call t1 l t2) thus ?case
proof (auto)
fix n s p t
assume
"s ∉ FV t1" and "s ∉ FV t2" and "p ∉ FV t1" and "p ∉ FV t2" and
"s ≠ p" and "s ∉ FV t" and "p ∉ FV t" and
"Call ({n -> [Fvar s,Fvar p]} t1) l ({n -> [Fvar s,Fvar p]} t2)
= {n -> [Fvar s,Fvar p]} t"
thus "Call t1 l t2 = t" using Call
proof (cases t, auto)
fix b
assume
"Call ({n -> [Fvar s,Fvar p]} t1) l ({n -> [Fvar s,Fvar p]} t2)
= (case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b)"
from cT[OF sym[OF this]] show False by auto
qed
qed
next
case (Upd t1 l t2) thus ?case
proof (auto)
fix n s p t
assume
"s ∉ FV t1" and "s ∉ FV t2" and "p ∉ FV t1" and "p ∉ FV t2" and
"s ≠ p" and "s ∉ FV t" and "p ∉ FV t" and
"Upd ({n -> [Fvar s,Fvar p]} t1) l ({Suc n -> [Fvar s,Fvar p]} t2)
= {n -> [Fvar s,Fvar p]} t"
thus "Upd t1 l t2 = t" using Upd
proof (cases t, auto)
fix b
assume
"Upd ({n -> [Fvar s,Fvar p]} t1) l ({Suc n -> [Fvar s,Fvar p]} t2)
= (case b of Self i => if n = i then Fvar s else Bvar b
| Param i => if n = i then Fvar p else Bvar b)"
from cT[OF sym[OF this]] show False by auto
qed
qed
next
case None_sterm thus ?case
proof (auto)
fix u s p n
assume "None = sopen_option n (Fvar s) (Fvar p) u"
thus "None = u" by (cases u, auto)
qed
next
case (Some_sterm t) thus ?case
proof (auto)
fix u s p n
assume
"Some ({n -> [Fvar s,Fvar p]} t) = sopen_option n (Fvar s) (Fvar p) u" and
"s ∉ FV t" and "p ∉ FV t" and "s ≠ p" and
"s ∉ FVoption u" and "p ∉ FVoption u"
with Some_sterm show "Some t = u" by (cases u) auto
qed
qed
from conjunct1[OF this] show ?thesis by assumption
qed
subsubsection {* Variable closing *}
primrec
sclose :: "[nat, fVariable, fVariable, sterm] => sterm"
("{_ \<leftarrow> [_,_]} _" [0, 0, 0, 300] 300)
and
sclose_option :: "[nat, fVariable, fVariable, sterm option] => sterm option"
where
sclose_Bvar: "{k \<leftarrow> [s,p]}(Bvar b) = Bvar b"
| sclose_Fvar:
"{k \<leftarrow> [s,p]}(Fvar x) = (if x = s then (Bvar (Self k))
else (if x = p then (Bvar (Param k))
else (Fvar x)))"
| sclose_Call: "{k \<leftarrow> [s,p]}(Call t l a) = Call ({k \<leftarrow> [s,p]}t) l ({k \<leftarrow> [s,p]}a)"
| sclose_Upd : "{k \<leftarrow> [s,p]}(Upd t l u) = Upd ({k \<leftarrow> [s,p]}t) l ({(Suc k) \<leftarrow> [s,p]}u)"
| sclose_Obj : "{k \<leftarrow> [s,p]}(Obj f T) = Obj (λl. sclose_option (Suc k) s p (f l)) T"
| sclose_None: "sclose_option k s p None = None"
| sclose_Some: "sclose_option k s p (Some t) = Some ({k \<leftarrow> [s,p]}t)"
definition closez :: "[fVariable, fVariable, sterm] => sterm" ("σ[_,_] _" [0, 0, 300]) where
"σ[s,p] t = {0 \<leftarrow> [s,p]}t"
lemma dom_scloseoption_lem[simp]: "dom (λl. sclose_option k s t (f l)) = dom f"
by (auto, case_tac "x ∈ dom f", auto)
lemma sclose_option_lem:
"∀l∈dom f. {n \<leftarrow> [s,p]} the(f l) = the (sclose_option n s p (f l))"
by auto
lemma pred_scloseoption_lem:
"(∀l∈dom (λl. sclose_option n s p (f l)).
(P::sterm => bool) (the (sclose_option n s p (f l)))) =
(∀l∈dom f. (P::sterm => bool) ({n \<leftarrow> [s,p]} the (f l)))"
by (simp, force)
lemma sclose_fresh[simp, rule_format]:
"∀n s p. s ∉ FV t --> p ∉ FV t --> {n \<leftarrow> [s,p]} t = t"
proof -
have
"(∀n s p. s ∉ FV t --> p ∉ FV t --> {n \<leftarrow> [s,p]} t = t)
&(∀n s p. s ∉ FVoption u --> p ∉ FVoption u
--> sclose_option n s p u = u)"
proof (induct _ t _ u rule: sterm.induct, auto simp: bVariable.split)
fix f n s p
assume
nin_s: "∀l∈dom f. s ∉ FVoption (f l)" and
nin_p: "∀l∈dom f. p ∉ FVoption (f l)"
{
fix l from nin_s have "s ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover
{
fix l from nin_p have "p ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover
assume
"!!x. ∀n s. s ∉ FVoption (f x)
--> (∀p. p ∉ FVoption (f x)
--> sclose_option n s p (f x) = f x)"
ultimately
have "!!l. sclose_option (Suc n) s p (f l) = f l" by auto
with ext show "(λl. sclose_option (Suc n) s p (f l)) = f" by auto
qed
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sclose_FV[rule_format]:
"∀n s p. FV ({n \<leftarrow> [s,p]} t) = FV t - {s} - {p}"
proof -
have
"(∀n s p. FV ({n \<leftarrow> [s,p]} t) = FV t - {s} - {p})
&(∀n s p. FVoption (sclose_option n s p u) = FVoption u - {s} - {p})"
by (rule sterm.induct, simp_all split: bVariable.split, blast+)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sclose_subset_FV[rule_format]:
"FV ({n \<leftarrow> [s,p]} t) ⊆ FV t"
by (simp add: sclose_FV, blast)
lemma Self_not_in_closed[simp]: "sa ∉ FV ({n \<leftarrow> [sa,pa]} t)"
by (simp add: sclose_FV)
lemma Param_not_in_closed[simp]: "pa ∉ FV ({n \<leftarrow> [sa,pa]} t)"
by (simp add: sclose_FV)
subsubsection {* Substitution *}
primrec
ssubst :: "[fVariable, sterm, sterm] => sterm"
("[_ -> _] _" [0, 0, 300] 300)
and
ssubst_option :: "[fVariable, sterm, sterm option] => sterm option"
where
ssubst_Bvar: "[z -> u](Bvar v) = Bvar v"
| ssubst_Fvar: "[z -> u](Fvar x) = (if (z = x) then u else (Fvar x))"
| ssubst_Call: "[z -> u](Call t l s) = Call ([z -> u]t) l ([z -> u]s)"
| ssubst_Upd : "[z -> u](Upd t l s) = Upd ([z -> u]t) l ([z -> u]s)"
| ssubst_Obj : "[z -> u](Obj f T) = Obj (λl. ssubst_option z u (f l)) T"
| ssubst_None: "ssubst_option z u None = None"
| ssubst_Some: "ssubst_option z u (Some t) = Some ([z -> u]t)"
lemma dom_ssubstoption_lem[simp]: "dom (λl. ssubst_option z u (f l)) = dom f"
by (auto, case_tac "x ∈ dom f", auto)
lemma ssubst_option_lem:
"∀l∈dom f. [z -> u] the(f l) = the (ssubst_option z u (f l))"
by auto
lemma pred_ssubstoption_lem:
"(∀l∈dom (λl. ssubst_option x t (f l)).
(P::sterm => bool) (the (ssubst_option x t (f l)))) =
(∀l∈dom f. (P::sterm => bool) ([x -> t] the (f l)))"
by (simp, force)
lemma ssubst_fresh[simp, rule_format]:
"∀s sa. sa ∉ FV t --> [sa -> s] t = t"
proof -
have
"(∀s sa. sa ∉ FV t --> [sa -> s] t = t)
&(∀s sa. sa ∉ FVoption u --> ssubst_option sa s u = u)"
proof (induct _ t _ u rule: sterm.induct, auto)
fix s sa f
assume
sa: "∀l∈dom f. sa ∉ FVoption (f l)" and
ssubst: "!!x. ∀s sa. sa ∉ FVoption (f x) --> ssubst_option sa s (f x) = f x"
{
fix l from sa have "sa ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
with ssubst have "ssubst_option sa s (f l) = f l" by auto
}
with ext show "(λl. ssubst_option sa s (f l)) = f" by auto
qed
from conjunct1[OF this] show ?thesis by assumption
qed
lemma ssubst_commute[rule_format]:
"∀s p sa pa. s ≠ p --> s ∉ FV pa --> p ∉ FV sa
--> [s -> sa] [p -> pa] t = [p -> pa] [s -> sa] t"
proof -
have
"(∀s p sa pa. s ≠ p --> s ∉ FV pa --> p ∉ FV sa
--> [s -> sa] [p -> pa] t = [p -> pa] [s -> sa] t)
&(∀s p sa pa. s ≠ p --> s ∉ FV pa --> p ∉ FV sa
--> ssubst_option s sa (ssubst_option p pa u)
= ssubst_option p pa (ssubst_option s sa u))"
by (rule sterm.induct, simp_all split: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma ssubst_FV[rule_format]:
"∀x s. FV ([x -> s] t) ⊆ FV s ∪ (FV t - {x})"
proof -
have
"(∀x s. FV ([x -> s] t) ⊆ FV s ∪ (FV t - {x}))
&(∀x s. FVoption (ssubst_option x s u) ⊆ FV s ∪ (FVoption u - {x}))"
by (rule sterm.induct, simp_all split: bVariable.split, blast+)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma ssubstoption_insert:
"l ∈ dom f
==> (λ(la::Label). ssubst_option x t' (if la = l then Some t else f la))
= (λ(la::Label). ssubst_option x t' (f la))(l \<mapsto> [x -> t'] t)"
by (rule Ltake_eq_all, force, simp add: Ltake_eq_def)
subsubsection {* Local closure *}
inductive lc :: "sterm => bool"
where
lc_Fvar[simp, intro!]: "lc (Fvar x)"
| lc_Call[simp, intro!]: "[| lc t; lc a |] ==> lc (Call t l a)"
| lc_Upd[simp, intro!] :
"[| lc t; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> lc (u⇗[Fvar s, Fvar p]⇖) |]
==> lc (Upd t l u)"
| lc_Obj[simp, intro!] :
"[| finite L; ∀l∈dom f.
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> lc (the(f l)⇗[Fvar s, Fvar p]⇖) |]
==> lc (Obj f T)"
definition body :: "sterm => bool" where
"body t <-> (∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> lc (t⇗[Fvar s, Fvar p]⇖)))"
lemma lc_bvar: "lc (Bvar b) = False"
by (rule iffI, erule lc.cases, simp_all)
lemma lc_obj:
"lc (Obj f T) = (∀l∈dom f. body (the(f l)))"
proof
fix f T assume "lc (Obj f T)"
thus "∀l∈dom f. body (the(f l))"
unfolding body_def
by (rule lc.cases, auto)
next
fix f :: "Label -~> sterm" and T :: type
assume "∀l∈dom f. body (the (f l))"
hence
"∃L. finite L ∧ (∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> lc (the (f l)⇗[Fvar s, Fvar p]⇖))"
proof (induct f rule: fmap_induct)
case empty thus ?case by blast
next
case (insert F x y) thus ?case
proof -
assume "x ∉ dom F" hence "∀l∈dom F. the(F l) = the ((F(x \<mapsto> y)) l)"
by auto
with `∀l∈dom (F(x \<mapsto> y)). body (the((F(x \<mapsto> y)) l))`
have "∀l∈dom F. body (the (F l))" by force
from insert(2)[OF this]
obtain L where
"finite L" and
"∀l∈dom F. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> lc (the (F l)⇗[Fvar s, Fvar p]⇖)" by auto
moreover
from `∀l∈dom (F(x \<mapsto> y)). body (the((F(x \<mapsto> y)) l))` have "body y" by force
then obtain L' where
"finite L'" and
"∀s p. s ∉ L' ∧ p ∉ L' ∧ s ≠ p
--> lc (y⇗[Fvar s, Fvar p]⇖)" by (auto simp: body_def)
ultimately
show
"∃L. finite L ∧ (∀l∈dom (F(x \<mapsto> y)). ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> lc (the ((F(x \<mapsto> y)) l)⇗[Fvar s,Fvar p]⇖))"
by (rule_tac x = "L ∪ L'" in exI, auto)
qed
qed
thus "lc (Obj f T)" by auto
qed
lemma lc_upd: "lc (Upd t l s) = (lc t ∧ body s)"
by (unfold body_def, rule iffI, erule lc.cases, auto)
lemma lc_call: "lc (Call t l s) = (lc t ∧ lc s)"
by (rule iffI, erule lc.cases, simp_all)
lemma lc_induct[consumes 1, case_names Fvar Call Upd Obj Bnd]:
fixes P1 :: "sterm => bool" and P2 :: "sterm => bool"
assumes
"lc t" and
"!!x. P1 (Fvar x)" and
"!!t l a. [| lc t; P1 t; lc a; P1 a |] ==> P1 (Call t l a)" and
"!!t l u. [| lc t; P1 t; P2 u |] ==> P1 (Upd t l u)" and
"!!f T. ∀l∈dom f. P2 (the(f l)) ==> P1 (Obj f T)" and
"!!L t. [| finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> lc (t⇗[Fvar s, Fvar p]⇖) ∧ P1 (t⇗[Fvar s, Fvar p]⇖) |]
==> P2 t"
shows "P1 t"
using assms by (induct rule: lc.induct, auto)
subsubsection {* Connections between sopen, sclose, ssubst, lc and body and resulting properties *}
lemma ssubst_intro[rule_format]:
"∀n s p sa pa. sa ∉ FV t --> pa ∉ FV t --> sa ≠ pa
--> sa ∉ FV p
--> {n -> [s,p]} t = [sa -> s] [pa -> p] {n -> [Fvar sa, Fvar pa]} t"
proof -
have
"(∀n s p sa pa. sa ∉ FV t --> pa ∉ FV t --> sa ≠ pa
--> sa ∉ FV p
--> {n -> [s,p]} t = [sa -> s] [pa -> p] {n -> [Fvar sa, Fvar pa]} t)
&(∀n s p sa pa. sa ∉ FVoption u --> pa ∉ FVoption u --> sa ≠ pa
--> sa ∉ FV p
--> sopen_option n s p u
= ssubst_option sa s (ssubst_option pa p
(sopen_option n (Fvar sa) (Fvar pa) u)))"
proof (induct _ t _ u rule: sterm.induct)
case Bvar thus ?case by (simp split: bVariable.split)
next
case Fvar thus ?case by simp
next
case Upd thus ?case by simp
next
case Call thus ?case by simp
next
case None_sterm thus ?case by simp
next
case (Obj f T) thus ?case
proof (clarify)
fix n s p sa pa
assume "sa ∉ FV (Obj f T)" and "pa ∉ FV (Obj f T)"
{
fix l
from `sa ∉ FV (Obj f T)` have "sa ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover
{
fix l
from `pa ∉ FV (Obj f T)` have pa: "pa ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover assume "sa ≠ pa" and "sa ∉ FV p"
ultimately
have
"!!l. sopen_option (Suc n) s p (f l)
= ssubst_option sa s (ssubst_option pa p
(sopen_option (Suc n) (Fvar sa) (Fvar pa) (f l)))"
using Obj by auto
with ext
show
"{n -> [s,p]} Obj f T
= [sa -> s] [pa -> p] {n -> [Fvar sa,Fvar pa]} Obj f T"
by auto
qed
next
case (Some_sterm t) thus ?case
proof (clarify)
fix n s p sa pa
assume "sa ∉ FVoption (Some t)"
hence "sa ∉ FV t" by simp
moreover assume "pa ∉ FVoption (Some t)"
hence "pa ∉ FV t" by simp
moreover assume "sa ≠ pa" and "sa ∉ FV p"
ultimately
have "{n -> [s,p]} t = [sa -> s] [pa -> p] {n -> [Fvar sa,Fvar pa]} t"
using Some_sterm by blast
thus
"sopen_option n s p (Some t)
= ssubst_option sa s (ssubst_option pa p
(sopen_option n (Fvar sa) (Fvar pa) (Some t)))"
by simp
qed
qed
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sopen_lc_FV[rule_format]:
fixes t
assumes "lc t"
shows "∀n s p. {n -> [Fvar s, Fvar p]} t = t"
using assms
proof
(induct
taking: "λt. ∀n s p. {Suc n -> [Fvar s, Fvar p]} t = t"
rule: lc_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case Upd thus ?case by simp
next
case (Obj f T) note pred = this
show ?case
proof (intro strip, simp)
fix n s p
{
fix l
have "sopen_option (Suc n) (Fvar s) (Fvar p) (f l) = f l"
proof (cases "l ∈ dom f")
case False hence "f l = None" by force
thus ?thesis by force
next
case True with pred show ?thesis by force
qed
} with ext
show "(λl. sopen_option (Suc n) (Fvar s) (Fvar p) (f l)) = f"
by auto
qed
next
case (Bnd L t) note cof = this(2)
show ?case
proof (intro strip)
fix n s p
from `finite L` exFresh_s_p_cof[of "L ∪ FV t ∪ {s} ∪ {p}"]
obtain sa pa where
sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
by auto
with cof
have "{Suc n -> [Fvar s,Fvar p]} (t⇗[Fvar sa, Fvar pa]⇖) = (t⇗[Fvar sa, Fvar pa]⇖)"
by auto
with sopen_commute[OF Suc_not_Zero[of n]]
have
eq: "{0 -> [Fvar sa,Fvar pa]} {Suc n -> [Fvar s,Fvar p]} t
= {0 -> [Fvar sa,Fvar pa]} t"
by (simp add: openz_def)
from sapa contra_subsetD[OF sopen_FV[of _ "Fvar s" "Fvar p" t]]
have
"sa ∉ FV ({Suc n -> [Fvar s,Fvar p]} t)" and "sa ∉ FV t" and
"pa ∉ FV ({Suc n -> [Fvar s,Fvar p]} t)" and "pa ∉ FV t" and
"sa ≠ pa"
by auto
from sopen_fresh_inj[OF eq this]
show "{Suc n -> [Fvar s,Fvar p]} t = t" by assumption
qed
qed
lemma sopen_lc[simp]:
fixes t n s p
assumes "lc t"
shows "{n -> [s,p]} t = t"
proof -
from exFresh_s_p_cof[of "FV t ∪ FV p"]
obtain sa pa where
"sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and
"sa ∉ FV p" and "pa ∉ FV p"
by auto
from ssubst_intro[OF this(1-4)]
have "{n -> [s,p]} t = [sa -> s] [pa -> p] {n -> [Fvar sa,Fvar pa]} t"
by simp
with assms have "{n -> [s,p]} t = [sa -> s] [pa -> p] t"
using sopen_lc_FV
by simp
with ssubst_fresh[OF `pa ∉ FV t`]
have "{n -> [s,p]} t = [sa -> s] t" by simp
with ssubst_fresh[OF `sa ∉ FV t`]
show "{n -> [s,p]} t = t" by simp
qed
lemma sopen_twice[rule_format]:
"∀s p s' p' n. lc s --> lc p
--> {n -> [s',p']} {n -> [s,p]} t = {n -> [s,p]} t"
proof -
have
"(∀s p s' p' n. lc s --> lc p
--> {n -> [s',p']} {n -> [s,p]} t = {n -> [s,p]} t)
&(∀s p s' p' n. lc s --> lc p
--> sopen_option n s' p' (sopen_option n s p u) = sopen_option n s p u)"
by (rule sterm.induct, auto simp: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sopen_sclose_commute[rule_format]:
"∀n k s p sa pa. n ≠ k --> sa ∉ FV s --> sa ∉ FV p
--> pa ∉ FV s --> pa ∉ FV p
--> {n -> [s, p]} {k \<leftarrow> [sa,pa]} t = {k \<leftarrow> [sa,pa]} {n -> [s, p]} t"
proof -
have
"(∀n k s p sa pa. n ≠ k --> sa ∉ FV s --> sa ∉ FV p
--> pa ∉ FV s --> pa ∉ FV p
--> {n -> [s, p]} {k \<leftarrow> [sa,pa]} t = {k \<leftarrow> [sa,pa]} {n -> [s, p]} t)
&(∀n k s p sa pa. n ≠ k --> sa ∉ FV s --> sa ∉ FV p
--> pa ∉ FV s --> pa ∉ FV p
--> sopen_option n s p (sclose_option k sa pa u)
= sclose_option k sa pa (sopen_option n s p u))"
by (rule sterm.induct, simp_all split: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sclose_sopen_eq_t[rule_format]:
"∀n s p. s ∉ FV t --> p ∉ FV t --> s ≠ p
--> {n \<leftarrow> [s,p]} {n -> [Fvar s, Fvar p]} t = t"
proof -
have
"(∀n s p. s ∉ FV t --> p ∉ FV t --> s ≠ p
--> {n \<leftarrow> [s,p]} {n -> [Fvar s, Fvar p]} t = t)
&(∀n s p. s ∉ FVoption u --> p ∉ FVoption u --> s ≠ p
--> sclose_option n s p (sopen_option n (Fvar s) (Fvar p) u) = u)"
proof (induct _ t _ u rule: sterm.induct, simp_all split: bVariable.split, auto)
fix f n s p
assume
nin_s: "∀l∈dom f. s ∉ FVoption (f l)" and
nin_p: "∀l∈dom f. p ∉ FVoption (f l)"
{
fix l from nin_s have "s ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover
{
fix l from nin_p have "p ∉ FVoption (f l)"
by (case_tac "l ∈ dom f", auto)
}
moreover
assume
"s ≠ p" and
"!!x. ∀n s. s ∉ FVoption (f x)
--> (∀p. p ∉ FVoption (f x) --> s ≠ p
--> sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f x))
= f x)"
ultimately
have "!!l. sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f l)) = f l"
by auto
with ext
show "(λl. sclose_option n s p (sopen_option n (Fvar s) (Fvar p) (f l))) = f "
by auto
qed
from conjunct1[OF this] show ?thesis by assumption
qed
lemma sopen_sclose_eq_t[simp, rule_format]:
fixes t
assumes "lc t"
shows "∀n s p. {n -> [Fvar s, Fvar p]} {n \<leftarrow> [s,p]} t = t"
using assms
proof
(induct
taking: "λt. ∀n s p. {Suc n -> [Fvar s, Fvar p]} {Suc n \<leftarrow> [s,p]} t = t"
rule: lc_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case Upd thus ?case by simp
next
case (Obj f T) note pred = this
show ?case
proof (intro strip, simp)
fix n s p
{
fix l
have
"sopen_option (Suc n) (Fvar s) (Fvar p) (sclose_option (Suc n) s p (f l))
= f l"
proof (cases "l ∈ dom f")
case False hence "f l = None" by force
thus ?thesis by simp
next
case True with pred
show ?thesis by force
qed
}
with ext
show "(λl. sopen_option (Suc n) (Fvar s) (Fvar p)
(sclose_option (Suc n) s p (f l))) = f"
by simp
qed
next
case (Bnd L t) note cof = this(2)
show ?case
proof (intro strip)
fix n s p
from `finite L` exFresh_s_p_cof[of "L ∪ FV t ∪ {s} ∪ {p}"]
obtain sa pa where
sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p}
∧ sa ≠ pa"
by auto
with cof
have
eq: "{Suc n -> [Fvar s,Fvar p]} {Suc n \<leftarrow> [s,p]} (t⇗[Fvar sa, Fvar pa]⇖)
= (t⇗[Fvar sa, Fvar pa]⇖)" by blast
{
fix x assume "x ∉ FV t"
from contra_subsetD[OF sclose_subset_FV this]
have "x ∉ FV ({Suc n \<leftarrow> [s,p]} t)" by simp
moreover assume "x ≠ p" and "x ≠ s"
ultimately
have "x ∉ FV ({Suc n \<leftarrow> [s,p]} t) ∪ FV (Fvar s) ∪ FV (Fvar p)"
by simp
from contra_subsetD[OF sopen_FV this]
have "x ∉ FV ({Suc n -> [Fvar s,Fvar p]} {Suc n \<leftarrow> [s,p]} t)"
by simp
} with sapa
have
"s ∉ FV (Fvar sa)" and "s ∉ FV (Fvar pa)" and
"p ∉ FV (Fvar sa)" and "p ∉ FV (Fvar pa)" and
"sa ∉ FV ({Suc n -> [Fvar s,Fvar p]} {Suc n \<leftarrow> [s,p]} t)" and
"sa ∉ FV t" and
"pa ∉ FV ({Suc n -> [Fvar s,Fvar p]} {Suc n \<leftarrow> [s,p]} t)" and
"pa ∉ FV t" and "sa ≠ pa"
by auto
from
eq
sym[OF sopen_sclose_commute[OF not_sym[OF Suc_not_Zero[of n]]
this(1-4)]]
sopen_commute[OF Suc_not_Zero[of n]]
sopen_fresh_inj[OF _ this(5-9)]
show "{Suc n -> [Fvar s,Fvar p]} {Suc n \<leftarrow> [s,p]} t = t"
by (auto simp: openz_def)
qed
qed
lemma ssubst_sopen_distrib[rule_format]:
"∀n s p t'. lc t' --> [x -> t'] {n -> [s,p]} t
= {n -> [[x -> t']s, [x -> t']p]} [x -> t'] t"
proof -
have
"(∀n s p t'. lc t'
--> [x -> t'] {n -> [s,p]} t = {n -> [[x -> t']s, [x -> t']p]} [x -> t'] t)
&(∀n s p t'. lc t'
--> ssubst_option x t' (sopen_option n s p u)
= sopen_option n ([x -> t']s) ([x -> t']p) (ssubst_option x t' u))"
by (rule sterm.induct, simp_all split: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma ssubst_openz_distrib:
"lc t' ==> [x -> t'] (t⇗[s,p]⇖) = (([x -> t'] t)⇗[[x -> t'] s, [x -> t'] p]⇖)"
by (simp add: openz_def ssubst_sopen_distrib)
lemma ssubst_sopen_commute: "[| lc t'; x ∉ FV s; x ∉ FV p |]
==> [x -> t'] {n -> [s,p]} t = {n -> [s,p]} [x -> t'] t"
by (frule ssubst_sopen_distrib[of t' x n s p t], simp)
lemma sopen_commute_gen:
fixes s p s' p' n k t
assumes "lc s" and "lc p" and "lc s'" and "lc p'" and "n ≠ k"
shows "{n -> [s,p]} {k -> [s',p']} t = {k -> [s',p']} {n -> [s,p]} t"
proof -
have "finite (FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t)" by auto
from exFresh_s_p_cof[OF this]
obtain sa pa where
"sa ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t
∧ pa ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∧ sa ≠ pa" by auto
moreover
hence "finite (FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa})" by auto
from exFresh_s_p_cof[OF this]
obtain sb pb where
"sb ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa}
∧ pb ∉ FV s ∪ FV p ∪ FV s' ∪ FV p' ∪ FV t ∪ {sa} ∪ {pa}
∧ sb ≠ pb" by auto
ultimately
have
"sa ∉ FV t" and "pa ∉ FV t" and "sb ∉ FV t" and "pb ∉ FV t" and
"sa ∉ FV ({n -> [s,p]} t)" and "pa ∉ FV ({n -> [s,p]} t)" and
"sb ∉ FV ({k -> [s',p']} t)" and "pb ∉ FV ({k -> [s',p']} t)" and
"sa ≠ pa" and "sb ≠ pb" and "sb ≠ sa" and "sb ≠ pa" and
"pb ≠ sa" and "pb ≠ pa" and
"sa ∉ FV s" and "sa ∉ FV p" and "pa ∉ FV s" and "pa ∉ FV p" and
"sb ∉ FV s'" and "sb ∉ FV p'" and "pb ∉ FV s'" and "pb ∉ FV p'" and
"sa ∉ FV p'" and "sb ∉ FV p" and
"sa ∉ FV (Fvar sb)" and "sa ∉ FV (Fvar pb)" and
"pa ∉ FV (Fvar sb)" and "pa ∉ FV (Fvar pb)" and
"pb ∉ FV (Fvar sa)" and "pb ∉ FV (Fvar pa)" and
"sb ∉ FV (Fvar sa)" and "sb ∉ FV (Fvar pa)" and
"lc s" and "lc p" and "lc s'" and "lc p'"
using contra_subsetD[OF sopen_FV] assms(1-4)
by auto
from
ssubst_intro[OF `sa ∉ FV t` `pa ∉ FV t` `sa ≠ pa` `sa ∉ FV p'`]
ssubst_intro[OF `sb ∉ FV ({k -> [s',p']} t)` `pb ∉ FV ({k -> [s',p']} t)`
`sb ≠ pb` `sb ∉ FV p`]
sym[OF ssubst_sopen_commute[OF `lc s'`
`sa ∉ FV (Fvar sb)` `sa ∉ FV (Fvar pb)`]]
sym[OF ssubst_sopen_commute[OF `lc p'`
`pa ∉ FV (Fvar sb)` `pa ∉ FV (Fvar pb)`]]
sopen_commute[OF `n ≠ k`]
ssubst_commute[OF `pb ≠ sa` `pb ∉ FV s'` `sa ∉ FV p`]
ssubst_commute[OF `sb ≠ sa` `sb ∉ FV s'` `sa ∉ FV s`]
ssubst_commute[OF `pb ≠ pa` `pb ∉ FV p'` `pa ∉ FV p`]
ssubst_commute[OF `sb ≠ pa` `sb ∉ FV p'` `pa ∉ FV s`]
ssubst_sopen_commute[OF `lc s` `sb ∉ FV (Fvar sa)` `sb ∉ FV (Fvar pa)`]
ssubst_sopen_commute[OF `lc p` `pb ∉ FV (Fvar sa)` `pb ∉ FV (Fvar pa)`]
sym[OF ssubst_intro[OF `sb ∉ FV t` `pb ∉ FV t` `sb ≠ pb` `sb ∉ FV p`]]
sym[OF ssubst_intro[OF `sa ∉ FV ({n -> [s,p]} t)` `pa ∉ FV ({n -> [s,p]} t)`
`sa ≠ pa` `sa ∉ FV p'`]]
show "{n -> [s,p]} {k -> [s',p']} t = {k -> [s',p']} {n -> [s,p]} t"
by force
qed
lemma ssubst_preserves_lc[simp, rule_format]:
fixes t
assumes "lc t"
shows "∀x t'. lc t' --> lc ([x -> t'] t)"
proof -
def pred_cof ≡ "λL t. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> lc (t⇗[Fvar s, Fvar p]⇖))"
{
fix x v t
assume
"lc v" and
"∀x v. lc v --> (∃L. finite L ∧ pred_cof L ([x -> v] t))"
hence
"∃L. finite L ∧ pred_cof L ([x -> v] t)"
by auto
}note Lex = this
from assms show ?thesis
proof
(induct
taking: "λt. ∀x t'. lc t' --> (∃L. finite L ∧ pred_cof L ([x -> t'] t))"
rule: lc_induct)
case Fvar thus ?case by simp
next
case Call thus ?case by simp
next
case (Upd t l u) note pred_t = this(2) and pred_bnd = this(3)
show ?case
proof (intro strip)
fix x t' assume "lc t'"
note Lex[OF this pred_bnd]
from this[of x]
obtain L where "finite L" and "pred_cof L ([x -> t'] u)"
by auto
with `lc t'` pred_t show "lc ([x -> t'] Upd t l u)"
unfolding pred_cof_def
by simp
qed
next
case (Obj f T) note pred = this
show ?case
proof (intro strip)
fix x t' assume "lc t'"
def pred_fl ≡ "λs p b l::Label. lc ([x -> t'] the b⇗[Fvar s, Fvar p]⇖)"
from `lc t'` fmap_ball_all2[OF pred]
have "∀l∈dom f. ∃L. finite L ∧ pred_cof L ([x -> t'] the(f l))"
unfolding pred_cof_def
by simp
with fmap_ex_cof[of f pred_fl]
obtain L where
"finite L" and "∀l∈dom f. pred_cof L ([x -> t'] the(f l))"
unfolding pred_cof_def pred_fl_def
by auto
with pred_ssubstoption_lem[of x t' f "pred_cof L"]
show "lc ([x -> t'] Obj f T)"
unfolding pred_cof_def
by simp
qed
next
case (Bnd L t) note pred = this(2)
show ?case
proof (intro strip)
fix x t' assume "lc t'"
with `finite L` show "∃L. finite L ∧ pred_cof L ([x -> t'] t)"
unfolding pred_cof_def
proof (
rule_tac x = "L ∪ {x}" in exI,
intro conjI, simp, intro strip)
fix s p assume sp: "s ∉ L ∪ {x} ∧ p ∉ L ∪ {x} ∧ s ≠ p"
hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)"
by auto
from sp pred `lc t'`
have "lc ([x -> t'] (t⇗[Fvar s,Fvar p]⇖))"
by blast
with ssubst_sopen_commute[OF `lc t'` `x ∉ FV (Fvar s)`
`x ∉ FV (Fvar p)`]
show "lc ([x -> t'] t⇗[Fvar s,Fvar p]⇖)"
by (auto simp: openz_def)
qed
qed
qed
qed
lemma sopen_sclose_eq_ssubst: "[| sa ≠ pa; sa ∉ FV p; lc t |]
==> {n -> [s,p]} {n \<leftarrow> [sa,pa]} t = [sa -> s] [pa -> p] t"
by (rule_tac sa1 = sa and pa1 = pa and t1 = "{n \<leftarrow> [sa,pa]} t"
in ssubst[OF ssubst_intro], simp+)
lemma ssubst_sclose_commute[rule_format]:
"∀x n s p t'. s ∉ FV t' --> p ∉ FV t' --> x ≠ s --> x ≠ p
--> [x -> t'] {n \<leftarrow> [s,p]} t = {n \<leftarrow> [s,p]} [x -> t'] t"
proof -
have
"(∀x n s p t'. s ∉ FV t' --> p ∉ FV t' --> x ≠ s --> x ≠ p
--> [x -> t'] {n \<leftarrow> [s,p]} t = {n \<leftarrow> [s,p]} [x -> t'] t)
&(∀x n s p t'. s ∉ FV t' --> p ∉ FV t' --> x ≠ s --> x ≠ p
--> ssubst_option x t' (sclose_option n s p u)
= sclose_option n s p (ssubst_option x t' u))"
by (rule sterm.induct, simp_all split: bVariable.split)
from conjunct1[OF this] show ?thesis by assumption
qed
lemma body_lc_FV:
fixes t s p
assumes "body t"
shows "lc (t⇗[Fvar s, Fvar p]⇖)"
proof -
from assms
obtain L where
"finite L" and pred_sp: "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> lc (t⇗[Fvar s,Fvar p]⇖)"
unfolding body_def by auto
hence "finite (L ∪ FV t ∪ {s} ∪ {p})" by simp
from exFresh_s_p_cof[OF this] obtain sa pa where sapa:
"sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
by auto
hence "sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and "sa ∉ FV (Fvar p)" by auto
from pred_sp sapa have "lc (t⇗[Fvar sa,Fvar pa]⇖)" by blast
with
ssubst_intro[OF `sa ∉ FV t` `pa ∉ FV t` `sa ≠ pa` `sa ∉ FV (Fvar p)`]
ssubst_preserves_lc
show "lc (t⇗[Fvar s,Fvar p]⇖)" by (auto simp: openz_def)
qed
lemma body_lc:
fixes t s p
assumes "body t" and "lc s" and "lc p"
shows "lc (t⇗[s, p]⇖)"
proof -
have "finite (FV t ∪ FV p)" by simp
from exFresh_s_p_cof[OF this] obtain sa pa where
"sa ∉ FV t ∪ FV p ∧ pa ∉ FV t ∪ FV p ∧ sa ≠ pa" by auto
hence "sa ∉ FV t" and "pa ∉ FV t" and "sa ≠ pa" and "sa ∉ FV p"
by auto
from body_lc_FV[OF `body t`] have lc: "lc (t⇗[Fvar sa,Fvar pa]⇖)"
by assumption
from
ssubst_intro[OF `sa ∉ FV t` `pa ∉ FV t` `sa ≠ pa` `sa ∉ FV p`]
ssubst_preserves_lc[OF lc] `lc s` `lc p`
show "lc (t⇗[s,p]⇖)" by (auto simp: openz_def)
qed
lemma lc_body:
fixes t s p
assumes "lc t" and "s ≠ p"
shows "body (σ[s,p] t)"
unfolding body_def
proof
have
"∀sa pa. sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
--> lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖)"
proof (intro strip)
fix sa :: fVariable and pa :: fVariable
assume "sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
hence "s ∉ FV (Fvar pa)" by auto
from
sopen_sclose_eq_ssubst[OF `s ≠ p` this `lc t`]
ssubst_preserves_lc[OF `lc t`]
show "lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖)" by (simp add: openz_def closez_def)
qed
thus
"finite (FV t ∪ {s} ∪ {p})
∧ (∀sa pa. sa ∉ FV t ∪ {s} ∪ {p} ∧ pa ∉ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
--> lc (σ[s,p] t⇗[Fvar sa,Fvar pa]⇖))" by simp
qed
lemma ssubst_preserves_lcE_lem[rule_format]:
fixes t
assumes "lc t"
shows "∀x u t'. t = [x -> u] t' --> lc u --> lc t'"
using assms
proof
(induct
taking:
"λt. ∀x u t'. t = [x -> u] t' --> lc u --> body t'"
rule: lc_induct)
case Fvar thus ?case by (intro strip, case_tac t', simp_all)
next
case Call thus ?case by (intro strip, case_tac t', simp_all)
next
case (Upd t l u) note pred_t = this(2) and pred_u = this(3)
show ?case
proof (intro strip)
fix x v t'' assume "Upd t l u = [x -> v] t''" and "lc v"
from this(1) have t'': "(∃t' u'. t'' = Upd t' l u') ∨ (t'' = Fvar x)"
proof (cases t'', auto)
fix y
assume "Upd t l u = (if x = y then v else Fvar y)"
thus "y = x" by (case_tac "y = x", auto)
qed
show "lc t''"
proof (cases "t'' = Fvar x")
case True thus ?thesis by simp
next
case False with `Upd t l u = [x -> v] t''` t''
show ?thesis
proof (clarify)
fix t' u' assume "Upd t l u = [x -> v] Upd t' l u'"
hence "t = [x -> v] t'" and "u = [x -> v] u'"
by auto
with `lc v` pred_t pred_u lc_upd[of t' l u']
show "lc (Upd t' l u')" by auto
qed
qed
qed
next
case (Obj f T) note pred = this
show ?case
proof (intro strip)
fix x v t' assume "Obj f T = [x -> v] t'" and "lc v"
from this(1) have t': "(∃f'. t' = Obj f' T) ∨ (t' = Fvar x)"
proof (cases t', auto)
fix y :: fVariable
assume "Obj f T = (if x = y then v else Fvar y)"
thus "y = x" by (case_tac "y = x", auto)
qed
show "lc t'"
proof (cases "t' = Fvar x")
case True thus ?thesis by simp
next
case False with `Obj f T = [x -> v] t'` t'
show ?thesis
proof (clarify)
fix f' assume "Obj f T = [x -> v] Obj f' T"
hence
ssubst: "∀l∈dom f. the(f l) = [x -> v] the(f' l)" and
"dom f = dom f'"
by auto
with pred `lc v` lc_obj[of f' T]
show "lc (Obj f' T)"
by auto
qed
qed
qed
next
case (Bnd L t) note pred = this(2)
show ?case
proof (intro strip)
fix x v t' assume "t = [x -> v] t'" and "lc v"
from `finite L` exFresh_s_p_cof[of "L ∪ {x} ∪ FV t'"]
obtain s p where
"s ∉ L" and "p ∉ L" and "s ≠ p" and
"x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" and
"s ∉ FV t'" and "p ∉ FV t'"
by auto
from
`t = [x -> v] t'`
ssubst_sopen_commute[OF `lc v` `x ∉ FV (Fvar s)` `x ∉ FV (Fvar p)`]
have "(t⇗[Fvar s, Fvar p]⇖) = [x -> v] (t'⇗[Fvar s, Fvar p]⇖)"
by (auto simp: openz_def)
with
`s ∉ L` `p ∉ L` `s ≠ p` `lc v` pred
have "lc (t'⇗[Fvar s, Fvar p]⇖)" by blast
from
lc_body[OF this `s ≠ p`]
sclose_sopen_eq_t[OF `s ∉ FV t'` `p ∉ FV t'` `s ≠ p`]
show "body t'" by (auto simp: openz_def closez_def)
qed
qed
lemma ssubst_preserves_lcE: "[| lc ([x -> t'] t); lc t' |] ==> lc t"
by (drule_tac t = "[x -> t'] t" and x = x and u = t' and t' = t
in ssubst_preserves_lcE_lem, simp+)
lemma obj_openz_lc: "[| lc (Obj f T); lc p; l ∈ dom f |] ==> lc (the(f l)⇗[Obj f T, p]⇖)"
by (rule_tac s = "Obj f T" and p = p in body_lc, (simp add: lc_obj)+)
lemma obj_insert_lc:
fixes f T t l
assumes "lc (Obj f T)" and "body t"
shows "lc (Obj (f(l \<mapsto> t)) T)"
proof (rule ssubst[OF lc_obj], rule ballI)
fix l' :: Label assume "l' ∈ dom (f(l \<mapsto> t))"
with assms show "body (the ((f(l \<mapsto> t)) l'))"
by (cases "l' = l", (auto simp: lc_obj))
qed
lemma ssubst_preserves_body[simp]:
fixes t t' x
assumes "body t" and "lc t'"
shows "body ([x -> t'] t)"
unfolding body_def
proof -
have
"∀s p. s ∉ FV t' ∪ {x} ∧ p ∉ FV t' ∪ {x} ∧ s ≠ p
--> lc ([x -> t'] t⇗[Fvar s,Fvar p]⇖)"
proof (intro strip)
fix s :: fVariable and p :: fVariable
from body_lc_FV[OF `body t`]
have "lc ({0 -> [Fvar s,Fvar p]} t)" by (simp add: openz_def)
from ssubst_preserves_lc[OF this `lc t'`]
have "lc ([x -> t'] (t⇗[Fvar s,Fvar p]⇖))" by (simp add: openz_def)
moreover assume "s ∉ FV t' ∪ {x} ∧ p ∉ FV t' ∪ {x} ∧ s ≠ p"
hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" by auto
note ssubst_sopen_commute[OF `lc t'` this]
ultimately
show "lc ([x -> t'] t⇗[Fvar s,Fvar p]⇖)" by (simp add: openz_def)
qed
thus
"∃L. finite L ∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> lc ([x -> t'] t⇗[Fvar s,Fvar p]⇖))"
by (rule_tac x = "FV t' ∪ {x}" in exI, simp)
qed
lemma sopen_preserves_body[simp]:
fixes t s p
assumes "body t" and "lc s" and "lc p"
shows "body ({n -> [s,p]} t)"
unfolding body_def
proof -
have
"∀sa pa. sa ∉ FV t ∪ FV s ∧ pa ∉ FV p ∧ sa ≠ pa
--> lc ({n -> [s,p]} t⇗[Fvar sa,Fvar pa]⇖)"
proof (cases "n = 0")
case True thus ?thesis
using body_lc[OF `body t` `lc s` `lc p`] sopen_twice[OF `lc s` `lc p`]
by (simp add: openz_def)
next
case False thus ?thesis
proof (intro strip)
fix sa :: fVariable and pa :: fVariable
from body_lc_FV[OF `body t`] have "lc (t⇗[Fvar sa,Fvar pa]⇖)" by assumption
moreover
from sopen_commute_gen[OF _ _ `lc s` `lc p` not_sym[OF `n ≠ 0`]]
have "{n -> [s,p]} t⇗[Fvar sa,Fvar pa]⇖ = {n -> [s,p]} (t⇗[Fvar sa,Fvar pa]⇖)"
by (simp add: openz_def)
ultimately show "lc ({n -> [s,p]} t⇗[Fvar sa,Fvar pa]⇖)" by simp
qed
qed
thus "∃L. finite L
∧ (∀sa pa. sa ∉ L ∧ pa ∉ L ∧ sa ≠ pa
--> lc ({n -> [s,p]} t⇗[Fvar sa,Fvar pa]⇖))"
by (rule_tac x = "FV t ∪ FV s ∪ FV p" in exI, simp)
qed
subsection {* Beta-reduction *}
inductive beta :: "[sterm, sterm] => bool" (infixl "->⇩β" 50)
where
beta[simp, intro!] :
"[| l ∈ dom f; lc (Obj f T); lc a |] ==> Call (Obj f T) l a ->⇩β (the (f l)⇗[(Obj f T), a]⇖)"
| beta_Upd[simp, intro!] :
"[| l ∈ dom f; lc (Obj f T); body t |] ==> Upd (Obj f T) l t ->⇩β Obj (f(l \<mapsto> t)) T"
| beta_CallL[simp, intro!]: "[| t ->⇩β t'; lc u |] ==> Call t l u ->⇩β Call t' l u"
| beta_CallR[simp, intro!]: "[| t ->⇩β t'; lc u |] ==> Call u l t ->⇩β Call u l t'"
| beta_UpdL[simp, intro!] : "[| t ->⇩β t'; body u |] ==> Upd t l u ->⇩β Upd t' l u"
| beta_UpdR[simp, intro!] :
"[| finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β t''∧ t'= σ[s,p]t'');
lc u |] ==> Upd u l t ->⇩β Upd u l t'"
| beta_Obj[simp, intro!] :
"[| l ∈ dom f; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p --> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β t'' ∧ t'= σ[s,p]t'');
∀l∈dom f. body (the (f l)) |]
==> Obj (f(l \<mapsto> t)) T ->⇩β Obj (f(l \<mapsto> t')) T"
inductive_cases beta_cases [elim!]:
"Call s l t ->⇩β u"
"Upd s l t ->⇩β u"
"Obj s T ->⇩β t"
abbreviation
beta_reds :: "[sterm, sterm] => bool" (infixl "->>" 50) where
"s ->> t == beta^** s t"
abbreviation
beta_ascii :: "[sterm, sterm] => bool" (infixl "->" 50) where
"s -> t == beta s t"
notation (latex)
beta_reds (infixl "->⇩β⇧*" 50)
lemma beta_induct[consumes 1,
case_names CallL CallR UpdL UpdR Upd Obj beta Bnd]:
fixes
t :: sterm and t' :: sterm and
P1 :: "sterm => sterm => bool" and P2 :: "sterm => sterm => bool"
assumes
"t ->⇩β t'" and
"!!t t' u l. [| t ->⇩β t'; P1 t t'; lc u |] ==> P1 (Call t l u) (Call t' l u)" and
"!!t t' u l. [| t ->⇩β t'; P1 t t'; lc u |] ==> P1 (Call u l t) (Call u l t')" and
"!!t t' u l. [| t ->⇩β t'; P1 t t'; body u|] ==> P1 (Upd t l u) (Upd t' l u)" and
"!!t t' u l. [| P2 t t'; lc u |] ==> P1 (Upd u l t) (Upd u l t')" and
"!!l f T t. [| l ∈ dom f; lc (Obj f T); body t |]
==> P1 (Upd (Obj f T) l t) (Obj (f(l \<mapsto> t)) T)" and
"!!l f t t' T. [| l ∈ dom f; P2 t t'; ∀l∈dom f. body (the (f l)) |]
==> P1 (Obj (f(l \<mapsto> t)) T) (Obj (f(l \<mapsto> t')) T)" and
"!!l f T a. [| l ∈ dom f; lc (Obj f T); lc a |]
==> P1 (Call (Obj f T) l a) (the (f l)⇗[Obj f T,a]⇖)" 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'"
using assms by (induct rule: beta.induct, auto)
lemma Fvar_beta: "Fvar x ->⇩β t ==> False"
by (erule beta.cases, auto)
lemma Obj_beta:
assumes "Obj f T ->⇩β z"
shows
"∃l f' t t'. dom f = dom f' ∧ f = (f'(l \<mapsto> t)) ∧ l ∈ dom f'
∧ (∃L. finite L
∧ (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β t'' ∧ t'= σ[s,p]t'')))
∧ z = Obj (f'(l \<mapsto> t')) T"
proof (cases rule: beta_cases(3)[OF assms])
case (1 l fa L t t') thus ?thesis
by (rule_tac x = l in exI,
rule_tac x = fa in exI,
rule_tac x = t in exI,
rule_tac x = t' in exI, auto)
qed
lemma Upd_beta: "Upd t l u ->⇩β z ==>
(∃t'. t ->⇩β t' ∧ z = Upd t' l u)
∨(∃u' L. 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')
∨(∃f T. l ∈ dom f ∧ Obj f T = t ∧ z = Obj (f(l \<mapsto> u)) T)"
by (erule beta_cases, auto)
lemma Call_beta: "Call t l u ->⇩β z ==>
(∃t'. t ->⇩β t' ∧ z = Call t' l u) ∨ (∃u'. u ->⇩β u' ∧ z = Call t l u')
∨(∃f T. Obj f T = t ∧ l ∈ dom f ∧ z = (the (f l)⇗[Obj f T, u]⇖))"
by (erule beta_cases, auto)
subsubsection {* Properties *}
lemma beta_lc[simp]:
fixes t t'
assumes "t ->⇩β t'"
shows "lc t ∧ lc t'"
using assms
proof
(induct
taking: "λt t'. body t ∧ body t'"
rule: beta_induct)
case CallL thus ?case by simp
next
case CallR thus ?case by simp
next
case UpdR thus ?case by (simp add: lc_upd)
next
case UpdL thus ?case by (simp add: lc_upd)
next
case beta thus ?case by (simp add: obj_openz_lc)
next
case Upd thus ?case by (simp add: lc_obj lc_upd)
next
case Obj thus ?case by (simp add: lc_obj)
next
case (Bnd L t t') note cof = this(2)
from `finite L` exFresh_s_p_cof[of "L ∪ FV t"]
obtain s p where
"s ∉ L" and "s ∉ FV t" and "p ∉ L" and "p ∉ FV t" and "s ≠ p"
by auto
with cof obtain t'' where
"lc (t⇗[Fvar s, Fvar p]⇖)" and "lc t''" and
"t' = σ[s,p] t''" by auto
from
lc_body[OF this(1) `s ≠ p`]
sclose_sopen_eq_t[OF `s ∉ FV t` `p ∉ FV t` `s ≠ p`]
this(3) lc_body[OF this(2) `s ≠ p`]
show ?case by (simp add: openz_def closez_def)
qed
lemma beta_ssubst[rule_format]:
fixes t t'
assumes "t ->⇩β t'"
shows "∀x v. lc v --> [x -> v] t ->⇩β [x -> v] t'"
proof -
def pred_cof ≡ "λL t t'. (∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. t⇗[Fvar s, Fvar p]⇖ ->⇩β t'' ∧ t' = σ[s,p] t''))"
{
fix x v t t'
assume
"lc v" and
"∀x v. lc 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. lc v
--> (∃L. finite L
∧ pred_cof L ([x -> v] t) ([x -> v] t'))"
rule: beta_induct)
case CallL thus ?case by simp
next
case CallR thus ?case by simp
next
case UpdL thus ?case by simp
next
case (UpdR t t' u l) note pred = this(1)
show ?case
proof (intro strip)
fix x v assume "lc v"
from Lex[OF this pred]
obtain L where
"finite L" and "pred_cof L ([x -> v] t) ([x -> v] t')"
by auto
with ssubst_preserves_lc[OF `lc u` `lc v`]
show "[x -> v] Upd u l t ->⇩β [x -> v] Upd u l t'"
unfolding pred_cof_def
by auto
qed
next
case (beta l f T t) thus ?case
proof (intro strip, simp)
fix x v assume "lc v"
from ssubst_preserves_lc[OF `lc t` this] have "lc ([x -> v] t)"
by simp
note lem =
beta.beta[OF domssubst[OF `l ∈ dom f`]
lcobj[OF `lc (Obj f T)` `lc v`] this]
from `l ∈ dom f` have "the (ssubst_option x v (f l)) = [x -> v] the (f l)"
by auto
with lem[of x] ssubst_openz_distrib[OF `lc v`]
show
"Call (Obj (λl. ssubst_option x v (f l)) T) l ([x -> v] t)
->⇩β [x -> v] (the (f l)⇗[Obj f T, t]⇖)"
by simp
qed
next
case (Upd l f T t) thus ?case
proof (intro strip, simp)
fix x v assume "lc v"
from ssubst_preserves_body[OF `body t` `lc v`] have "body ([x -> v] t)"
by simp
from
beta.beta_Upd[OF domssubst[OF `l ∈ dom f`]
lcobj[OF `lc (Obj f T)` `lc v`] this]
ssubstoption_insert[OF `l ∈ dom f`]
show
"Upd (Obj (λl. ssubst_option x v (f l)) T) l ([x -> v] t)
->⇩β Obj (λla. ssubst_option x v (if la = l then Some t else f la)) T"
by simp
qed
next
case (Obj l f t t' T) note pred = this(2)
show ?case
proof (intro strip, simp)
fix x v assume "lc v"
note Lex[OF this pred]
from this[of x] obtain L where
"finite L" and "pred_cof L ([x -> v] t) ([x -> v] t')"
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 `lc v`]
with `l' ∈ dom f` ssubst_option_lem
show "body (the (ssubst_option x v (f l')))" by auto
qed
from
beta.beta_Obj[OF domssubst[OF `l ∈ dom f`] `finite L` _ this]
ssubstoption_insert[OF `l ∈ dom f`] `pred_cof L ([x -> v] t) ([x -> v] t')`
show
"Obj (λla. ssubst_option x v (if la = l then Some t else f la)) T
->⇩β Obj (λla. ssubst_option x v (if la = l then Some t' else f la)) T"
unfolding pred_cof_def
by simp
qed
next
case (Bnd L t t') note pred = this(2)
show ?case
proof (intro strip)
fix x v assume "lc 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 `lc v` obtain t'' where
"t⇗[Fvar s,Fvar p]⇖ ->⇩β t''" and
ssubst_beta: "[x -> v] (t⇗[Fvar s,Fvar p]⇖) ->⇩β [x -> v] t''" and
"t' = σ[s,p] t''"
by blast
assume "s ≠ x" and "p ≠ x"
hence "x ∉ FV (Fvar s)" and "x ∉ FV (Fvar p)" by auto
from ssubst_sopen_commute[OF `lc v` this] ssubst_beta
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
declare if_not_P [simp] not_less_eq [simp]
-- {* don't add @{text "r_into_rtrancl[intro!]"} *}
lemma 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: beta_induct)
case CallL thus ?case by simp
next
case CallR thus ?case by simp
next
case UpdL thus ?case by simp
next
case UpdR thus ?case by simp
next
case Upd thus ?case by simp
next
case Obj thus ?case by simp
next
case (beta l f T t) thus ?case
proof (intro strip)
assume "x ∉ FV (Call (Obj f T) l t)"
with `l ∈ dom f` have "x ∉ FV (the (f l)) ∪ FV (Obj f T) ∪ FV t"
proof (auto)
fix y :: sterm
assume "x ∈ FV y" and "f l = Some y"
hence "x ∈ FVoption (f l)"
by auto
moreover assume "∀l∈dom f. x ∉ FVoption (f l)"
ultimately show False using `l ∈ dom f`
by blast
qed
from contra_subsetD[OF sopen_FV this]
show "x ∉ FV (the (f l)⇗[Obj f T,t]⇖)" by (simp add: openz_def)
qed
next
case (Bnd L t t') thus ?case
proof (intro strip)
assume "x ∉ FV t"
from `finite L` exFresh_s_p_cof[of "L ∪ {x}"]
obtain s p where sp: "s ∉ L ∪ {x} ∧ p ∉ L ∪ {x} ∧ s ≠ p" by auto
with `x ∉ FV t` sopen_FV[of 0 "Fvar s" "Fvar p" t]
have "x ∉ FV (t⇗[Fvar s, Fvar p]⇖)" by (auto simp: openz_def)
with sp Bnd(2) obtain t'' where
"x ∉ FV t''" and "t' = σ[s,p] t''"
by auto
with sclose_subset_FV[of 0 s p t''] show "x ∉ FV t'"
by (auto simp: closez_def)
qed
qed
lemma rtrancl_beta_lc[simp, rule_format]: "t ->⇩β⇧* t' ==> t ≠ t' --> lc t ∧ lc t'"
by (erule rtranclp.induct, simp,
drule beta_lc, blast)
lemma rtrancl_beta_lc2[simp]: "[| t ->⇩β⇧* t'; lc t |] ==> lc t'"
by (case_tac "t = t'", simp+)
lemma rtrancl_beta_body:
fixes L t t'
assumes
"finite L" and
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t'' ∧ t' = σ[s,p] t'')" and
"body t"
shows "body t'"
proof (cases "t = t'")
case True with assms(3) show ?thesis by simp
next
from exFresh_s_p_cof[OF `finite L`]
obtain s p where sp: "s ∉ L ∧ p ∉ L ∧ s ≠ p" by auto
hence "s ≠ p" by simp
from assms(2) sp
obtain t'' where "t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''" and "t' = σ[s,p] t''"
by auto
with `body t` have "lc t''"
proof (cases "(t⇗[Fvar s,Fvar p]⇖) = t''")
case True with body_lc[OF `body t`] show "lc t''" by auto
next
case False with rtrancl_beta_lc[OF `t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''`]
show "lc t''" by auto
qed
from lc_body[OF this `s ≠ p`] `t' = σ[s,p] t''` show "body t'" by simp
qed
lemma rtrancl_beta_preserves_FV[simp, rule_format]:
"t ->⇩β⇧* t' ==> x ∉ FV t --> x ∉ FV t'"
proof (induct t t' rule: rtranclp.induct, simp)
case (rtrancl_into_rtrancl a b c) thus ?case
proof (clarify)
assume "x ∉ FV b" and "x ∈ FV c"
from beta_preserves_FV[OF `b ->⇩β c` this(1)] this(2)
show False by simp
qed
qed
subsubsection {* Congruence rules *}
lemma rtrancl_beta_CallL [intro!, rule_format]:
"[| t ->⇩β⇧* t'; lc u |] ==> Call t l u ->⇩β⇧* Call t' l u"
proof (induct t t' rule: rtranclp.induct, simp)
case (rtrancl_into_rtrancl a b c) thus ?case
proof (auto)
from `b ->⇩β c` `lc u` have "Call b l u ->⇩β Call c l u" by simp
with rtrancl_into_rtrancl(2)[OF `lc u`]
show "Call a l u ->⇩β⇧* Call c l u" by auto
qed
qed
lemma rtrancl_beta_CallR [intro!, rule_format]:
"[| t ->⇩β⇧* t'; lc u |] ==> Call u l t ->⇩β⇧* Call u l t'"
proof (induct t t' rule: rtranclp.induct, simp)
case (rtrancl_into_rtrancl a b c) thus ?case
proof (auto)
from `b ->⇩β c` `lc u` have "Call u l b ->⇩β Call u l c" by simp
with rtrancl_into_rtrancl(2)[OF `lc u`]
show "Call u l a ->⇩β⇧* Call u l c" by auto
qed
qed
lemma rtrancl_beta_Call [intro!, rule_format]:
"[| t ->⇩β⇧* t'; lc t; u ->⇩β⇧* u'; lc u |]
==> Call t l u ->⇩β⇧* Call t' l u'"
proof (induct t t' rule: rtranclp.induct, blast)
case (rtrancl_into_rtrancl a b c) thus ?case
proof (auto)
from `u ->⇩β⇧* u'` `lc u` have "lc u'" by auto
with `b ->⇩β c` have "Call b l u' ->⇩β Call c l u'" by simp
with rtrancl_into_rtrancl(2)[OF `lc a` `u ->⇩β⇧* u'` `lc u`]
show "Call a l u ->⇩β⇧* Call c l u'" by auto
qed
qed
lemma rtrancl_beta_UpdL:
"[| t ->⇩β⇧* t'; body u |] ==> Upd t l u ->⇩β⇧* Upd t' l u"
proof (induct t t' rule: rtranclp.induct, simp)
case (rtrancl_into_rtrancl a b c) thus ?case
proof (auto)
from `b ->⇩β c` `body u` have "Upd b l u ->⇩β Upd c l u" by simp
with rtrancl_into_rtrancl(2)[OF `body u`]
show "Upd a l u ->⇩β⇧* Upd c l u" by auto
qed
qed
lemma beta_binder[rule_format]:
fixes t t'
assumes "t ->⇩β t'"
shows
"∀L s p. finite L --> s ∉ L --> p ∉ L --> s ≠ p
--> (∃L'. finite L' ∧ (∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
--> (∃t''. (σ[s,p] t)⇗[Fvar sa,Fvar pa]⇖ ->⇩β t''
∧ σ[s,p] t' = σ[sa,pa] t'')))"
proof (intro strip)
fix L :: "fVariable set" and s :: fVariable and p :: fVariable
assume "s ≠ p"
have
"∀sa pa. sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa
--> (∃t''. (σ[s,p] t)⇗[Fvar sa,Fvar pa]⇖ ->⇩β t'' ∧ σ[s,p] t' = σ[sa,pa] t'')"
proof (intro strip)
fix sa :: fVariable and pa :: fVariable
from beta_ssubst[OF `t ->⇩β t'`]
have "[p -> Fvar pa] t ->⇩β [p -> Fvar pa] t'" by simp
from beta_ssubst[OF this]
have
betasubst: "[s -> Fvar sa] [p -> Fvar pa] t ->⇩β [s -> Fvar sa] [p -> Fvar pa] t'"
by simp
from beta_lc[OF `t ->⇩β t'`] have "lc t" and "lc t'" by auto
assume
sapa: "sa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ pa ∉ L ∪ FV t ∪ {s} ∪ {p} ∧ sa ≠ pa"
hence "s ∉ FV (Fvar pa)" by auto
from
sopen_sclose_eq_ssubst[OF `s ≠ p` this `lc t`]
sopen_sclose_eq_ssubst[OF `s ≠ p` this `lc t'`]
betasubst
have "σ[s,p] t⇗[Fvar sa, Fvar pa]⇖ ->⇩β (σ[s,p] t'⇗[Fvar sa, Fvar pa]⇖)"
by (simp add: openz_def closez_def)
moreover
{
from sapa have "sa ∉ FV t" by simp
from
contra_subsetD[OF sclose_subset_FV
beta_preserves_FV[OF `t ->⇩β t'` this]]
have "sa ∉ FV (σ[s,p] t')" by (simp add: closez_def)
moreover
from sapa have "pa ∉ FV t" by simp
from
contra_subsetD[OF sclose_subset_FV
beta_preserves_FV[OF `t ->⇩β t'` this]]
have "pa ∉ FV (σ[s,p] t')" by (simp add: closez_def)
ultimately
have "sa ∉ FV (σ[s,p] t')" and "pa ∉ FV (σ[s,p] t')" and "sa ≠ pa"
using sapa
by auto
note sym[OF sclose_sopen_eq_t[OF this]]
}
ultimately
show
"∃t''. σ[s,p] t⇗[Fvar sa,Fvar pa]⇖ ->⇩β t'' ∧ σ[s,p] t' = σ[sa,pa] t''"
by (auto simp: openz_def closez_def)
qed
moreover assume "finite L"
ultimately
show
"∃L'. finite L' ∧ (∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
--> (∃t''. σ[s,p] t⇗[Fvar sa,Fvar pa]⇖ ->⇩β t''
∧ σ[s,p] t' = σ[sa,pa] t''))"
by (rule_tac x = "L ∪ FV t ∪ {s} ∪ {p}" in exI, simp)
qed
lemma rtrancl_beta_UpdR:
fixes L t t' u l
assumes
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. (t⇗[Fvar s, Fvar p]⇖) ->⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
"finite L" and "lc u"
shows "Upd u l t ->⇩β⇧* Upd u l t'"
proof -
from `finite L` have "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
with assms(1) obtain t'' where "t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''" and t': "t' = σ[s,p] t''"
by auto
with `lc u` have "Upd u l t ->⇩β⇧* Upd u l σ[s,p] t''"
proof (erule_tac rtranclp_induct)
from sp have "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" by auto
from sclose_sopen_eq_t[OF this]
show "Upd u l t ->⇩β⇧* Upd u l (σ[s,p](t⇗[Fvar s,Fvar p]⇖))"
by (simp add: openz_def closez_def)
next
fix y :: sterm and z :: sterm
assume "y ->⇩β z"
from sp have "s ∉ L" and "p ∉ L" and "s ≠ p" by auto
from beta_binder[OF `y ->⇩β z` `finite L` this]
obtain L' where
"finite L'" and
"∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
--> (∃t''. σ[s,p] y⇗[Fvar sa,Fvar pa]⇖ ->⇩β t'' ∧ σ[s,p] z = σ[sa,pa] t'')"
by auto
from beta.beta_UpdR[OF this `lc u`]
have "Upd u l (σ[s,p] y) ->⇩β Upd u l (σ[s,p] z)" by assumption
moreover assume "Upd u l t ->⇩β⇧* Upd u l (σ[s,p] y)"
ultimately show "Upd u l t ->⇩β⇧* Upd u l (σ[s,p] z)" by simp
qed
with t' show "Upd u l t ->⇩β⇧* Upd u l t'" by simp
qed
lemma rtrancl_beta_Upd:
"[| u ->⇩β⇧* u'; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t'' ∧ t' = σ[s,p]t'');
lc u; body t |]
==> Upd u l t ->⇩β⇧* Upd u' l t'"
proof (induct u u' rule: rtranclp.induct)
case rtrancl_refl thus ?case by (simp add: rtrancl_beta_UpdR)
next
case (rtrancl_into_rtrancl a b c) thus ?case
proof (auto)
from rtrancl_beta_body[OF `finite L` rtrancl_into_rtrancl(5) `body t`] `b ->⇩β c`
have "Upd b l t' ->⇩β Upd c l t'" by simp
with rtrancl_into_rtrancl(2)[OF `finite L` rtrancl_into_rtrancl(5) `lc a` `body t`]
show "Upd a l t ->⇩β⇧* Upd c l t'" by simp
qed
qed
lemma rtrancl_beta_obj:
fixes l f L T t t'
assumes
"l ∈ dom f" and "finite L" and
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
"∀l∈dom f. body (the(f l))" and "body t"
shows "Obj (f (l \<mapsto> t)) T ->⇩β⇧* Obj (f (l \<mapsto> t')) T"
proof -
from `finite L` have "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
with assms(3) obtain t'' where "t⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''" and "t' = σ[s,p] t''"
by auto
with `l ∈ dom f` `∀l∈dom f. body (the(f l))`
have "Obj (f(l \<mapsto> t)) T ->⇩β⇧* Obj (f(l \<mapsto> σ[s,p] t'')) T"
proof (erule_tac rtranclp_induct)
from sp have "s ∉ FV t" and "p ∉ FV t" and "s ≠ p" by auto
from sclose_sopen_eq_t[OF this]
show "Obj (f(l \<mapsto> t)) T ->⇩β⇧* Obj (f(l \<mapsto> σ[s,p] (t⇗[Fvar s,Fvar p]⇖))) T"
by (simp add: openz_def closez_def)
next
fix y :: sterm and z :: sterm assume "y ->⇩β z"
from sp have "s ∉ L" and "p ∉ L" and "s ≠ p" by auto
from beta_binder[OF `y ->⇩β z` `finite L` this]
obtain L' where
"finite L'" and
"∀sa pa. sa ∉ L' ∧ pa ∉ L' ∧ sa ≠ pa
--> (∃t''. σ[s,p] y⇗[Fvar sa,Fvar pa]⇖ ->⇩β t'' ∧ σ[s,p] z = σ[sa,pa] t'')"
by auto
from beta.beta_Obj[OF `l ∈ dom f` this `∀l∈dom f. body (the(f l))`]
have "Obj (f(l \<mapsto> σ[s,p] y)) T ->⇩β Obj (f(l \<mapsto> σ[s,p] z)) T"
by assumption
moreover assume "Obj (f(l \<mapsto> t)) T ->⇩β⇧* Obj (f(l \<mapsto> σ[s,p] y)) T"
ultimately
show "Obj (f(l \<mapsto> t)) T ->⇩β⇧* Obj (f(l \<mapsto> σ[s,p] z)) T" by simp
qed
with `t' = σ[s,p] t''` show "Obj (f(l \<mapsto> t)) T ->⇩β⇧* Obj (f(l \<mapsto> t')) T"
by simp
qed
lemma obj_lem:
fixes l f T L t'
assumes
"l ∈ dom f" and "finite L" and
"∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. ((the(f l))⇗[Fvar s,Fvar p]⇖) ->⇩β⇧* t'' ∧ t' = σ[s,p]t'')" and
"∀l∈dom f. body (the(f l))"
shows "Obj f T ->⇩β⇧* Obj (f(l \<mapsto> t')) T"
proof
(rule_tac P = "λy. Obj y T ->⇩β⇧* Obj (f(l \<mapsto> t')) T" and s = "(f(l \<mapsto> the(f l)))"
in subst)
from `l ∈ dom f` fun_upd_idem show "f(l \<mapsto> the (f l)) = f" by force
next
from `l ∈ dom f` `∀l∈dom f. body (the(f l))` have "body (the (f l))"
by blast
with
rtrancl_beta_obj[OF `l ∈ dom f` `finite L` assms(3) `∀l∈dom f. body (the(f l))`]
show "Obj (f(l \<mapsto> the (f l))) T ->⇩β⇧* Obj (f(l \<mapsto> t')) T" by simp
qed
lemma rtrancl_beta_obj_lem00:
fixes L f g
assumes
"finite L" and
"∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. ((the(f l))⇗[Fvar s, Fvar p]⇖) ->⇩β⇧* t''
∧ the(g l) = σ[s,p]t'')" and
"dom f = dom g" and "∀l∈dom f. body (the (f l))"
shows
"∀k ≤ (card (dom f)).
(∃ob. length ob = (k + 1)
∧ (∀obi. obi ∈ set ob --> dom (fst(obi)) = dom f ∧ ((snd obi) ⊆ dom f))
∧ (fst (ob!0) = f)
∧ (card (snd (ob!k)) = k)
∧ (∀i < k. snd (ob!i) ⊂ snd (ob!k))
∧ (Obj (fst (ob!0)) T ->⇩β⇧* Obj (fst (ob!k)) T)
∧ (card (snd (ob!k)) = k
--> (Ltake_eq (snd (ob!k)) (fst (ob!k)) g)
∧ (Ltake_eq ((dom f) - (snd (ob!k))) (fst (ob!k)) f)))"
proof
fix k :: nat
show
"k ≤ card (dom f)
--> (∃ob. length ob = k + 1
∧ (∀obi. obi ∈ set ob --> dom (fst obi) = dom f ∧ snd obi ⊆ dom f)
∧ fst (ob ! 0) = f
∧ card (snd (ob ! k)) = k
∧ (∀i<k. snd (ob ! i) ⊂ snd (ob ! k))
∧ Obj (fst (ob ! 0)) T ->⇩β⇧* Obj (fst (ob ! k)) T
∧ (card (snd (ob ! k)) = k
--> Ltake_eq (snd (ob ! k)) (fst (ob ! k)) g
∧ Ltake_eq (dom f - snd (ob ! k)) (fst (ob ! k)) f))"
proof (induct k)
case 0 thus ?case
by (simp, rule_tac x = "[(f,{})]" in exI, simp add: Ltake_eq_def)
next
case (Suc k) thus ?case
proof (clarify)
assume "Suc k ≤ card (dom f)" hence "k < card (dom f)" by arith
with Suc.hyps
obtain ob where
"length ob = k + 1" and
mem_ob: "∀obi. obi ∈ set ob
--> dom (fst obi) = dom f ∧ snd obi ⊆ dom f" and
"fst (ob ! 0) = f" and
"card (snd (ob ! k)) = k" and
"∀i<k. snd (ob ! i) ⊂ snd (ob ! k)" and
"Obj (fst (ob ! 0)) T ->⇩β⇧* Obj (fst (ob ! k)) T" and
card_k: "card (snd (ob ! k)) = k
--> Ltake_eq (snd (ob ! k)) (fst (ob ! k)) g
∧ Ltake_eq (dom f - snd (ob ! k)) (fst (ob ! k)) f"
by auto
from `length ob = k + 1` have obkmem: "(ob!k) ∈ set ob" by auto
with mem_ob have obksnd: "snd(ob!k) ⊆ dom f" by blast
from
card_psubset[OF finite_dom_fmap this] `card (snd(ob!k)) = k`
`k < card (dom f)`
have "snd (ob!k) ⊂ dom f" by simp
then obtain l' where "l' ∈ dom f" and "l' ∉ snd (ob!k)" by auto
from obkmem mem_ob have obkfst: "dom (fst(ob!k)) = dom f" by blast
def ob' ≡ "ob @ [(fst(ob!k)(l' \<mapsto> the (g l')), insert l' (snd(ob!k)))]"
from nth_fst[OF `length ob = k + 1`] have first: "ob'!0 = ob!0"
by (simp add: ob'_def)
from `length ob = k + 1` nth_last[of ob "Suc k"]
have last: "ob'!Suc k = (fst(ob!k)(l' \<mapsto> the (g l')), insert l' (snd(ob!k)))"
by (simp add: ob'_def)
from `length ob = k + 1` nth_append[of ob _ k] have kth: "ob'!k = ob!k"
by (auto simp: ob'_def)
from `card (snd(ob!k)) = k` card_k
have ass:
"∀l∈(snd(ob!k)). fst(ob!k) l = g l"
"∀l∈(dom f - snd(ob!k)). fst(ob!k) l = f l"
by (auto simp: Ltake_eq_def)
from `length ob = k + 1` have "length ob' = Suc k + 1"
by (auto simp: ob'_def)
moreover
have "∀obi. obi ∈ set ob' --> dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
unfolding ob'_def
proof (intro strip)
fix obi :: "(Label -~> sterm) × (Label set)"
assume "obi ∈ set (ob @ [(fst(ob!k)(l' \<mapsto> the (g l')), insert l' (snd (ob!k)))])"
note mem_append_lem'[OF this]
thus "dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
proof (rule disjE, simp_all)
assume "obi ∈ set ob"
with mem_ob show "dom (fst obi) = dom f ∧ snd obi ⊆ dom f"
by blast
next
from obkfst obksnd `l' ∈ dom f`
show
"insert l' (dom (fst (ob!k))) = dom f
∧ l' ∈ dom f ∧ snd(ob!k) ⊆ dom f"
by blast
qed
qed
moreover
from first `fst(ob!0) = f` have "fst(ob'!0) = f" by simp
moreover
from obksnd finite_dom_fmap finite_subset
have "finite (snd (ob!k))" by auto
from card_insert[OF this]
have "card (insert l' (snd (ob!k))) = Suc (card (snd(ob!k) - {l'}))"
by simp
with `l' ∉ snd (ob!k)` `card (snd(ob!k)) = k` last
have "card(snd(ob'!Suc k)) = Suc k" by auto
moreover
have "∀i<Suc k. snd (ob'!i) ⊂ snd (ob'!Suc k)"
proof (intro strip)
fix i :: nat
from last have "snd(ob'!Suc k) = insert l' (snd (ob!k))" by simp
with `l' ∉ snd (ob!k)` have "snd(ob!k) ⊂ snd(ob'!Suc k)" by auto
moreover
assume "i < Suc k"
with `length ob = k + 1` have "i < length ob" by simp
with nth_append[of ob _ i] have "ob'!i = ob!i" by (simp add: ob'_def)
ultimately show "snd(ob'!i) ⊂ snd(ob'!Suc k)"
proof (cases "i < k")
case True
with
`∀i<k. snd(ob!i) ⊂ snd(ob!k)` `ob'!i = ob!i`
`snd(ob!k) ⊂ snd(ob'!Suc k)`
show "snd (ob'!i) ⊂ snd (ob'!Suc k)" by auto
next
case False with `i < Suc k` have "i = k" by arith
with `ob'!i = ob!i` `snd(ob!k) ⊂ snd(ob'!Suc k)`
show "snd (ob'!i) ⊂ snd (ob'!Suc k)" by auto
qed
qed
moreover
{
from `l' ∈ dom f` `l' ∉ snd(ob!k)` have "l' ∈ (dom f - snd(ob!k))"
by auto
with ass have "the(fst(ob!k) l') = the(f l')" by auto
with `l' ∈ dom f` assms(2)
have
sp: "∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. the(fst(ob!k) l')⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t''
∧ the (g l') = σ[s,p] t'')"
by simp
moreover
have "∀l∈dom (fst(ob!k)). body (the(fst(ob!k) l))"
proof (intro strip)
fix la :: Label
assume "la ∈ dom (fst(ob!k))"
with obkfst have inf: "la ∈ dom f" by auto
with assms(4) have bodyf: "body (the(f la))" by auto
show "body (the(fst(ob!k) la))"
proof (cases "la ∈ snd(ob!k)")
case False with inf have "la ∈ (dom f - snd(ob!k))" by auto
with ass have "fst(ob!k) la = f la" by blast
with bodyf show "body (the (fst(ob!k) la))" by auto
next
from exFresh_s_p_cof[OF `finite L`]
obtain s p where "s ∉ L ∧ p ∉ L ∧ s ≠ p" by auto
with assms(2) inf
obtain t' where
"the (f la)⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t'" and
"the (g la) = σ[s,p] t'" by blast
from body_lc[OF bodyf] have lcf: "lc (the (f la)⇗[Fvar s,Fvar p]⇖)" by auto
hence bodyg: "body (the(g la))"
proof (cases "(the (f la)⇗[Fvar s,Fvar p]⇖) = t'")
case True
with
lcf lc_body `s ∉ L ∧ p ∉ L ∧ s ≠ p`
`the(g la) = σ[s,p] t'`
show "body (the(g la))" by auto
next
case False
with
rtrancl_beta_lc[OF `the (f la)⇗[Fvar s,Fvar p]⇖ ->⇩β⇧* t'`]
lc_body `s ∉ L ∧ p ∉ L ∧ s ≠ p` `the(g la) = σ[s,p] t'`
show "body (the(g la))" by auto
qed
case True with ass bodyg show "body (the(fst(ob!k) la))" by simp
qed
qed
moreover
from `l' ∈ dom f` obkfst have "l' ∈ dom(fst(ob!k))" by auto
note obj_lem[OF this `finite L`]
ultimately
have "Obj (fst(ob!k)) T ->⇩β⇧* Obj (fst(ob!k)(l' \<mapsto> the (g l'))) T"
by blast
moreover
from last have "fst(ob'!Suc k) = fst(ob!k)(l' \<mapsto> the (g l'))"
by auto
ultimately
have "Obj (fst(ob'!0)) T ->⇩β⇧* Obj (fst(ob'!Suc k)) T"
using
rtranclp_trans[OF `Obj (fst (ob!0)) T ->⇩β⇧* Obj (fst (ob!k)) T`] first kth
by auto
}
moreover
from `l' ∈ dom f` `dom f = dom g`
have
"card (snd(ob'!Suc k)) = Suc k
--> Ltake_eq (snd (ob'!Suc k)) (fst (ob'!Suc k)) g
∧ Ltake_eq (dom f - snd(ob'!Suc k)) (fst(ob'!Suc k)) f"
by (auto simp: Ltake_eq_def last ass)
ultimately
show
"∃ob. length ob = Suc k + 1
∧ (∀obi. obi ∈ set ob --> dom (fst obi) = dom f ∧ snd obi ⊆ dom f)
∧ fst (ob ! 0) = f
∧ card (snd (ob ! Suc k)) = Suc k
∧ (∀i<Suc k. snd (ob ! i) ⊂ snd (ob ! Suc k))
∧ Obj (fst (ob ! 0)) T ->⇩β⇧* Obj (fst (ob ! Suc k)) T
∧ (card (snd (ob ! Suc k)) = Suc k
--> Ltake_eq (snd (ob ! Suc k)) (fst (ob ! Suc k)) g
∧ Ltake_eq (dom f - snd (ob ! Suc k)) (fst (ob ! Suc k)) f)"
by (rule_tac x = ob' in exI, simp)
qed
qed
qed
lemma rtrancl_beta_obj_n:
fixes f g L T
assumes
"finite L" and
"∀l∈dom f. ∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> (∃t''. ((the(f l))⇗[Fvar s, Fvar p]⇖) ->⇩β⇧* t''
∧ the(g l) = σ[s,p]t'')" and
"dom f = dom g" and "∀l∈dom f. body (the(f l))"
shows "Obj f T ->⇩β⇧* Obj g T"
proof (cases "f = empty")
case True with `dom f = dom g` have "{} = dom g" by simp
from `f = empty` empty_dom[OF this] show ?thesis by simp
next
from rtrancl_beta_obj_lem00[OF assms]
obtain ob :: "((Label -~> sterm) × (Label set)) list"
where
"length ob = card(dom f) + 1" and
"∀obi. obi ∈ set ob --> dom (fst obi) = dom f ∧ snd obi ⊆ dom f" and
"fst(ob!0) = f" and
"card (snd(ob!card(dom f))) = card(dom f)" and
"Obj (fst(ob!0)) T ->⇩β⇧* Obj (fst(ob!card(dom f))) T" and
"Ltake_eq (snd(ob!card(dom f))) (fst(ob!card(dom f))) g"
by blast
from `length ob = card (dom f) + 1` have "(ob!card(dom f)) ∈ set ob" by auto
with `∀obi. obi ∈ set ob --> dom (fst obi) = dom f ∧ snd obi ⊆ dom f`
have "dom (fst(ob!card(dom f))) = dom f" and "snd(ob!card(dom f)) ⊆ dom f"
by blast+
{
fix l :: Label
from
`snd(ob!card(dom f)) ⊆ dom f` `card (snd(ob!card(dom f))) = card(dom f)`
Ltake_eq_dom
have "snd(ob!card(dom f)) = dom f" by blast
with `Ltake_eq (snd(ob!card (dom f))) (fst(ob!card (dom f))) g`
have "fst(ob!card(dom f)) l = g l"
proof (cases "l ∈ dom f", simp_all add: Ltake_eq_def)
assume "l ∉ dom f"
with `dom f = dom g` `dom (fst(ob!card(dom f))) = dom f`
show "fst(ob!card(dom f)) l = g l" by auto
qed
}
with ext have "fst(ob!card(dom f)) = g" by auto
with `fst(ob!0) = f` `Obj (fst(ob!0)) T ->⇩β⇧* Obj (fst(ob!card (dom f))) T`
show "Obj f T ->⇩β⇧* Obj g T" by simp
qed
subsection {*Size of sterms*}
definition fsize0 :: "(Label -~> sterm) => (sterm => nat) => nat" where
"fsize0 f sts =
foldl (op +) 0 (map sts (Finite_Set.fold (λx z. z@[THE y. Some y = f x]) [] (dom f)))"
primrec
ssize :: "sterm => nat"
and
ssize_option :: "sterm option => nat"
where
ssize_Bvar : "ssize (Bvar b) = 0"
| ssize_Fvar : "ssize (Fvar x) = 0"
| ssize_Call : "ssize (Call a l b) = (ssize a) + (ssize b) + Suc 0"
| ssize_Upd : "ssize (Upd a l b) = (ssize a) + (ssize b) + Suc 0"
| ssize_Obj : "ssize (Obj f T) = Finite_Set.fold (λx y. y + ssize_option (f x)) (Suc 0) (dom f)"
| ssize_None : "ssize_option (None) = 0"
| ssize_Some : "ssize_option (Some y) = ssize y + Suc 0"
interpretation comp_fun_commute "(λx y::nat. y + (f x))"
by (unfold comp_fun_commute_def, force)
lemma SizeOfObjectPos: "ssize (Obj (f::Label -~> sterm) T) > 0"
proof (simp)
from finite_dom_fmap have "finite (dom f)" by auto
thus "0 < Finite_Set.fold (λx y. y + ssize_option (f x)) (Suc 0) (dom f)"
proof (induct)
case empty thus ?case by simp
next
case (insert A a) thus ?case by auto
qed
qed
end