Up to index of Isabelle/HOL/Locally-Nameless-Sigma
theory TypedSigma(* Title: Sigma/Typed_Sigma.thy
Author: Florian Kammuller and Henry Sudhof, 2006
*)
header {* First Order Types for Sigma terms *}
theory TypedSigma imports "../preliminary/Environments" Sigma begin
subsubsection {* Types and typing rules *}
text{* The inductive definition of the typing relation.*}
definition
return :: "(type × type) => type" where
"return a = fst a"
definition
param :: "(type × type) => type" where
"param a = snd a"
primrec
do :: "type => (Label set)"
where
"do (Object l) = (dom l)"
primrec
type_get :: "type => Label => (type × type) option " ("_^_" 1000)
where
"(Object l)^n = (l n)"
(* we need to restrict objects to ok environments,
as the empty object does not yield ok env otherwise *)
inductive
typing :: "(type environment) => sterm => type => bool"
("_ \<turnstile> _ : _" [80, 0, 80] 230)
where
T_Var[intro!]:
"[| ok env; x ∈ env_dom env; (the (env!x)) = T |]
==> env \<turnstile> (Fvar x) : T"
| T_Obj[intro!]:
"[| ok env; dom b = do A; finite F;
∀l∈do A. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:A|)),(|p:param(the (A^l))|)),
\<turnstile> (the (b l)⇗[Fvar s,Fvar p]⇖) : return(the (A^l)) |]
==> env \<turnstile> (Obj b A) : A"
| T_Upd[intro!]:
"[| finite F;
∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:A|)),(|p:param(the (A^l))|)),
\<turnstile> (n⇗[Fvar s,Fvar p]⇖) : return(the (A^l));
env \<turnstile> a : A; l ∈ do A |] ==> env \<turnstile> Upd a l n : A"
| T_Call[intro!]:
"[| env \<turnstile> a : A; env \<turnstile> b : param(the (A^l)); l ∈ do A |]
==> env \<turnstile> (Call a l b) : return(the (A^l))"
inductive_cases typing_elims [elim!]:
"e \<turnstile> Obj b T : T"
"e \<turnstile> Fvar x : T"
"e \<turnstile> Call a l b : T"
"e \<turnstile> Upd a l n : T"
subsubsection {*Basic lemmas *}
text{*Basic treats of the type system.*}
lemma not_bvar: "e \<turnstile> t : T ==> ∀i. t ≠ Bvar i"
by (erule typing.cases, simp_all)
lemma typing_regular': "e \<turnstile> t : T ==> ok e"
by (induct rule:typing.induct, auto)
lemma typing_regular'': "e \<turnstile> t : T ==> lc t"
by (induct rule:typing.induct, auto)
theorem typing_regular: "e \<turnstile> t : T ==> ok e ∧ lc t"
by (simp add: typing_regular' typing_regular'')
lemma obj_inv: "e \<turnstile> Obj f U : A ==> A = U"
by (erule typing.cases, auto)
lemma obj_inv_elim:
"e \<turnstile> Obj f U : U
==> (dom f = do U)
∧ (∃F. finite F ∧ (∀l∈do U. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> e(|s:U|)),(|p:param(the U^l)|)),
\<turnstile> (the (f l)⇗[Fvar s,Fvar p]⇖) : return(the (U^l))))"
by (erule typing.cases, simp_all, blast)
lemma typing_induct[consumes 1, case_names Fvar Call Upd Obj Bnd]:
fixes
env :: "type environment" and t :: sterm and T :: type and
P1 :: "type environment => sterm => type => bool" and
P2 :: "type environment => sterm => type => Label => bool"
assumes
"env \<turnstile> t : T" and
"!!env T x. [| ok env; x ∈ env_dom env; the env!x = T |]
==> P1 env (Fvar x) T" and
"!!env T t l p. [| env \<turnstile> t : T; P1 env t T; env \<turnstile> p : param (the(T^l));
P1 env p (param (the(T^l))); l ∈ do T |]
==> P1 env (Call t l p) (return (the(T^l)))" and
"!!env T t l u. [| env \<turnstile> t : T; P1 env t T; l ∈ do T; P2 env u T l |]
==> P1 env (Upd t l u) T" and
"!!env T f. [| ok env; dom f = do T; ∀l∈dom f. P2 env (the(f l)) T l |]
==> P1 env (Obj f T) T" and
"!!env T l t L. [| ok env; finite L;
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> env(|s:T|)),(|p:param (the(T^l))|)),
\<turnstile> (t⇗[Fvar s, Fvar p]⇖) : return (the(T^l))
∧ P1 (env(|s:T|)),(|p:param (the(T^l))|)),) (t⇗[Fvar s, Fvar p]⇖)
(return (the(T^l))) |]
==> P2 env t T l"
shows
"P1 env t T"
using assms by (induct rule: typing.induct, auto simp: typing_regular')
(* TODO: delete after refactoring of disjunct_env *)
lemma ball_Tltsp:
fixes
P1 :: "type => Label => sterm => string => string => bool" and
P2 :: "type => Label => sterm => string => string => bool"
assumes
"!!l t t'. [| ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p --> P1 T l t s p |]
==> ∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p --> P2 T l t s p" and
"∀l∈do T. ∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p --> P1 T l (the(f l)) s p"
shows "∀l∈do T. ∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p --> P2 T l (the(f l)) s p"
proof
fix l assume "l ∈ do T"
with assms(2)
have "∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p --> P1 T l (the(f l)) s p"
by simp
with assms(1)
show "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p --> P2 T l (the(f l)) s p"
by simp
qed
(* TODO: delete after refactoring of subject_reduction *)
lemma ball_ex_finite:
fixes
S :: "'a set" and F :: "'b set" and x :: 'a and
P :: "'a => 'b => 'b => bool"
assumes
"finite S" and "finite F" and
"∀x∈S. (∃F'. finite F'
∧ (∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
--> P x s p))"
shows
"∃F'. finite F'
∧ (∀x∈S. ∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
--> P x s p)"
proof -
from assms show ?thesis
proof (induct S)
case empty thus ?case by force
next
case (insert x S)
from insert(5)
have
"∀y∈S. (∃F'. finite F'
∧ (∀s p. s ∉ F' ∪ F ∧ p ∉ F' ∪ F ∧ s ≠ p
--> P y s p))"
by simp
from insert(3)[OF `finite F` this]
obtain F1 where
"finite F1" and
pred_S: "∀y∈S. ∀s p. s ∉ F1 ∪ F ∧ p ∉ F1 ∪ F ∧ s ≠ p
--> P y s p"
by auto
from insert(5)
obtain F2 where
"finite F2" and
"∀s p. s ∉ F2 ∪ F ∧ p ∉ F2 ∪ F ∧ s ≠ p --> P x s p"
by auto
with pred_S have
"∀y∈insert x S. ∀s p. s ∉ F1 ∪ F2 ∪ F ∧ p ∉ F1 ∪ F2 ∪ F ∧ s ≠ p
--> P y s p"
by auto
moreover
from `finite F1` `finite F2` have "finite (F1 ∪ F2)" by simp
ultimately
show ?case by blast
qed
qed
(* TODO: delete after refactoring of type_renaming' *)
lemma bnd_renaming_lem:
assumes
"s ∉ FV t'" and "p ∉ FV t'" and "x ∉ FV t'" and "y ∉ FV t'" and
"x ∉ env_dom env'" and "y ∉ env_dom env'" and "s ≠ p" and "x ≠ y" and
"t = {Suc n -> [Fvar s, Fvar p]} t'" and "env = env'(|s:A|)),(|p:B|))," and
pred_bnd:
"∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
--> env(|sa:T|)),(|pa:param(the(T^l))|)), \<turnstile> (t⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
∧ (∀env'' t'' s' p' x' y' A' B' n'.
s' ∉ FV t'' --> p' ∉ FV t'' --> x' ∉ FV t'' --> y' ∉ FV t'' -->
x' ∉ env_dom env'' --> y' ∉ env_dom env'' --> x' ≠ y' --> s' ≠ p'
--> (t⇗[Fvar sa,Fvar pa]⇖) = {n' -> [Fvar s',Fvar p']} t''
--> env(|sa:T|)),(|pa:param(the(T^l))|)), = env''(|s':A'|)),(|p':B'|)),
--> env''(|x':A'|)),(|y':B'|)),
\<turnstile> {n' -> [Fvar x',Fvar y']} t'' : return(the(T^l)))" and
"FV t' ⊆ F'"
shows
"∀sa pa. sa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'
∧ pa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'
∧ sa ≠ pa
--> env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> ({Suc n -> [Fvar x, Fvar y]} t'⇗[Fvar sa,Fvar pa]⇖) : return (the(T^l))"
proof (intro strip, elim conjE)
fix sa pa
assume
nin_sa: "sa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'" and
nin_pa: "pa ∉ F ∪ {s,p,x,y} ∪ F' ∪ env_dom env'" and "sa ≠ pa"
hence "sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa" by auto
moreover
{
fix a assume "a ∉ FV t'" and "a ∈ {s,p,x,y}"
with
`FV t' ⊆ F'` nin_sa nin_pa `sa ≠ pa`
sopen_FV[of 0 "Fvar sa" "Fvar pa" t']
have "a ∉ FV (t'⇗[Fvar sa,Fvar pa]⇖)" by (auto simp: openz_def)
} note
this[OF `s ∉ FV t'`] this[OF `p ∉ FV t'`]
this[OF `x ∉ FV t'`] this[OF `y ∉ FV t'`]
moreover
from
not_in_env_bigger_2[OF `x ∉ env_dom env'`]
not_in_env_bigger_2[OF `y ∉ env_dom env'`]
nin_sa nin_pa
have
"x ∉ env_dom (env'(|sa:T|)),(|pa:param(the(T^l))|)),)
∧ y ∉ env_dom (env'(|sa:T|)),(|pa:param(the(T^l))|)),)" by auto
moreover
from `t = {Suc n -> [Fvar s, Fvar p]} t'` sopen_commute[OF Suc_not_Zero]
have "(t⇗[Fvar sa,Fvar pa]⇖) = {Suc n -> [Fvar s,Fvar p]} (t'⇗[Fvar sa,Fvar pa]⇖)"
by (auto simp: openz_def)
moreover
from
subst_add[of s sa env' A T] subst_add[of sa p "env'(|s:A|))," T B]
subst_add[of s pa "env'(|sa:T|))," A "param(the(T^l))"]
subst_add[of p pa "env'(|sa:T|)),(|s:A|))," B "param(the(T^l))"]
`env = env'(|s:A|)),(|p:B|)),` nin_sa nin_pa
have "env(|sa:T|)),(|pa:param(the(T^l))|)), = env'(|sa:T|)),(|pa:param(the(T^l))|)),(|s:A|)),(|p:B|)),"
by auto
ultimately
have
"env'(|sa:T|)),(|pa:param(the T^l)|)),(|x:A|)),(|y:B|)),
\<turnstile> {Suc n -> [Fvar x, Fvar y]} (t'⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
using `s ≠ p` `x ≠ y` pred_bnd by auto
moreover
from
subst_add[of y sa "env'(|x:A|))," B T] subst_add[of x sa env' A T]
subst_add[of y pa "env'(|sa:T|)),(|x:A|))," B "param(the(T^l))"]
subst_add[of x pa "env'(|sa:T|))," A "param(the(T^l))"]
nin_sa nin_pa
have
"env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
= env'(|sa:T|)),(|pa:param(the(T^l))|)),(|x:A|)),(|y:B|)),"
by auto
ultimately
show
"env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> ({Suc n -> [Fvar x, Fvar y]} t'⇗[Fvar sa,Fvar pa]⇖) : return (the(T^l))"
using sopen_commute[OF not_sym[OF Suc_not_Zero]]
by (simp add: openz_def)
qed
(* TODO: refactor to work with typing_induct *)
lemma type_renaming'[rule_format]:
"e \<turnstile> t : C ==>
(!!env t' s p x y A B n. [| s ∉ FV t'; p ∉ FV t'; x ∉ FV t'; y ∉ FV t';
x ∉ env_dom env; y ∉ env_dom env; s ≠ p; x ≠ y;
t = {n -> [Fvar s,Fvar p]} t'; e = env(|s:A|)),(|p:B|)), |]
==> env(|x:A|)),(|y:B|)), \<turnstile> {n -> [Fvar x,Fvar y]} t' : C)"
proof (induct set:typing)
case (T_Call env t1 T t2 l env' t' s p x y A B n)
with sopen_eq_Call[OF sym[OF `Call t1 l t2 = {n -> [Fvar s,Fvar p]} t'`]]
show ?case by auto
next
case (T_Var env a T env' t' s p x y A B n)
from `ok env` `env = env'(|s:A|)),(|p:B|)),` ok_add_2[of env' s A p B]
have "ok env'" by simp
from
ok_add_ok[OF ok_add_ok[OF this `x ∉ env_dom env'`]
not_in_env_bigger[OF `y ∉ env_dom env'` not_sym[OF `x ≠ y`]]]
have ok: "ok (env'(|x:A|)),(|y:B|)),)" by assumption
from sopen_eq_Fvar[OF sym[OF `Fvar a = {n -> [Fvar s,Fvar p]} t'`]]
show ?case
proof (elim disjE conjE)
assume "t' = Fvar a" with T_Var(4-7)
obtain "a ≠ s" and "a ≠ p" and "a ≠ x" and "a ≠ y" by auto
note in_env_smaller2[OF _ this(1-2)]
from `a ∈ env_dom env` `env = env'(|s:A|)),(|p:B|)),` this[of env' A B]
have "a ∈ env_dom env'" by simp
from env_bigger2[OF `x ∉ env_dom env'` `y ∉ env_dom env'` this `x ≠ y`]
have inenv: "a ∈ env_dom (env'(|x:A|)),(|y:B|)),)" by assumption
note get_env_bigger2[OF _ `a ≠ s` `a ≠ p`]
from
this[of env' A B] `a ∈ env_dom env` `the env!a = T`
`env = env'(|s:A|)),(|p:B|)),` get_env_bigger2[OF inenv `a ≠ x` `a ≠ y`]
have "the (env'(|x:A|)),(|y:B|)),!a) = T" by simp
from typing.T_Var[OF ok inenv this] `t' = Fvar a` show ?case by simp
next
assume "a = s" and "t' = Bvar (Self n)"
from
this(1) `ok env` `env = env'(|s:A|)),(|p:B|)),` `the env!a = T`
add_get2_1[of env' s A p B]
have "T = A" by simp
moreover
from `t' = Bvar (Self n)` have "{n -> [Fvar x,Fvar y]} t' = Fvar x" by simp
ultimately
show ?case using in_add_2[OF ok] typing.T_Var[OF ok _ add_get2_1[OF ok]]
by simp
next
note subst = subst_add[OF `x ≠ y`]
from subst[of env' A B] ok have ok': "ok (env'(|y:B|)),(|x:A|)),)" by simp
assume "a = p" and "t' = Bvar (Param n)"
from
this(1) `ok env` `env = env'(|s:A|)),(|p:B|)),` `the env!a = T`
add_get2_2[of env' s A p B]
have "T = B" by simp
moreover
from `t' = Bvar (Param n)` have "{n -> [Fvar x,Fvar y]} t' = Fvar y" by simp
ultimately
show ?case
using
subst[of env' A B] in_add_2[OF ok']
typing.T_Var[OF ok' _ add_get2_1[OF ok']]
by simp
qed
next
case (T_Upd F env T l t2 t1 env' t' s p x y A B n)
from sopen_eq_Upd[OF sym[OF `Upd t1 l t2 = {n -> [Fvar s,Fvar p]} t'`]]
obtain t1' t2' where
t1: "t1 = {n -> [Fvar s,Fvar p]} t1'" and
t2: "t2 = {Suc n -> [Fvar s,Fvar p]} t2'" and
t': "t' = Upd t1' l t2'"
by auto
{ fix a assume "a ∉ FV t'" with t' have "a ∉ FV t1'" by simp }
note
t1' = T_Upd(4)[OF this[OF `s ∉ FV t'`] this[OF `p ∉ FV t'`]
this[OF `x ∉ FV t'`] this[OF `y ∉ FV t'`]
`x ∉ env_dom env'` `y ∉ env_dom env'`
`s ≠ p` `x ≠ y` t1 `env = env'(|s:A|)),(|p:B|)),`]
from ok_finite[of env'] ok_add_2[OF typing_regular'[OF this]]
have findom: "finite (env_dom env')" by simp
{ fix a assume "a ∉ FV t'" with t' have "a ∉ FV t2'" by simp }
note
bnd_renaming_lem[OF this[OF `s ∉ FV t'`] this[OF `p ∉ FV t'`]
this[OF `x ∉ FV t'`] this[OF `y ∉ FV t'`]
`x ∉ env_dom env'` `y ∉ env_dom env'`
`s ≠ p` `x ≠ y` t2 `env = env'(|s:A|)),(|p:B|)),`]
from this[of F T l "FV t2'"] T_Upd(2)
have
"∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV t2' ∪ env_dom env'
∧ pa ∉ F ∪ {s, p, x, y} ∪ FV t2' ∪ env_dom env'
∧ sa ≠ pa
--> env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> ({Suc n -> [Fvar x,Fvar y]} t2'⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
by simp
from
typing.T_Upd[OF _ this t1' `l ∈ do T`]
`finite F` findom t'
show ?case by simp
next
case (T_Obj env f T F env' t' s p x y A B n)
from `ok env` `env = env'(|s:A|)),(|p:B|)),` ok_add_2[of env' s A p B]
have "ok env'" by simp
from
ok_add_ok[OF ok_add_ok[OF this `x ∉ env_dom env'`]
not_in_env_bigger[OF `y ∉ env_dom env'` not_sym[OF `x ≠ y`]]]
have ok: "ok (env'(|x:A|)),(|y:B|)),)" by assumption
from sopen_eq_Obj[OF sym[OF `Obj f T = {n -> [Fvar s,Fvar p]} t'`]]
obtain f' where
obj: "{n -> [Fvar s,Fvar p]} Obj f' T = Obj f T" and
t': "t' = Obj f' T" by auto
from
this(1) `dom f = do T`
sym[OF dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']]
dom_sopenoption_lem[of "Suc n" "Fvar x" "Fvar y" f']
have dom: "dom (λl. sopen_option (Suc n) (Fvar x) (Fvar y) (f' l)) = do T"
by simp
from
`finite F` finite_FV[of "Obj f' T"]
ok_finite[of env'] ok_add_2[OF ok]
have finF: "finite (F ∪ {s,p,x,y} ∪ FV (Obj f' T) ∪ env_dom env')"
by simp
have
"∀l∈do T. ∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env'
∧ pa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env'
∧ sa ≠ pa
--> env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(sopen_option (Suc n) (Fvar x) (Fvar y) (f' l))⇗[Fvar sa,Fvar pa]⇖) :
return(the(T^l))"
proof
fix l assume "l ∈ do T" with T_Obj(4)
have cof:
"∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
--> env(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
∧ (∀env'' t'' s' p' x' y' A' B' n'.
s' ∉ FV t'' --> p' ∉ FV t'' --> x' ∉ FV t'' --> y' ∉ FV t''
--> x' ∉ env_dom env'' --> y' ∉ env_dom env'' --> x' ≠ y'
--> s' ≠ p'
--> (the(f l)⇗[Fvar sa,Fvar pa]⇖) = {n' -> [Fvar s',Fvar p']} t''
--> env(|sa:T|)),(|pa:param(the(T^l))|)), = env''(|s':A'|)),(|p':B'|)),
--> env''(|x':A'|)),(|y':B'|)),
\<turnstile> {n' -> [Fvar x',Fvar y']} t'' : return(the(T^l)))"
by simp
from
`l ∈ do T` `dom f = do T` `Obj f T = {n -> [Fvar s,Fvar p]} t'` obj t'
dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']
have indomf': "l ∈ dom f'" by auto
hence
opened: "the (sopen_option (Suc n) (Fvar x) (Fvar y) (f' l))
= {Suc n -> [Fvar x,Fvar y]} the(f' l)"
by force
from indomf' have FVsubset: "FV (the(f' l)) ⊆ FV (Obj f' T)" by force
with
`s ∉ FV t'` `p ∉ FV t'` `x ∉ FV t'` `y ∉ FV t'` obj t'
indomf' FV_option_lem[of f']
obtain
"s ∉ FV (the(f' l))" and "p ∉ FV (the(f' l))" and
"x ∉ FV (the(f' l))" and "y ∉ FV (the(f' l))" and
"the(f l) = {Suc n -> [Fvar s,Fvar p]} the(f' l)" by auto
from
bnd_renaming_lem[OF this(1-4) `x ∉ env_dom env'` `y ∉ env_dom env'`
`s ≠ p` `x ≠ y` this(5) `env = env'(|s:A|)),(|p:B|)),`
cof FVsubset]
show
"∀sa pa. sa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env'
∧ pa ∉ F ∪ {s, p, x, y} ∪ FV (Obj f' T) ∪ env_dom env'
∧ sa ≠ pa
--> env'(|x:A|)),(|y:B|)),(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(sopen_option (Suc n) (Fvar x) (Fvar y) (f' l))⇗[Fvar sa,Fvar pa]⇖) :
return(the(T^l))"
by (subst opened, assumption)
qed
from typing.T_Obj[OF ok dom finF this] t' show ?case by simp
qed
lemma type_renaming:
"[| e(|s:A|)),(|p:B|)), \<turnstile> {n -> [Fvar s,Fvar p]} t : T;
s ∉ FV t; p ∉ FV t; x ∉ FV t; y ∉ FV t;
x ∉ env_dom e; y ∉ env_dom e; x ≠ y; s ≠ p|]
==> e(|x:A|)),(|y:B|)), \<turnstile> {n -> [Fvar x,Fvar y]} t : T"
by (auto simp: type_renaming')
(* too weak, as we need specific s,p *)
lemma obj_inv_elim':
assumes
"e \<turnstile> Obj f U : U" and
nin_s: "s ∉ FV (Obj f U) ∪ env_dom e" and
nin_p: "p ∉ FV (Obj f U) ∪ env_dom e" and "s ≠ p"
shows
"(dom f = do U) ∧ (∀l∈do U. e(|s:U|)),(|p:param(the(U^l))|)),
\<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(U^l)))"
using assms
proof (cases rule: typing.cases)
case (T_Obj F)
(* from `e = env` `Obj f U = Obj f' T` `dom f' = do T`
have "dom f = do U" by simp*)
thus ?thesis
proof (simp, intro strip)
fix l assume "l ∈ do U"
from `finite F` finite_FV[of "Obj f U"] have "finite (F ∪ FV (Obj f U) ∪ {s,p})"
by simp
from exFresh_s_p_cof[OF this]
obtain sa pa where
"sa ≠ pa" and
nin_sa: "sa ∉ F ∪ FV (Obj f U)" and
nin_pa: "pa ∉ F ∪ FV (Obj f U)" by auto
with `l ∈ do U` T_Obj(4)
have
"e(|sa:U|)),(|pa:param(the(U^l))|)),
\<turnstile> (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(U^l))"
by simp
moreover
from `l ∈ do U` `dom f = do U`
have "l ∈ dom f" by simp
with nin_s nin_p nin_sa nin_pa FV_option_lem[of f]
have
"sa ∉ FV (the(f l)) ∧ pa ∉ FV (the(f l))
∧ s ∉ FV (the(f l)) ∧ p ∉ FV (the(f l))
∧ s ∉ env_dom e ∧ p ∉ env_dom e" by auto
ultimately
show
"e(|s:U|)),(|p:param(the(U^l))|)),
\<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(U^l))"
using type_renaming[OF _ _ _ _ _ _ _ `s ≠ p` `sa ≠ pa`]
by (simp add: openz_def)
qed
qed
lemma dom_lem: "e \<turnstile> Obj f (Object fun) : Object fun ==> dom f = dom fun"
by (erule typing.cases, auto)
lemma abs_typeE:
assumes "e \<turnstile> Call (Obj f U) l b : T"
shows
"(∃F. finite F
∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> e(|s:U|)),(|p: param(the(U^l))|)), \<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : T) ==> P)
==> P"
using assms
proof (cases rule: typing.cases)
case (T_Call A (*env t1 t2=b*))
assume
cof: "∃F. finite F
∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> e(|s:U|)),(|p: param(the(U^l))|)), \<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : T)
==> P"
from
`T = return(the(A^l))`
`e \<turnstile> Obj f U : A` `l ∈ do A` obj_inv[of e f U A]
obtain "e \<turnstile> (Obj f U) : U" and "T = return(the(U^l))" and "l ∈ do U"
by simp
from obj_inv_elim[OF this(1)] this(2-3) cof show ?thesis by blast
qed
subsubsection {* Substitution preserves Well-Typedness *}
lemma bigger_env_lemma[rule_format]:
assumes "e \<turnstile> t : T"
shows "∀x X. x ∉ env_dom e --> e(|x:X|)), \<turnstile> t: T"
proof -
def pred_cof ≡ "λL env t T l.
∀s p. s ∉ L ∧ p ∉ L ∧ s ≠ p
--> env(|s:T|)),(|p:param (the(T^l))|)), \<turnstile> (t⇗[Fvar s,Fvar p]⇖) : return (the(T^l))"
from assms show ?thesis
proof (induct
taking: "λenv t T l. ∀x X. x ∉ env_dom env
--> (∃L. finite L ∧ pred_cof L (env(|x:X|)),) t T l)"
rule: typing_induct)
case Call thus ?case by auto
next
case (Fvar env Ta xa) thus ?case
proof (intro strip)
fix x X assume "x ∉ env_dom env"
from
get_env_smaller[OF `xa ∈ env_dom env` this]
T_Var[OF ok_add_ok[OF `ok env` this]
env_bigger[OF this `xa ∈ env_dom env`]]
`the env!xa = Ta`
show "env(|x:X|)), \<turnstile> Fvar xa : Ta" by simp
qed
next
case (Obj env Ta f) note pred_o = this(3)
def pred_cof' ≡ "λx X b l. ∃L. finite L ∧ pred_cof L (env(|x:X|)),) (the b) Ta l"
from pred_o
have pred: "∀x X. x ∉ env_dom env --> (∀l∈dom f. pred_cof' x X (f l) l)"
by (intro fmap_ball_all2'[of f "λx X. x ∉ env_dom env" pred_cof'],
unfold pred_cof_def pred_cof'_def, simp)
show ?case
proof (intro strip)
fix x X
def pred_bnd ≡ "λs p b l. env(|x:X|)),(|s:Ta|)),(|p:param (the(Ta^l))|)),
\<turnstile> (the b⇗[Fvar s,Fvar p]⇖) : return (the(Ta^l))"
assume "x ∉ env_dom env"
with pred fmap_ex_cof[of f pred_bnd] `dom f = do Ta`
obtain L where
"finite L" and "∀l∈do Ta. pred_cof L (env(|x:X|)),) (the(f l)) Ta l"
unfolding pred_bnd_def pred_cof_def pred_cof'_def
by auto
from
T_Obj[OF ok_add_ok[OF `ok env` `x ∉ env_dom env`]
`dom f = do Ta` this(1)]
this(2)
show "env<x:X> \<turnstile> Obj f Ta : Ta"
unfolding pred_cof_def
by simp
qed
next
case (Upd env Ta t l u)
note pred_t = this(2) and pred_u = this(4)
show ?case
proof (intro strip)
fix x X assume "x ∉ env_dom env"
with pred_u obtain L where
"finite L" and "pred_cof L (env(|x:X|)),) u Ta l" by auto
with `l ∈ do Ta` `x ∉ env_dom env` pred_t
show "env(|x:X|)), \<turnstile> Upd t l u : Ta"
unfolding pred_cof_def
by auto
qed
next
case (Bnd env Ta l t L) note pred = this(3)
show ?case
proof (intro strip)
fix x X assume "x ∉ env_dom env"
thus "∃L. finite L ∧ pred_cof L (env<x:X>) t Ta l"
proof (rule_tac x = "L ∪ {x}" in exI, simp add: `finite L`,
unfold pred_cof_def, auto)
fix s p
assume
"s ∉ L" and "p ∉ L" and "s ≠ p" and
"s ≠ x" and "p ≠ x"
note
subst_add[OF not_sym[OF `s ≠ x`]]
subst_add[OF not_sym[OF `p ≠ x`]]
from
this(1)[of env X Ta] this(2)[of "env(|s:Ta|))," X "param (the(Ta^l))"]
pred `s ∉ L` `p ∉ L` `s ≠ p`
not_in_env_bigger_2[OF `x ∉ env_dom env`
not_sym[OF `s ≠ x`] not_sym[OF `p ≠ x`]]
show
"env(|x:X|)),(|s:Ta|)),(|p:param (the(Ta^l))|)),
\<turnstile> (t⇗[Fvar s,Fvar p]⇖) : return (the(Ta^l))"
by auto
qed
qed
qed
qed
lemma bnd_disj_env_lem:
assumes
"ok e1" and "env_dom e1 ∩ env_dom e2 = {}" and "ok e2" and
"∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> e1(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))
∧ (env_dom (e1(|s:T|)),(|p:param(the(T^l))|)),) ∩ env_dom e2 = {}
--> ok e2
--> e1(|s:T|)),(|p:param(the(T^l))|)),+e2
\<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))"
shows
"∀s p. s ∉ F ∪ env_dom (e1+e2) ∧ p ∉ F ∪ env_dom (e1+e2) ∧ s ≠ p
--> (e1+e2)(|s:T|)),(|p:param(the(T^l))|)), \<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
proof (intro strip, elim conjE)
fix s p assume
nin_s: "s ∉ F ∪ env_dom (e1+e2)" and
nin_p: "p ∉ F ∪ env_dom (e1+e2)" and "s ≠ p"
from
this(1-2) env_add_dom_2[OF assms(1) _ _ this(3)]
assms(2) env_app_dom[OF assms(1-3)]
have "env_dom (e1(|s:T|)),(|p:param(the(T^l))|)),) ∩ env_dom e2 = {}" by simp
with
env_app_add2[OF assms(1-3) _ _ _ _ `s ≠ p`]
env_app_dom[OF assms(1-3)] `ok e2` assms(4) nin_s nin_p `s ≠ p`
show "(e1+e2)(|s:T|)),(|p:param(the(T^l))|)), \<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
by auto
qed
(* TODO: refactor to work with typing_induct *)
lemma disjunct_env:
assumes "e \<turnstile> t : A"
shows "(env_dom e ∩ env_dom e' = {} ==> ok e' ==> e + e' \<turnstile> t : A)"
using assms
proof (induct rule: typing.induct)
case T_Call thus ?case by auto
next
case (T_Var env x T)
from
env_app_dom[OF `ok env` `env_dom env ∩ env_dom e' = {}` `ok e'`]
`x ∈ env_dom env`
have indom: "x ∈ env_dom (env+e')" by simp
from
`ok env` `x ∈ env_dom env` `the env!x = T` `env_dom env ∩ env_dom e' = {}`
`ok e'`
have "the (env+e')!x = T" by simp
from
typing.T_Var[OF env_app_ok[OF `ok env` `env_dom env ∩ env_dom e' = {}`
`ok e'`]
indom this]
show ?case by assumption
next
case (T_Upd F env T l t2 t1)
from
typing.T_Upd[OF _ bnd_disj_env_lem[OF typing_regular'[OF `env \<turnstile> t1 : T`]
`env_dom env ∩ env_dom e' = {}` `ok e'`
T_Upd(2)]
T_Upd(4)[OF `env_dom env ∩ env_dom e' = {}` `ok e'`]
`l ∈ do T`]
`finite F` ok_finite[OF env_app_ok[OF typing_regular'[OF `env \<turnstile> t1 : T`]
`env_dom env ∩ env_dom e' = {}` `ok e'`]]
show ?case by simp
next
case (T_Obj env f T F)
from
ok_finite[OF env_app_ok[OF `ok env` `env_dom env ∩ env_dom e' = {}` `ok e'`]]
`finite F`
have finF: "finite (F ∪ env_dom (env+e'))" by simp
note
ball_Tltsp[of F
"λT l t s p. env(|s:T|)),(|p:param(the(T^l))|)), \<turnstile> (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l))
∧ (env_dom (env(|s:T|)),(|p:param(the(T^l))|)),) ∩ env_dom e' = {}
--> ok e'
--> env(|s:T|)),(|p:param(the(T^l))|)),+e'
\<turnstile> (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))"
T "F ∪ env_dom (env+e')"
"λT l t s p. (env+e')(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> (t⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"]
from
this[OF _ T_Obj(4)]
bnd_disj_env_lem[OF `ok env` `env_dom env ∩ env_dom e' = {}` `ok e'`]
typing.T_Obj[OF env_app_ok[OF `ok env`
`env_dom env ∩ env_dom e' = {}` `ok e'`]
`dom f = do T` finF]
show ?case by simp
qed
text {* Typed in the Empty Environment implies typed in any Environment *}
lemma empty_env:
assumes "(Env empty) \<turnstile> t : A" and "ok env"
shows "env \<turnstile> t : A"
proof -
from `ok env` have "env = (Env empty)+env" by (cases env, auto)
with disjunct_env[OF assms(1) _ assms(2)] show ?thesis by simp
qed
lemma bnd_open_lem:
assumes
pred_bnd:
"∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
--> env(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (t⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
∧ (∀env'' t'' s' p' x' y' A' B' n'. s' ∉ FV t'' ∪ FV x' ∪ FV y'
--> p' ∉ FV t'' ∪ FV x' ∪ FV y' --> s' ≠ p'
--> env'' \<turnstile> x' : A' --> env'' \<turnstile> y' : B'
--> (t⇗[Fvar sa,Fvar pa]⇖) = {n' -> [Fvar s',Fvar p']} t''
--> env(|sa:T|)),(|pa:param(the(T^l))|)), = env''(|s':A'|)),(|p':B'|)),
--> env'' \<turnstile> {n' -> [x',y']} t'' : return(the(T^l)))" and
"ok env" and "env = env'(|s:A|)),(|p:B|))," and
"s ∉ FV t'' ∪ FV x ∪ FV y" and "p ∉ FV t'' ∪ FV x ∪ FV y" and "s ≠ p" and
"env' \<turnstile> x : A" and "env' \<turnstile> y : B" and
"t = {Suc n -> [Fvar s,Fvar p]} t'" and "FV t' ⊆ FV t''"
shows
"∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env'
∧ pa ∉ F ∪ {s,p} ∪ env_dom env' ∧ sa ≠ pa
--> env'(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> ({Suc n -> [x,y]} t'⇗[Fvar sa, Fvar pa]⇖) : return(the(T^l))"
proof (intro strip, elim conjE)
fix sa pa assume
nin_sa: "sa ∉ F ∪ {s,p} ∪ env_dom env'" and
nin_pa: "pa ∉ F ∪ {s,p} ∪ env_dom env'" and "sa ≠ pa"
hence "sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa" by auto
moreover
{
fix a assume "a ∉ FV t'' ∪ FV x ∪ FV y" and "a ∈ {s,p}"
with
`FV t' ⊆ FV t''` nin_sa nin_pa `sa ≠ pa`
sopen_FV[of 0 "Fvar sa" "Fvar pa" t']
have "a ∉ FV (t'⇗[Fvar sa,Fvar pa]⇖) ∪ FV x ∪ FV y" by (auto simp: openz_def)
} note
this[OF `s ∉ FV t'' ∪ FV x ∪ FV y`]
this[OF `p ∉ FV t'' ∪ FV x ∪ FV y`]
moreover
{
from `ok env` `env = env'(|s:A|)),(|p:B|)),` ok_add_2[of env' s A p B]
have "ok env'" by simp
from nin_sa nin_pa `sa ≠ pa` env_add_dom[OF this]
obtain "sa ∉ env_dom env'" and "pa ∉ env_dom (env'(|sa:T|)),)" by auto
note
bigger_env_lemma[OF bigger_env_lemma[OF `env' \<turnstile> x : A` this(1)] this(2)]
bigger_env_lemma[OF bigger_env_lemma[OF `env' \<turnstile> y : B` this(1)] this(2)]
}note
this(1)[of "param(the(T^l))"]
this(2)[of "param(the(T^l))"]
moreover
from `t = {Suc n -> [Fvar s,Fvar p]} t'` sopen_commute[of 0 "Suc n" sa pa s p t']
have "(t⇗[Fvar sa,Fvar pa]⇖) = {Suc n -> [Fvar s,Fvar p]} (t'⇗[Fvar sa,Fvar pa]⇖)"
by (simp add: openz_def)
moreover
from
subst_add[of p sa "env'(|s:A|))," B T] subst_add[of s sa env' A T]
subst_add[of p pa "env'(|sa:T|)),(|s:A|))," B "param(the(T^l))"]
subst_add[of s pa "env'(|sa:T|))," A "param(the(T^l))"]
`env = env'(|s:A|)),(|p:B|)),` nin_sa nin_pa
have "env(|sa:T|)),(|pa:param(the(T^l))|)), = env'(|sa:T|)),(|pa:param(the(T^l))|)),(|s:A|)),(|p:B|)),"
by auto
ultimately
show
"env'(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> ({Suc n -> [x,y]} t'⇗[Fvar sa, Fvar pa]⇖) : return(the(T^l))"
using
pred_bnd `s ≠ p`
sopen_commute_gen[OF lc_Fvar[of sa] lc_Fvar[of pa]
typing_regular''[OF `env' \<turnstile> x : A`]
typing_regular''[OF `env' \<turnstile> y : B`]
not_sym[OF Suc_not_Zero]]
by (auto simp: openz_def)
qed
(* A variation of the Type Renaming lemma above. This is stronger and could be extended to show type renaming, using that a term typed in one environment is typed in any bigger environment *)
(* TODO: refactor to work with typing_induct *)
lemma open_lemma':
shows
"e \<turnstile> t : C
==> (!!env t' s p x y A B n. s ∉ FV t' ∪ FV x ∪ FV y
==> p ∉ FV t' ∪ FV x ∪ FV y ==> s ≠ p
==> env \<turnstile> x : A ==> env \<turnstile> y : B
==> t = {n -> [Fvar s,Fvar p]} t'
==> e = env(|s:A|)),(|p:B|)),
==> env \<turnstile> {n -> [x,y]} t' : C)"
proof (induct set:typing)
case (T_Var env x T env' t' s p y z A B n)
from sopen_eq_Fvar[OF sym[OF `Fvar x = {n -> [Fvar s,Fvar p]} t'`]]
show ?case
proof (elim disjE conjE)
assume "t' = Fvar x"
with `s ∉ FV t' ∪ FV y ∪ FV z` `p ∉ FV t' ∪ FV y ∪ FV z`
obtain "x ≠ s" and "x ≠ p" by auto
from `x ∈ env_dom env` `env = env'(|s:A|)),(|p:B|)),` in_env_smaller2[OF _ this]
have indom: "x ∈ env_dom env'" by simp
from
`ok env` `the env!x = T` `env = env'(|s:A|)),(|p:B|)),`
ok_add_2[of env' s A p B] get_env_smaller2[OF this _ _ `s ≠ p`]
have "the env'!x = T" by simp
from
`ok env` `env = env'(|s:A|)),(|p:B|)),` `t' = Fvar x`
ok_add_2[of env' s A p B] typing.T_Var[OF _ indom this]
show ?case by simp
next
assume "x = s"
with
`ok env` `the env!x = T` `env = env'(|s:A|)),(|p:B|)),`
add_get2_1[of env' s A p B]
have "T = A" by simp
moreover assume "t' = Bvar (Self n)"
ultimately show ?thesis using `env' \<turnstile> y : A` by simp
next
assume "x = p"
with
`ok env` `the env!x = T` `env = env'(|s:A|)),(|p:B|)),`
add_get2_2[of env' s A p B] have "T = B" by simp
moreover assume "t' = Bvar (Param n)"
ultimately show ?thesis using `env' \<turnstile> z : B` by simp
qed
next
case (T_Upd F env T l t2 t1 env' t' s p x y A B n)
from sopen_eq_Upd[OF sym[OF `Upd t1 l t2 = {n -> [Fvar s,Fvar p]} t'`]]
obtain t1' t2' where
t1': "t1 = {n -> [Fvar s,Fvar p]} t1'" and
t2': "t2 = {Suc n -> [Fvar s,Fvar p]} t2'" and
t': "t' = Upd t1' l t2'" by auto
hence "FV t2' ⊆ FV t'" by auto
from
`s ∉ FV t' ∪ FV x ∪ FV y` `p ∉ FV t' ∪ FV x ∪ FV y`
t' `finite F` ok_finite[OF typing_regular'[OF `env' \<turnstile> x : A`]]
typing.T_Upd[OF _ bnd_open_lem[OF T_Upd(2)
typing_regular'[OF `env \<turnstile> t1 : T`]
`env = env'(|s:A|)),(|p:B|)),`
`s ∉ FV t' ∪ FV x ∪ FV y`
`p ∉ FV t' ∪ FV x ∪ FV y` `s ≠ p`
`env' \<turnstile> x : A` `env' \<turnstile> y : B` t2' this]
T_Upd(4)[OF _ _ `s ≠ p` `env' \<turnstile> x : A` `env' \<turnstile> y : B`
t1' `env = env'(|s:A|)),(|p:B|)),`] `l ∈ do T`]
show ?case by simp
next
case (T_Obj env f T F env' t' s p x y A B n)
from sopen_eq_Obj[OF sym[OF `Obj f T = {n -> [Fvar s,Fvar p]} t'`]]
obtain f' where
obj: "Obj f T = {n -> [Fvar s,Fvar p]} Obj f' T" and
t': "t' = Obj f' T" by auto
from
sym[OF this(1)] `dom f = do T`
sym[OF dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']]
dom_sopenoption_lem[of "Suc n" x y f']
have dom: "dom (λl. sopen_option (Suc n) x y (f' l)) = do T" by simp
from `finite F` ok_finite[OF typing_regular'[OF `env' \<turnstile> x : A`]]
have finF: "finite (F ∪ {s,p} ∪ env_dom env')"
by simp
have
"∀l∈do T. ∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env'
∧ pa ∉ F ∪ {s,p} ∪ env_dom env'
∧ sa ≠ pa
--> env'(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(sopen_option (Suc n) x y (f' l))⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
proof
fix l assume "l ∈ do T" with T_Obj(4)
have
cof:
"∀sa pa. sa ∉ F ∧ pa ∉ F ∧ sa ≠ pa
--> env(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(f l)⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))
∧ (∀env'' t'' s' p' x' y' A' B' n'.
s' ∉ FV t'' ∪ FV x' ∪ FV y' --> p' ∉ FV t'' ∪ FV x' ∪ FV y'
--> s' ≠ p' --> env'' \<turnstile> x' : A' --> env'' \<turnstile> y' : B'
--> (the(f l)⇗[Fvar sa,Fvar pa]⇖) = {n' -> [Fvar s',Fvar p']} t''
--> env(|sa:T|)),(|pa:param(the(T^l))|)), = env''(|s':A'|)),(|p':B'|)),
--> env'' \<turnstile> {n' -> [x',y']} t'' : return(the(T^l)))"
by simp
from
`l ∈ do T` `dom f = do T` `Obj f T = {n -> [Fvar s,Fvar p]} t'` obj t'
dom_sopenoption_lem[of "Suc n" "Fvar s" "Fvar p" f']
have indomf': "l ∈ dom f'" by auto
with obj sopen_option_lem[of f' "Suc n" "Fvar s" "Fvar p"] FV_option_lem[of f'] t'
obtain
"the(f l) = {Suc n -> [Fvar s,Fvar p]} the(f' l)" and
"FV (the(f' l)) ⊆ FV t'" by auto
from
bnd_open_lem[OF cof `ok env` `env = env'(|s:A|)),(|p:B|)),`
`s ∉ FV t' ∪ FV x ∪ FV y` `p ∉ FV t' ∪ FV x ∪ FV y`
`s ≠ p` `env' \<turnstile> x : A` `env' \<turnstile> y : B` this]
indomf' sopen_option_lem[of f' "Suc n" x y] T_Obj(4)
show
"∀sa pa. sa ∉ F ∪ {s,p} ∪ env_dom env'
∧ pa ∉ F ∪ {s,p} ∪ env_dom env' ∧ sa ≠ pa
--> env'(|sa:T|)),(|pa:param(the(T^l))|)),
\<turnstile> (the(sopen_option (Suc n) x y (f' l))⇗[Fvar sa,Fvar pa]⇖) : return(the(T^l))"
by simp
qed
from typing.T_Obj[OF typing_regular'[OF `env' \<turnstile> x : A`] dom finF this] t'
show ?case by simp
next
case (T_Call env t1 T t2 l env' t' s p x y A B n)
from sopen_eq_Call[OF sym[OF `Call t1 l t2 = {n -> [Fvar s,Fvar p]} t'`]]
obtain t1' t2' where
t1: "t1 = {n -> [Fvar s,Fvar p]} t1'" and
t2: "t2 = {n -> [Fvar s,Fvar p]} t2'" and
t': "t' = Call t1' l t2'" by auto
{ fix a assume "a ∉ FV t' ∪ FV x ∪ FV y"
with t' have "a ∉ FV t1' ∪ FV x ∪ FV y" by simp
}note
t1' = T_Call(2)[OF this[OF `s ∉ FV t' ∪ FV x ∪ FV y`]
this[OF `p ∉ FV t' ∪ FV x ∪ FV y`]
`s ≠ p` `env' \<turnstile> x : A` `env' \<turnstile> y : B`
t1 `env = env'(|s:A|)),(|p:B|)),`]
{ fix a assume "a ∉ FV t' ∪ FV x ∪ FV y"
with t' have "a ∉ FV t2' ∪ FV x ∪ FV y" by simp
}
from
typing.T_Call[OF t1' T_Call(4)[OF this[OF `s ∉ FV t' ∪ FV x ∪ FV y`]
this[OF `p ∉ FV t' ∪ FV x ∪ FV y`]
`s ≠ p` `env' \<turnstile> x : A` `env' \<turnstile> y : B`
t2 `env = env'(|s:A|)),(|p:B|)),`]
`l ∈ do T`]
t'
show ?case by simp
qed
lemma open_lemma:
"[| env(|s:A|)),(|p:B|)), \<turnstile> {n -> [Fvar s,Fvar p]} t : T;
s ∉ FV t ∪ FV x ∪ FV y; p ∉ FV t ∪ FV x ∪ FV y; s ≠ p;
env \<turnstile> x : A; env \<turnstile> y : B |]
==> env \<turnstile> {n -> [x,y]} t : T"
by (simp add: open_lemma')
subsubsection {* Subject reduction *}
lemma type_dom[simp]: "env \<turnstile> (Obj a A) : A ==> dom a = do A"
by (erule typing.cases, auto)
lemma select_preserve_type[simp]:
assumes
"env \<turnstile> Obj f (Object t) : Object t" and "s ∉ FV a" and "p ∉ FV a" and
"env(|s:(Object t)|)),(|p:param(the(t l2))|)), \<turnstile> (a⇗[Fvar s,Fvar p]⇖) : return(the(t l2))" and
"l1 ∈ dom t" and "l2 ∈ dom t"
shows
"∃F. finite F
∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:(Object t)|)),(|p:param(the(t l1))|)),
\<turnstile> (the((f(l2 \<mapsto> a)) l1)⇗[Fvar s,Fvar p]⇖) : return(the(t l1)))"
proof -
from ok_finite[OF typing_regular'[OF `env \<turnstile> Obj f (Object t) : Object t`]]
have finF: "finite ({s,p} ∪ env_dom env)" by simp
{
note
ok_env = typing_regular'[OF `env \<turnstile> Obj f (Object t) : Object t`] and
ok_env_sp = typing_regular'[OF assms(4)]
fix sa pa assume
nin_sa: "sa ∉ {s,p} ∪ env_dom env" and
nin_pa: "pa ∉ {s,p} ∪ env_dom env" and "sa ≠ pa"
from this(1) ok_add_2[OF ok_env_sp] env_add_dom_2[OF ok_env]
have "sa ∉ env_dom (env(|s:Object t|)),(|p:param(the(t l2))|)),)" by simp
from
nin_sa bigger_env_lemma[OF assms(4) this]
subst_add[of sa p "env(|s:Object t|))," "Object t" "param(the(t l2))"]
subst_add[of sa s env "Object t" "Object t"]
have
aT_sa: "env(|sa:Object t|)),(|s:Object t|)),(|p:param(the(t l2))|)),
\<turnstile> (a⇗[Fvar s,Fvar p]⇖) : return(the(t l2))" by simp
from
`sa ≠ pa` nin_sa nin_pa env_add_dom[OF ok_env]
ok_add_2[OF ok_env_sp]
obtain
"s ∉ env_dom (env(|sa:Object t|)),)" and
"p ∉ env_dom (env(|sa:Object t|)),)" and "s ≠ p" and
"sa ∉ env_dom env" and "pa ∉ env_dom (env(|sa:Object t|)),)"
by auto
with env_add_dom_2[OF ok_add_ok[OF ok_env this(4)] this(1-3)] nin_pa
have "pa ∉ env_dom (env(|sa:Object t|)),(|s:Object t|)),(|p:param(the(t l2))|)),)"
by simp
from
nin_pa bigger_env_lemma[OF aT_sa this]
subst_add[of pa p "env(|sa:Object t|)),(|s:Object t|)),"
"param(the(t l2))" "param(the(t l2))"]
subst_add[of pa s "env(|sa:Object t|))," "param(the(t l2))" "Object t"]
have
aT_sapa:
"env(|sa:Object t|)),(|pa:param(the(t l2))|)),(|s:Object t|)),(|p:param(the(t l2))|)),
\<turnstile> {0 -> [Fvar s, Fvar p]} a : return(the(t l2))" by (simp add: openz_def)
from nin_sa nin_pa `s ∉ FV a` `p ∉ FV a` ok_add_2[OF ok_env_sp]
obtain
ninFV_s: "s ∉ FV a ∪ FV (Fvar sa) ∪ FV (Fvar pa)" and
ninFV_p: "p ∉ FV a ∪ FV (Fvar sa) ∪ FV (Fvar pa)" and "s ≠ p"
by auto
from ok_add_2[OF typing_regular'[OF aT_sapa]]
have ok_env_sapa: "ok (env(|sa:Object t|)),(|pa:param(the(t l2))|)),)"
by simp
with ok_add_reverse[OF this]
have ok_env_pasa: "ok (env(|pa:param(the(t l2))|)),(|sa:Object t|)),)"
by simp
from
open_lemma[OF aT_sapa ninFV_s ninFV_p `s ≠ p` _
T_Var[OF ok_env_sapa in_add[OF ok_env_sapa]
add_get2_2[OF ok_env_sapa]]]
T_Var[OF ok_env_pasa in_add[OF ok_env_pasa] add_get2_2[OF ok_env_pasa]]
ok_add_reverse[OF ok_env_sapa]
have
"env(|sa:(Object t)|)),(|pa:param(the(t l2))|)),
\<turnstile> (a⇗[Fvar sa,Fvar pa]⇖) : return(the(t l2))"
by (simp add: openz_def)
}note alem = this
(* case split *)
show ?thesis
proof (cases "l1 = l2")
case True with assms obj_inv_elim'[OF assms(1)] show ?thesis
by (simp (no_asm_simp), rule_tac x = "{s,p} ∪ env_dom env" in exI,
auto simp: finF alem)
next
case False
from obj_inv_elim[OF `env \<turnstile> Obj f (Object t) : Object t`]
obtain F where
"finite F" and
"∀l∈dom t.
∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:Object t|)),(|p:param(the(Object t^l))|)),
\<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(Object t^l))"
by auto
from this(2) `l1 ∈ dom t`
have
"∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:Object t|)),(|p:param(the(Object t^l1))|)),
\<turnstile> (the(f l1)⇗[Fvar s,Fvar p]⇖) : return(the(Object t^l1))"
by auto
thus ?thesis using `finite F` `l1 ≠ l2` by (simp,blast)
qed
qed
text {* Main Lemma *}
(* TODO: refactor to work with typing_induct *)
lemma subject_reduction: "e \<turnstile> t : T ==> (!!t'. t ->⇩β t' ==> e \<turnstile> t' : T)"
proof (induct set: typing)
case (T_Var env x T t')
from Fvar_beta[OF `Fvar x ->⇩β t'`] show ?case by simp
next
case (T_Upd F env T l t2 t1 t')
from Upd_beta[OF `Upd t1 l t2 ->⇩β t'`] show ?case
proof (elim disjE exE conjE)
fix t1' assume "t1 ->⇩β t1'" and "t' = Upd t1' l t2"
from
this(2) T_Upd(2)
typing.T_Upd[OF `finite F` _ T_Upd(4)[OF this(1)] `l ∈ do T`]
show ?case by simp
next
fix t2' F'
assume
"finite F'" and
pred_F': "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p
--> (∃t''. t2⇗[Fvar s,Fvar p]⇖ ->⇩β t'' ∧ t2' = σ[s,p] t'')" and
t': "t' = Upd t1 l t2'"
have
"∀s p. s ∉ F ∪ F' ∧ p ∉ F ∪ F' ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l))|)), \<turnstile> (t2'⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
proof (intro strip, elim conjE)
fix s p assume
nin_s: "s ∉ F ∪ F'" and
nin_p: "p ∉ F ∪ F'" and "s ≠ p"
with pred_F' obtain t'' where "t2⇗[Fvar s,Fvar p]⇖ ->⇩β t''" and "t2' = σ[s,p] t''"
by auto
with beta_lc[OF this(1)] sopen_sclose_eq_t[of t'' 0 s p]
have "t2⇗[Fvar s,Fvar p]⇖ ->⇩β (t2'⇗[Fvar s,Fvar p]⇖)"
by (simp add: openz_def closez_def)
with nin_s nin_p `s ≠ p` T_Upd(2)
show "env(|s:T|)),(|p:param(the(T^l))|)), \<turnstile> (t2'⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
by auto
qed
from t' `finite F` `finite F'` typing.T_Upd[OF _ this `env \<turnstile> t1 : T` `l ∈ do T`]
show ?case by simp
next
fix f U assume
"l ∈ dom f" and "Obj f U = t1" and
t': "t' = Obj (f(l \<mapsto> t2)) U"
from this(1-2) `env \<turnstile> t1 : T` obj_inv[of env f U T]
obtain t where
objT: "env \<turnstile> Obj f (Object t) : (Object t)" and
"Object t = T" and "T = U"
by (cases T, auto)
from obj_inv_elim[OF objT] `Object t = T` `l ∈ dom f`
have domf': "dom (f(l \<mapsto> t2)) = do T" by auto
have
exF: "∀l'∈do T.
(∃F'. finite F'
∧ (∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the ((f(l \<mapsto> t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))))"
proof
fix l' assume "l' ∈ do T"
with dom_lem[OF objT] `l ∈ dom f` `Object t = T`
obtain ll': "l' ∈ dom t" and "l ∈ dom t" by auto
from `finite F` have "finite (F ∪ FV t2)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where
nin_s: "s ∉ F ∪ FV t2" and
nin_p: "p ∉ F ∪ FV t2" and "s ≠ p"
by auto
with T_Upd(2) `Object t = T`
have
"env(|s:Object t|)),(|p:param(the(t l))|)),
\<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(t l))"
by auto
from
select_preserve_type[OF objT _ _ this ll'] sym[OF `Object t = T`]
nin_s nin_p `l ∈ dom t`
obtain F' where
"finite F'" and
"∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the ((f(l \<mapsto> t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
by auto
thus
"∃F'. finite F'
∧ (∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the ((f(l \<mapsto> t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l')))"
by blast
qed
{ fix Ta from finite_dom_fmap have "finite (do Ta)" by (cases Ta, auto) }
note fin_doT = this ball_ex_finite[of "do T" "F ∪ FV t2"]
from this(2)[OF this(1)[of T] _ exF] `finite F`
obtain F' where
"finite F'" and
"∀l'∈do T. ∀s p. s ∉ F' ∪ (F ∪ FV t2) ∧ p ∉ F' ∪ (F ∪ FV t2) ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the ((f(l \<mapsto> t2)) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
by auto
moreover
from `finite F'` `finite F` have "finite (F' ∪ (F ∪ FV t2))" by simp
note typing.T_Obj[OF typing_regular'[OF `env \<turnstile> t1 : T`] domf' this]
ultimately show ?case using t' `T = U` by auto
qed
next
case (T_Obj env f T F t')
from Obj_beta[OF `Obj f T ->⇩β t'`] show ?case
proof (elim exE conjE)
fix l f' a a' F' assume
"dom f = dom f'" and "f = f'(l \<mapsto> a)" and "l ∈ dom f'" and
t': "t' = Obj (f'(l \<mapsto> a')) T" and "finite F'" and
red_sp: "∀s p. s ∉ F' ∧ p ∉ F' ∧ s ≠ p
--> (∃t''. a⇗[Fvar s, Fvar p]⇖ ->⇩β t'' ∧ a' = σ[s,p] t'')"
from this(2) `dom f = do T` have domf': "dom (f'(l \<mapsto> a')) = do T" by auto
have
exF: "∀l'∈do T. ∀s p. s ∉ F ∪ F' ∧ p ∉ F ∪ F' ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the ((f'(l \<mapsto> a')) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
proof (intro strip, elim conjE)
fix l' s p assume
"l' ∈ do T" and
nin_s: "s ∉ F ∪ F'" and
nin_p: "p ∉ F ∪ F'" and "s ≠ p"
with red_sp obtain t'' where "a⇗[Fvar s,Fvar p]⇖ ->⇩β t''" and "a' = σ[s,p] t''"
by auto
with
beta_lc[OF this(1)] sopen_sclose_eq_t[of t'' 0 s p]
`f = f'(l \<mapsto> a)`
have "the (f l)⇗[Fvar s,Fvar p]⇖ ->⇩β (the((f'(l \<mapsto> a')) l)⇗[Fvar s,Fvar p]⇖)"
by (simp add: openz_def closez_def)
with T_Obj(4) nin_s nin_p `s ≠ p` `l' ∈ do T` `f = f'(l \<mapsto> a)`
show
"env(|s:T|)),(|p:param(the(T^l'))|)),
\<turnstile> (the((f'(l \<mapsto> a')) l')⇗[Fvar s,Fvar p]⇖) : return(the(T^l'))"
by auto
qed
from typing.T_Obj[OF `ok env` domf' _ this] `finite F` `finite F'` t'
show ?case by (simp (no_asm_simp))
qed
next
case (T_Call env t1 T t2 l t')
from Call_beta[OF `Call t1 l t2 ->⇩β t'`] show ?case
proof (elim disjE conjE exE)
fix t1' assume "t1 ->⇩β t1'" and "t' = Call t1' l t2"
from
typing.T_Call[OF T_Call(2)[OF this(1)]
`env \<turnstile> t2 : param(the(T^l))` `l ∈ do T`]
this(2)
show ?case by simp
next
fix t2' assume "t2 ->⇩β t2'" and "t' = Call t1 l t2'"
from
typing.T_Call[OF `env \<turnstile> t1 : T` T_Call(4)[OF this(1)] `l ∈ do T`]
this(2)
show ?case by simp
next
fix f U assume "Obj f U = t1" and "l ∈ dom f" and t': "t' = (the(f l)⇗[Obj f U,t2]⇖)"
from
typing.T_Call[OF `env \<turnstile> t1 : T` `env \<turnstile> t2 : param(the(T^l))` `l ∈ do T`]
sym[OF this(1)] `env \<turnstile> t1 : T` `env \<turnstile> t2 : param(the(T^l))`
obj_inv[of env f U T]
obtain
objT: "env \<turnstile> (Obj f T) : T" and "T = U" and
callT: "env \<turnstile> Call (Obj f T) l t2 : return(the(T^l))"
by auto
have
"(∃F. finite F
∧ (∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(T^l)))
==> env \<turnstile> (the (f l)⇗[Obj f T,t2]⇖) : return (the(T^l)))"
proof (elim exE conjE)
fix F
assume
"finite F" and
pred_F:
"∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> env(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> (the(f l)⇗[Fvar s,Fvar p]⇖) : return(the(T^l))"
from this(1) finite_FV[of "Obj f T"]
have "finite (F ∪ FV (Obj f T) ∪ FV t2)" by simp
from exFresh_s_p_cof[OF this]
obtain s p where
nin_s: "s ∉ F ∪ FV (Obj f T) ∪ FV t2" and
nin_p: "p ∉ F ∪ FV (Obj f T) ∪ FV t2" and "s ≠ p"
by auto
with pred_F
have
type_opened: "env(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> {0 -> [Fvar s,Fvar p]} the(f l) : return(the(T^l))"
by (auto simp: openz_def)
from nin_s nin_p FV_option_lem[of f] objT `l ∈ do T`
obtain
"s ∉ FV (the(f l)) ∪ FV (Obj f T) ∪ FV t2" and
"p ∉ FV (the(f l)) ∪ FV (Obj f T) ∪ FV t2" by auto
from
open_lemma[OF type_opened this `s ≠ p`
objT `env \<turnstile> t2 : param(the(T^l))`]
show ?thesis by (simp add: openz_def)
qed
with abs_typeE[OF callT] t' `T = U` show ?case by auto
qed
qed
theorem subject_reduction': "t ->⇩β⇧* t' ==> e \<turnstile> t : T ==> e \<turnstile> t' : T"
by (induct set: rtranclp) (iprover intro: subject_reduction)+
lemma type_members_equal:
fixes A :: type and B :: type
assumes "do A = do B" and "∀i. (A^i) = (B^i)"
shows "A = B"
proof (cases A)
case (Object ta) thus ?thesis
proof (cases B)
case (Object tb)
from `∀i. (A^i) = (B^i)` `A = Object ta` `B = Object tb`
have "!!i. ta i = tb i" by auto
with `A = Object ta` `B = Object tb` show ?thesis by (simp add: ext)
qed
qed
lemma not_var: "Env empty \<turnstile> a : A ==> ∀x. a ≠ Fvar x"
by (rule allI, case_tac x, auto)
lemma Call_label_range: "(Env empty) \<turnstile> Call (Obj c T) l b : A ==> l ∈ dom c"
by (erule typing_elims, erule typing.cases, simp_all)
lemma Call_subterm_type: "Env empty \<turnstile> Call t l b: T
==> (∃T'. Env empty \<turnstile> t : T') ∧ (∃T'. Env empty \<turnstile> b : T')"
by (erule typing.cases) auto
lemma Upd_label_range: "Env empty \<turnstile> Upd (Obj c T) l x : A ==> l ∈ dom c"
by (erule typing_elims, erule typing.cases, simp_all)
lemma Upd_subterm_type:
"Env empty \<turnstile> Upd t l x : T ==> ∃T'. Env empty \<turnstile> t : T'"
by (erule typing.cases) auto
lemma no_var: "∃T. Env empty \<turnstile> Fvar x : T ==> False"
by (case_tac x, auto)
lemma no_bvar: "e \<turnstile> Bvar x : T ==> False"
by (erule typing.cases, auto)
subsubsection{*Unique Type*}
theorem type_unique[rule_format]:
assumes "env \<turnstile> a: T"
shows "∀T'. env \<turnstile> a: T' --> T = T'"
using assms
proof (induct rule: typing.induct)
case T_Var thus ?case by (auto simp: add_get_eq)
next
case T_Obj show ?case by (auto simp: sym[OF obj_inv])
next
case T_Call from this(2) show ?case by auto
next
case T_Upd from this(4) show ?case by auto
qed
subsubsection{*Progress*}
text {* Final Type Soundness Lemma *}
theorem progress:
assumes "Env empty \<turnstile> t : A" and "¬(∃c A. t = Obj c A)"
shows "∃b. t ->⇩β b"
proof -
fix f
have
"(∀A. Env empty \<turnstile> t : A --> ¬(∃c T. t = Obj c T) --> (∃b. t ->⇩β b))
&(∀A. Env empty \<turnstile> Obj f A : A --> ¬(∃c T. Obj f A = Obj c T)
--> (∃b. Obj f A ->⇩β b))"
proof (induct rule: sterm_induct)
case (Bvar b) with no_bvar[of "Env empty" b] show ?case
by auto (* contradiction *)
next
case (Fvar x) with Fvar_beta[of x] show ?case
by auto (* contradiction *)
next
case Obj show ?case by auto (* contradiction *)
next
case empty thus ?case by auto (* contradiction *)
next
case insert show ?case by auto (* contradiction *)
next
case (Call t1 l t2) show ?case
proof (clarify)
fix T assume
"Env empty \<turnstile> t1 : T" and "Env empty \<turnstile> t2 : param(the(T^l))" and "l ∈ do T"
note lc = typing_regular''[OF this(1)] typing_regular''[OF this(2)]
from
`Env empty \<turnstile> t1 : T`
`∀A. Env empty \<turnstile> t1 : A --> ¬ (∃c T. t1 = Obj c T) --> (∃b. t1 ->⇩β b)`
have "(∃c B. t1 = Obj c B) ∨ (∃b. t1 ->⇩β b)" by auto
thus "∃b. Call t1 l t2 ->⇩β b"
proof (elim disjE exE)
fix c B assume "t1 = Obj c B"
with
`Env empty \<turnstile> t1 : T` obj_inv[of "Env empty" c B T]
`l ∈ do T` obj_inv_elim[of "Env empty" c B]
have "l ∈ dom c" by auto
with `t1 = Obj c B` lc beta.beta[of l c B t2]
show ?thesis by auto
next
fix b assume "t1 ->⇩β b"
from beta.beta_CallL[OF this lc(2)] show ?thesis by auto
qed
qed
next
case (Upd t1 l t2) show ?case
proof (clarify)
fix T F
assume
"finite F" and
"∀s p. s ∉ F ∧ p ∉ F ∧ s ≠ p
--> Env empty(|s:T|)),(|p:param(the(T^l))|)),
\<turnstile> (t2⇗[Fvar s,Fvar p]⇖) : return(the(T^l))" and
"Env empty \<turnstile> t1 : T" and
"l ∈ do T"
from typing_regular''[OF T_Upd[OF this]] lc_upd[of t1 l t2]
obtain "lc t1" and "body t2" by auto
from
`Env empty \<turnstile> t1 : T`
`∀A. Env empty \<turnstile> t1 : A --> ¬ (∃c T. t1 = Obj c T) --> (∃b. t1 ->⇩β b)`
have "(∃c B. t1 = Obj c B) ∨ (∃b. t1 ->⇩β b)" by auto
thus "∃b. Upd t1 l t2 ->⇩β b"
proof (elim disjE exE)
fix c B assume "t1 = Obj c B"
with
`Env empty \<turnstile> t1 : T` obj_inv[of "Env empty" c B T]
`l ∈ do T` obj_inv_elim[of "Env empty" c B]
have "l ∈ dom c" by auto
with `t1 = Obj c B` `lc t1` `body t2` beta.beta_Upd[of l c B t2]
show ?thesis by auto
next
fix b assume "t1 ->⇩β b"
from beta.beta_UpdL[OF this `body t2`] show ?thesis by auto
qed
qed
qed
with assms show ?thesis by auto
qed
end