Up to index of Isabelle/Bali5
theory TypeSafe = Eval + WellForm + Conform:(* Title: isabelle/Bali/TypeSafe.thy
ID: $Id: TypeSafe.thy,v 1.23 2001/05/11 14:42:00 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The type soundness proof for Java
*)
theory TypeSafe = Eval + WellForm + Conform:
section "result conformance"
constdefs
assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env \<Rightarrow> bool"
("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E"
rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
"G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T \<equiv> case T of
Inl T \<Rightarrow> if (\<exists>vf. t=In2 vf)
then G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T \<and> s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L)
else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
| Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
lemma rconf_In1 [simp]:
"G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T = G,s\<turnstile>v\<Colon>\<preceq>T"
apply (unfold rconf_def)
apply (simp (no_asm))
done
lemma rconf_In2 [simp]:
"G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T = (G,s\<turnstile>fst vf\<Colon>\<preceq>T \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
apply (unfold rconf_def)
apply (simp (no_asm))
done
lemma rconf_In3 [simp]:
"G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (\<lambda>v T. G,s\<turnstile>v\<Colon>\<preceq>T) vs Ts"
apply (unfold rconf_def)
apply (simp (no_asm))
done
section "fits & conf"
(* unused *)
lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
apply (unfold fits_def)
apply clarify
apply (erule swap, simp (no_asm_use))
apply (drule conf_RefTD)
apply auto
done
lemma fits_conf: "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
apply (force dest: conf_RefTD intro: conf_AddrI)
done
lemma fits_Array:
"\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
apply (force dest: conf_RefTD intro: conf_AddrI)
done
section "gext"
lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule halloc.induct)
apply (auto dest!: new_AddrD)
done
lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule sxalloc.induct)
apply (auto dest!: halloc_gext)
done
lemma eval_gext_lemma [rule_format (no_asm)]:
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of
In1 v \<Rightarrow> True
| In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))
| In3 vs \<Rightarrow> True)"
apply (erule eval_induct)
prefer 22
apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext
simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2
split del: split_if_asm split add: sum3.split)
(* 6 subgoals *)
apply force+
done
lemma evar_gext_f: "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
apply (drule eval_gext_lemma [THEN conjunct2])
apply auto
done
lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2"
apply (drule eval_gext)
apply auto
done
lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
apply (erule eval_cases , auto split del: split_if_asm)
apply (case_tac "inited C (globs s1)")
apply (clarsimp split del: split_if_asm)+
apply (drule eval_gext')+
apply (drule init_class_obj_inited)
apply (erule inited_gext)
apply (simp (no_asm_use))
done
section "Lemmas"
lemma oconf_init_obj: "\<lbrakk>wf_prog G;
(case r of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs)) | Stat C \<Rightarrow> is_class G C)\<rbrakk> \<Longrightarrow>
G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r"
apply (auto intro!: oconf_init_obj_lemma unique_fields)
done
lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);
wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty (oi,fs))
| Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>
(x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
apply (unfold init_obj_def)
apply (auto elim!: conforms_gupd oconf_init_obj)
done
lemma conforms_init_class_obj:
"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; ¬ inited C (globs s)\<rbrakk> \<Longrightarrow>
(x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
apply (rule not_initedD [THEN conforms_newG])
apply auto
done
lemma fst_init_lvars: "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) =
(if m then x else (np a') x)"
apply (simp (no_asm) add: init_lvars_def2)
done
declare fst_init_lvars [simp]
lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
is_type G (obj_ty (oi,fs))\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (case_tac "aa")
apply (auto elim!: halloc_elim_cases dest!: new_AddrD
intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
done
lemma halloc_type_sound: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
T = obj_ty (oi,fs); is_type G T\<rbrakk> \<Longrightarrow>
(x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
apply (auto elim!: halloc_conforms)
apply (case_tac "aa")
apply (subst obj_ty_eq)
apply (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
done
lemma sxalloc_type_sound:
"\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> case fst s1 of
None \<Rightarrow> s2 = s1 | Some x \<Rightarrow>
(\<exists>a. fst s2 = Some(XcptLoc a) \<and> (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule sxalloc.induct)
apply auto
apply (rule halloc_conforms [THEN conforms_xconf])
apply (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
done
lemma wt_init_comp_ty:
"is_type G T \<Longrightarrow> (G,L)\<turnstile>init_comp_ty T\<Colon>\<surd>"
apply (unfold init_comp_ty_def)
apply clarsimp
done
declare fun_upd_same [simp]
declare fun_upd_apply [simp del]
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
ML_setup {*
simpset_ref() := simpset() delloop "split_all_tac";
claset_ref () := claset () delSWrapper "split_all_tac"
*}
constdefs
DynT_prop::"[prog,inv_mode,tname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
"G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and>
(if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
lemma DynT_propI:
"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT t; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> \<Longrightarrow>
G\<turnstile>mode\<rightarrow>target mode s a' cT\<preceq>t"
apply (unfold DynT_prop_def)
apply clarsimp
apply (drule (2) conforms_RefTD)
apply clarsimp
apply (frule obj_ty_widenD)
apply (auto dest!: widen_Array widen_Array2 split add: split_if)
done
ML {*
fun exhaust_cmethd_tac s = EVERY'[
res_inst_tac [("p",s)] PairE, rename_tac "md' j0",
res_inst_tac [("p","j0")] PairE, rename_tac "j00 j1",
res_inst_tac [("p","j1")] PairE, rename_tac "lvars body",
res_inst_tac [("p","body")] PairE, rename_tac "blk res",
res_inst_tac [("p","j00")] PairE, rename_tac "m' j2",
res_inst_tac [("p","j2")] PairE, rename_tac "pns' rT'",
hyp_subst_tac, K prune_params_tac]
*}
lemma DynT_mheadsD:
"\<lbrakk>the (cmethd G dynT sig)=(md,(m',pns,rT),lvars,bdy); G\<turnstile>invmode m e\<rightarrow>dynT\<preceq>t;
wf_prog G; (G, L)\<turnstile>e\<Colon>-RefT t; (cT, m, pnsa, T) \<in> mheads G t sig;
target (invmode m e) s2 a' cT = dynT\<rbrakk> \<Longrightarrow>
cmethd G dynT sig = Some (md, (m, pns, rT), lvars, bdy) \<and> G\<turnstile>rT\<preceq>T \<and> m' = m \<and>
wf_mdecl G md (sig, (m, pns, rT), lvars, bdy) \<and>
is_class G dynT \<and> G\<turnstile>dynT\<preceq>C md \<and> is_class G md \<and>
(invmode m e \<noteq> IntVir \<longrightarrow> (\<exists>C. t=ClassT C \<and> G\<turnstile>C \<preceq>C md) \<and> cT = ClassT md)"
apply (unfold DynT_prop_def)
apply (frule (1) ty_expr_is_type)
apply (case_tac "invmode m e = IntVir")
apply (clarsimp simp add: target_notIntVir)
defer
apply (clarsimp simp add: target_notIntVir)
apply (clarsimp simp add: invmode_IntVir_eq)
defer
apply (clarsimp simp add: invmode_IntVir_eq)
apply (drule (4) class_mheadsD)
defer
apply (drule (3) static_mheadsD, clarsimp, frule cmethd_defpl,
erule wf_ws_prog, simp (no_asm_simp))
apply (clarsimp, drule (2) cmethd_wf_mdecl, clarsimp)+
done
lemma DynT_conf: "\<lbrakk>G\<turnstile>target mode s2 a' cT\<preceq>C md; wf_prog G;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; mode = IntVir \<longrightarrow> a' \<noteq> Null;
mode \<noteq> IntVir \<longrightarrow> (\<exists>C. t=ClassT C \<and> G\<turnstile>C\<preceq>C md) \<and> cT = ClassT md\<rbrakk>\<Longrightarrow>
G,s2\<turnstile>a'\<Colon>\<preceq>Class md"
apply (case_tac "mode \<noteq> IntVir")
apply clarsimp
apply (erule (1) widen.subcls [THEN conf_widen])
apply (erule wf_ws_prog)
apply (drule conf_RefTD)
apply (auto intro!: conf_AddrI
simp add: obj_class_def split add: obj_tag.split_asm)
done
lemma Ass_lemma: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2; G,s2\<turnstile>v\<Colon>\<preceq>T'; s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and> (\<lambda>(x',s'). x' = None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T') (assign f v (Norm s2))"
apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
apply (drule eval_gext', clarsimp)
apply (erule conf_gext)
apply simp
done
lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);
x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq>Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
apply (auto split add: split_xcpt_if simp add: throw_def2)
apply (erule conforms_xconf)
apply (frule conf_RefTD)
apply (auto elim: widen.subcls [THEN conf_widen])
done
lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; (Some (XcptLoc a), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
apply (rule conforms_allocL)
apply (erule conforms_NormI)
apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
apply (auto intro!: conf_AddrI)
done
lemma Fin_lemma:
"\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>
(xcpt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
apply (force elim: eval_gext' conforms_xgext split add: split_xcpt_if)
done
lemma FVar_lemma1: "\<lbrakk>table_of (fields G Ca) (fn, C) = Some (stat, fT);
x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; wf_prog G; G\<turnstile>Ca\<preceq>C C; C \<noteq> Object;
class G C = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1);
(if stat then id else np a) x2 = None\<rbrakk> \<Longrightarrow>
\<exists>oi fs. globs s2 (if stat then Inr C else Inl (the_Addr a)) = Some (oi,fs) \<and>
var_tys G oi (if stat then Inr C else Inl(the_Addr a)) (Inl(fn,C)) = Some fT"
apply (drule initedD)
apply (frule subcls_is_class2, simp (no_asm_simp))
apply (case_tac "stat")
apply clarsimp
apply (drule (1) rev_gext_objD, clarsimp)
apply (frule fields_defpl, erule wf_ws_prog, simp (no_asm_simp))
apply (rule var_tys_Some_eq [THEN iffD2])
apply clarsimp
apply (erule fields_table_SomeI, simp (no_asm))
apply clarsimp
apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
apply (auto dest!: widen_Array split add: obj_tag.split)
apply (rule fields_table_SomeI)
apply (auto elim!: fields_mono subcls_is_class2)
done
lemma FVar_lemma:
"\<lbrakk>((v, f), Norm s2') = fvar C stat fn a (x2, s2); G\<turnstile>Ca\<preceq>C C;
table_of (fields G Ca) (fn, C) = Some (stat, fT); wf_prog G;
x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C \<noteq> Object; class G C = Some y;
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1)\<rbrakk> \<Longrightarrow>
G,s2'\<turnstile>v\<Colon>\<preceq>fT \<and> s2'\<le>|f\<preceq>fT\<Colon>\<preceq>(G, L)"
apply (unfold assign_conforms_def)
apply (drule sym)
apply (clarsimp simp add: fvar_def2)
apply (drule (9) FVar_lemma1)
apply (clarsimp, drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
apply clarsimp
apply (drule (1) rev_gext_objD,fast elim!: conforms_upd_gobj)
done
lemma AVar_lemma1: "\<lbrakk>globs s2 (Inl a) = Some (Arr ty i, vs); the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s2\<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> G,s2\<turnstile>the (vs (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
apply (erule widen_Array_Array [THEN conf_widen])
apply (erule_tac [2] wf_ws_prog)
apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
defer apply assumption
apply (force intro: var_tys_Some_eq [THEN iffD2])
done
lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);
((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>v\<Colon>\<preceq>Ta \<and> s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)"
apply (unfold assign_conforms_def)
apply (drule sym)
apply (clarsimp simp add: avar_def2)
apply (drule (1) conf_gext)
apply (drule conf_RefTD, clarsimp)
apply (frule obj_ty_widenD)
apply (auto dest!: widen_Class)
apply (erule (4) AVar_lemma1)
apply (auto split add: split_if)
apply (force elim!: fits_Array dest: gext_objD
intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
done
section "Call"
lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;
wf_mhead G (mn,pTs) (m,pns,rT); Ball (set lvars) (split (\<lambda>vn. is_type G));
list_all2 (conf G s2) pvs pTsa; G\<turnstile>pTsa[\<preceq>]pTs\<rbrakk> \<Longrightarrow>
G,s2\<turnstile>init_vals (table_of lvars)(pns[\<mapsto>]pvs)[\<Colon>\<preceq>]table_of lvars(pns[\<mapsto>]pTs)"
apply (unfold wf_mhead_def)
apply clarify
apply (erule (2) Ball_set_table [THEN lconf_init_vals, THEN lconf_ext_list])
apply (drule wf_ws_prog)
apply (erule (2) conf_list_widen)
done
lemma conforms_init_lvars: "\<lbrakk>wf_mhead G (mn, pTs) (m, pns', rT'); wf_prog G;
Ball (set lvars) (split (\<lambda>vn. is_type G));
list_all2 (conf G s2) pvs pTsa; G\<turnstile>pTsa[\<preceq>] pTs;
(x2, s2)\<Colon>\<preceq>(G, L); cmethd G (target (invmode m e) s2 a' cT) (mn, pTs) =
Some (md, (ma, pns', rT'), lvars, blk, res);
G\<turnstile>target (invmode m e) s2 a' cT\<preceq>C md; G,s2\<turnstile>a'\<Colon>\<preceq>RefT t;
invmode m e = IntVir \<longrightarrow> a' \<noteq> Null; invmode m e \<noteq> IntVir \<longrightarrow>
(\<exists>C. t = ClassT C \<and> G\<turnstile>C\<preceq>C md) \<and> cT = ClassT md\<rbrakk> \<Longrightarrow>
init_lvars G (target (invmode m e) s2 a' cT) (mn, pTs) (invmode m e) a'
pvs (x2,s2)\<Colon>\<preceq>(G, table_of lvars(pns'[\<mapsto>]pTs) (+) (if m then empty else empty(()\<mapsto>Class md)))"
apply (simp add: init_lvars_def2)
apply (rule conforms_set_locals)
apply (simp (no_asm_simp) split add: split_if)
apply (drule (4) DynT_conf)
apply (case_tac "m")
apply simp
defer apply simp
apply (rule conjI)
defer
apply (rule lconf_ext, simp, assumption)
apply (erule (4) conforms_init_lvars_lemma)+
done
lemma Call_type_sound: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2, s2);
C = target (invmode m e) s2 a' cT;
s2' = init_lvars G C (mn, pTs) (invmode m e) a' pvs (x2,s2);
G\<turnstile>s2' \<midarrow>Methd C (mn, pTs)-\<succ>v\<rightarrow> (x3, s3);
\<forall>L. s2'\<Colon>\<preceq>(G, L) \<longrightarrow> (\<forall>T. (G, L)\<turnstile>Methd C (mn, pTs)\<Colon>-T \<longrightarrow>
(x3, s3)\<Colon>\<preceq>(G, L) \<and> (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>T));
Norm s0\<Colon>\<preceq>(G, L); (G, L)\<turnstile>e\<Colon>-RefT t; (G, L)\<turnstile>ps\<Colon>\<doteq>pTsa;
max_spec G t (mn, pTsa) = {((cT, m, pns, rT), pTs)}; (x1, s1)\<Colon>\<preceq>(G, L);
x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq>RefT t; (x2, s2)\<Colon>\<preceq>(G, L);
x2 = None \<longrightarrow> list_all2 (conf G s2) pvs pTsa\<rbrakk> \<Longrightarrow>
(x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) \<and> (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>rT)"
apply clarify
apply (case_tac "x2")
defer
apply (clarsimp split add: split_if_asm simp add: init_lvars_def2)
apply (case_tac "a' = Null \<and> ¬ m \<and> e \<noteq> Super")
apply (clarsimp simp add: init_lvars_def2)
apply clarsimp
apply (drule eval_gext')
apply (frule (1) conf_gext)
apply (drule max_spec2mheads, clarsimp)
apply (subgoal_tac "invmode m e = IntVir \<longrightarrow> a' \<noteq> Null")
defer
apply (clarsimp simp add: invmode_IntVir_eq)
apply (tactic {* exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s2 a' cT) (mn, pTs))" 1*})
apply (drule (7) DynT_mheadsD [OF _ DynT_propI], rule HOL.refl)
apply clarify
apply (drule wf_mdeclD1, clarsimp)
apply (drule (10) conforms_init_lvars, tactic "smp_tac 1 1")
apply (frule (2) wt_MethdI, clarsimp)
apply (tactic "smp_tac 1 1")
apply (clarify, rule conjI)
apply (erule (1) conforms_return)
apply (force dest!: eval_gext del: impCE simp add: init_lvars_def2)
apply clarsimp
apply (drule (2) widen_trans, erule (1) conf_widen)
apply (erule wf_ws_prog)
done
section "main proof of type safety"
ML {*
val forward_hyp_tac = EVERY' [smp_tac 1,
FIRST'[mp_tac,etac exI,smp_tac 1,EVERY'[etac impE,etac exI]],
REPEAT o (etac conjE)];
val typD_tac = eresolve_tac (thms "wt_elim_cases") THEN_ALL_NEW
EVERY' [full_simp_tac (simpset() setloop (K no_tac)),
clarify_tac(claset() addSEs[])]
*}
lemma eval_type_sound [rule_format (no_asm)]:
"wf_prog G \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1) \<Longrightarrow> (\<forall>L. s0\<Colon>\<preceq>(G,L) \<longrightarrow>
(\<forall>T. (G,L)\<turnstile>t\<Colon>T \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and>
(let (x,s) = s1 in x = None \<longrightarrow> G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T)))"
apply (erule eval_induct)
(* 27 subgoals *)
(* Xcpt, Inst, Methd, Nil, Skip, Expr, Comp, Body *)
apply (simp_all (no_asm_use) add: Let_def body_def)
apply (tactic "ALLGOALS (EVERY'[Clarify_tac, TRY o typD_tac,
TRY o forward_hyp_tac])")
apply (tactic"ALLGOALS(EVERY'[asm_simp_tac(simpset()),TRY o Clarify_tac])")
(* 19 subgoals *)
(* Cons *)
apply (erule_tac V = "G\<turnstile>Norm s0 \<midarrow>?ea\<succ>\<rightarrow> ?vs1" in thin_rl)
apply (frule eval_gext')
apply force
(* LVar *)
apply (force elim: conforms_localD [THEN lconfD] conforms_lupd
simp add: assign_conforms_def lvar_def)
(* Cast *)
apply (force dest: fits_conf)
(* Lit *)
apply (rule conf_litval)
apply (simp add: empty_dt_def)
(* Super *)
apply (rule conf_widen)
apply (erule (1) subcls_direct [THEN widen.subcls])
apply (erule (1) conforms_localD [THEN lconfD])
apply (erule wf_ws_prog)
(* Acc *)
apply fast
(* Body *)
(* Cond *)
apply (simp split: split_if_asm)
apply (tactic "forward_hyp_tac 1", force)
apply (tactic "forward_hyp_tac 1", force)
(* If *)
apply (force split add: split_if_asm)
(* Loop *)
apply (drule (1) wt.Loop)
apply (clarsimp split: split_if_asm)
(* Fin *)
apply (case_tac "x1", force)
apply (drule spec, erule impE, erule conforms_NormI)
apply (clarsimp)
apply (erule (3) Fin_lemma)
(* Throw *)
apply (erule (3) Throw_lemma)
(* NewC *)
apply (drule (2) halloc_type_sound, rule HOL.refl, simp, simp)
(* NewA *)
apply (tactic "smp_tac 1 1", frule wt_init_comp_ty, erule (1) notE impE)
apply (tactic "forward_hyp_tac 1")
apply (case_tac "check_neg i' ab")
apply clarsimp
apply (drule (2) halloc_type_sound, rule HOL.refl, simp, simp)
apply force
(* Level 34, 6 subgoals *)
(* Init *)
apply (case_tac "inited C (globs s0)")
apply (clarsimp)
apply (clarsimp)
apply (frule (1) wf_prog_cdecl)
apply (drule spec, erule impE, erule (3) conforms_init_class_obj)
apply (drule_tac "psi" = "class G C = ?x" in asm_rl, erule impE,
force dest!: wf_cdecl_supD split add: split_if)
apply (drule spec, erule impE, erule conforms_set_locals, rule lconf_empty)
apply (erule impE, erule wf_cdecl_wt_init)
apply (drule (1) conforms_return, force dest: eval_gext', assumption)
(* Ass *)
apply (tactic "forward_hyp_tac 1")
apply (rename_tac x1 s1 x2 s2 v va w L Ta T', case_tac x1)
prefer 2 apply force
apply (case_tac x2)
prefer 2 apply force
apply (simp, drule conjunct2)
apply (drule (1) conf_widen)
apply (erule wf_ws_prog)
apply (erule (2) Ass_lemma)
apply (clarsimp simp add: assign_conforms_def)
(* Try *)
apply (drule (1) sxalloc_type_sound, simp (no_asm_use))
apply (case_tac a)
apply clarsimp
apply clarsimp
apply (tactic "smp_tac 1 1")
apply (simp split add: split_if_asm)
apply (fast dest: conforms_deallocL Try_lemma)
(* FVar *)
apply (frule cfield_fields)
apply (frule (1) ty_expr_is_type [THEN type_is_class])
apply (frule wf_ws_prog)
apply (frule (2) fields_defpl)
apply clarsimp
(*b y EVERY'[datac cfield_defpl_is_class 2, Clarsimp_tac] 1; not useful here*)
apply (tactic "smp_tac 1 1")
apply (tactic "forward_hyp_tac 1")
apply (rule conjI, force split add: split_if simp add: fvar_def2)
apply (drule init_yields_initd, frule eval_gext')
apply clarsimp
apply (case_tac "C=Object")
apply clarsimp
apply (erule (9) FVar_lemma)
(* AVar *)
apply (tactic "forward_hyp_tac 1")
apply (erule_tac V = "G\<turnstile>Norm s0 \<midarrow>?e1-\<succ>?a'\<rightarrow> (?x1 1, ?s1)" in thin_rl,
frule eval_gext')
apply (rule conjI)
apply (clarsimp simp add: avar_def2)
apply clarsimp
apply (erule (5) AVar_lemma)
(* Call *)
apply (tactic "forward_hyp_tac 1")
apply (erule (1) Call_type_sound, (rule HOL.refl)+, assumption+)
done
declare fun_upd_apply [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
ML_setup {*
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac);
claset_ref() := claset () addSbefore ("split_all_tac", split_all_tac)
*}
theorem eval_ts: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
(x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T)"
apply (drule (3) eval_type_sound)
apply (unfold Let_def)
apply clarsimp
done
theorem evals_ts: "\<lbrakk>G\<turnstile>s \<midarrow>es\<doteq>\<succ>vs\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
(x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> list_all2 (conf G s') vs Ts)"
apply (drule (3) eval_type_sound)
apply (unfold Let_def)
apply clarsimp
done
theorem evar_ts: "\<lbrakk>G\<turnstile>s \<midarrow>v=\<succ>vf\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>v\<Colon>=T\<rbrakk> \<Longrightarrow>
(x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,L,s'\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T)"
apply (drule (3) eval_type_sound)
apply (unfold Let_def)
apply clarsimp
done
theorem exec_ts: "\<lbrakk>G\<turnstile>s \<midarrow>s0\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); (G,L)\<turnstile>s0\<Colon>\<surd>\<rbrakk> \<Longrightarrow> s'\<Colon>\<preceq>(G,L)"
apply (drule (3) eval_type_sound)
apply (unfold Let_def)
apply clarsimp
done
theorem dyn_methods_understood:
"\<And>s. \<lbrakk>wf_prog G; (G,L)\<turnstile>{t,md,IntVir}e..mn({pTs'}ps)\<Colon>-rT;
s\<Colon>\<preceq>(G,L); G\<turnstile>s \<midarrow>e-\<succ>a'\<rightarrow> Norm s'; a' \<noteq> Null\<rbrakk> \<Longrightarrow>
\<exists>a obj. a'=Addr a \<and> heap s' a = Some obj \<and> cmethd G (obj_class obj) (mn, pTs') \<noteq> None"
apply (erule wt_elim_cases)
apply (drule max_spec2mheads)
apply (drule (3) eval_ts)
apply (clarsimp split del: split_if split_if_asm)
apply (drule (2) DynT_propI)
apply (simp (no_asm_simp))
apply (tactic {* exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s' a' md) (mn, pTs'))" 1 *})
apply (drule (4) DynT_mheadsD [THEN conjunct1], rule HOL.refl)
apply (drule conf_RefTD)
apply clarsimp
done
end
lemma rconf_In1:
G,L,s\<turnstile>In1 ec\<succ>In1 v\<Colon>\<preceq>Inl T = G,s\<turnstile>v\<Colon>\<preceq>T
lemma rconf_In2:
G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T = (G,s\<turnstile>fst vf\<Colon>\<preceq>T & s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G, L))
lemma rconf_In3:
G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (conf G s) vs Ts
lemma conf_fits:
G,s\<turnstile>v\<Colon>\<preceq>T ==> G,s\<turnstile>v fits T [!]
lemma fits_conf:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T<=:? T'; G,s\<turnstile>v fits T';
ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
[!]
lemma fits_Array:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T'.[]<=:T.[];
G,s\<turnstile>v fits T'; ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
[!]
lemma halloc_gext:
G|-s1 -halloc oi>a-> s2 ==> snd s1\<le>|snd s2 [!]
lemma sxalloc_gext:
G|-s1 -sxalloc-> s2 ==> snd s1\<le>|snd s2 [!]
lemma eval_gext_lemma:
G|-s -t>-> (w, s')
==> snd s\<le>|snd s' &
(case w of In1 v => True
| In2 vf => normal s --> (ALL v x s. s\<le>|snd (assign (snd vf) v (x, s)))
| In3 vs => True)
[!]
lemma evar_gext_f:
G|-Norm s1 -e=>vf-> s2 ==> s\<le>|snd (assign (snd vf) v (x, s)) [!]
lemmas eval_gext:
G_1|-s_1 -t_1>-> (w_1, s'_1) ==> snd s_1\<le>|snd s'_1 [!]
lemma eval_gext':
G|-(x1, s1) -t>-> (w, x2, s2) ==> s1\<le>|s2 [!]
lemma init_yields_initd:
G|-Norm s1 -init C-> s2 ==> initd C s2 [!]
lemma oconf_init_obj:
[| wf_prog G;
case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r
[!]
lemma conforms_newG:
[| globs s oref = None; (x, s)\<Colon>\<preceq>(G, L); wf_prog G;
case oref of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)
[!]
lemma conforms_init_class_obj:
[| (x, s)\<Colon>\<preceq>(G, L); wf_prog G; class G C = Some y;
¬ inited C (globs s) |]
==> (x, (init_class_obj G C) s)\<Colon>\<preceq>(G, L)
[!]
lemma fst_init_lvars:
fst (init_lvars G C sig (invmode m e) a' pvs (x, s)) = (if m then x else (np a') x)
lemma halloc_conforms:
[| G|-s1 -halloc oi>a-> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
is_type G (obj_ty (oi, fs)) |]
==> s2\<Colon>\<preceq>(G, L)
[!]
lemma halloc_type_sound:
[| G|-s1 -halloc oi>a-> (x, s); wf_prog G; s1\<Colon>\<preceq>(G, L);
T = obj_ty (oi, fs); is_type G T |]
==> (x, s)\<Colon>\<preceq>(G, L) &
(x = None --> G,s\<turnstile>Addr a\<Colon>\<preceq>T)
[!]
lemma sxalloc_type_sound:
[| G|-s1 -sxalloc-> s2; wf_prog G |]
==> case fst s1 of None => s2 = s1
| Some x =>
EX a. fst s2 = Some (XcptLoc a) &
(ALL L. s1\<Colon>\<preceq>(G, L) --> s2\<Colon>\<preceq>(G, L))
[!]
lemma wt_init_comp_ty:
is_type G T ==> (G, L)|-init_comp_ty T:<> [!]
lemma DynT_propI:
[| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT t;
wf_prog G; mode = IntVir --> a' ~= Null |]
==> G\<turnstile>mode\<rightarrow>target mode s a' cT\<preceq>t
[!]
lemma DynT_mheadsD:
[| the (cmethd G dynT sig) = (md, (m', pns, rT), lvars, bdy);
G\<turnstile>invmode m e\<rightarrow>dynT\<preceq>t; wf_prog G;
(G, L)|-e:-RefT t; (cT, m, pnsa, T) : mheads G t sig;
target (invmode m e) s2 a' cT = dynT |]
==> cmethd G dynT sig = Some (md, (m, pns, rT), lvars, bdy) &
G|-rT<=:T &
m' = m &
wf_mdecl G md (sig, (m, pns, rT), lvars, bdy) &
is_class G dynT &
G|-dynT<=:C md &
is_class G md &
(invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md)
[!]
lemma DynT_conf:
[| G|-target mode s2 a' cT<=:C md; wf_prog G;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; mode = IntVir --> a' ~= Null;
mode ~= IntVir --> (EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> G,s2\<turnstile>a'\<Colon>\<preceq>Class md
[!]
lemma Ass_lemma:
[| G|-Norm s0 -va=>(w, f)-> Norm s1; G|-Norm s1 -e->v-> Norm s2;
G,s2\<turnstile>v\<Colon>\<preceq>T';
s1\<le>|s2 --> assign f v (Norm s2)\<Colon>\<preceq>(G, L) |]
==> assign f v (Norm s2)\<Colon>\<preceq>(G, L) &
(%(x', s'). x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T')
(assign f v (Norm s2))
[!]
lemma Throw_lemma:
[| G|-tn<=:C SXcpt Throwable; wf_prog G; (x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>Class tn |]
==> (throw a' x1, s1)\<Colon>\<preceq>(G, L)
[!]
lemma Try_lemma:
[| G|-obj_ty (the (globs s1' (Inl a)))<=:Class tn;
(Some (XcptLoc a), s1')\<Colon>\<preceq>(G, L); wf_prog G |]
==> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn|->Class tn))
[!]
lemma Fin_lemma:
[| G|-Norm s1 -c2-> (x2, s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L);
(x2, s2)\<Colon>\<preceq>(G, L) |]
==> (xcpt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)
[!]
lemma FVar_lemma1:
[| table_of (fields G Ca) (fn, C) = Some (stat, fT);
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; wf_prog G;
G|-Ca<=:C C; C ~= Object; class G C = Some y;
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1);
(if stat then id else np a) x2 = None |]
==> EX oi fs.
globs s2 (if stat then Inr C else Inl (the_Addr a)) = Some (oi, fs) &
var_tys G oi (if stat then Inr C else Inl (the_Addr a)) (Inl (fn, C)) =
Some fT
[!]
lemma FVar_lemma:
[| ((v, f), Norm s2') = fvar C stat fn a (x2, s2); G|-Ca<=:C C;
table_of (fields G Ca) (fn, C) = Some (stat, fT); wf_prog G;
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C ~= Object;
class G C = Some y; (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2;
inited C (globs s1) |]
==> G,s2'\<turnstile>v\<Colon>\<preceq>fT &
s2'\<le>|f\<preceq>fT\<Colon>\<preceq>(G, L)
[!]
lemma AVar_lemma1:
[| globs s2 (Inl a) = Some (Arr ty i, vs); the_Intg i' in_bounds i; wf_prog G;
G|-ty.[]<=:Tb.[]; Norm s2\<Colon>\<preceq>(G, L) |]
==> G,s2\<turnstile>the (vs (Inr (the_Intg i')))\<Colon>\<preceq>Tb
[!]
lemma AVar_lemma:
[| wf_prog G; G|-(x1, s1) -e2->i-> (x2, s2);
((v, f), Norm s2') = avar G i a (x2, s2);
x1 = None --> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2 |]
==> G,s2'\<turnstile>v\<Colon>\<preceq>Ta &
s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)
[!]
lemma conforms_init_lvars_lemma:
[| wf_prog G; wf_mhead G (mn, pTs) (m, pns, rT);
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs |]
==> G,s2\<turnstile>init_vals (table_of lvars)(pns[|->]pvs
)[\<Colon>\<preceq>]table_of lvars(pns[|->]pTs)
[!]
lemma conforms_init_lvars:
[| wf_mhead G (mn, pTs) (m, pns', rT'); wf_prog G;
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs; (x2, s2)\<Colon>\<preceq>(G, L);
cmethd G (target (invmode m e) s2 a' cT) (mn, pTs) =
Some (md, (ma, pns', rT'), lvars, blk, res);
G|-target (invmode m e) s2 a' cT<=:C md;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t;
invmode m e = IntVir --> a' ~= Null;
invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> init_lvars G (target (invmode m e) s2 a' cT) (mn, pTs) (invmode m e) a' pvs
(x2, s2)\<Colon>\<preceq>(G, table_of lvars(pns'[|->]pTs) (+)
(if m then empty else empty(()|->Class md)))
[!]
lemma Call_type_sound:
[| wf_prog G; G|-(x1, s1) -ps#>pvs-> (x2, s2);
C = target (invmode m e) s2 a' cT;
s2' = init_lvars G C (mn, pTs) (invmode m e) a' pvs (x2, s2);
G|-s2' -Methd C (mn, pTs)->v-> (x3, s3);
ALL L. s2'\<Colon>\<preceq>(G, L) -->
(ALL T. (G, L)|-Methd C (mn, pTs):-T -->
(x3, s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>T));
Norm s0\<Colon>\<preceq>(G, L); (G, L)|-e:-RefT t; (G, L)|-ps:#pTsa;
max_spec G t (mn, pTsa) = {((cT, m, pns, rT), pTs)};
(x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>RefT t;
(x2, s2)\<Colon>\<preceq>(G, L);
x2 = None --> list_all2 (conf G s2) pvs pTsa |]
==> (x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>rT)
[!]
lemma eval_type_sound:
[| wf_prog G; G|-s0 -t>-> (v, s1); s0\<Colon>\<preceq>(G, L); (G, L)|-t::T |]
==> s1\<Colon>\<preceq>(G, L) &
(let (x, s) = s1
in x = None --> G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T)
[!]
theorem eval_ts:
[| G|-s -e->v-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-e:-T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T)
[!]
theorem evals_ts:
[| G|-s -es#>vs-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-es:#Ts |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> list_all2 (conf G s') vs Ts)
[!]
theorem evar_ts:
[| G|-s -v=>vf-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-v:=T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> G,L,s'\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T)
[!]
theorem exec_ts:
[| G|-s -s0-> s'; wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-s0:<> |]
==> s'\<Colon>\<preceq>(G, L)
[!]
theorem dyn_methods_understood:
[| wf_prog G; (G, L)|-{t,md,IntVir}e..mn( {pTs'}ps):-rT;
s\<Colon>\<preceq>(G, L); G|-s -e->a'-> Norm s'; a' ~= Null |]
==> EX a obj.
a' = Addr a &
heap s' a = Some obj & cmethd G (obj_class obj) (mn, pTs') ~= None
[!]