Theory TypeSafe
subsection ‹The type soundness proof for Java›
theory TypeSafe
imports DefiniteAssignmentCorrect Conform
begin
subsubsection "error free"
lemma error_free_halloc:
assumes halloc: "G⊢s0 ─halloc oi≻a→ s1" and
error_free_s0: "error_free s0"
shows "error_free s1"
proof -
from halloc error_free_s0
obtain abrupt0 store0 abrupt1 store1
where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
halloc': "G⊢(abrupt0,store0) ─halloc oi≻a→ (abrupt1,store1)" and
error_free_s0': "error_free (abrupt0,store0)"
by (cases s0,cases s1) auto
from halloc' error_free_s0'
have "error_free (abrupt1,store1)"
proof (induct)
case Abrupt
then show ?case .
next
case New
then show ?case
by auto
qed
with eqs
show ?thesis
by simp
qed
lemma error_free_sxalloc:
assumes sxalloc: "G⊢s0 ─sxalloc→ s1" and error_free_s0: "error_free s0"
shows "error_free s1"
proof -
from sxalloc error_free_s0
obtain abrupt0 store0 abrupt1 store1
where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
sxalloc': "G⊢(abrupt0,store0) ─sxalloc→ (abrupt1,store1)" and
error_free_s0': "error_free (abrupt0,store0)"
by (cases s0,cases s1) auto
from sxalloc' error_free_s0'
have "error_free (abrupt1,store1)"
proof (induct)
qed (auto)
with eqs
show ?thesis
by simp
qed
lemma error_free_check_field_access_eq:
"error_free (check_field_access G accC statDeclC fn stat a s)
⟹ (check_field_access G accC statDeclC fn stat a s) = s"
apply (cases s)
apply (auto simp add: check_field_access_def Let_def error_free_def
abrupt_if_def
split: if_split_asm)
done
lemma error_free_check_method_access_eq:
"error_free (check_method_access G accC statT mode sig a' s)
⟹ (check_method_access G accC statT mode sig a' s) = s"
apply (cases s)
apply (auto simp add: check_method_access_def Let_def error_free_def
abrupt_if_def)
done
lemma error_free_FVar_lemma:
"error_free s
⟹ error_free (abupd (if stat then id else np a) s)"
by (case_tac s) auto
lemma error_free_init_lvars [simp,intro]:
"error_free s ⟹
error_free (init_lvars G C sig mode a pvs s)"
by (cases s) (auto simp add: init_lvars_def Let_def)
lemma error_free_LVar_lemma:
"error_free s ⟹ error_free (assign (λv. supd lupd(vn↦v)) w s)"
by (cases s) simp
lemma error_free_throw [simp,intro]:
"error_free s ⟹ error_free (abupd (throw x) s)"
by (cases s) (simp add: throw_def)
subsubsection "result conformance"
definition
assign_conforms :: "st ⇒ (val ⇒ state ⇒ state) ⇒ ty ⇒ env' ⇒ bool" ("_≤|_≼_∷≼_" [71,71,71,71] 70)
where
"s≤|f≼T∷≼E =
((∀s' w. Norm s'∷≼E ⟶ fst E,s'⊢w∷≼T ⟶ s≤|s' ⟶ assign f w (Norm s')∷≼E) ∧
(∀s' w. error_free s' ⟶ (error_free (assign f w s'))))"
definition
rconf :: "prog ⇒ lenv ⇒ st ⇒ term ⇒ vals ⇒ tys ⇒ bool" ("_,_,_⊢_≻_∷≼_" [71,71,71,71,71,71] 70)
where
"G,L,s⊢t≻v∷≼T =
(case T of
Inl T ⇒ if (∃ var. t=In2 var)
then (∀ n. (the_In2 t) = LVar n
⟶ (fst (the_In2 v) = the (locals s n)) ∧
(locals s n ≠ None ⟶ G,s⊢fst (the_In2 v)∷≼T)) ∧
(¬ (∃ n. the_In2 t=LVar n) ⟶ (G,s⊢fst (the_In2 v)∷≼T))∧
(s≤|snd (the_In2 v)≼T∷≼(G,L))
else G,s⊢the_In1 v∷≼T
| Inr Ts ⇒ list_all2 (conf G s) (the_In3 v) Ts)"
text ‹
With \<^term>‹rconf› we describe the conformance of the result value of a term.
This definition gets rather complicated because of the relations between the
injections of the different terms, types and values. The main case distinction
is between single values and value lists. In case of value lists, every
value has to conform to its type. For single values we have to do a further
case distinction, between values of variables \<^term>‹∃var. t=In2 var› and
ordinary values. Values of variables are modelled as pairs consisting of the
current value and an update function which will perform an assignment to the
variable. This stems form the decision, that we only have one evaluation rule
for each kind of variable. The decision if we read or write to the
variable is made by syntactic enclosing rules. So conformance of
variable-values must ensure that both the current value and an update will
conform to the type. With the introduction of definite assignment of local
variables we have to do another case distinction. For the notion of conformance
local variables are allowed to be \<^term>‹None›, since the definedness is not
ensured by conformance but by definite assignment. Field and array variables
must contain a value.
›
lemma rconf_In1 [simp]:
"G,L,s⊢In1 ec≻In1 v ∷≼Inl T = G,s⊢v∷≼T"
apply (unfold rconf_def)
apply (simp (no_asm))
done
lemma rconf_In2_no_LVar [simp]:
"∀ n. va≠LVar n ⟹
G,L,s⊢In2 va≻In2 vf∷≼Inl T = (G,s⊢fst vf∷≼T ∧ s≤|snd vf≼T∷≼(G,L))"
apply (unfold rconf_def)
apply auto
done
lemma rconf_In2_LVar [simp]:
"va=LVar n ⟹
G,L,s⊢In2 va≻In2 vf∷≼Inl T
= ((fst vf = the (locals s n)) ∧
(locals s n ≠ None ⟶ G,s⊢fst vf∷≼T) ∧ s≤|snd vf≼T∷≼(G,L))"
apply (unfold rconf_def)
by simp
lemma rconf_In3 [simp]:
"G,L,s⊢In3 es≻In3 vs∷≼Inr Ts = list_all2 (λv T. G,s⊢v∷≼T) vs Ts"
apply (unfold rconf_def)
apply (simp (no_asm))
done
subsubsection "fits and conf"
lemma conf_fits: "G,s⊢v∷≼T ⟹ G,s⊢v fits T"
apply (unfold fits_def)
apply clarify
apply (erule contrapos_np, simp (no_asm_use))
apply (drule conf_RefTD)
apply auto
done
lemma fits_conf:
"⟦G,s⊢v∷≼T; G⊢T≼? T'; G,s⊢v fits T'; ws_prog G⟧ ⟹ G,s⊢v∷≼T'"
apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
apply (force dest: conf_RefTD intro: conf_AddrI)
done
lemma fits_Array:
"⟦G,s⊢v∷≼T; G⊢T'.[]≼T.[]; G,s⊢v fits T'; ws_prog G⟧ ⟹ G,s⊢v∷≼T'"
apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
apply (force dest: conf_RefTD intro: conf_AddrI)
done
subsubsection "gext"
lemma halloc_gext: "⋀s1 s2. G⊢s1 ─halloc oi≻a→ s2 ⟹ snd s1≤|snd s2"
apply (simp (no_asm_simp) only: split_tupled_all)
apply (erule halloc.induct)
apply (auto dest!: new_AddrD)
done
lemma sxalloc_gext: "⋀s1 s2. G⊢s1 ─sxalloc→ s2 ⟹ snd s1≤|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⊢s ─t≻→ (w,s') ⟹ snd s≤|snd s' ∧ (case w of
In1 v ⇒ True
| In2 vf ⇒ normal s ⟶ (∀v x s. s≤|snd (assign (snd vf) v (x,s)))
| In3 vs ⇒ True)"
apply (erule eval_induct)
prefer 26
apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl)
apply (auto del: conjI dest!: not_initedD gext_new sxalloc_gext halloc_gext
simp add: lvar_def fvar_def2 avar_def2 init_lvars_def2
check_field_access_def check_method_access_def Let_def
split del: if_split_asm split: sum3.split)
apply force+
done
lemma evar_gext_f:
"G⊢Norm s1 ─e=≻vf → s2 ⟹ s≤|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⊢(x1,s1) ─t≻→ (w,(x2,s2)) ⟹ s1≤|s2"
apply (drule eval_gext)
apply auto
done
lemma init_yields_initd: "G⊢Norm s1 ─Init C→ s2 ⟹ initd C s2"
apply (erule eval_cases , auto split del: if_split_asm)
apply (case_tac "inited C (globs s1)")
apply (clarsimp split del: if_split_asm)+
apply (drule eval_gext')+
apply (drule init_class_obj_inited)
apply (erule inited_gext)
apply (simp (no_asm_use))
done
subsubsection "Lemmas"
lemma obj_ty_obj_class1:
"⟦wf_prog G; is_type G (obj_ty obj)⟧ ⟹ is_class G (obj_class obj)"
apply (case_tac "tag obj")
apply (auto simp add: obj_ty_def obj_class_def)
done
lemma oconf_init_obj:
"⟦wf_prog G;
(case r of Heap a ⇒ is_type G (obj_ty obj) | Stat C ⇒ is_class G C)
⟧ ⟹ G,s⊢obj ⦇values:=init_vals (var_tys G (tag obj) r)⦈∷≼√r"
apply (auto intro!: oconf_init_obj_lemma unique_fields)
done
lemma conforms_newG: "⟦globs s oref = None; (x, s)∷≼(G,L);
wf_prog G; case oref of Heap a ⇒ is_type G (obj_ty ⦇tag=oi,values=vs⦈)
| Stat C ⇒ is_class G C⟧ ⟹
(x, init_obj G oi oref s)∷≼(G, L)"
apply (unfold init_obj_def)
apply (auto elim!: conforms_gupd dest!: oconf_init_obj
)
done
lemma conforms_init_class_obj:
"⟦(x,s)∷≼(G, L); wf_prog G; class G C=Some y; ¬ inited C (globs s)⟧ ⟹
(x,init_class_obj G C s)∷≼(G, L)"
apply (rule not_initedD [THEN conforms_newG])
apply (auto)
done
lemma fst_init_lvars[simp]:
"fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) =
(if is_static m then x else (np a') x)"
apply (simp (no_asm) add: init_lvars_def2)
done
lemma halloc_conforms: "⋀s1. ⟦G⊢s1 ─halloc oi≻a→ s2; wf_prog G; s1∷≼(G, L);
is_type G (obj_ty ⦇tag=oi,values=fs⦈)⟧ ⟹ s2∷≼(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:
"⋀s1. ⟦G⊢s1 ─halloc oi≻a→ (x,s); wf_prog G; s1∷≼(G, L);
T = obj_ty ⦇tag=oi,values=fs⦈; is_type G T⟧ ⟹
(x,s)∷≼(G, L) ∧ (x = None ⟶ G,s⊢Addr a∷≼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:
"⋀s1 s2. ⟦G⊢s1 ─sxalloc→ s2; wf_prog G⟧ ⟹
case fst s1 of
None ⇒ s2 = s1
| Some abr ⇒ (case abr of
Xcpt x ⇒ (∃a. fst s2 = Some(Xcpt (Loc a)) ∧
(∀L. s1∷≼(G,L) ⟶ s2∷≼(G,L)))
| Jump j ⇒ s2 = s1
| Error e ⇒ s2 = s1)"
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_acc_type G (pid C) T ⟹ ⦇prg=G,cls=C,lcl=L⦈⊢init_comp_ty T∷√"
apply (unfold init_comp_ty_def)
apply (clarsimp simp add: accessible_in_RefT_simp
is_acc_type_def is_acc_class_def)
done
declare fun_upd_same [simp]
declare fun_upd_apply [simp del]
definition
DynT_prop :: "[prog,inv_mode,qtname,ref_ty] ⇒ bool" ("_⊢_→_≼_"[71,71,71,71]70)
where
"G⊢mode→D≼t = (mode = IntVir ⟶ is_class G D ∧
(if (∃T. t=ArrayT T) then D=Object else G⊢Class D≼RefT t))"
lemma DynT_propI:
"⟦(x,s)∷≼(G, L); G,s⊢a'∷≼RefT statT; wf_prog G; mode = IntVir ⟶ a' ≠ Null⟧
⟹ G⊢mode→invocation_class mode s a' statT≼statT"
proof (unfold DynT_prop_def)
assume state_conform: "(x,s)∷≼(G, L)"
and statT_a': "G,s⊢a'∷≼RefT statT"
and wf: "wf_prog G"
and mode: "mode = IntVir ⟶ a' ≠ Null"
let ?invCls = "(invocation_class mode s a' statT)"
let ?IntVir = "mode = IntVir"
let ?Concl = "λinvCls. is_class G invCls ∧
(if ∃T. statT = ArrayT T
then invCls = Object
else G⊢Class invCls≼RefT statT)"
show "?IntVir ⟶ ?Concl ?invCls"
proof
assume modeIntVir: ?IntVir
with mode have not_Null: "a' ≠ Null" ..
from statT_a' not_Null state_conform
obtain a obj
where obj_props: "a' = Addr a" "globs s (Inl a) = Some obj"
"G⊢obj_ty obj≼RefT statT" "is_type G (obj_ty obj)"
by (blast dest: conforms_RefTD)
show "?Concl ?invCls"
proof (cases "tag obj")
case CInst
with modeIntVir obj_props
show ?thesis
by (auto dest!: widen_Array2)
next
case Arr
from Arr obtain T where "obj_ty obj = T.[]" by blast
moreover from Arr have "obj_class obj = Object"
by blast
moreover note modeIntVir obj_props wf
ultimately show ?thesis by (auto dest!: widen_Array )
qed
qed
qed
lemma invocation_methd:
"⟦wf_prog G; statT ≠ NullT;
(∀ statC. statT = ClassT statC ⟶ is_class G statC);
(∀ I. statT = IfaceT I ⟶ is_iface G I ∧ mode ≠ SuperM);
(∀ T. statT = ArrayT T ⟶ mode ≠ SuperM);
G⊢mode→invocation_class mode s a' statT≼statT;
dynlookup G statT (invocation_class mode s a' statT) sig = Some m ⟧
⟹ methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
proof -
assume wf: "wf_prog G"
and not_NullT: "statT ≠ NullT"
and statC_prop: "(∀ statC. statT = ClassT statC ⟶ is_class G statC)"
and statI_prop: "(∀ I. statT = IfaceT I ⟶ is_iface G I ∧ mode ≠ SuperM)"
and statA_prop: "(∀ T. statT = ArrayT T ⟶ mode ≠ SuperM)"
and invC_prop: "G⊢mode→invocation_class mode s a' statT≼statT"
and dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig
= Some m"
show ?thesis
proof (cases statT)
case NullT
with not_NullT show ?thesis by simp
next
case IfaceT
with statI_prop obtain I
where statI: "statT = IfaceT I" and
is_iface: "is_iface G I" and
not_SuperM: "mode ≠ SuperM" by blast
show ?thesis
proof (cases mode)
case Static
with wf dynlookup statI is_iface
show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def
dynimethd_def dynmethd_C_C
intro: dynmethd_declclass
dest!: wf_imethdsD
dest: table_of_map_SomeI)
next
case SuperM
with not_SuperM show ?thesis ..
next
case IntVir
with wf dynlookup IfaceT invC_prop show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
DynT_prop_def
intro: methd_declclass dynmethd_declclass)
qed
next
case ClassT
show ?thesis
proof (cases mode)
case Static
with wf ClassT dynlookup statC_prop
show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
intro: dynmethd_declclass)
next
case SuperM
with wf ClassT dynlookup statC_prop
show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
intro: dynmethd_declclass)
next
case IntVir
with wf ClassT dynlookup statC_prop invC_prop
show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
DynT_prop_def
intro: dynmethd_declclass)
qed
next
case ArrayT
show ?thesis
proof (cases mode)
case Static
with wf ArrayT dynlookup show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def
dynimethd_def dynmethd_C_C
intro: dynmethd_declclass
dest: table_of_map_SomeI)
next
case SuperM
with ArrayT statA_prop show ?thesis by blast
next
case IntVir
with wf ArrayT dynlookup invC_prop show ?thesis
by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
DynT_prop_def dynmethd_C_C
intro: dynmethd_declclass
dest: table_of_map_SomeI)
qed
qed
qed
lemma DynT_mheadsD:
"⟦G⊢invmode sm e→invC≼statT;
wf_prog G; ⦇prg=G,cls=C,lcl=L⦈⊢e∷-RefT statT;
(statDeclT,sm) ∈ mheads G C statT sig;
invC = invocation_class (invmode sm e) s a' statT;
declC =invocation_declclass G (invmode sm e) s a' statT sig
⟧ ⟹
∃ dm.
methd G declC sig = Some dm ∧ dynlookup G statT invC sig = Some dm ∧
G⊢resTy (mthd dm)≼resTy sm ∧
wf_mdecl G declC (sig, mthd dm) ∧
declC = declclass dm ∧
is_static dm = is_static sm ∧
is_class G invC ∧ is_class G declC ∧ G⊢invC≼⇩C declC ∧
(if invmode sm e = IntVir
then (∀ statC. statT=ClassT statC ⟶ G⊢invC ≼⇩C statC)
else ( (∃ statC. statT=ClassT statC ∧ G⊢statC≼⇩C declC)
∨ (∀ statC. statT≠ClassT statC ∧ declC=Object)) ∧
statDeclT = ClassT (declclass dm))"
proof -
assume invC_prop: "G⊢invmode sm e→invC≼statT"
and wf: "wf_prog G"
and wt_e: "⦇prg=G,cls=C,lcl=L⦈⊢e∷-RefT statT"
and sm: "(statDeclT,sm) ∈ mheads G C statT sig"
and invC: "invC = invocation_class (invmode sm e) s a' statT"
and declC: "declC =
invocation_declclass G (invmode sm e) s a' statT sig"
from wt_e wf have type_statT: "is_type G (RefT statT)"
by (auto dest: ty_expr_is_type)
from sm have not_Null: "statT ≠ NullT" by auto
from type_statT
have wf_C: "(∀ statC. statT = ClassT statC ⟶ is_class G statC)"
by (auto)
from type_statT wt_e
have wf_I: "(∀I. statT = IfaceT I ⟶ is_iface G I ∧
invmode sm e ≠ SuperM)"
by (auto dest: invocationTypeExpr_noClassD)
from wt_e
have wf_A: "(∀ T. statT = ArrayT T ⟶ invmode sm e ≠ SuperM)"
by (auto dest: invocationTypeExpr_noClassD)
show ?thesis
proof (cases "invmode sm e = IntVir")
case True
with invC_prop not_Null
have invC_prop': " is_class G invC ∧
(if (∃T. statT=ArrayT T) then invC=Object
else G⊢Class invC≼RefT statT)"
by (auto simp add: DynT_prop_def)
from True
have "¬ is_static sm"
by (simp add: invmode_IntVir_eq member_is_static_simp)
with invC_prop' not_Null
have "G,statT ⊢ invC valid_lookup_cls_for (is_static sm)"
by (cases statT) auto
with sm wf type_statT obtain dm where
dm: "dynlookup G statT invC sig = Some dm" and
resT_dm: "G⊢resTy (mthd dm)≼resTy sm" and
static: "is_static dm = is_static sm"
by - (drule dynamic_mheadsD,force+)
with declC invC not_Null
have declC': "declC = (declclass dm)"
by (auto simp add: invocation_declclass_def)
with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm
have dm': "methd G declC sig = Some dm"
by - (drule invocation_methd,auto)
from wf dm invC_prop' declC' type_statT
have declC_prop: "G⊢invC ≼⇩C declC ∧ is_class G declC"
by (auto dest: dynlookup_declC)
from wf dm' declC_prop declC'
have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
by (auto dest: methd_wf_mdecl)
from invC_prop'
have statC_prop: "(∀ statC. statT=ClassT statC ⟶ G⊢invC ≼⇩C statC)"
by auto
from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
dm
show ?thesis by auto
next
case False
with type_statT wf invC not_Null wf_I wf_A
have invC_prop': "is_class G invC ∧
((∃ statC. statT=ClassT statC ∧ invC=statC) ∨
(∀ statC. statT≠ClassT statC ∧ invC=Object))"
by (case_tac "statT") (auto simp add: invocation_class_def
split: inv_mode.splits)
with not_Null wf
have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
dynimethd_def)
from sm wf wt_e not_Null False invC_prop' obtain "dm" where
dm: "methd G invC sig = Some dm" and
eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)" and
eq_mheads:"sm=mhead (mthd dm) "
by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
then have static: "is_static dm = is_static sm" by - (auto)
with declC invC dynlookup_static dm
have declC': "declC = (declclass dm)"
by (auto simp add: invocation_declclass_def)
from invC_prop' wf declC' dm
have dm': "methd G declC sig = Some dm"
by (auto intro: methd_declclass)
from dynlookup_static dm
have dm'': "dynlookup G statT invC sig = Some dm"
by simp
from wf dm invC_prop' declC' type_statT
have declC_prop: "G⊢invC ≼⇩C declC ∧ is_class G declC"
by (auto dest: methd_declC )
then have declC_prop1: "invC=Object ⟶ declC=Object" by auto
from wf dm' declC_prop declC'
have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
by (auto dest: methd_wf_mdecl)
from invC_prop' declC_prop declC_prop1
have statC_prop: "( (∃ statC. statT=ClassT statC ∧ G⊢statC≼⇩C declC)
∨ (∀ statC. statT≠ClassT statC ∧ declC=Object))"
by auto
from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC'
eq_declC_sm_dm eq_mheads static
show ?thesis by auto
qed
qed
corollary DynT_mheadsE [consumes 7]:
assumes invC_compatible: "G⊢mode→invC≼statT"
and wf: "wf_prog G"
and wt_e: "⦇prg=G,cls=C,lcl=L⦈⊢e∷-RefT statT"
and mheads: "(statDeclT,sm) ∈ mheads G C statT sig"
and mode: "mode=invmode sm e"
and invC: "invC = invocation_class mode s a' statT"
and declC: "declC =invocation_declclass G mode s a' statT sig"
and dm: "⋀ dm. ⟦methd G declC sig = Some dm;
dynlookup G statT invC sig = Some dm;
G⊢resTy (mthd dm)≼resTy sm;
wf_mdecl G declC (sig, mthd dm);
declC = declclass dm;
is_static dm = is_static sm;
is_class G invC; is_class G declC; G⊢invC≼⇩C declC;
(if invmode sm e = IntVir
then (∀ statC. statT=ClassT statC ⟶ G⊢invC ≼⇩C statC)
else ( (∃ statC. statT=ClassT statC ∧ G⊢statC≼⇩C declC)
∨ (∀ statC. statT≠ClassT statC ∧ declC=Object)) ∧
statDeclT = ClassT (declclass dm))⟧ ⟹ P"
shows "P"
proof -
from invC_compatible mode have "G⊢invmode sm e→invC≼statT" by simp
moreover note wf wt_e mheads
moreover from invC mode
have "invC = invocation_class (invmode sm e) s a' statT" by simp
moreover from declC mode
have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
ultimately show ?thesis
by (rule DynT_mheadsD [THEN exE,rule_format])
(elim conjE,rule dm)
qed
lemma DynT_conf: "⟦G⊢invocation_class mode s a' statT ≼⇩C declC; wf_prog G;
isrtype G (statT);
G,s⊢a'∷≼RefT statT; mode = IntVir ⟶ a' ≠ Null;
mode ≠ IntVir ⟶ (∃ statC. statT=ClassT statC ∧ G⊢statC≼⇩C declC)
∨ (∀ statC. statT≠ClassT statC ∧ declC=Object)⟧
⟹G,s⊢a'∷≼ Class declC"
apply (case_tac "mode = IntVir")
apply (drule conf_RefTD)
apply (force intro!: conf_AddrI
simp add: obj_class_def split: obj_tag.split_asm)
apply clarsimp
apply safe
apply (erule (1) widen.subcls [THEN conf_widen])
apply (erule wf_ws_prog)
apply (frule widen_Object) apply (erule wf_ws_prog)
apply (erule (1) conf_widen) apply (erule wf_ws_prog)
done
lemma Ass_lemma:
"⟦ G⊢Norm s0 ─var=≻(w, f)→ Norm s1; G⊢Norm s1 ─e-≻v→ Norm s2;
G,s2⊢v∷≼eT;s1≤|s2 ⟶ assign f v (Norm s2)∷≼(G, L)⟧
⟹ assign f v (Norm s2)∷≼(G, L) ∧
(normal (assign f v (Norm s2)) ⟶ G,store (assign f v (Norm s2))⊢v∷≼eT)"
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: "⟦G⊢tn≼⇩C SXcpt Throwable; wf_prog G; (x1,s1)∷≼(G, L);
x1 = None ⟶ G,s1⊢a'∷≼ Class tn⟧ ⟹ (throw a' x1, s1)∷≼(G, L)"
apply (auto split: split_abrupt_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: "⟦G⊢obj_ty (the (globs s1' (Heap a)))≼ Class tn;
(Some (Xcpt (Loc a)), s1')∷≼(G, L); wf_prog G⟧
⟹ Norm (lupd(vn↦Addr a) s1')∷≼(G, L(vn↦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:
"⟦G⊢Norm s1 ─c2→ (x2,s2); wf_prog G; (Some a, s1)∷≼(G, L); (x2,s2)∷≼(G, L);
dom (locals s1) ⊆ dom (locals s2)⟧
⟹ (abrupt_if True (Some a) x2, s2)∷≼(G, L)"
apply (auto elim: eval_gext' conforms_xgext split: split_abrupt_if)
done
lemma FVar_lemma1:
"⟦table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ;
x2 = None ⟶ G,s2⊢a∷≼ Class statC; wf_prog G; G⊢statC≼⇩C statDeclC;
statDeclC ≠ Object;
class G statDeclC = Some y; (x2,s2)∷≼(G, L); s1≤|s2;
inited statDeclC (globs s1);
(if static f then id else np a) x2 = None⟧
⟹
∃obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a))
= Some obj ∧
var_tys G (tag obj) (if static f then Inr statDeclC else Inl(the_Addr a))
(Inl(fn,statDeclC)) = Some (type f)"
apply (drule initedD)
apply (frule subcls_is_class2, simp (no_asm_simp))
apply (case_tac "static f")
apply clarsimp
apply (drule (1) rev_gext_objD, clarsimp)
apply (frule fields_declC, 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: obj_tag.split)
apply (rule fields_table_SomeI)
apply (auto elim!: fields_mono subcls_is_class2)
done
lemma FVar_lemma2: "error_free state
⟹ error_free
(assign
(λv. supd
(upd_gobj
(if static field then Inr statDeclC
else Inl (the_Addr a))
(Inl (fn, statDeclC)) v))
w state)"
proof -
assume error_free: "error_free state"
obtain a s where "state=(a,s)"
by (cases state)
with error_free
show ?thesis
by (cases a) auto
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
setup ‹map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")›
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›
lemma FVar_lemma:
"⟦((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2);
G⊢statC≼⇩C statDeclC;
table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field;
wf_prog G;
x2 = None ⟶ G,s2⊢a∷≼Class statC;
statDeclC ≠ Object; class G statDeclC = Some y;
(x2, s2)∷≼(G, L); s1≤|s2; inited statDeclC (globs s1)⟧ ⟹
G,s2'⊢v∷≼type field ∧ s2'≤|f≼type field∷≼(G, L)"
apply (unfold assign_conforms_def)
apply (drule sym)
apply (clarsimp simp add: fvar_def2)
apply (drule (9) FVar_lemma1)
apply (clarsimp)
apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (drule (1) rev_gext_objD)
apply (force elim!: conforms_upd_gobj)
apply (blast intro: FVar_lemma2)
done
declare split_paired_All [simp] split_paired_Ex [simp]
declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup ‹map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))›
setup ‹map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))›
lemma AVar_lemma1: "⟦globs s (Inl a) = Some obj;tag obj=Arr ty i;
the_Intg i' in_bounds i; wf_prog G; G⊢ty.[]≼Tb.[]; Norm s∷≼(G, L)
⟧ ⟹ G,s⊢the ((values obj) (Inr (the_Intg i')))∷≼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 obj_split: "∃ t vs. obj = ⦇tag=t,values=vs⦈"
by (cases obj) auto
lemma AVar_lemma2: "error_free state
⟹ error_free
(assign
(λv (x, s').
((raise_if (¬ G,s'⊢v fits T) ArrStore) x,
upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
w state)"
proof -
assume error_free: "error_free state"
obtain a s where "state=(a,s)"
by (cases state)
with error_free
show ?thesis
by (cases a) auto
qed
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⊢a∷≼Ta.[];
(x2, s2)∷≼(G, L); s1≤|s2⟧ ⟹ G,s2'⊢v∷≼Ta ∧ s2'≤|f≼Ta∷≼(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 (subgoal_tac "∃ t vs. obj = ⦇tag=t,values=vs⦈")
defer
apply (rule obj_split)
apply clarify
apply (frule obj_ty_widenD)
apply (auto dest!: widen_Class)
apply (force dest: AVar_lemma1)
apply (force elim!: fits_Array dest: gext_objD
intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
done
subsubsection "Call"
lemma conforms_init_lvars_lemma: "⟦wf_prog G;
wf_mhead G P sig mh;
list_all2 (conf G s) pvs pTsa; G⊢pTsa[≼](parTs sig)⟧ ⟹
G,s⊢Map.empty (pars mh[↦]pvs)
[∼∷≼](table_of lvars)(pars mh[↦]parTs sig)"
apply (unfold wf_mhead_def)
apply clarify
apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
apply (drule wf_ws_prog)
apply (erule (2) conf_list_widen)
done
lemma lconf_map_lname [simp]:
"G,s⊢(case_lname l1 l2)[∷≼](case_lname L1 L2)
=
(G,s⊢l1[∷≼]L1 ∧ G,s⊢(λx::unit . l2)[∷≼](λx::unit. L2))"
apply (unfold lconf_def)
apply (auto split: lname.splits)
done
lemma wlconf_map_lname [simp]:
"G,s⊢(case_lname l1 l2)[∼∷≼](case_lname L1 L2)
=
(G,s⊢l1[∼∷≼]L1 ∧ G,s⊢(λx::unit . l2)[∼∷≼](λx::unit. L2))"
apply (unfold wlconf_def)
apply (auto split: lname.splits)
done
lemma lconf_map_ename [simp]:
"G,s⊢(case_ename l1 l2)[∷≼](case_ename L1 L2)
=
(G,s⊢l1[∷≼]L1 ∧ G,s⊢(λx::unit. l2)[∷≼](λx::unit. L2))"
apply (unfold lconf_def)
apply (auto split: ename.splits)
done
lemma wlconf_map_ename [simp]:
"G,s⊢(case_ename l1 l2)[∼∷≼](case_ename L1 L2)
=
(G,s⊢l1[∼∷≼]L1 ∧ G,s⊢(λx::unit. l2)[∼∷≼](λx::unit. L2))"
apply (unfold wlconf_def)
apply (auto split: ename.splits)
done
lemma defval_conf1 [rule_format (no_asm), elim]:
"is_type G T ⟶ (∃v∈Some (default_val T): G,s⊢v∷≼T)"
apply (unfold conf_def)
apply (induct "T")
apply (auto intro: prim_ty.induct)
done
lemma np_no_jump: "x≠Some (Jump j) ⟹ (np a') x ≠ Some (Jump j)"
by (auto simp add: abrupt_if_def)
declare split_paired_All [simp del] split_paired_Ex [simp del]
declare if_split [split del] if_split_asm [split del]
option.split [split del] option.split_asm [split del]
setup ‹map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")›
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›
lemma conforms_init_lvars:
"⟦wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;
list_all2 (conf G s) pvs pTsa; G⊢pTsa[≼](parTs sig);
(x, s)∷≼(G, L);
methd G declC sig = Some dm;
isrtype G statT;
G⊢invC≼⇩C declC;
G,s⊢a'∷≼RefT statT;
invmode (mhd sm) e = IntVir ⟶ a' ≠ Null;
invmode (mhd sm) e ≠ IntVir ⟶
(∃ statC. statT=ClassT statC ∧ G⊢statC≼⇩C declC)
∨ (∀ statC. statT≠ClassT statC ∧ declC=Object);
invC = invocation_class (invmode (mhd sm) e) s a' statT;
declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
x≠Some (Jump Ret)
⟧ ⟹
init_lvars G declC sig (invmode (mhd sm) e) a'
pvs (x,s)∷≼(G,λ k.
(case k of
EName e ⇒ (case e of
VNam v
⇒ ((table_of (lcls (mbody (mthd dm))))
(pars (mthd dm)[↦]parTs sig)) v
| Res ⇒ Some (resTy (mthd dm)))
| This ⇒ if (is_static (mthd sm))
then None else Some (Class declC)))"
apply (simp add: init_lvars_def2)
apply (rule conforms_set_locals)
apply (simp (no_asm_simp) split: if_split)
apply (drule (4) DynT_conf)
apply clarsimp
apply (drule (3) conforms_init_lvars_lemma
[where ?lvars="(lcls (mbody (mthd dm)))"])
apply (case_tac "dm",simp)
apply (rule conjI)
apply (unfold wlconf_def, clarify)
apply (clarsimp simp add: wf_mhead_def is_acc_type_def)
apply (case_tac "is_static sm")
apply simp
apply simp
apply simp
apply (case_tac "is_static sm")
apply simp
apply (simp add: np_no_jump)
done
declare split_paired_All [simp] split_paired_Ex [simp]
declare if_split [split] if_split_asm [split]
option.split [split] option.split_asm [split]
setup ‹map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))›
setup ‹map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))›
subsection "accessibility"
theorem dynamic_field_access_ok:
assumes wf: "wf_prog G" and
not_Null: "¬ stat ⟶ a≠Null" and
conform_a: "G,(store s)⊢a∷≼ Class statC" and
conform_s: "s∷≼(G, L)" and
normal_s: "normal s" and
wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-Class statC" and
f: "accfield G accC statC fn = Some f" and
dynC: "if stat then dynC=declclass f
else dynC=obj_class (lookup_obj (store s) a)" and
stat: "if stat then (is_static f) else (¬ is_static f)"
shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)∧
G⊢Field fn f in dynC dyn_accessible_from accC"
proof (cases "stat")
case True
with stat have static: "(is_static f)" by simp
from True dynC
have dynC': "dynC=declclass f" by simp
with f
have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
moreover
from wt_e wf have "is_class G statC"
by (auto dest!: ty_expr_is_type)
moreover note wf dynC'
ultimately have
"table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
by (auto dest: fields_declC)
with dynC' f static wf
show ?thesis
by (auto dest: static_to_dynamic_accessible_from_static
dest!: accfield_accessibleD )
next
case False
with wf conform_a not_Null conform_s dynC
obtain subclseq: "G⊢dynC ≼⇩C statC" and
"is_class G dynC"
by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
dest: obj_ty_obj_class1
simp add: obj_ty_obj_class )
with wf f
have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
by (auto simp add: accfield_def Let_def
dest: fields_mono
dest!: table_of_remap_SomeD)
moreover
from f subclseq
have "G⊢Field fn f in dynC dyn_accessible_from accC"
by (auto intro!: static_to_dynamic_accessible_from wf
dest: accfield_accessibleD)
ultimately show ?thesis
by blast
qed
lemma error_free_field_access:
assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-Class statC" and
eval_init: "G⊢Norm s0 ─Init statDeclC→ s1" and
eval_e: "G⊢s1 ─e-≻a→ s2" and
conf_s2: "s2∷≼(G, L)" and
conf_a: "normal s2 ⟹ G, store s2⊢a∷≼Class statC" and
fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
wf: "wf_prog G"
shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
proof -
from fvar
have store_s2': "store s2'=store s2"
by (cases s2) (simp add: fvar_def2)
with fvar conf_s2
have conf_s2': "s2'∷≼(G, L)"
by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
from eval_init
have initd_statDeclC_s1: "initd statDeclC s1"
by (rule init_yields_initd)
with eval_e store_s2'
have initd_statDeclC_s2': "initd statDeclC s2'"
by (auto dest: eval_gext intro: inited_gext)
show ?thesis
proof (cases "normal s2'")
case False
then show ?thesis
by (auto simp add: check_field_access_def Let_def)
next
case True
with fvar store_s2'
have not_Null: "¬ (is_static f) ⟶ a≠Null"
by (cases s2) (auto simp add: fvar_def2)
from True fvar store_s2'
have "normal s2"
by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
with conf_a store_s2'
have conf_a': "G,store s2'⊢a∷≼Class statC"
by simp
from conf_a' conf_s2' True initd_statDeclC_s2'
dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2'
True wt_e accfield ]
show ?thesis
by (cases "is_static f")
(auto dest!: initedD
simp add: check_field_access_def Let_def)
qed
qed
lemma call_access_ok:
assumes invC_prop: "G⊢invmode statM e→invC≼statT"
and wf: "wf_prog G"
and wt_e: "⦇prg=G,cls=C,lcl=L⦈⊢e∷-RefT statT"
and statM: "(statDeclT,statM) ∈ mheads G accC statT sig"
and invC: "invC = invocation_class (invmode statM e) s a statT"
shows "∃ dynM. dynlookup G statT invC sig = Some dynM ∧
G⊢Methd sig dynM in invC dyn_accessible_from accC"
proof -
from wt_e wf have type_statT: "is_type G (RefT statT)"
by (auto dest: ty_expr_is_type)
from statM have not_Null: "statT ≠ NullT" by auto
from type_statT wt_e
have wf_I: "(∀I. statT = IfaceT I ⟶ is_iface G I ∧
invmode statM e ≠ SuperM)"
by (auto dest: invocationTypeExpr_noClassD)
from wt_e
have wf_A: "(∀ T. statT = ArrayT T ⟶ invmode statM e ≠ SuperM)"
by (auto dest: invocationTypeExpr_noClassD)
show ?thesis
proof (cases "invmode statM e = IntVir")
case True
with invC_prop not_Null
have invC_prop': "is_class G invC ∧
(if (∃T. statT=ArrayT T) then invC=Object
else G⊢Class invC≼RefT statT)"
by (auto simp add: DynT_prop_def)
with True not_Null
have "G,statT ⊢ invC valid_lookup_cls_for is_static statM"
by (cases statT) (auto simp add: invmode_def)
with statM type_statT wf
show ?thesis
by - (rule dynlookup_access,auto)
next
case False
with type_statT wf invC not_Null wf_I wf_A
have invC_prop': " is_class G invC ∧
((∃ statC. statT=ClassT statC ∧ invC=statC) ∨
(∀ statC. statT≠ClassT statC ∧ invC=Object)) "
by (case_tac "statT") (auto simp add: invocation_class_def
split: inv_mode.splits)
with not_Null wf
have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
dynimethd_def)
from statM wf wt_e not_Null False invC_prop' obtain dynM where
"accmethd G accC invC sig = Some dynM"
by (auto dest!: static_mheadsD)
from invC_prop' False not_Null wf_I
have "G,statT ⊢ invC valid_lookup_cls_for is_static statM"
by (cases statT) (auto simp add: invmode_def)
with statM type_statT wf
show ?thesis
by - (rule dynlookup_access,auto)
qed
qed
lemma error_free_call_access:
assumes
eval_args: "G⊢s1 ─args≐≻vs→ s2" and
wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-(RefT statT)" and
statM: "max_spec G accC statT ⦇name = mn, parTs = pTs⦈
= {((statDeclT, statM), pTs')}" and
conf_s2: "s2∷≼(G, L)" and
conf_a: "normal s1 ⟹ G, store s1⊢a∷≼RefT statT" and
invProp: "normal s3 ⟹
G⊢invmode statM e→invC≼statT" and
s3: "s3=init_lvars G invDeclC ⦇name = mn, parTs = pTs'⦈
(invmode statM e) a vs s2" and
invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2)
a statT ⦇name = mn, parTs = pTs'⦈" and
wf: "wf_prog G"
shows "check_method_access G accC statT (invmode statM e) ⦇name=mn,parTs=pTs'⦈ a s3
= s3"
proof (cases "normal s2")
case False
with s3
have "abrupt s3 = abrupt s2"
by (auto simp add: init_lvars_def2)
with False
show ?thesis
by (auto simp add: check_method_access_def Let_def)
next
case True
note normal_s2 = True
with eval_args
have normal_s1: "normal s1"
by (cases "normal s1") auto
with conf_a eval_args
have conf_a_s2: "G, store s2⊢a∷≼RefT statT"
by (auto dest: eval_gext intro: conf_gext)
show ?thesis
proof (cases "a=Null ⟶ (is_static statM)")
case False
then obtain "¬ is_static statM" "a=Null"
by blast
with normal_s2 s3
have "abrupt s3 = Some (Xcpt (Std NullPointer))"
by (auto simp add: init_lvars_def2)
then show ?thesis
by (auto simp add: check_method_access_def Let_def)
next
case True
from statM
obtain
statM': "(statDeclT,statM)∈mheads G accC statT ⦇name=mn,parTs=pTs'⦈"
by (blast dest: max_spec2mheads)
from True normal_s2 s3
have "normal s3"
by (auto simp add: init_lvars_def2)
then have "G⊢invmode statM e→invC≼statT"
by (rule invProp)
with wt_e statM' wf invC
obtain dynM where
dynM: "dynlookup G statT invC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and
acc_dynM: "G ⊢Methd ⦇name=mn,parTs=pTs'⦈ dynM
in invC dyn_accessible_from accC"
by (force dest!: call_access_ok)
moreover
from s3 invC
have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
by (cases s2,cases "invmode statM e")
(simp add: init_lvars_def2 del: invmode_Static_eq)+
ultimately
show ?thesis
by (auto simp add: check_method_access_def Let_def)
qed
qed
lemma map_upds_eq_length_append_simp:
"⋀ tab qs. length ps = length qs ⟹ tab(ps[↦]qs@zs) = tab(ps[↦]qs)"
proof (induct ps)
case Nil thus ?case by simp
next
case (Cons p ps tab qs)
from ‹length (p#ps) = length qs›
obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length have "(tab(p↦q))(ps[↦]qs'@zs)=(tab(p↦q))(ps[↦]qs')"
by (rule Cons.hyps)
with qs show ?case
by simp
qed
lemma map_upds_upd_eq_length_simp:
"⋀ tab qs x y. length ps = length qs
⟹ tab(ps[↦]qs, x↦y) = tab(ps@[x][↦]qs@[y])"
proof (induct "ps")
case Nil thus ?case by simp
next
case (Cons p ps tab qs x y)
from ‹length (p#ps) = length qs›
obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
have "(tab(p↦q))(ps[↦]qs', x↦y) = (tab(p↦q))(ps@[x][↦]qs'@[y])"
by (rule Cons.hyps)
with qs show ?case
by simp
qed
lemma map_upd_cong: "tab=tab'⟹ tab(x↦y) = tab'(x↦y)"
by simp
lemma map_upd_cong_ext: "tab z=tab' z⟹ (tab(x↦y)) z = (tab'(x↦y)) z"
by (simp add: fun_upd_def)
lemma map_upds_cong: "tab=tab'⟹ tab(xs[↦]ys) = tab'(xs[↦]ys)"
by (cases xs) simp+
lemma map_upds_cong_ext:
"⋀ tab tab' ys. tab z=tab' z ⟹ (tab(xs[↦]ys)) z = (tab'(xs[↦]ys)) z"
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs tab tab' ys)
note Hyps = this
show ?case
proof (cases ys)
case Nil
with Hyps
show ?thesis by simp
next
case (Cons y ys')
have "(tab(x↦y, xs[↦]ys')) z = (tab'(x↦y, xs[↦]ys')) z"
by (iprover intro: Hyps map_upd_cong_ext)
with Cons show ?thesis
by simp
qed
qed
lemma map_upd_override: "(tab(x↦y)) x = (tab'(x↦y)) x"
by simp
lemma map_upds_eq_length_suffix: "⋀ tab qs.
length ps = length qs ⟹ tab(ps@xs[↦]qs) = tab(ps[↦]qs, xs[↦][])"
proof (induct ps)
case Nil thus ?case by simp
next
case (Cons p ps tab qs)
then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
have "tab(p↦q, ps @ xs[↦]qs') = tab(p↦q, ps[↦]qs', xs[↦][])"
by (rule Cons.hyps)
with qs show ?case
by simp
qed
lemma map_upds_upds_eq_length_prefix_simp:
"⋀ tab qs. length ps = length qs
⟹ tab(ps[↦]qs, xs[↦]ys) = tab(ps@xs[↦]qs@ys)"
proof (induct ps)
case Nil thus ?case by simp
next
case (Cons p ps tab qs)
then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
by (cases qs) auto
from eq_length
have "tab(p↦q, ps[↦]qs', xs[↦]ys) = tab(p↦q, ps @ xs[↦](qs' @ ys))"
by (rule Cons.hyps)
with qs
show ?case by simp
qed
lemma map_upd_cut_irrelevant:
"⟦(tab(x↦y)) vn = Some el; (tab'(x↦y)) vn = None⟧
⟹ tab vn = Some el"
by (cases "tab' vn = None") (simp add: fun_upd_def)+
lemma map_upd_Some_expand:
"⟦tab vn = Some z⟧
⟹ ∃ z. (tab(x↦y)) vn = Some z"
by (simp add: fun_upd_def)
lemma map_upds_Some_expand:
"⋀ tab ys z. ⟦tab vn = Some z⟧
⟹ ∃ z. (tab(xs[↦]ys)) vn = Some z"
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs tab ys z)
note z = ‹tab vn = Some z›
show ?case
proof (cases ys)
case Nil
with z show ?thesis by simp
next
case (Cons y ys')
note ys = ‹ys = y#ys'›
from z obtain z' where "(tab(x↦y)) vn = Some z'"
by (rule map_upd_Some_expand [of tab,elim_format]) blast
hence "∃z. ((tab(x↦y))(xs[↦]ys')) vn = Some z"
by (rule Cons.hyps)
with ys show ?thesis
by simp
qed
qed
lemma map_upd_Some_swap:
"(tab(r↦w, u↦v)) vn = Some z ⟹ ∃ z. (tab(u↦v, r↦w)) vn = Some z"
by (simp add: fun_upd_def)
lemma map_upd_None_swap:
"(tab(r↦w, u↦v)) vn = None ⟹ (tab(u↦v, r↦w)) vn = None"
by (simp add: fun_upd_def)
lemma map_eq_upd_eq: "tab vn = tab' vn ⟹ (tab(x↦y)) vn = (tab'(x↦y)) vn"
by (simp add: fun_upd_def)
lemma map_upd_in_expansion_map_swap:
"⟦(tab(x↦y)) vn = Some z;tab vn ≠ Some z⟧
⟹ (tab'(x↦y)) vn = Some z"
by (simp add: fun_upd_def)
lemma map_upds_in_expansion_map_swap:
"⋀tab tab' ys z. ⟦(tab(xs[↦]ys)) vn = Some z;tab vn ≠ Some z⟧
⟹ (tab'(xs[↦]ys)) vn = Some z"
proof (induct xs)
case Nil thus ?case by simp
next
case (Cons x xs tab tab' ys z)
note some = ‹(tab(x # xs[↦]ys)) vn = Some z›
note tab_not_z = ‹tab vn ≠ Some z›
show ?case
proof (cases ys)
case Nil with some tab_not_z show ?thesis by simp
next
case (Cons y tl)
note ys = ‹ys = y#tl›
show ?thesis
proof (cases "(tab(x↦y)) vn ≠ Some z")
case True
with some ys have "(tab'(x↦y, xs[↦]tl)) vn = Some z"
by (fastforce intro: Cons.hyps)
with ys show ?thesis
by simp
next
case False
hence tabx_z: "(tab(x↦y)) vn = Some z" by blast
moreover
from tabx_z tab_not_z
have "(tab'(x↦y)) vn = Some z"
by (rule map_upd_in_expansion_map_swap)
ultimately
have "(tab(x↦y)) vn =(tab'(x↦y)) vn"
by simp
hence "(tab(x↦y, xs[↦]tl)) vn = (tab'(x↦y, xs[↦]tl)) vn"
by (rule map_upds_cong_ext)
with some ys
show ?thesis
by simp
qed
qed
qed
lemma map_upds_Some_swap:
assumes r_u: "(tab(r↦w, u↦v, xs[↦]ys)) vn = Some z"
shows "∃ z. (tab(u↦v, r↦w, xs[↦]ys)) vn = Some z"
proof (cases "(tab(r↦w, u↦v)) vn = Some z")
case True
then obtain z' where "(tab(u↦v, r↦w)) vn = Some z'"
by (rule map_upd_Some_swap [elim_format]) blast
thus "∃ z. (tab(u↦v, r↦w, xs[↦]ys)) vn = Some z"
by (rule map_upds_Some_expand)
next
case False
with r_u
have "(tab(u↦v, r↦w, xs[↦]ys)) vn = Some z"
by (rule map_upds_in_expansion_map_swap)
thus ?thesis
by simp
qed
lemma map_upds_Some_insert:
assumes z: "(tab(xs[↦]ys)) vn = Some z"
shows "∃ z. (tab(u↦v, xs[↦]ys)) vn = Some z"
proof (cases "∃ z. tab vn = Some z")
case True
then obtain z' where "tab vn = Some z'" by blast
then obtain z'' where "(tab(u↦v)) vn = Some z''"
by (rule map_upd_Some_expand [elim_format]) blast
thus ?thesis
by (rule map_upds_Some_expand)
next
case False
hence "tab vn ≠ Some z" by simp
with z
have "(tab(u↦v, xs[↦]ys)) vn = Some z"
by (rule map_upds_in_expansion_map_swap)
thus ?thesis ..
qed
lemma map_upds_None_cut:
assumes expand_None: "(tab(xs[↦]ys)) vn = None"
shows "tab vn = None"
proof (cases "tab vn = None")
case True thus ?thesis by simp
next
case False then obtain z where "tab vn = Some z" by blast
then obtain z' where "(tab(xs[↦]ys)) vn = Some z'"
by (rule map_upds_Some_expand [where ?tab="tab",elim_format]) blast
with expand_None show ?thesis
by simp
qed
lemma map_upds_cut_irrelevant:
"⋀ tab tab' ys. ⟦(tab(xs[↦]ys)) vn = Some el; (tab'(xs[↦]ys)) vn = None⟧
⟹ tab vn = Some el"
proof (induct "xs")
case Nil thus ?case by simp
next
case (Cons x xs tab tab' ys)
note tab_vn = ‹(tab(x # xs[↦]ys)) vn = Some el›
note tab'_vn = ‹(tab'(x # xs[↦]ys)) vn = None›
show ?case
proof (cases ys)
case Nil
with tab_vn show ?thesis by simp
next
case (Cons y tl)
note ys = ‹ys=y#tl›
with tab_vn tab'_vn
have "(tab(x↦y)) vn = Some el"
by - (rule Cons.hyps,auto)
moreover from tab'_vn ys
have "(tab'(x↦y, xs[↦]tl)) vn = None"
by simp
hence "(tab'(x↦y)) vn = None"
by (rule map_upds_None_cut)
ultimately show "tab vn = Some el"
by (rule map_upd_cut_irrelevant)
qed
qed
lemma dom_vname_split:
"dom (case_lname (case_ename (tab(x↦y, xs[↦]ys)) a) b)
= dom (case_lname (case_ename (tab(x↦y)) a) b) ∪
dom (case_lname (case_ename (tab(xs[↦]ys)) a) b)"
(is "?List x xs y ys = ?Hd x y ∪ ?Tl xs ys")
proof
show "?List x xs y ys ⊆ ?Hd x y ∪ ?Tl xs ys"
proof
fix el
assume el_in_list: "el ∈ ?List x xs y ys"
show "el ∈ ?Hd x y ∪ ?Tl xs ys"
proof (cases el)
case This
with el_in_list show ?thesis by (simp add: dom_def)
next
case (EName en)
show ?thesis
proof (cases en)
case Res
with EName el_in_list show ?thesis by (simp add: dom_def)
next
case (VNam vn)
with EName el_in_list show ?thesis
by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
qed
qed
qed
next
show "?Hd x y ∪ ?Tl xs ys ⊆ ?List x xs y ys"
proof (rule subsetI)
fix el
assume el_in_hd_tl: "el ∈ ?Hd x y ∪ ?Tl xs ys"
show "el ∈ ?List x xs y ys"
proof (cases el)
case This
with el_in_hd_tl show ?thesis by (simp add: dom_def)
next
case (EName en)
show ?thesis
proof (cases en)
case Res
with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
next
case (VNam vn)
with EName el_in_hd_tl show ?thesis
by (auto simp add: dom_def intro: map_upds_Some_expand
map_upds_Some_insert)
qed
qed
qed
qed
lemma dom_map_upd: "⋀ tab. dom (tab(x↦y)) = dom tab ∪ {x}"
by (auto simp add: dom_def fun_upd_def)
lemma dom_map_upds: "⋀ tab ys. length xs = length ys
⟹ dom (tab(xs[↦]ys)) = dom tab ∪ set xs"
proof (induct xs)
case Nil thus ?case by (simp add: dom_def)
next
case (Cons x xs tab ys)
note Hyp = Cons.hyps
note len = ‹length (x#xs)=length ys›
show ?case
proof (cases ys)
case Nil with len show ?thesis by simp
next
case (Cons y tl)
with len have "dom (tab(x↦y, xs[↦]tl)) = dom (tab(x↦y)) ∪ set xs"
by - (rule Hyp,simp)
moreover
have "dom (tab(x↦hd ys)) = dom tab ∪ {x}"
by (rule dom_map_upd)
ultimately
show ?thesis using Cons
by simp
qed
qed
lemma dom_case_ename_None_simp:
"dom (case_ename vname_tab None) = VNam ` (dom vname_tab)"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
lemma dom_case_ename_Some_simp:
"dom (case_ename vname_tab (Some a)) = VNam ` (dom vname_tab) ∪ {Res}"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
lemma dom_case_lname_None_simp:
"dom (case_lname ename_tab None) = EName ` (dom ename_tab)"
apply (auto simp add: dom_def image_def )
apply (case_tac "x")
apply auto
done
lemma dom_case_lname_Some_simp:
"dom (case_lname ename_tab (Some a)) = EName ` (dom ename_tab) ∪ {This}"
apply (auto simp add: dom_def image_def)
apply (case_tac "x")
apply auto
done
lemmas dom_lname_case_ename_simps =
dom_case_ename_None_simp dom_case_ename_Some_simp
dom_case_lname_None_simp dom_case_lname_Some_simp
lemma image_comp:
"f ` g ` A = (f ∘ g) ` A"
by (auto simp add: image_def)
lemma dom_locals_init_lvars:
assumes m: "m=(mthd (the (methd G C sig)))"
assumes len: "length (pars m) = length pvs"
shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))
= parameters m"
proof -
from m
have static_m': "is_static m = static m"
by simp
from len
have dom_vnames: "dom (Map.empty(pars m[↦]pvs))=set (pars m)"
by (simp add: dom_map_upds)
show ?thesis
proof (cases "static m")
case True
with static_m' dom_vnames m
show ?thesis
by (cases s) (simp add: init_lvars_def Let_def parameters_def
dom_lname_case_ename_simps image_comp)
next
case False
with static_m' dom_vnames m
show ?thesis
by (cases s) (simp add: init_lvars_def Let_def parameters_def
dom_lname_case_ename_simps image_comp)
qed
qed
lemma da_e2_BinOp:
assumes da: "⦇prg=G,cls=accC,lcl=L⦈
⊢dom (locals (store s0)) »⟨BinOp binop e1 e2⟩⇩e» A"
and wt_e1: "⦇prg=G,cls=accC,lcl=L⦈⊢e1∷-e1T"
and wt_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢e2∷-e2T"
and wt_binop: "wt_binop G binop e1T e2T"
and conf_s0: "s0∷≼(G,L)"
and normal_s1: "normal s1"
and eval_e1: "G⊢s0 ─e1-≻v1→ s1"
and conf_v1: "G,store s1⊢v1∷≼e1T"
and wf: "wf_prog G"
shows "∃ E2. ⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1))
»(if need_second_arg binop v1 then ⟨e2⟩⇩e else ⟨Skip⟩⇩s)» E2"
proof -
note inj_term_simps [simp]
from da obtain E1 where
da_e1: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ dom (locals (store s0)) »⟨e1⟩⇩e» E1"
by cases simp+
obtain E2 where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1))
»(if need_second_arg binop v1 then ⟨e2⟩⇩e else ⟨Skip⟩⇩s)» E2"
proof (cases "need_second_arg binop v1")
case False
obtain S where
daSkip: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s1)) »⟨Skip⟩⇩s» S"
by (auto intro: da_Skip [simplified] assigned.select_convs)
thus ?thesis
using that by (simp add: False)
next
case True
from eval_e1 have
s0_s1:"dom (locals (store s0)) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
{
assume condAnd: "binop=CondAnd"
have ?thesis
proof -
from da obtain E2' where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s0)) ∪ assigns_if True e1 »⟨e2⟩⇩e» E2'"
by cases (simp add: condAnd)+
moreover
have "dom (locals (store s0))
∪ assigns_if True e1 ⊆ dom (locals (store s1))"
proof -
from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
by simp
with normal_s1 conf_v1 obtain b where "v1=Bool b"
by (auto dest: conf_Boolean)
with True condAnd
have v1: "v1=Bool True"
by simp
from eval_e1 normal_s1
have "assigns_if True e1 ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx' [elim_format])
(insert wt_e1, simp_all add: e1T v1)
with s0_s1 show ?thesis by (rule Un_least)
qed
ultimately
show ?thesis
using that by (cases rule: da_weakenE) (simp add: True)
qed
}
moreover
{
assume condOr: "binop=CondOr"
have ?thesis
proof -
from da obtain E2' where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s0)) ∪ assigns_if False e1 »⟨e2⟩⇩e» E2'"
by cases (simp add: condOr)+
moreover
have "dom (locals (store s0))
∪ assigns_if False e1 ⊆ dom (locals (store s1))"
proof -
from condOr wt_binop have e1T: "e1T=PrimT Boolean"
by simp
with normal_s1 conf_v1 obtain b where "v1=Bool b"
by (auto dest: conf_Boolean)
with True condOr
have v1: "v1=Bool False"
by simp
from eval_e1 normal_s1
have "assigns_if False e1 ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx' [elim_format])
(insert wt_e1, simp_all add: e1T v1)
with s0_s1 show ?thesis by (rule Un_least)
qed
ultimately
show ?thesis
using that by (rule da_weakenE) (simp add: True)
qed
}
moreover
{
assume notAndOr: "binop≠CondAnd" "binop≠CondOr"
have ?thesis
proof -
from da notAndOr obtain E1' where
da_e1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s0)) »⟨e1⟩⇩e» E1'"
and da_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E1' »In1l e2» A"
by cases simp+
from eval_e1 wt_e1 da_e1 wf normal_s1
have "nrm E1' ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_e2 show ?thesis
using that by (rule da_weakenE) (simp add: True)
qed
}
ultimately show ?thesis
by (cases binop) auto
qed
thus ?thesis ..
qed
subsubsection "main proof of type safety"
lemma eval_type_sound:
assumes eval: "G⊢s0 ─t≻→ (v,s1)"
and wt: "⦇prg=G,cls=accC,lcl=L⦈⊢t∷T"
and da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»A"
and wf: "wf_prog G"
and conf_s0: "s0∷≼(G,L)"
shows "s1∷≼(G,L) ∧ (normal s1 ⟶ G,L,store s1⊢t≻v∷≼T) ∧
(error_free s0 = error_free s1)"
proof -
note inj_term_simps [simp]
let ?TypeSafeObj = "λ s0 s1 t v.
∀ L accC T A. s0∷≼(G,L) ⟶ ⦇prg=G,cls=accC,lcl=L⦈⊢t∷T
⟶ ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»A
⟶ s1∷≼(G,L) ∧ (normal s1 ⟶ G,L,store s1⊢t≻v∷≼T)
∧ (error_free s0 = error_free s1)"
from eval
have "⋀ L accC T A. ⟦s0∷≼(G,L);⦇prg=G,cls=accC,lcl=L⦈⊢t∷T;
⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»A⟧
⟹ s1∷≼(G,L) ∧ (normal s1 ⟶ G,L,store s1⊢t≻v∷≼T)
∧ (error_free s0 = error_free s1)"
(is "PROP ?TypeSafe s0 s1 t v"
is "⋀ L accC T A. ?Conform L s0 ⟹ ?WellTyped L accC T t
⟹ ?DefAss L accC s0 t A
⟹ ?Conform L s1 ∧ ?ValueTyped L T s1 t v ∧
?ErrorFree s0 s1")
proof (induct)
case (Abrupt xc s t L accC T A)
from ‹(Some xc, s)∷≼(G,L)›
show "(Some xc, s)∷≼(G,L) ∧
(normal (Some xc, s)
⟶ G,L,store (Some xc,s)⊢t≻undefined3 t∷≼T) ∧
(error_free (Some xc, s) = error_free (Some xc, s))"
by simp
next
case (Skip s L accC T A)
from ‹Norm s∷≼(G, L)› and
‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r Skip∷T›
show "Norm s∷≼(G, L) ∧
(normal (Norm s) ⟶ G,L,store (Norm s)⊢In1r Skip≻♢∷≼T) ∧
(error_free (Norm s) = error_free (Norm s))"
by simp
next
case (Expr s0 e v s1 L accC T A)
note ‹G⊢Norm s0 ─e-≻v→ s1›
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
moreover
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (Expr e)∷T›
then obtain eT
where "⦇prg = G, cls = accC, lcl = L⦈⊢In1l e∷eT"
by (rule wt_elim_cases) blast
moreover
from Expr.prems obtain E where
"⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store ((Norm s0)::state)))»In1l e»E"
by (elim da_elim_cases) simp
ultimately
obtain "s1∷≼(G, L)" and "error_free s1"
by (rule hyp [elim_format]) simp
with wt
show "s1∷≼(G, L) ∧
(normal s1 ⟶ G,L,store s1⊢In1r (Expr e)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s1)"
by (simp)
next
case (Lab s0 c s1 l L accC T A)
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1r c) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
moreover
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (l∙ c)∷T›
then have "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√"
by (rule wt_elim_cases) blast
moreover from Lab.prems obtain C where
"⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store ((Norm s0)::state)))»In1r c»C"
by (elim da_elim_cases) simp
ultimately
obtain conf_s1: "s1∷≼(G, L)" and
error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
from conf_s1 have "abupd (absorb l) s1∷≼(G, L)"
by (cases s1) (auto intro: conforms_absorb)
with wt error_free_s1
show "abupd (absorb l) s1∷≼(G, L) ∧
(normal (abupd (absorb l) s1)
⟶ G,L,store (abupd (absorb l) s1)⊢In1r (l∙ c)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free (abupd (absorb l) s1))"
by (simp)
next
case (Comp s0 c1 s1 c2 s2 L accC T A)
note eval_c1 = ‹G⊢Norm s0 ─c1→ s1›
note eval_c2 = ‹G⊢s1 ─c2→ s2›
note hyp_c1 = ‹PROP ?TypeSafe (Norm s0) s1 (In1r c1) ♢›
note hyp_c2 = ‹PROP ?TypeSafe s1 s2 (In1r c2) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (c1;; c2)∷T›
then obtain wt_c1: "⦇prg = G, cls = accC, lcl = L⦈⊢c1∷√" and
wt_c2: "⦇prg = G, cls = accC, lcl = L⦈⊢c2∷√"
by (rule wt_elim_cases) blast
from Comp.prems
obtain C1 C2
where da_c1: "⦇prg=G, cls=accC, lcl=L⦈⊢
dom (locals (store ((Norm s0)::state))) »In1r c1» C1" and
da_c2: "⦇prg=G, cls=accC, lcl=L⦈⊢ nrm C1 »In1r c2» C2"
by (elim da_elim_cases) simp
from conf_s0 wt_c1 da_c1
obtain conf_s1: "s1∷≼(G, L)" and
error_free_s1: "error_free s1"
by (rule hyp_c1 [elim_format]) simp
show "s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In1r (c1;; c2)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
proof (cases "normal s1")
case False
with eval_c2 have "s2=s1" by auto
with conf_s1 error_free_s1 False wt show ?thesis
by simp
next
case True
obtain C2' where
"⦇prg=G, cls=accC, lcl=L⦈⊢ dom (locals (store s1)) »In1r c2» C2'"
proof -
from eval_c1 wt_c1 da_c1 wf True
have "nrm C1 ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_c2 show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_c2
obtain "s2∷≼(G, L)" and "error_free s2"
by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
thus ?thesis
using wt by simp
qed
next
case (If s0 e b s1 c1 c2 s2 L accC T A)
note eval_e = ‹G⊢Norm s0 ─e-≻b→ s1›
note eval_then_else = ‹G⊢s1 ─(if the_Bool b then c1 else c2)→ s2›
note hyp_e = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)›
note hyp_then_else =
‹PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (If(e) c1 Else c2)∷T›
then obtain
wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-PrimT Boolean" and
wt_then_else: "⦇prg=G, cls=accC, lcl=L⦈⊢(if the_Bool b then c1 else c2)∷√"
by (rule wt_elim_cases) auto
from If.prems obtain E C where
da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store ((Norm s0)::state)))
»In1l e» E" and
da_then_else:
"⦇prg=G,cls=accC,lcl=L⦈⊢
(dom (locals (store ((Norm s0)::state))) ∪ assigns_if (the_Bool b) e)
»In1r (if the_Bool b then c1 else c2)» C"
by (elim da_elim_cases) (cases "the_Bool b",auto)
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_e [elim_format]) simp
show "s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In1r (If(e) c1 Else c2)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
proof (cases "normal s1")
case False
with eval_then_else have "s2=s1" by auto
with conf_s1 error_free_s1 False wt show ?thesis
by simp
next
case True
obtain C' where
"⦇prg=G,cls=accC,lcl=L⦈⊢
(dom (locals (store s1)))»In1r (if the_Bool b then c1 else c2)» C'"
proof -
from eval_e have
"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
moreover
from eval_e True wt_e
have "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx')
ultimately
have "dom (locals (store ((Norm s0)::state)))
∪ assigns_if (the_Bool b) e ⊆ dom (locals (store s1))"
by (rule Un_least)
with da_then_else show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_then_else
obtain "s2∷≼(G, L)" and "error_free s2"
by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
with wt show ?thesis
by simp
qed
next
case (Loop s0 e b s1 c s2 l s3 L accC T A)
note eval_e = ‹G⊢Norm s0 ─e-≻b→ s1›
note hyp_e = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (l∙ While(e) c)∷T›
then obtain wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-PrimT Boolean" and
wt_c: "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√"
by (rule wt_elim_cases) blast
note da = ‹⦇prg=G, cls=accC, lcl=L⦈
⊢ dom (locals(store ((Norm s0)::state))) »In1r (l∙ While(e) c)» A›
then
obtain E C where
da_e: "⦇prg=G, cls=accC, lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» E" and
da_c: "⦇prg=G, cls=accC, lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state)))
∪ assigns_if True e) »In1r c» C"
by (rule da_elim_cases) simp
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_e [elim_format]) simp
show "s3∷≼(G, L) ∧
(normal s3 ⟶ G,L,store s3⊢In1r (l∙ While(e) c)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s3)"
proof (cases "normal s1")
case True
note normal_s1 = this
show ?thesis
proof (cases "the_Bool b")
case True
with Loop.hyps obtain
eval_c: "G⊢s1 ─c→ s2" and
eval_while: "G⊢abupd (absorb (Cont l)) s2 ─l∙ While(e) c→ s3"
by simp
have "?TypeSafeObj s1 s2 (In1r c) ♢"
using Loop.hyps True by simp
note hyp_c = this [rule_format]
have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
s3 (In1r (l∙ While(e) c)) ♢"
using Loop.hyps True by simp
note hyp_w = this [rule_format]
from eval_e have
s0_s1: "dom (locals (store ((Norm s0)::state)))
⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
obtain C' where
"⦇prg=G, cls=accC, lcl=L⦈⊢(dom (locals (store s1)))»In1r c» C'"
proof -
note s0_s1
moreover
from eval_e normal_s1 wt_e
have "assigns_if True e ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
ultimately
have "dom (locals (store ((Norm s0)::state)))
∪ assigns_if True e ⊆ dom (locals (store s1))"
by (rule Un_least)
with da_c show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_c
obtain conf_s2: "s2∷≼(G, L)" and error_free_s2: "error_free s2"
by (rule hyp_c [elim_format]) (simp add: error_free_s1)
from error_free_s2
have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
by simp
from conf_s2 have "abupd (absorb (Cont l)) s2 ∷≼(G, L)"
by (cases s2) (auto intro: conforms_absorb)
moreover note wt
moreover
obtain A' where
"⦇prg=G,cls=accC,lcl=L⦈⊢
dom (locals(store (abupd (absorb (Cont l)) s2)))
»In1r (l∙ While(e) c)» A'"
proof -
note s0_s1
also from eval_c
have "dom (locals (store s1)) ⊆ dom (locals (store s2))"
by (rule dom_locals_eval_mono_elim)
also have "… ⊆ dom (locals (store (abupd (absorb (Cont l)) s2)))"
by simp
finally
have "dom (locals (store ((Norm s0)::state))) ⊆ …" .
with da show thesis
by (rule da_weakenE) (rule that)
qed
ultimately obtain "s3∷≼(G, L)" and "error_free s3"
by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
with wt show ?thesis
by simp
next
case False
with Loop.hyps have "s3=s1" by simp
with conf_s1 error_free_s1 wt
show ?thesis
by simp
qed
next
case False
have "s3=s1"
proof -
from False obtain abr where abr: "abrupt s1 = Some abr"
by (cases s1) auto
from eval_e _ wt_e have no_jmp: "⋀ j. abrupt s1 ≠ Some (Jump j)"
by (rule eval_expression_no_jump
[where ?Env="⦇prg=G,cls=accC,lcl=L⦈",simplified])
(simp_all add: wf)
show ?thesis
proof (cases "the_Bool b")
case True
with Loop.hyps obtain
eval_c: "G⊢s1 ─c→ s2" and
eval_while: "G⊢abupd (absorb (Cont l)) s2 ─l∙ While(e) c→ s3"
by simp
from eval_c abr have "s2=s1" by auto
moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
by (cases s1) (simp add: absorb_def)
ultimately show ?thesis
using eval_while abr
by auto
next
case False
with Loop.hyps show ?thesis by simp
qed
qed
with conf_s1 error_free_s1 wt
show ?thesis
by simp
qed
next
case (Jmp s j L accC T A)
note ‹Norm s∷≼(G, L)›
moreover
from Jmp.prems
have "j=Ret ⟶ Result ∈ dom (locals (store ((Norm s)::state)))"
by (elim da_elim_cases)
ultimately have "(Some (Jump j), s)∷≼(G, L)" by auto
then
show "(Some (Jump j), s)∷≼(G, L) ∧
(normal (Some (Jump j), s)
⟶ G,L,store (Some (Jump j), s)⊢In1r (Jmp j)≻♢∷≼T) ∧
(error_free (Norm s) = error_free (Some (Jump j), s))"
by simp
next
case (Throw s0 e a s1 L accC T A)
note ‹G⊢Norm s0 ─e-≻a→ s1›
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (Throw e)∷T›
then obtain tn
where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-Class tn" and
throwable: "G⊢tn≼⇩C SXcpt Throwable"
by (rule wt_elim_cases) (auto)
from Throw.prems obtain E where
da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» E"
by (elim da_elim_cases) simp
from conf_s0 wt_e da_e obtain
"s1∷≼(G, L)" and
"(normal s1 ⟶ G,store s1⊢a∷≼Class tn)" and
error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
with wf throwable
have "abupd (throw a) s1∷≼(G, L)"
by (cases s1) (auto dest: Throw_lemma)
with wt error_free_s1
show "abupd (throw a) s1∷≼(G, L) ∧
(normal (abupd (throw a) s1) ⟶
G,L,store (abupd (throw a) s1)⊢In1r (Throw e)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free (abupd (throw a) s1))"
by simp
next
case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A)
note eval_c1 = ‹G⊢Norm s0 ─c1→ s1›
note sx_alloc = ‹G⊢s1 ─sxalloc→ s2›
note hyp_c1 = ‹PROP ?TypeSafe (Norm s0) s1 (In1r c1) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg=G,cls=accC,lcl=L⦈⊢In1r (Try c1 Catch(catchC vn) c2)∷T›
then obtain
wt_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√" and
wt_c2: "⦇prg=G,cls=accC,lcl=L(VName vn↦Class catchC)⦈⊢c2∷√" and
fresh_vn: "L(VName vn)=None"
by (rule wt_elim_cases) simp
from Try.prems obtain C1 C2 where
da_c1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r c1» C1" and
da_c2:
"⦇prg=G,cls=accC,lcl=L(VName vn↦Class catchC)⦈
⊢ (dom (locals (store ((Norm s0)::state))) ∪ {VName vn}) »In1r c2» C2"
by (elim da_elim_cases) simp
from conf_s0 wt_c1 da_c1
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_c1 [elim_format]) simp
from conf_s1 sx_alloc wf
have conf_s2: "s2∷≼(G, L)"
by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits)
from sx_alloc error_free_s1
have error_free_s2: "error_free s2"
by (rule error_free_sxalloc)
show "s3∷≼(G, L) ∧
(normal s3 ⟶ G,L,store s3⊢In1r (Try c1 Catch(catchC vn) c2)≻♢∷≼T)∧
(error_free (Norm s0) = error_free s3)"
proof (cases "∃ x. abrupt s1 = Some (Xcpt x)")
case False
from sx_alloc wf
have eq_s2_s1: "s2=s1"
by (rule sxalloc_type_sound [elim_format])
(insert False, auto split: option.splits abrupt.splits )
with False
have "¬ G,s2⊢catch catchC"
by (simp add: catch_def)
with Try
have "s3=s2"
by simp
with wt conf_s1 error_free_s1 eq_s2_s1
show ?thesis
by simp
next
case True
note exception_s1 = this
show ?thesis
proof (cases "G,s2⊢catch catchC")
case False
with Try
have "s3=s2"
by simp
with wt conf_s2 error_free_s2
show ?thesis
by simp
next
case True
with Try have "G⊢new_xcpt_var vn s2 ─c2→ s3" by simp
from True Try.hyps
have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) ♢"
by simp
note hyp_c2 = this [rule_format]
from exception_s1 sx_alloc wf
obtain a
where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
with True
have "G⊢obj_ty (the (globs (store s2) (Heap a)))≼Class catchC"
by (cases s2) simp
with xcpt_s2 conf_s2 wf
have "new_xcpt_var vn s2 ∷≼(G, L(VName vn↦Class catchC))"
by (auto dest: Try_lemma)
moreover note wt_c2
moreover
obtain C2' where
"⦇prg=G,cls=accC,lcl=L(VName vn↦Class catchC)⦈
⊢ (dom (locals (store (new_xcpt_var vn s2)))) »In1r c2» C2'"
proof -
have "(dom (locals (store ((Norm s0)::state))) ∪ {VName vn})
⊆ dom (locals (store (new_xcpt_var vn s2)))"
proof -
from ‹G⊢Norm s0 ─c1→ s1›
have "dom (locals (store ((Norm s0)::state)))
⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
also
from sx_alloc
have "… ⊆ dom (locals (store s2))"
by (rule dom_locals_sxalloc_mono)
also
have "… ⊆ dom (locals (store (new_xcpt_var vn s2)))"
by (cases s2) (simp add: new_xcpt_var_def, blast)
also
have "{VName vn} ⊆ …"
by (cases s2) simp
ultimately show ?thesis
by (rule Un_least)
qed
with da_c2 show thesis
by (rule da_weakenE) (rule that)
qed
ultimately
obtain conf_s3: "s3∷≼(G, L(VName vn↦Class catchC))" and
error_free_s3: "error_free s3"
by (rule hyp_c2 [elim_format])
(cases s2, simp add: xcpt_s2 error_free_s2)
from conf_s3 fresh_vn
have "s3∷≼(G,L)"
by (blast intro: conforms_deallocL)
with wt error_free_s3
show ?thesis
by simp
qed
qed
next
case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A)
note eval_c1 = ‹G⊢Norm s0 ─c1→ (x1, s1)›
note eval_c2 = ‹G⊢Norm s1 ─c2→ s2›
note s3 = ‹s3 = (if ∃err. x1 = Some (Error err)
then (x1, s1)
else abupd (abrupt_if (x1 ≠ None) x1) s2)›
note hyp_c1 = ‹PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) ♢›
note hyp_c2 = ‹PROP ?TypeSafe (Norm s1) s2 (In1r c2) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (c1 Finally c2)∷T›
then obtain
wt_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√" and
wt_c2: "⦇prg=G,cls=accC,lcl=L⦈⊢c2∷√"
by (rule wt_elim_cases) blast
from Fin.prems obtain C1 C2 where
da_c1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r c1» C1" and
da_c2: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r c2» C2"
by (elim da_elim_cases) simp
from conf_s0 wt_c1 da_c1
obtain conf_s1: "(x1,s1)∷≼(G, L)" and error_free_s1: "error_free (x1,s1)"
by (rule hyp_c1 [elim_format]) simp
from conf_s1 have "Norm s1∷≼(G, L)"
by (rule conforms_NormI)
moreover note wt_c2
moreover obtain C2'
where "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s1)::state))) »In1r c2» C2'"
proof -
from eval_c1
have "dom (locals (store ((Norm s0)::state)))
⊆ dom (locals (store (x1,s1)))"
by (rule dom_locals_eval_mono_elim)
hence "dom (locals (store ((Norm s0)::state)))
⊆ dom (locals (store ((Norm s1)::state)))"
by simp
with da_c2 show thesis
by (rule da_weakenE) (rule that)
qed
ultimately
obtain conf_s2: "s2∷≼(G, L)" and error_free_s2: "error_free s2"
by (rule hyp_c2 [elim_format]) simp
from error_free_s1 s3
have s3': "s3=abupd (abrupt_if (x1 ≠ None) x1) s2"
by simp
show "s3∷≼(G, L) ∧
(normal s3 ⟶ G,L,store s3 ⊢In1r (c1 Finally c2)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s3)"
proof (cases x1)
case None with conf_s2 s3' wt error_free_s2
show ?thesis by auto
next
case (Some x)
from eval_c2 have
"dom (locals (store ((Norm s1)::state))) ⊆ dom (locals (store s2))"
by (rule dom_locals_eval_mono_elim)
with Some eval_c2 wf conf_s1 conf_s2
have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)∷≼(G, L)"
by (cases s2) (auto dest: Fin_lemma)
from Some error_free_s1
have "¬ (∃ err. x=Error err)"
by (simp add: error_free_def)
with error_free_s2
have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
by (cases s2) simp
with Some wt conf s3' show ?thesis
by (cases s2) auto
qed
next
case (Init C c s0 s3 s1 s2 L accC T A)
note cls = ‹the (class G C) = c›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1r (Init C)∷T›
with cls
have cls_C: "class G C = Some c"
by - (erule wt_elim_cases, auto)
show "s3∷≼(G, L) ∧ (normal s3 ⟶ G,L,store s3⊢In1r (Init C)≻♢∷≼T) ∧
(error_free (Norm s0) = error_free s3)"
proof (cases "inited C (globs s0)")
case True
with Init.hyps have "s3 = Norm s0"
by simp
with conf_s0 wt show ?thesis
by simp
next
case False
with Init.hyps obtain
eval_init_super:
"G⊢Norm ((init_class_obj G C) s0)
─(if C = Object then Skip else Init (super c))→ s1" and
eval_init: "G⊢(set_lvars Map.empty) s1 ─init c→ s2" and
s3: "s3 = (set_lvars (locals (store s1))) s2"
by simp
have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
(In1r (if C = Object then Skip else Init (super c))) ♢"
using False Init.hyps by simp
note hyp_init_super = this [rule_format]
have "?TypeSafeObj ((set_lvars Map.empty) s1) s2 (In1r (init c)) ♢"
using False Init.hyps by simp
note hyp_init_c = this [rule_format]
from conf_s0 wf cls_C False
have "(Norm ((init_class_obj G C) s0))∷≼(G, L)"
by (auto dest: conforms_init_class_obj)
moreover from wf cls_C have
wt_init_super: "⦇prg = G, cls = accC, lcl = L⦈
⊢(if C = Object then Skip else Init (super c))∷√"
by (cases "C=Object")
(auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
moreover
obtain S where
da_init_super:
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm ((init_class_obj G C) s0))::state)))
»In1r (if C = Object then Skip else Init (super c))» S"
proof (cases "C=Object")
case True
with da_Skip show ?thesis
using that by (auto intro: assigned.select_convs)
next
case False
with da_Init show ?thesis
by - (rule that, auto intro: assigned.select_convs)
qed
ultimately
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_init_super [elim_format]) simp
from eval_init_super wt_init_super wf
have s1_no_ret: "⋀ j. abrupt s1 ≠ Some (Jump j)"
by - (rule eval_statement_no_jump [where ?Env="⦇prg=G,cls=accC,lcl=L⦈"],
auto)
with conf_s1
have "(set_lvars Map.empty) s1∷≼(G, Map.empty)"
by (cases s1) (auto intro: conforms_set_locals)
moreover
from error_free_s1
have error_free_empty: "error_free ((set_lvars Map.empty) s1)"
by simp
from cls_C wf have wt_init_c: "⦇prg=G, cls=C,lcl=Map.empty⦈⊢(init c)∷√"
by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
moreover from cls_C wf obtain I
where "⦇prg=G,cls=C,lcl=Map.empty⦈⊢ {} »In1r (init c)» I"
by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
then obtain I' where
"⦇prg=G,cls=C,lcl=Map.empty⦈⊢dom (locals (store ((set_lvars Map.empty) s1)))
»In1r (init c)» I'"
by (rule da_weakenE) simp
ultimately
obtain conf_s2: "s2∷≼(G, Map.empty)" and error_free_s2: "error_free s2"
by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
have "abrupt s2 ≠ Some (Jump Ret)"
proof -
from s1_no_ret
have "⋀ j. abrupt ((set_lvars Map.empty) s1) ≠ Some (Jump j)"
by simp
moreover
from cls_C wf have "jumpNestingOkS {} (init c)"
by (rule wf_prog_cdecl [THEN wf_cdeclE])
ultimately
show ?thesis
using eval_init wt_init_c wf
by - (rule eval_statement_no_jump
[where ?Env="⦇prg=G,cls=C,lcl=Map.empty⦈"],simp+)
qed
with conf_s2 s3 conf_s1 eval_init
have "s3∷≼(G, L)"
by (cases s2,cases s1) (force dest: conforms_return eval_gext')
moreover from error_free_s2 s3
have "error_free s3"
by simp
moreover note wt
ultimately show ?thesis
by simp
qed
next
case (NewC s0 C s1 a s2 L accC T A)
note ‹G⊢Norm s0 ─Init C→ s1›
note halloc = ‹G⊢s1 ─halloc CInst C≻a→ s2›
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
moreover
note wt = ‹⦇prg=G, cls=accC, lcl=L⦈⊢In1l (NewC C)∷T›
then obtain is_cls_C: "is_class G C" and
T: "T=Inl (Class C)"
by (rule wt_elim_cases) (auto dest: is_acc_classD)
hence "⦇prg=G, cls=accC, lcl=L⦈⊢Init C∷√" by auto
moreover obtain I where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r (Init C)» I"
by (auto intro: da_Init [simplified] assigned.select_convs)
ultimately
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
from conf_s1 halloc wf is_cls_C
obtain halloc_type_safe: "s2∷≼(G, L)"
"(normal s2 ⟶ G,store s2⊢Addr a∷≼Class C)"
by (cases s2) (auto dest!: halloc_type_sound)
from halloc error_free_s1
have "error_free s2"
by (rule error_free_halloc)
with halloc_type_safe T
show "s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In1l (NewC C)≻In1 (Addr a)∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
by auto
next
case (NewA s0 elT s1 e i s2 a s3 L accC T A)
note eval_init = ‹G⊢Norm s0 ─init_comp_ty elT→ s1›
note eval_e = ‹G⊢s1 ─e-≻i→ s2›
note halloc = ‹G⊢abupd (check_neg i) s2─halloc Arr elT (the_Intg i)≻a→ s3›
note hyp_init = ‹PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) ♢›
note hyp_size = ‹PROP ?TypeSafe s1 s2 (In1l e) (In1 i)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (New elT[e])∷T›
then obtain
wt_init: "⦇prg = G, cls = accC, lcl = L⦈⊢init_comp_ty elT∷√" and
wt_size: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-PrimT Integer" and
elT: "is_type G elT" and
T: "T=Inl (elT.[])"
by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
from NewA.prems
have da_e:"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» A"
by (elim da_elim_cases) simp
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
proof -
note conf_s0 wt_init
moreover obtain I where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r (init_comp_ty elT)» I"
proof (cases "∃C. elT = Class C")
case True
thus ?thesis
by - (rule that, (auto intro: da_Init [simplified]
assigned.select_convs
simp add: init_comp_ty_def))
next
case False
thus ?thesis
by - (rule that, (auto intro: da_Skip [simplified]
assigned.select_convs
simp add: init_comp_ty_def))
qed
ultimately show thesis
by (rule hyp_init [elim_format]) (auto intro: that)
qed
obtain conf_s2: "s2∷≼(G, L)" and error_free_s2: "error_free s2"
proof -
from eval_init
have "dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
with da_e
obtain A' where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s1)) »In1l e» A'"
by (rule da_weakenE)
with conf_s1 wt_size
show ?thesis
by (rule hyp_size [elim_format]) (simp add: that error_free_s1)
qed
from conf_s2 have "abupd (check_neg i) s2∷≼(G, L)"
by (cases s2) auto
with halloc wf elT
have halloc_type_safe:
"s3∷≼(G, L) ∧ (normal s3 ⟶ G,store s3⊢Addr a∷≼elT.[])"
by (cases s3) (auto dest!: halloc_type_sound)
from halloc error_free_s2
have "error_free s3"
by (auto dest: error_free_halloc)
with halloc_type_safe T
show "s3∷≼(G, L) ∧
(normal s3 ⟶ G,L,store s3⊢In1l (New elT[e])≻In1 (Addr a)∷≼T) ∧
(error_free (Norm s0) = error_free s3) "
by simp
next
case (Cast s0 e v s1 s2 castT L accC T A)
note ‹G⊢Norm s0 ─e-≻v→ s1›
note s2 = ‹s2 = abupd (raise_if (¬ G,store s1⊢v fits castT) ClassCast) s1›
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (Cast castT e)∷T›
then obtain eT
where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" and
eT: "G⊢eT≼? castT" and
T: "T=Inl castT"
by (rule wt_elim_cases) auto
from Cast.prems
have "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» A"
by (elim da_elim_cases) simp
with conf_s0 wt_e
obtain conf_s1: "s1∷≼(G, L)" and
v_ok: "normal s1 ⟶ G,store s1⊢v∷≼eT" and
error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
from conf_s1 s2
have conf_s2: "s2∷≼(G, L)"
by (cases s1) simp
from error_free_s1 s2
have error_free_s2: "error_free s2"
by simp
{
assume norm_s2: "normal s2"
have "G,L,store s2⊢In1l (Cast castT e)≻In1 v∷≼T"
proof -
from s2 norm_s2 have "normal s1"
by (cases s1) simp
with v_ok
have "G,store s1⊢v∷≼eT"
by simp
with eT wf s2 T norm_s2
show ?thesis
by (cases s1) (auto dest: fits_conf)
qed
}
with conf_s2 error_free_s2
show "s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In1l (Cast castT e)≻In1 v∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
by blast
next
case (Inst s0 e v s1 b instT L accC T A)
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
from Inst.prems obtain eT
where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-RefT eT" and
T: "T=Inl (PrimT Boolean)"
by (elim wt_elim_cases) simp
from Inst.prems
have da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» A"
by (elim da_elim_cases) simp
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and
v_ok: "normal s1 ⟶ G,store s1⊢v∷≼RefT eT" and
error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
with T show ?case
by simp
next
case (Lit s v L accC T A)
then show ?case
by (auto elim!: wt_elim_cases
intro: conf_litval simp add: empty_dt_def)
next
case (UnOp s0 e v s1 unop L accC T A)
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (UnOp unop e)∷T›
then obtain eT
where wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" and
wt_unop: "wt_unop unop eT" and
T: "T=Inl (PrimT (unop_type unop))"
by (auto elim!: wt_elim_cases)
from UnOp.prems obtain A where
da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» A"
by (elim da_elim_cases) simp
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and
wt_v: "normal s1 ⟶ G,store s1⊢v∷≼eT" and
error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
from wt_v T wt_unop
have "normal s1⟶G,L,snd s1⊢In1l (UnOp unop e)≻In1 (eval_unop unop v)∷≼T"
by (cases unop) auto
with conf_s1 error_free_s1
show "s1∷≼(G, L) ∧
(normal s1 ⟶ G,L,snd s1⊢In1l (UnOp unop e)≻In1 (eval_unop unop v)∷≼T) ∧
error_free (Norm s0) = error_free s1"
by simp
next
case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A)
note eval_e1 = ‹G⊢Norm s0 ─e1-≻v1→ s1›
note eval_e2 = ‹G⊢s1 ─(if need_second_arg binop v1 then In1l e2
else In1r Skip)≻→ (In1 v2, s2)›
note hyp_e1 = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)›
note hyp_e2 = ‹PROP ?TypeSafe s1 s2
(if need_second_arg binop v1 then In1l e2 else In1r Skip)
(In1 v2)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (BinOp binop e1 e2)∷T›
then obtain e1T e2T where
wt_e1: "⦇prg = G, cls = accC, lcl = L⦈⊢e1∷-e1T" and
wt_e2: "⦇prg = G, cls = accC, lcl = L⦈⊢e2∷-e2T" and
wt_binop: "wt_binop G binop e1T e2T" and
T: "T=Inl (PrimT (binop_type binop))"
by (elim wt_elim_cases) simp
have wt_Skip: "⦇prg = G, cls = accC, lcl = L⦈⊢Skip∷√"
by simp
obtain S where
daSkip: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s1)) »In1r Skip» S"
by (auto intro: da_Skip [simplified] assigned.select_convs)
note da = ‹⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store ((Norm s0::state))))
»⟨BinOp binop e1 e2⟩⇩e» A›
then obtain E1 where
da_e1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e1» E1"
by (elim da_elim_cases) simp+
from conf_s0 wt_e1 da_e1
obtain conf_s1: "s1∷≼(G, L)" and
wt_v1: "normal s1 ⟶ G,store s1⊢v1∷≼e1T" and
error_free_s1: "error_free s1"
by (rule hyp_e1 [elim_format]) simp
from wt_binop T
have conf_v:
"G,L,snd s2⊢In1l (BinOp binop e1 e2)≻In1 (eval_binop binop v1 v2)∷≼T"
by (cases binop) auto
from eval_e1 have
s0_s1:"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
show "s2∷≼(G, L) ∧
(normal s2 ⟶
G,L,snd s2⊢In1l (BinOp binop e1 e2)≻In1 (eval_binop binop v1 v2)∷≼T) ∧
error_free (Norm s0) = error_free s2"
proof (cases "normal s1")
case False
with eval_e2 have "s2=s1" by auto
with conf_s1 error_free_s1 False show ?thesis
by auto
next
case True
note normal_s1 = this
show ?thesis
proof (cases "need_second_arg binop v1")
case False
with normal_s1 eval_e2 have "s2=s1"
by (cases s1) (simp, elim eval_elim_cases,simp)
with conf_s1 conf_v error_free_s1
show ?thesis by simp
next
case True
note need_second_arg = this
with hyp_e2
have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1
wt_v1 [rule_format,OF normal_s1] wf
obtain E2 where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »In1l e2» E2"
by (rule da_e2_BinOp [elim_format])
(auto simp add: need_second_arg )
with conf_s1 wt_e2
obtain "s2∷≼(G, L)" and "error_free s2"
by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
with conf_v show ?thesis by simp
qed
qed
next
case (Super s L accC T A)
note conf_s = ‹Norm s∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l Super∷T›
then obtain C c where
C: "L This = Some (Class C)" and
neq_Obj: "C≠Object" and
cls_C: "class G C = Some c" and
T: "T=Inl (Class (super c))"
by (rule wt_elim_cases) auto
from Super.prems
obtain "This ∈ dom (locals s)"
by (elim da_elim_cases) simp
with conf_s C have "G,s⊢val_this s∷≼Class C"
by (auto dest: conforms_localD [THEN wlconfD])
with neq_Obj cls_C wf
have "G,s⊢val_this s∷≼Class (super c)"
by (auto intro: conf_widen
dest: subcls_direct[THEN widen.subcls])
with T conf_s
show "Norm s∷≼(G, L) ∧
(normal (Norm s) ⟶
G,L,store (Norm s)⊢In1l Super≻In1 (val_this s)∷≼T) ∧
(error_free (Norm s) = error_free (Norm s))"
by simp
next
case (Acc s0 v w upd s1 L accC T A)
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))›
note conf_s0 = ‹Norm s0∷≼(G, L)›
from Acc.prems obtain vT where
wt_v: "⦇prg = G, cls = accC, lcl = L⦈⊢v∷=vT" and
T: "T=Inl vT"
by (elim wt_elim_cases) simp
from Acc.prems obtain V where
da_v: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In2 v» V"
by (cases "∃ n. v=LVar n") (insert da.LVar, auto elim!: da_elim_cases)
{
fix n assume lvar: "v=LVar n"
have "locals (store s1) n ≠ None"
proof -
from Acc.prems lvar have
"n ∈ dom (locals s0)"
by (cases "∃ n. v=LVar n") (auto elim!: da_elim_cases)
also
have "dom (locals s0) ⊆ dom (locals (store s1))"
proof -
from ‹G⊢Norm s0 ─v=≻(w, upd)→ s1›
show ?thesis
by (rule dom_locals_eval_mono_elim) simp
qed
finally show ?thesis
by blast
qed
} note lvar_in_locals = this
from conf_s0 wt_v da_v
obtain conf_s1: "s1∷≼(G, L)"
and conf_var: "(normal s1 ⟶ G,L,store s1⊢In2 v≻In2 (w, upd)∷≼Inl vT)"
and error_free_s1: "error_free s1"
by (rule hyp [elim_format]) simp
from lvar_in_locals conf_var T
have "(normal s1 ⟶ G,L,store s1⊢In1l (Acc v)≻In1 w∷≼T)"
by (cases "∃ n. v=LVar n") auto
with conf_s1 error_free_s1 show ?case
by simp
next
case (Ass s0 var w upd s1 e v s2 L accC T A)
note eval_var = ‹G⊢Norm s0 ─var=≻(w, upd)→ s1›
note eval_e = ‹G⊢s1 ─e-≻v→ s2›
note hyp_var = ‹PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))›
note hyp_e = ‹PROP ?TypeSafe s1 s2 (In1l e) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (var:=e)∷T›
then obtain varT eT where
wt_var: "⦇prg = G, cls = accC, lcl = L⦈⊢var∷=varT" and
wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" and
widen: "G⊢eT≼varT" and
T: "T=Inl eT"
by (rule wt_elim_cases) auto
show "assign upd v s2∷≼(G, L) ∧
(normal (assign upd v s2) ⟶
G,L,store (assign upd v s2)⊢In1l (var:=e)≻In1 v∷≼T) ∧
(error_free (Norm s0) = error_free (assign upd v s2))"
proof (cases "∃ vn. var=LVar vn")
case False
with Ass.prems
obtain V E where
da_var: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In2 var» V" and
da_e: "⦇prg=G,cls=accC,lcl=L⦈ ⊢ nrm V »In1l e» E"
by (elim da_elim_cases) simp+
from conf_s0 wt_var da_var
obtain conf_s1: "s1∷≼(G, L)"
and conf_var: "normal s1
⟶ G,L,store s1⊢In2 var≻In2 (w, upd)∷≼Inl varT"
and error_free_s1: "error_free s1"
by (rule hyp_var [elim_format]) simp
show ?thesis
proof (cases "normal s1")
case False
with eval_e have "s2=s1" by auto
with False have "assign upd v s2=s1"
by simp
with conf_s1 error_free_s1 False show ?thesis
by auto
next
case True
note normal_s1=this
obtain A' where "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s1)) »In1l e» A'"
proof -
from eval_var wt_var da_var wf normal_s1
have "nrm V ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_e show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e
obtain conf_s2: "s2∷≼(G, L)" and
conf_v: "normal s2 ⟶ G,store s2⊢v∷≼eT" and
error_free_s2: "error_free s2"
by (rule hyp_e [elim_format]) (simp add: error_free_s1)
show ?thesis
proof (cases "normal s2")
case False
with conf_s2 error_free_s2
show ?thesis
by auto
next
case True
from True conf_v
have conf_v_eT: "G,store s2⊢v∷≼eT"
by simp
with widen wf
have conf_v_varT: "G,store s2⊢v∷≼varT"
by (auto intro: conf_widen)
from normal_s1 conf_var
have "G,L,store s1⊢In2 var≻In2 (w, upd)∷≼Inl varT"
by simp
then
have conf_assign: "store s1≤|upd≼varT∷≼(G, L)"
by (simp add: rconf_def)
from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var
eval_e T conf_s2 error_free_s2
show ?thesis
by (cases s1, cases s2)
(auto dest!: Ass_lemma simp add: assign_conforms_def)
qed
qed
next
case True
then obtain vn where vn: "var=LVar vn"
by blast
with Ass.prems
obtain E where
da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1l e» E"
by (elim da_elim_cases) simp+
from da.LVar vn obtain V where
da_var: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In2 var» V"
by auto
obtain E' where
da_e': "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s1)) »In1l e» E'"
proof -
have "dom (locals (store ((Norm s0)::state)))
⊆ dom (locals (store (s1)))"
by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
with da_e show thesis
by (rule da_weakenE) (rule that)
qed
from conf_s0 wt_var da_var
obtain conf_s1: "s1∷≼(G, L)"
and conf_var: "normal s1
⟶ G,L,store s1⊢In2 var≻In2 (w, upd)∷≼Inl varT"
and error_free_s1: "error_free s1"
by (rule hyp_var [elim_format]) simp
show ?thesis
proof (cases "normal s1")
case False
with eval_e have "s2=s1" by auto
with False have "assign upd v s2=s1"
by simp
with conf_s1 error_free_s1 False show ?thesis
by auto
next
case True
note normal_s1 = this
from conf_s1 wt_e da_e'
obtain conf_s2: "s2∷≼(G, L)" and
conf_v: "normal s2 ⟶ G,store s2⊢v∷≼eT" and
error_free_s2: "error_free s2"
by (rule hyp_e [elim_format]) (simp add: error_free_s1)
show ?thesis
proof (cases "normal s2")
case False
with conf_s2 error_free_s2
show ?thesis
by auto
next
case True
from True conf_v
have conf_v_eT: "G,store s2⊢v∷≼eT"
by simp
with widen wf
have conf_v_varT: "G,store s2⊢v∷≼varT"
by (auto intro: conf_widen)
from normal_s1 conf_var
have "G,L,store s1⊢In2 var≻In2 (w, upd)∷≼Inl varT"
by simp
then
have conf_assign: "store s1≤|upd≼varT∷≼(G, L)"
by (simp add: rconf_def)
from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var
eval_e T conf_s2 error_free_s2
show ?thesis
by (cases s1, cases s2)
(auto dest!: Ass_lemma simp add: assign_conforms_def)
qed
qed
qed
next
case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A)
note eval_e0 = ‹G⊢Norm s0 ─e0-≻b→ s1›
note eval_e1_e2 = ‹G⊢s1 ─(if the_Bool b then e1 else e2)-≻v→ s2›
note hyp_e0 = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)›
note hyp_if = ‹PROP ?TypeSafe s1 s2
(In1l (if the_Bool b then e1 else e2)) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (e0 ? e1 : e2)∷T›
then obtain T1 T2 statT where
wt_e0: "⦇prg = G, cls = accC, lcl = L⦈⊢e0∷-PrimT Boolean" and
wt_e1: "⦇prg = G, cls = accC, lcl = L⦈⊢e1∷-T1" and
wt_e2: "⦇prg = G, cls = accC, lcl = L⦈⊢e2∷-T2" and
statT: "G⊢T1≼T2 ∧ statT = T2 ∨ G⊢T2≼T1 ∧ statT = T1" and
T : "T=Inl statT"
by (rule wt_elim_cases) auto
with Cond.prems obtain E0 E1 E2 where
da_e0: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state)))
»In1l e0» E0" and
da_e1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state)))
∪ assigns_if True e0) »In1l e1» E1" and
da_e2: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state)))
∪ assigns_if False e0) »In1l e2» E2"
by (elim da_elim_cases) simp+
from conf_s0 wt_e0 da_e0
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_e0 [elim_format]) simp
show "s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In1l (e0 ? e1 : e2)≻In1 v∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
proof (cases "normal s1")
case False
with eval_e1_e2 have "s2=s1" by auto
with conf_s1 error_free_s1 False show ?thesis
by auto
next
case True
have s0_s1: "dom (locals (store ((Norm s0)::state)))
∪ assigns_if (the_Bool b) e0 ⊆ dom (locals (store s1))"
proof -
from eval_e0 have
"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
moreover
from eval_e0 True wt_e0
have "assigns_if (the_Bool b) e0 ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx')
ultimately show ?thesis by (rule Un_least)
qed
show ?thesis
proof (cases "the_Bool b")
case True
with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)"
by simp
from da_e1 s0_s1 True obtain E1' where
"⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s1)))»In1l e1» E1'"
by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
with conf_s1 wt_e1
obtain
"s2∷≼(G, L)"
"(normal s2 ⟶ G,L,store s2⊢In1l e1≻In1 v∷≼Inl T1)"
"error_free s2"
by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
moreover
from statT
have "G⊢T1≼statT"
by auto
ultimately show ?thesis
using T wf by auto
next
case False
with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)"
by simp
from da_e2 s0_s1 False obtain E2' where
"⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s1)))»In1l e2» E2'"
by - (rule da_weakenE, auto iff del: Un_subset_iff sup.bounded_iff)
with conf_s1 wt_e2
obtain
"s2∷≼(G, L)"
"(normal s2 ⟶ G,L,store s2⊢In1l e2≻In1 v∷≼Inl T2)"
"error_free s2"
by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
moreover
from statT
have "G⊢T2≼statT"
by auto
ultimately show ?thesis
using T wf by auto
qed
qed
next
case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC'
v s4 L accC T A)
note eval_e = ‹G⊢Norm s0 ─e-≻a→ s1›
note eval_args = ‹G⊢s1 ─args≐≻vs→ s2›
note invDeclC = ‹invDeclC
= invocation_declclass G mode (store s2) a statT
⦇name = mn, parTs = pTs'⦈›
note init_lvars =
‹s3 = init_lvars G invDeclC ⦇name = mn, parTs = pTs'⦈ mode a vs s2›
note check = ‹s3' =
check_method_access G accC' statT mode ⦇name = mn, parTs = pTs'⦈ a s3›
note eval_methd =
‹G⊢s3' ─Methd invDeclC ⦇name = mn, parTs = pTs'⦈-≻v→ s4›
note hyp_e = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)›
note hyp_args = ‹PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)›
note hyp_methd = ‹PROP ?TypeSafe s3' s4
(In1l (Methd invDeclC ⦇name = mn, parTs = pTs'⦈)) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg=G, cls=accC, lcl=L⦈
⊢In1l ({accC',statT,mode}e⋅mn( {pTs'}args))∷T›
from wt obtain pTs statDeclT statM where
wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-RefT statT" and
wt_args: "⦇prg=G, cls=accC, lcl=L⦈⊢args∷≐pTs" and
statM: "max_spec G accC statT ⦇name=mn,parTs=pTs⦈
= {((statDeclT,statM),pTs')}" and
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
by (rule wt_elim_cases) fastforce+
from Call.prems obtain E where
da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))»In1l e» E" and
da_args: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E »In3 args» A"
by (elim da_elim_cases) simp
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and
conf_a: "normal s1 ⟹ G, store s1⊢a∷≼RefT statT" and
error_free_s1: "error_free s1"
by (rule hyp_e [elim_format]) simp
{
assume abnormal_s2: "¬ normal s2"
have "set_lvars (locals (store s2)) s4 = s2"
proof -
from abnormal_s2 init_lvars
obtain keep_abrupt: "abrupt s3 = abrupt s2" and
"store s3 = store (init_lvars G invDeclC ⦇name = mn, parTs = pTs'⦈
mode a vs s2)"
by (auto simp add: init_lvars_def2)
moreover
from keep_abrupt abnormal_s2 check
have eq_s3'_s3: "s3'=s3"
by (auto simp add: check_method_access_def Let_def)
moreover
from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
have "s4=s3'"
by auto
ultimately show
"set_lvars (locals (store s2)) s4 = s2"
by (cases s2,cases s3) (simp add: init_lvars_def2)
qed
} note propagate_abnormal_s2 = this
show "(set_lvars (locals (store s2))) s4∷≼(G, L) ∧
(normal ((set_lvars (locals (store s2))) s4) ⟶
G,L,store ((set_lvars (locals (store s2))) s4)
⊢In1l ({accC',statT,mode}e⋅mn( {pTs'}args))≻In1 v∷≼T) ∧
(error_free (Norm s0) =
error_free ((set_lvars (locals (store s2))) s4))"
proof (cases "normal s1")
case False
with eval_args have "s2=s1" by auto
with False propagate_abnormal_s2 conf_s1 error_free_s1
show ?thesis
by auto
next
case True
note normal_s1 = this
obtain A' where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »In3 args» A'"
proof -
from eval_e wt_e da_e wf normal_s1
have "nrm E ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_args show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_args
obtain conf_s2: "s2∷≼(G, L)" and
conf_args: "normal s2
⟹ list_all2 (conf G (store s2)) vs pTs" and
error_free_s2: "error_free s2"
by (rule hyp_args [elim_format]) (simp add: error_free_s1)
from error_free_s2 init_lvars
have error_free_s3: "error_free s3"
by (auto simp add: init_lvars_def2)
from statM
obtain
statM': "(statDeclT,statM)∈mheads G accC statT ⦇name=mn,parTs=pTs'⦈" and
pTs_widen: "G⊢pTs[≼]pTs'"
by (blast dest: max_spec2mheads)
from check
have eq_store_s3'_s3: "store s3'=store s3"
by (cases s3) (simp add: check_method_access_def Let_def)
obtain invC
where invC: "invC = invocation_class mode (store s2) a statT"
by simp
with init_lvars
have invC': "invC = (invocation_class mode (store s3) a statT)"
by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
show ?thesis
proof (cases "normal s2")
case False
with propagate_abnormal_s2 conf_s2 error_free_s2
show ?thesis
by auto
next
case True
note normal_s2 = True
with normal_s1 conf_a eval_args
have conf_a_s2: "G, store s2⊢a∷≼RefT statT"
by (auto dest: eval_gext intro: conf_gext)
show ?thesis
proof (cases "a=Null ⟶ is_static statM")
case False
then obtain not_static: "¬ is_static statM" and Null: "a=Null"
by blast
with normal_s2 init_lvars mode
obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
"store s3 = store (init_lvars G invDeclC
⦇name = mn, parTs = pTs'⦈ mode a vs s2)"
by (auto simp add: init_lvars_def2)
moreover
from np check
have eq_s3'_s3: "s3'=s3"
by (auto simp add: check_method_access_def Let_def)
moreover
from eq_s3'_s3 np eval_methd
have "s4=s3'"
by auto
ultimately have
"set_lvars (locals (store s2)) s4
= (Some (Xcpt (Std NullPointer)),store s2)"
by (cases s2,cases s3) (simp add: init_lvars_def2)
with conf_s2 error_free_s2
show ?thesis
by (cases s2) (auto dest: conforms_NormI)
next
case True
with mode have notNull: "mode = IntVir ⟶ a ≠ Null"
by (auto dest!: Null_staticD)
with conf_s2 conf_a_s2 wf invC
have dynT_prop: "G⊢mode→invC≼statT"
by (cases s2) (auto intro: DynT_propI)
with wt_e statM' invC mode wf
obtain dynM where
dynM: "dynlookup G statT invC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and
acc_dynM: "G ⊢Methd ⦇name=mn,parTs=pTs'⦈ dynM
in invC dyn_accessible_from accC"
by (force dest!: call_access_ok)
with invC' check eq_accC_accC'
have eq_s3'_s3: "s3'=s3"
by (auto simp add: check_method_access_def Let_def)
from dynT_prop wf wt_e statM' mode invC invDeclC dynM
obtain
wf_dynM: "wf_mdecl G invDeclC (⦇name=mn,parTs=pTs'⦈,mthd dynM)" and
dynM': "methd G invDeclC ⦇name=mn,parTs=pTs'⦈ = Some dynM" and
iscls_invDeclC: "is_class G invDeclC" and
invDeclC': "invDeclC = declclass dynM" and
invC_widen: "G⊢invC≼⇩C invDeclC" and
resTy_widen: "G⊢resTy dynM≼resTy statM" and
is_static_eq: "is_static dynM = is_static statM" and
involved_classes_prop:
"(if invmode statM e = IntVir
then ∀statC. statT = ClassT statC ⟶ G⊢invC≼⇩C statC
else ((∃statC. statT = ClassT statC ∧ G⊢statC≼⇩C invDeclC) ∨
(∀statC. statT ≠ ClassT statC ∧ invDeclC = Object)) ∧
statDeclT = ClassT invDeclC)"
by (cases rule: DynT_mheadsE) simp
obtain L' where
L':"L'=(λ k.
(case k of
EName e
⇒ (case e of
VNam v
⇒((table_of (lcls (mbody (mthd dynM))))
(pars (mthd dynM)[↦]pTs')) v
| Res ⇒ Some (resTy dynM))
| This ⇒ if is_static statM
then None else Some (Class invDeclC)))"
by simp
from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
have conf_s3: "s3∷≼(G,L')"
apply -
apply (drule conforms_init_lvars [of G invDeclC
"⦇name=mn,parTs=pTs'⦈" dynM "store s2" vs pTs "abrupt s2"
L statT invC a "(statDeclT,statM)" e])
apply (rule wf)
apply (rule conf_args,assumption)
apply (simp add: pTs_widen)
apply (cases s2,simp)
apply (rule dynM')
apply (force dest: ty_expr_is_type)
apply (rule invC_widen)
apply (force intro: conf_gext dest: eval_gext)
apply simp
apply simp
apply (simp add: invC)
apply (simp add: invDeclC)
apply (simp add: normal_s2)
apply (cases s2, simp add: L' init_lvars
cong add: lname.case_cong ename.case_cong)
done
with eq_s3'_s3
have conf_s3': "s3'∷≼(G,L')" by simp
moreover
from is_static_eq wf_dynM L'
obtain mthdT where
"⦇prg=G,cls=invDeclC,lcl=L'⦈
⊢Body invDeclC (stmt (mbody (mthd dynM)))∷-mthdT" and
mthdT_widen: "G⊢mthdT≼resTy dynM"
by - (drule wf_mdecl_bodyD,
auto simp add: callee_lcl_def
cong add: lname.case_cong ename.case_cong)
with dynM' iscls_invDeclC invDeclC'
have
"⦇prg=G,cls=invDeclC,lcl=L'⦈
⊢(Methd invDeclC ⦇name = mn, parTs = pTs'⦈)∷-mthdT"
by (auto intro: wt.Methd)
moreover
obtain M where
"⦇prg=G,cls=invDeclC,lcl=L'⦈
⊢ dom (locals (store s3'))
»In1l (Methd invDeclC ⦇name = mn, parTs = pTs'⦈)» M"
proof -
from wf_dynM
obtain M' where
da_body:
"⦇prg=G, cls=invDeclC
,lcl=callee_lcl invDeclC ⦇name = mn, parTs = pTs'⦈ (mthd dynM)
⦈ ⊢ parameters (mthd dynM) »⟨stmt (mbody (mthd dynM))⟩» M'" and
res: "Result ∈ nrm M'"
by (rule wf_mdeclE) iprover
from da_body is_static_eq L' have
"⦇prg=G, cls=invDeclC,lcl=L'⦈
⊢ parameters (mthd dynM) »⟨stmt (mbody (mthd dynM))⟩» M'"
by (simp add: callee_lcl_def
cong add: lname.case_cong ename.case_cong)
moreover have "parameters (mthd dynM) ⊆ dom (locals (store s3'))"
proof -
from is_static_eq
have "(invmode (mthd dynM) e) = (invmode statM e)"
by (simp add: invmode_def)
moreover
have "length (pars (mthd dynM)) = length vs"
proof -
from normal_s2 conf_args
have "length vs = length pTs"
by (simp add: list_all2_iff)
also from pTs_widen
have "… = length pTs'"
by (simp add: widens_def list_all2_iff)
also from wf_dynM
have "… = length (pars (mthd dynM))"
by (simp add: wf_mdecl_def wf_mhead_def)
finally show ?thesis ..
qed
moreover note init_lvars dynM' is_static_eq normal_s2 mode
ultimately
have "parameters (mthd dynM) = dom (locals (store s3))"
using dom_locals_init_lvars
[of "mthd dynM" G invDeclC "⦇name=mn,parTs=pTs'⦈" vs e a s2]
by simp
also from check
have "dom (locals (store s3)) ⊆ dom (locals (store s3'))"
by (simp add: eq_s3'_s3)
finally show ?thesis .
qed
ultimately obtain M2 where
da:
"⦇prg=G, cls=invDeclC,lcl=L'⦈
⊢ dom (locals (store s3')) »⟨stmt (mbody (mthd dynM))⟩» M2" and
M2: "nrm M' ⊆ nrm M2"
by (rule da_weakenE)
from res M2 have "Result ∈ nrm M2"
by blast
moreover from wf_dynM
have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
by (rule wf_mdeclE)
ultimately
obtain M3 where
"⦇prg=G, cls=invDeclC,lcl=L'⦈ ⊢ dom (locals (store s3'))
»⟨Body (declclass dynM) (stmt (mbody (mthd dynM)))⟩» M3"
using da
by (iprover intro: da.Body assigned.select_convs)
from _ this [simplified]
show ?thesis
by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
qed
ultimately obtain
conf_s4: "s4∷≼(G, L')" and
conf_Res: "normal s4 ⟶ G,store s4⊢v∷≼mthdT" and
error_free_s4: "error_free s4"
by (rule hyp_methd [elim_format])
(simp add: error_free_s3 eq_s3'_s3)
from init_lvars eval_methd eq_s3'_s3
have "store s2≤|store s4"
by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
moreover
have "abrupt s4 ≠ Some (Jump Ret)"
proof -
from normal_s2 init_lvars
have "abrupt s3 ≠ Some (Jump Ret)"
by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
with check
have "abrupt s3' ≠ Some (Jump Ret)"
by (cases s3) (auto simp add: check_method_access_def Let_def)
with eval_methd
show ?thesis
by (rule Methd_no_jump)
qed
ultimately
have "(set_lvars (locals (store s2))) s4∷≼(G, L)"
using conf_s2 conf_s4
by (cases s2,cases s4) (auto intro: conforms_return)
moreover
from conf_Res mthdT_widen resTy_widen wf
have "normal s4
⟶ G,store s4⊢v∷≼(resTy statM)"
by (auto dest: widen_trans)
then
have "normal ((set_lvars (locals (store s2))) s4)
⟶ G,store((set_lvars (locals (store s2))) s4) ⊢v∷≼(resTy statM)"
by (cases s4) auto
moreover note error_free_s4 T
ultimately
show ?thesis
by simp
qed
qed
qed
next
case (Methd s0 D sig v s1 L accC T A)
note ‹G⊢Norm s0 ─body G D sig-≻v→ s1›
note hyp = ‹PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (Methd D sig)∷T›
then obtain m bodyT where
D: "is_class G D" and
m: "methd G D sig = Some m" and
wt_body: "⦇prg = G, cls = accC, lcl = L⦈
⊢Body (declclass m) (stmt (mbody (mthd m)))∷-bodyT" and
T: "T=Inl bodyT"
by (rule wt_elim_cases) auto
moreover
from Methd.prems m have
da_body: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))
»In1l (Body (declclass m) (stmt (mbody (mthd m))))» A"
by - (erule da_elim_cases,simp)
ultimately
show "s1∷≼(G, L) ∧
(normal s1 ⟶ G,L,snd s1⊢In1l (Methd D sig)≻In1 v∷≼T) ∧
(error_free (Norm s0) = error_free s1)"
using hyp [of _ _ "(Inl bodyT)"] conf_s0
by (auto simp add: Let_def body_def)
next
case (Body s0 D s1 c s2 s3 L accC T A)
note eval_init = ‹G⊢Norm s0 ─Init D→ s1›
note eval_c = ‹G⊢s1 ─c→ s2›
note hyp_init = ‹PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) ♢›
note hyp_c = ‹PROP ?TypeSafe s1 s2 (In1r c) ♢›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In1l (Body D c)∷T›
then obtain bodyT where
iscls_D: "is_class G D" and
wt_c: "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√" and
resultT: "L Result = Some bodyT" and
isty_bodyT: "is_type G bodyT" and
T: "T=Inl bodyT"
by (rule wt_elim_cases) auto
from Body.prems obtain C where
da_c: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))»In1r c» C" and
jmpOk: "jumpNestingOkS {Ret} c" and
res: "Result ∈ nrm C"
by (elim da_elim_cases) simp
note conf_s0
moreover from iscls_D
have "⦇prg=G, cls=accC, lcl=L⦈⊢Init D∷√" by auto
moreover obtain I where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r (Init D)» I"
by (auto intro: da_Init [simplified] assigned.select_convs)
ultimately obtain
conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_init [elim_format]) simp
obtain C' where da_C': "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store s1)))»In1r c» C'"
and nrm_C': "nrm C ⊆ nrm C'"
proof -
from eval_init
have "(dom (locals (store ((Norm s0)::state))))
⊆ (dom (locals (store s1)))"
by (rule dom_locals_eval_mono_elim)
with da_c show thesis by (rule da_weakenE) (rule that)
qed
from conf_s1 wt_c da_C'
obtain conf_s2: "s2∷≼(G, L)" and error_free_s2: "error_free s2"
by (rule hyp_c [elim_format]) (simp add: error_free_s1)
from conf_s2
have "abupd (absorb Ret) s2∷≼(G, L)"
by (cases s2) (auto intro: conforms_absorb)
moreover
from error_free_s2
have "error_free (abupd (absorb Ret) s2)"
by simp
moreover have "abrupt (abupd (absorb Ret) s3) ≠ Some (Jump Ret)"
by (cases s3) (simp add: absorb_def)
moreover have "s3=s2"
proof -
from iscls_D
have wt_init: "⦇prg=G, cls=accC, lcl=L⦈⊢(Init D)∷√"
by auto
from eval_init wf
have s1_no_jmp: "⋀ j. abrupt s1 ≠ Some (Jump j)"
by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
from eval_c _ wt_c wf
have "⋀ j. abrupt s2 = Some (Jump j) ⟹ j=Ret"
by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
moreover
note ‹s3 =
(if ∃l. abrupt s2 = Some (Jump (Break l)) ∨
abrupt s2 = Some (Jump (Cont l))
then abupd (λx. Some (Error CrossMethodJump)) s2 else s2)›
ultimately show ?thesis
by force
qed
moreover
{
assume normal_upd_s2: "normal (abupd (absorb Ret) s2)"
have "Result ∈ dom (locals (store s2))"
proof -
from normal_upd_s2
have "normal s2 ∨ abrupt s2 = Some (Jump Ret)"
by (cases s2) (simp add: absorb_def)
thus ?thesis
proof
assume "normal s2"
with eval_c wt_c da_C' wf res nrm_C'
show ?thesis
by (cases rule: da_good_approxE') blast
next
assume "abrupt s2 = Some (Jump Ret)"
with conf_s2 show ?thesis
by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
qed
qed
}
moreover note T resultT
ultimately
show "abupd (absorb Ret) s3∷≼(G, L) ∧
(normal (abupd (absorb Ret) s3) ⟶
G,L,store (abupd (absorb Ret) s3)
⊢In1l (Body D c)≻In1 (the (locals (store s2) Result))∷≼T) ∧
(error_free (Norm s0) = error_free (abupd (absorb Ret) s3)) "
by (cases s2) (auto intro: conforms_locals)
next
case (LVar s vn L accC T)
note conf_s = ‹Norm s∷≼(G, L)› and
wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In2 (LVar vn)∷T›
then obtain vnT where
vnT: "L vn = Some vnT" and
T: "T=Inl vnT"
by (auto elim!: wt_elim_cases)
from conf_s vnT
have conf_fst: "locals s vn ≠ None ⟶ G,s⊢fst (lvar vn s)∷≼vnT"
by (auto elim: conforms_localD [THEN wlconfD]
simp add: lvar_def)
moreover
from conf_s conf_fst vnT
have "s≤|snd (lvar vn s)≼vnT∷≼(G, L)"
by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
moreover note conf_s T
ultimately
show "Norm s∷≼(G, L) ∧
(normal (Norm s) ⟶
G,L,store (Norm s)⊢In2 (LVar vn)≻In2 (lvar vn s)∷≼T) ∧
(error_free (Norm s) = error_free (Norm s))"
by (simp add: lvar_def)
next
case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A)
note eval_init = ‹G⊢Norm s0 ─Init statDeclC→ s1›
note eval_e = ‹G⊢s1 ─e-≻a→ s2›
note fvar = ‹(v, s2') = fvar statDeclC stat fn a s2›
note check = ‹s3 = check_field_access G accC statDeclC fn stat a s2'›
note hyp_init = ‹PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) ♢›
note hyp_e = ‹PROP ?TypeSafe s1 s2 (In1l e) (In1 a)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg=G, cls=accC', lcl=L⦈⊢In2 ({accC,statDeclC,stat}e..fn)∷T›
then obtain statC f where
wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-Class statC" and
accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
eq_accC_accC': "accC=accC'" and
stat: "stat=is_static f" and
T: "T=(Inl (type f))"
by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
from FVar.prems eq_accC_accC'
have da_e: "⦇prg=G, cls=accC, lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))»In1l e» A"
by (elim da_elim_cases) simp
note conf_s0
moreover
from wf wt_e
have iscls_statC: "is_class G statC"
by (auto dest: ty_expr_is_type type_is_class)
with wf accfield
have iscls_statDeclC: "is_class G statDeclC"
by (auto dest!: accfield_fields dest: fields_declC)
hence "⦇prg=G, cls=accC, lcl=L⦈⊢(Init statDeclC)∷√"
by simp
moreover obtain I where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s0)::state))) »In1r (Init statDeclC)» I"
by (auto intro: da_Init [simplified] assigned.select_convs)
ultimately
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1"
by (rule hyp_init [elim_format]) simp
obtain A' where
"⦇prg=G, cls=accC, lcl=L⦈ ⊢ (dom (locals (store s1)))»In1l e» A'"
proof -
from eval_init
have "(dom (locals (store ((Norm s0)::state))))
⊆ (dom (locals (store s1)))"
by (rule dom_locals_eval_mono_elim)
with da_e show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e
obtain conf_s2: "s2∷≼(G, L)" and
conf_a: "normal s2 ⟶ G,store s2⊢a∷≼Class statC" and
error_free_s2: "error_free s2"
by (rule hyp_e [elim_format]) (simp add: error_free_s1)
from fvar
have store_s2': "store s2'=store s2"
by (cases s2) (simp add: fvar_def2)
with fvar conf_s2
have conf_s2': "s2'∷≼(G, L)"
by (cases s2,cases stat) (auto simp add: fvar_def2)
from eval_init
have initd_statDeclC_s1: "initd statDeclC s1"
by (rule init_yields_initd)
from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check wf
have eq_s3_s2': "s3=s2'"
by (auto dest!: error_free_field_access)
have conf_v: "normal s2' ⟹
G,store s2'⊢fst v∷≼type f ∧ store s2'≤|snd v≼type f∷≼(G, L)"
proof -
assume normal: "normal s2'"
obtain vv vf x2 store2 store2'
where v: "v=(vv,vf)" and
s2: "s2=(x2,store2)" and
store2': "store s2' = store2'"
by (cases v,cases s2,cases s2') blast
from iscls_statDeclC obtain c
where c: "class G statDeclC = Some c"
by auto
have "G,store2'⊢vv∷≼type f ∧ store2'≤|vf≼type f∷≼(G, L)"
proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2
statC G c L "store s1"])
from v normal s2 fvar stat store2'
show "((vv, vf), Norm store2') =
fvar statDeclC (static f) fn a (x2, store2)"
by (auto simp add: member_is_static_simp)
from accfield iscls_statC wf
show "G⊢statC≼⇩C statDeclC"
by (auto dest!: accfield_fields dest: fields_declC)
from accfield
show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
by (auto dest!: accfield_fields)
from wf show "wf_prog G" .
from conf_a s2 show "x2 = None ⟶ G,store2⊢a∷≼Class statC"
by auto
from fld wf iscls_statC
show "statDeclC ≠ Object "
by (cases "statDeclC=Object") (drule fields_declC,simp+)+
from c show "class G statDeclC = Some c" .
from conf_s2 s2 show "(x2, store2)∷≼(G, L)" by simp
from eval_e s2 show "snd s1≤|store2" by (auto dest: eval_gext)
from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))"
by simp
qed
with v s2 store2'
show ?thesis
by simp
qed
from fvar error_free_s2
have "error_free s2'"
by (cases s2)
(auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
with conf_v T conf_s2' eq_s3_s2'
show "s3∷≼(G, L) ∧
(normal s3
⟶ G,L,store s3⊢In2 ({accC,statDeclC,stat}e..fn)≻In2 v∷≼T) ∧
(error_free (Norm s0) = error_free s3)"
by auto
next
case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A)
note eval_e1 = ‹G⊢Norm s0 ─e1-≻a→ s1›
note eval_e2 = ‹G⊢s1 ─e2-≻i→ s2›
note hyp_e1 = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)›
note hyp_e2 = ‹PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)›
note avar = ‹(v, s2') = avar G i a s2›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In2 (e1.[e2])∷T›
then obtain elemT
where wt_e1: "⦇prg=G,cls=accC,lcl=L⦈⊢e1∷-elemT.[]" and
wt_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢e2∷-PrimT Integer" and
T: "T= Inl elemT"
by (rule wt_elim_cases) auto
from AVar.prems obtain E1 where
da_e1: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))»In1l e1» E1" and
da_e2: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E1 »In1l e2» A"
by (elim da_elim_cases) simp
from conf_s0 wt_e1 da_e1
obtain conf_s1: "s1∷≼(G, L)" and
conf_a: "(normal s1 ⟶ G,store s1⊢a∷≼elemT.[])" and
error_free_s1: "error_free s1"
by (rule hyp_e1 [elim_format]) simp
show "s2'∷≼(G, L) ∧
(normal s2' ⟶ G,L,store s2'⊢In2 (e1.[e2])≻In2 v∷≼T) ∧
(error_free (Norm s0) = error_free s2') "
proof (cases "normal s1")
case False
moreover
from False eval_e2 have eq_s2_s1: "s2=s1" by auto
moreover
from eq_s2_s1 False have "¬ normal s2" by simp
then have "snd (avar G i a s2) = s2"
by (cases s2) (simp add: avar_def2)
with avar have "s2'=s2"
by (cases "(avar G i a s2)") simp
ultimately show ?thesis
using conf_s1 error_free_s1
by auto
next
case True
obtain A' where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »In1l e2» A'"
proof -
from eval_e1 wt_e1 da_e1 wf True
have "nrm E1 ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_e2 show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_e2
obtain conf_s2: "s2∷≼(G, L)" and error_free_s2: "error_free s2"
by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
from avar
have "store s2'=store s2"
by (cases s2) (simp add: avar_def2)
with avar conf_s2
have conf_s2': "s2'∷≼(G, L)"
by (cases s2) (auto simp add: avar_def2)
from avar error_free_s2
have error_free_s2': "error_free s2'"
by (cases s2) (auto simp add: avar_def2 )
have "normal s2' ⟹
G,store s2'⊢fst v∷≼elemT ∧ store s2'≤|snd v≼elemT∷≼(G, L)"
proof -
assume normal: "normal s2'"
show ?thesis
proof -
obtain vv vf x1 store1 x2 store2 store2'
where v: "v=(vv,vf)" and
s1: "s1=(x1,store1)" and
s2: "s2=(x2,store2)" and
store2': "store2'=store s2'"
by (cases v,cases s1, cases s2, cases s2') blast
have "G,store2'⊢vv∷≼elemT ∧ store2'≤|vf≼elemT∷≼(G, L)"
proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
OF wf])
from s1 s2 eval_e2 show "G⊢(x1, store1) ─e2-≻i→ (x2, store2)"
by simp
from v normal s2 store2' avar
show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
by auto
from s2 conf_s2 show "(x2, store2)∷≼(G, L)" by simp
from s1 conf_a show "x1 = None ⟶ G,store1⊢a∷≼elemT.[]" by simp
from eval_e2 s1 s2 show "store1≤|store2" by (auto dest: eval_gext)
qed
with v s1 s2 store2'
show ?thesis
by simp
qed
qed
with conf_s2' error_free_s2' T
show ?thesis
by auto
qed
next
case (Nil s0 L accC T)
then show ?case
by (auto elim!: wt_elim_cases)
next
case (Cons s0 e v s1 es vs s2 L accC T A)
note eval_e = ‹G⊢Norm s0 ─e-≻v→ s1›
note eval_es = ‹G⊢s1 ─es≐≻vs→ s2›
note hyp_e = ‹PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)›
note hyp_es = ‹PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)›
note conf_s0 = ‹Norm s0∷≼(G, L)›
note wt = ‹⦇prg = G, cls = accC, lcl = L⦈⊢In3 (e # es)∷T›
then obtain eT esT where
wt_e: "⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT" and
wt_es: "⦇prg = G, cls = accC, lcl = L⦈⊢es∷≐esT" and
T: "T=Inr (eT#esT)"
by (rule wt_elim_cases) blast
from Cons.prems obtain E where
da_e: "⦇prg=G,cls=accC,lcl=L⦈
⊢ (dom (locals (store ((Norm s0)::state))))»In1l e» E" and
da_es: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm E »In3 es» A"
by (elim da_elim_cases) simp
from conf_s0 wt_e da_e
obtain conf_s1: "s1∷≼(G, L)" and error_free_s1: "error_free s1" and
conf_v: "normal s1 ⟶ G,store s1⊢v∷≼eT"
by (rule hyp_e [elim_format]) simp
show
"s2∷≼(G, L) ∧
(normal s2 ⟶ G,L,store s2⊢In3 (e # es)≻In3 (v # vs)∷≼T) ∧
(error_free (Norm s0) = error_free s2)"
proof (cases "normal s1")
case False
with eval_es have "s2=s1" by auto
with False conf_s1 error_free_s1
show ?thesis
by auto
next
case True
obtain A' where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »In3 es» A'"
proof -
from eval_e wt_e da_e wf True
have "nrm E ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_es show thesis
by (rule da_weakenE) (rule that)
qed
with conf_s1 wt_es
obtain conf_s2: "s2∷≼(G, L)" and
error_free_s2: "error_free s2" and
conf_vs: "normal s2 ⟶ list_all2 (conf G (store s2)) vs esT"
by (rule hyp_es [elim_format]) (simp add: error_free_s1)
moreover
from True eval_es conf_v
have conf_v': "G,store s2⊢v∷≼eT"
apply clarify
apply (rule conf_gext)
apply (auto dest: eval_gext)
done
ultimately show ?thesis using T by simp
qed
qed
from this and conf_s0 wt da show ?thesis .
qed
text ‹
›
corollary eval_type_soundE [consumes 5]:
assumes eval: "G⊢s0 ─t≻→ (v, s1)"
and conf: "s0∷≼(G, L)"
and wt: "⦇prg = G, cls = accC, lcl = L⦈⊢t∷T"
and da: "⦇prg = G, cls = accC, lcl = L⦈⊢ dom (locals (snd s0)) »t» A"
and wf: "wf_prog G"
and elim: "⟦s1∷≼(G, L); normal s1 ⟹ G,L,snd s1⊢t≻v∷≼T;
error_free s0 = error_free s1⟧ ⟹ P"
shows "P"
using eval wt da wf conf
by (rule eval_type_sound [elim_format]) (iprover intro: elim)
corollary eval_ts:
"⟦G⊢s ─e-≻v → s'; wf_prog G; s∷≼(G,L); ⦇prg=G,cls=C,lcl=L⦈⊢e∷-T;
⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»In1l e»A⟧
⟹ s'∷≼(G,L) ∧ (normal s' ⟶ G,store s'⊢v∷≼T) ∧
(error_free s = error_free s')"
apply (drule (4) eval_type_sound)
apply clarsimp
done
corollary evals_ts:
"⟦G⊢s ─es≐≻vs→ s'; wf_prog G; s∷≼(G,L); ⦇prg=G,cls=C,lcl=L⦈⊢es∷≐Ts;
⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»In3 es»A⟧
⟹ s'∷≼(G,L) ∧ (normal s' ⟶ list_all2 (conf G (store s')) vs Ts) ∧
(error_free s = error_free s')"
apply (drule (4) eval_type_sound)
apply clarsimp
done
corollary evar_ts:
"⟦G⊢s ─v=≻vf→ s'; wf_prog G; s∷≼(G,L); ⦇prg=G,cls=C,lcl=L⦈⊢v∷=T;
⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»In2 v»A⟧ ⟹
s'∷≼(G,L) ∧ (normal s' ⟶ G,L,(store s')⊢In2 v≻In2 vf∷≼Inl T) ∧
(error_free s = error_free s')"
apply (drule (4) eval_type_sound)
apply clarsimp
done
theorem exec_ts:
"⟦G⊢s ─c→ s'; wf_prog G; s∷≼(G,L); ⦇prg=G,cls=C,lcl=L⦈⊢c∷√;
⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»In1r c»A⟧
⟹ s'∷≼(G,L) ∧ (error_free s ⟶ error_free s')"
apply (drule (4) eval_type_sound)
apply clarsimp
done
lemma wf_eval_Fin:
assumes wf: "wf_prog G"
and wt_c1: "⦇prg = G, cls = C, lcl = L⦈⊢In1r c1∷Inl (PrimT Void)"
and da_c1: "⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store (Norm s0)))»In1r c1»A"
and conf_s0: "Norm s0∷≼(G, L)"
and eval_c1: "G⊢Norm s0 ─c1→ (x1,s1)"
and eval_c2: "G⊢Norm s1 ─c2→ s2"
and s3: "s3=abupd (abrupt_if (x1≠None) x1) s2"
shows "G⊢Norm s0 ─c1 Finally c2→ s3"
proof -
from eval_c1 wt_c1 da_c1 wf conf_s0
have "error_free (x1,s1)"
by (auto dest: eval_type_sound)
with eval_c1 eval_c2 s3
show ?thesis
by - (rule eval.Fin, auto simp add: error_free_def)
qed
subsection "Ideas for the future"
text ‹In the type soundness proof and the correctness proof of
definite assignment we perform induction on the evaluation relation with the
further preconditions that the term is welltyped and definitely assigned. During
the proofs we have to establish the welltypedness and definite assignment of
the subterms to be able to apply the induction hypothesis. So large parts of
both proofs are the same work in propagating welltypedness and definite
assignment. So we can derive a new induction rule for induction on the
evaluation of a wellformed term, were these propagations is already done, once
and forever.
Then we can do the proofs with this rule and can enjoy the time we have saved.
Here is a first and incomplete sketch of such a rule.›
theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab
Comp If]:
assumes eval: "G⊢s0 ─t≻→ (v,s1)"
and wt: "⦇prg=G,cls=accC,lcl=L⦈⊢t∷T"
and da: "⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»A"
and wf: "wf_prog G"
and abrupt: "⋀ s t abr L accC T A.
⟦⦇prg=G,cls=accC,lcl=L⦈⊢t∷T;
⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store (Some abr,s)))»t»A
⟧ ⟹ P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
and skip: "⋀ s L accC. P L accC (Norm s) ⟨Skip⟩⇩s ♢ (Norm s)"
and expr: "⋀ e s0 s1 v L accC eT E.
⟦⦇prg=G,cls=accC,lcl=L⦈⊢e∷-eT;
⦇prg=G,cls=accC,lcl=L⦈
⊢dom (locals (store ((Norm s0)::state)))»⟨e⟩⇩e»E;
P L accC (Norm s0) ⟨e⟩⇩e ⌊v⌋⇩e s1⟧
⟹ P L accC (Norm s0) ⟨Expr e⟩⇩s ♢ s1"
and lab: "⋀ c l s0 s1 L accC C.
⟦⦇prg=G,cls=accC,lcl=L⦈⊢c∷√;
⦇prg=G,cls=accC, lcl=L⦈
⊢dom (locals (store ((Norm s0)::state)))»⟨c⟩⇩s»C;
P L accC (Norm s0) ⟨c⟩⇩s ♢ s1⟧
⟹ P L accC (Norm s0) ⟨l∙ c⟩⇩s ♢ (abupd (absorb l) s1)"
and comp: "⋀ c1 c2 s0 s1 s2 L accC C1.
⟦G⊢Norm s0 ─c1 → s1;G⊢s1 ─c2 → s2;
⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√;
⦇prg=G,cls=accC,lcl=L⦈⊢c2∷√;
⦇prg=G,cls=accC,lcl=L⦈⊢
dom (locals (store ((Norm s0)::state))) »⟨c1⟩⇩s» C1;
P L accC (Norm s0) ⟨c1⟩⇩s ♢ s1;
⋀ Q. ⟦normal s1;
⋀ C2.⟦⦇prg=G,cls=accC,lcl=L⦈
⊢dom (locals (store s1)) »⟨c2⟩⇩s» C2;
P L accC s1 ⟨c2⟩⇩s ♢ s2⟧ ⟹ Q
⟧ ⟹ Q
⟧⟹ P L accC (Norm s0) ⟨c1;; c2⟩⇩s ♢ s2"
and "if": "⋀ b c1 c2 e s0 s1 s2 L accC E.
⟦G⊢Norm s0 ─e-≻b→ s1;
G⊢s1 ─(if the_Bool b then c1 else c2)→ s2;
⦇prg=G,cls=accC,lcl=L⦈⊢e∷-PrimT Boolean;
⦇prg=G, cls=accC, lcl=L⦈⊢(if the_Bool b then c1 else c2)∷√;
⦇prg=G,cls=accC,lcl=L⦈⊢
dom (locals (store ((Norm s0)::state))) »⟨e⟩⇩e» E;
P L accC (Norm s0) ⟨e⟩⇩e ⌊b⌋⇩e s1;
⋀ Q. ⟦normal s1;
⋀ C. ⟦⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s1)))
»⟨if the_Bool b then c1 else c2⟩⇩s» C;
P L accC s1 ⟨if the_Bool b then c1 else c2⟩⇩s ♢ s2
⟧ ⟹ Q
⟧ ⟹ Q
⟧ ⟹ P L accC (Norm s0) ⟨If(e) c1 Else c2⟩⇩s ♢ s2"
shows "P L accC s0 t v s1"
proof -
note inj_term_simps [simp]
from eval
have "⋀L accC T A. ⟦⦇prg=G,cls=accC,lcl=L⦈⊢t∷T;
⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s0))»t»A⟧
⟹ P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
proof (induct)
case Abrupt with abrupt show ?case .
next
case Skip from skip show ?case by simp
next
case (Expr s0 e v s1 L accC T A)
from Expr.prems obtain eT where
"⦇prg = G, cls = accC, lcl = L⦈⊢e∷-eT"
by (elim wt_elim_cases)
moreover
from Expr.prems obtain E where
"⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store ((Norm s0)::state)))»⟨e⟩⇩e»E"
by (elim da_elim_cases) simp
moreover from calculation
have "P L accC (Norm s0) ⟨e⟩⇩e ⌊v⌋⇩e s1"
by (rule Expr.hyps)
ultimately show ?case
by (rule expr)
next
case (Lab s0 c s1 l L accC T A)
from Lab.prems
have "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√"
by (elim wt_elim_cases)
moreover
from Lab.prems obtain C where
"⦇prg=G,cls=accC, lcl=L⦈⊢dom (locals (store ((Norm s0)::state)))»⟨c⟩⇩s»C"
by (elim da_elim_cases) simp
moreover from calculation
have "P L accC (Norm s0) ⟨c⟩⇩s ♢ s1"
by (rule Lab.hyps)
ultimately show ?case
by (rule lab)
next
case (Comp s0 c1 s1 c2 s2 L accC T A)
note eval_c1 = ‹G⊢Norm s0 ─c1→ s1›
note eval_c2 = ‹G⊢s1 ─c2→ s2›
from Comp.prems obtain
wt_c1: "⦇prg = G, cls = accC, lcl = L⦈⊢c1∷√" and
wt_c2: "⦇prg = G, cls = accC, lcl = L⦈⊢c2∷√"
by (elim wt_elim_cases)
from Comp.prems
obtain C1 C2
where da_c1: "⦇prg=G, cls=accC, lcl=L⦈⊢
dom (locals (store ((Norm s0)::state))) »⟨c1⟩⇩s» C1" and
da_c2: "⦇prg=G, cls=accC, lcl=L⦈⊢ nrm C1 »⟨c2⟩⇩s» C2"
by (elim da_elim_cases) simp
from wt_c1 da_c1
have P_c1: "P L accC (Norm s0) ⟨c1⟩⇩s ♢ s1"
by (rule Comp.hyps)
{
fix Q
assume normal_s1: "normal s1"
assume elim: "⋀ C2'.
⟦⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s1))»⟨c2⟩⇩s»C2';
P L accC s1 ⟨c2⟩⇩s ♢ s2⟧ ⟹ Q"
have Q
proof -
obtain C2' where
da: "⦇prg=G, cls=accC, lcl=L⦈⊢ dom (locals (store s1)) »⟨c2⟩⇩s» C2'"
proof -
from eval_c1 wt_c1 da_c1 wf normal_s1
have "nrm C1 ⊆ dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_c2 show thesis
by (rule da_weakenE) (rule that)
qed
with wt_c2 have "P L accC s1 ⟨c2⟩⇩s ♢ s2"
by (rule Comp.hyps)
with da show ?thesis
using elim by iprover
qed
}
with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1
show ?case
by (rule comp) iprover+
next
case (If s0 e b s1 c1 c2 s2 L accC T A)
note eval_e = ‹G⊢Norm s0 ─e-≻b→ s1›
note eval_then_else = ‹G⊢s1 ─(if the_Bool b then c1 else c2)→ s2›
from If.prems
obtain
wt_e: "⦇prg=G, cls=accC, lcl=L⦈⊢e∷-PrimT Boolean" and
wt_then_else: "⦇prg=G, cls=accC, lcl=L⦈⊢(if the_Bool b then c1 else c2)∷√"
by (elim wt_elim_cases) auto
from If.prems obtain E C where
da_e: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store ((Norm s0)::state)))
»⟨e⟩⇩e» E" and
da_then_else:
"⦇prg=G,cls=accC,lcl=L⦈⊢
(dom (locals (store ((Norm s0)::state))) ∪ assigns_if (the_Bool b) e)
»⟨if the_Bool b then c1 else c2⟩⇩s» C"
by (elim da_elim_cases) (cases "the_Bool b",auto)
from wt_e da_e
have P_e: "P L accC (Norm s0) ⟨e⟩⇩e ⌊b⌋⇩e s1"
by (rule If.hyps)
{
fix Q
assume normal_s1: "normal s1"
assume elim: "⋀ C. ⟦⦇prg=G,cls=accC,lcl=L⦈⊢ (dom (locals (store s1)))
»⟨if the_Bool b then c1 else c2⟩⇩s» C;
P L accC s1 ⟨if the_Bool b then c1 else c2⟩⇩s ♢ s2
⟧ ⟹ Q"
have Q
proof -
obtain C' where
da: "⦇prg=G,cls=accC,lcl=L⦈⊢
(dom (locals (store s1)))»⟨if the_Bool b then c1 else c2⟩⇩s » C'"
proof -
from eval_e have
"dom (locals (store ((Norm s0)::state))) ⊆ dom (locals (store s1))"
by (rule dom_locals_eval_mono_elim)
moreover
from eval_e normal_s1 wt_e
have "assigns_if (the_Bool b) e ⊆ dom (locals (store s1))"
by (rule assigns_if_good_approx')
ultimately
have "dom (locals (store ((Norm s0)::state)))
∪ assigns_if (the_Bool b) e ⊆ dom (locals (store s1))"
by (rule Un_least)
with da_then_else show thesis
by (rule da_weakenE) (rule that)
qed
with wt_then_else
have "P L accC s1 ⟨if the_Bool b then c1 else c2⟩⇩s ♢ s2"
by (rule If.hyps)
with da show ?thesis using elim by iprover
qed
}
with eval_e eval_then_else wt_e wt_then_else da_e P_e
show ?case
by (rule "if") iprover+
next
oops
end