# Theory TypeSafe

```(*  Title:      HOL/Bali/TypeSafe.thy
Author:     David von Oheimb and Norbert Schirmer
*)
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"

(* unused *)
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)
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) (* Init *)
apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2
check_field_access_def check_method_access_def Let_def
split del: if_split_asm split: sum3.split)
(* 6 subgoals *)
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)"
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
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)
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])
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)
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

"⟦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)"
from True
have "¬ is_static sm"
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"
with declC invC not_Null
have declC': "declC = (declclass dm)"
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
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)"
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'
show ?thesis by auto
qed
qed

― ‹Same as ‹DynT_mheadsD› but better suited for application in
typesafety proof›
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 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 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
(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  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)
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
(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 (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 (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;
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 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)"

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:
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 (rule conforms_set_locals)
apply  (simp (no_asm_simp) split: if_split)
apply (drule  (4) DynT_conf)
apply clarsimp
(* apply intro *)
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   (case_tac "is_static sm")
apply     simp
apply     simp

apply   simp
apply   (case_tac "is_static sm")
apply     simp
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
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
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)"
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"
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"
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))"
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'⦈"
from True normal_s2 s3
have "normal s3"
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")
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"

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"

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"

lemma map_upd_None_swap:
"(tab(r↦w, u↦v)) vn = None ⟹ (tab(u↦v, r↦w)) vn = None"

lemma map_eq_upd_eq: "tab vn = tab' vn ⟹ (tab(x↦y)) vn = (tab'(x↦y)) vn"

lemma map_upd_in_expansion_map_swap:
"⟦(tab(x↦y)) vn = Some z;tab vn ≠ Some z⟧
⟹  (tab'(x↦y)) vn = Some z"

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"

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)"
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
⊢ 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'"
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
(* Beweis durch Analogie/Example/Pattern?, True→False; And→Or *)
proof -
from da obtain E2' where
"⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s0)) ∪ assigns_if False e1 »⟨e2⟩⇩e» E2'"
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=```