src/HOL/Bali/TypeSafe.thy
author schirmer
Thu Oct 31 18:27:10 2002 +0100 (2002-10-31)
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 13690 ac335b2f4a39
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
     1 (*  Title:      HOL/Bali/TypeSafe.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb and Norbert Schirmer
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 header {* The type soundness proof for Java *}
     7 
     8 theory TypeSafe = DefiniteAssignmentCorrect + Conform:
     9 
    10 section "error free"
    11  
    12 lemma error_free_halloc:
    13   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    14           error_free_s0: "error_free s0"
    15   shows "error_free s1"
    16 proof -
    17   from halloc error_free_s0
    18   obtain abrupt0 store0 abrupt1 store1
    19     where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
    20           halloc': "G\<turnstile>(abrupt0,store0) \<midarrow>halloc oi\<succ>a\<rightarrow> (abrupt1,store1)" and
    21           error_free_s0': "error_free (abrupt0,store0)"
    22     by (cases s0,cases s1) auto
    23   from halloc' error_free_s0'
    24   have "error_free (abrupt1,store1)"
    25   proof (induct)
    26     case Abrupt 
    27     then show ?case .
    28   next
    29     case New
    30     then show ?case
    31       by (auto split: split_if_asm)
    32   qed
    33   with eqs 
    34   show ?thesis
    35     by simp
    36 qed
    37 
    38 lemma error_free_sxalloc:
    39   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
    40   shows "error_free s1"
    41 proof -
    42   from sxalloc error_free_s0
    43   obtain abrupt0 store0 abrupt1 store1
    44     where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
    45           sxalloc': "G\<turnstile>(abrupt0,store0) \<midarrow>sxalloc\<rightarrow> (abrupt1,store1)" and
    46           error_free_s0': "error_free (abrupt0,store0)"
    47     by (cases s0,cases s1) auto
    48   from sxalloc' error_free_s0'
    49   have "error_free (abrupt1,store1)"
    50   proof (induct)
    51   qed (auto)
    52   with eqs 
    53   show ?thesis 
    54     by simp
    55 qed
    56 
    57 lemma error_free_check_field_access_eq:
    58  "error_free (check_field_access G accC statDeclC fn stat a s)
    59  \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
    60 apply (cases s)
    61 apply (auto simp add: check_field_access_def Let_def error_free_def 
    62                       abrupt_if_def 
    63             split: split_if_asm)
    64 done
    65 
    66 lemma error_free_check_method_access_eq:
    67 "error_free (check_method_access G accC statT mode sig a' s)
    68  \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
    69 apply (cases s)
    70 apply (auto simp add: check_method_access_def Let_def error_free_def 
    71                       abrupt_if_def 
    72             split: split_if_asm)
    73 done
    74 
    75 lemma error_free_FVar_lemma: 
    76      "error_free s 
    77        \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
    78   by (case_tac s) (auto split: split_if) 
    79 
    80 lemma error_free_init_lvars [simp,intro]:
    81 "error_free s \<Longrightarrow> 
    82   error_free (init_lvars G C sig mode a pvs s)"
    83 by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
    84 
    85 lemma error_free_LVar_lemma:   
    86 "error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
    87 by (cases s) simp
    88 
    89 lemma error_free_throw [simp,intro]:
    90   "error_free s \<Longrightarrow> error_free (abupd (throw x) s)"
    91 by (cases s) (simp add: throw_def)
    92 
    93 
    94 section "result conformance"
    95 
    96 constdefs
    97   assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
    98           ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
    99 "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
   100  (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
   101  (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
   102 
   103 
   104 constdefs
   105   rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
   106           ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_"                               [71,71,71,71,71,71] 70)
   107   "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
   108     \<equiv> case T of
   109         Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
   110                   then (\<forall> n. (the_In2 t) = LVar n 
   111                          \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
   112                              (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
   113                       (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
   114                       (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
   115                   else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
   116       | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
   117 
   118 text {*
   119  With @{term rconf} we describe the conformance of the result value of a term.
   120  This definition gets rather complicated because of the relations between the
   121  injections of the different terms, types and values. The main case distinction
   122  is between single values and value lists. In case of value lists, every 
   123  value has to conform to its type. For single values we have to do a further
   124  case distinction, between values of variables @{term "\<exists>var. t=In2 var" } and
   125  ordinary values. Values of variables are modelled as pairs consisting of the
   126  current value and an update function which will perform an assignment to the
   127  variable. This stems form the decision, that we only have one evaluation rule
   128  for each kind of variable. The decision if we read or write to the 
   129  variable is made by syntactic enclosing rules. So conformance of 
   130  variable-values must ensure that both the current value and an update will 
   131  conform to the type. With the introduction of definite assignment of local
   132  variables we have to do another case distinction. For the notion of conformance
   133  local variables are allowed to be @{term None}, since the definedness is not 
   134  ensured by conformance but by definite assignment. Field and array variables 
   135  must contain a value. 
   136 *}
   137  
   138 
   139 
   140 lemma rconf_In1 [simp]: 
   141  "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
   142 apply (unfold rconf_def)
   143 apply (simp (no_asm))
   144 done
   145 
   146 lemma rconf_In2_no_LVar [simp]: 
   147  "\<forall> n. va\<noteq>LVar n \<Longrightarrow> 
   148    G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  = (G,s\<turnstile>fst vf\<Colon>\<preceq>T \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
   149 apply (unfold rconf_def)
   150 apply auto
   151 done
   152 
   153 lemma rconf_In2_LVar [simp]: 
   154  "va=LVar n \<Longrightarrow> 
   155    G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  
   156     = ((fst vf = the (locals s n)) \<and>
   157        (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst vf\<Colon>\<preceq>T) \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
   158 apply (unfold rconf_def)
   159 by simp
   160 
   161 lemma rconf_In3 [simp]: 
   162  "G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (\<lambda>v T. G,s\<turnstile>v\<Colon>\<preceq>T) vs Ts"
   163 apply (unfold rconf_def)
   164 apply (simp (no_asm))
   165 done
   166 
   167 section "fits and conf"
   168 
   169 (* unused *)
   170 lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
   171 apply (unfold fits_def)
   172 apply clarify
   173 apply (erule swap, simp (no_asm_use))
   174 apply (drule conf_RefTD)
   175 apply auto
   176 done
   177 
   178 lemma fits_conf: 
   179   "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
   180 apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
   181 apply (force dest: conf_RefTD intro: conf_AddrI)
   182 done
   183 
   184 lemma fits_Array: 
   185  "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
   186 apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
   187 apply (force dest: conf_RefTD intro: conf_AddrI)
   188 done
   189 
   190 
   191 
   192 section "gext"
   193 
   194 lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   195 apply (simp (no_asm_simp) only: split_tupled_all)
   196 apply (erule halloc.induct)
   197 apply  (auto dest!: new_AddrD)
   198 done
   199 
   200 lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   201 apply (simp (no_asm_simp) only: split_tupled_all)
   202 apply (erule sxalloc.induct)
   203 apply   (auto dest!: halloc_gext)
   204 done
   205 
   206 lemma eval_gext_lemma [rule_format (no_asm)]: 
   207  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
   208     In1 v \<Rightarrow> True  
   209   | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
   210   | In3 vs \<Rightarrow> True)"
   211 apply (erule eval_induct)
   212 prefer 26 
   213   apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
   214 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
   215  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
   216             check_field_access_def check_method_access_def Let_def
   217  split del: split_if_asm split add: sum3.split)
   218 (* 6 subgoals *)
   219 apply force+
   220 done
   221 
   222 lemma evar_gext_f: 
   223   "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
   224 apply (drule eval_gext_lemma [THEN conjunct2])
   225 apply auto
   226 done
   227 
   228 lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
   229 
   230 lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2"
   231 apply (drule eval_gext)
   232 apply auto
   233 done
   234 
   235 lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
   236 apply (erule eval_cases , auto split del: split_if_asm)
   237 apply (case_tac "inited C (globs s1)")
   238 apply  (clarsimp split del: split_if_asm)+
   239 apply (drule eval_gext')+
   240 apply (drule init_class_obj_inited)
   241 apply (erule inited_gext)
   242 apply (simp (no_asm_use))
   243 done
   244 
   245 
   246 section "Lemmas"
   247 
   248 lemma obj_ty_obj_class1: 
   249  "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
   250 apply (case_tac "tag obj")
   251 apply (auto simp add: obj_ty_def obj_class_def)
   252 done
   253 
   254 lemma oconf_init_obj: 
   255  "\<lbrakk>wf_prog G;  
   256  (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
   257 \<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   258 apply (auto intro!: oconf_init_obj_lemma unique_fields)
   259 done
   260 
   261 lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
   262   wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   263                         | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   264   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   265 apply (unfold init_obj_def)
   266 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   267             simp add: obj.update_defs)
   268 done
   269 
   270 lemma conforms_init_class_obj: 
   271  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   272   (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
   273 apply (rule not_initedD [THEN conforms_newG])
   274 apply    (auto)
   275 done
   276 
   277 
   278 lemma fst_init_lvars[simp]: 
   279  "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
   280   (if is_static m then x else (np a') x)"
   281 apply (simp (no_asm) add: init_lvars_def2)
   282 done
   283 
   284 
   285 lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
   286   is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
   287 apply (simp (no_asm_simp) only: split_tupled_all)
   288 apply (case_tac "aa")
   289 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
   290        intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
   291 done
   292 
   293 lemma halloc_type_sound: 
   294 "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
   295   T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
   296   (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
   297 apply (auto elim!: halloc_conforms)
   298 apply (case_tac "aa")
   299 apply (subst obj_ty_eq)
   300 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   301 done
   302 
   303 lemma sxalloc_type_sound: 
   304  "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> 
   305   case fst s1 of  
   306     None \<Rightarrow> s2 = s1 
   307   | Some abr \<Rightarrow> (case abr of
   308                    Xcpt x \<Rightarrow> (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> 
   309                                   (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))
   310                  | Jump j \<Rightarrow> s2 = s1
   311                  | Error e \<Rightarrow> s2 = s1)"
   312 apply (simp (no_asm_simp) only: split_tupled_all)
   313 apply (erule sxalloc.induct)
   314 apply   auto
   315 apply (rule halloc_conforms [THEN conforms_xconf])
   316 apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   317 done
   318 
   319 lemma wt_init_comp_ty: 
   320 "is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
   321 apply (unfold init_comp_ty_def)
   322 apply (clarsimp simp add: accessible_in_RefT_simp 
   323                           is_acc_type_def is_acc_class_def)
   324 done
   325 
   326 
   327 declare fun_upd_same [simp]
   328 
   329 declare fun_upd_apply [simp del]
   330 
   331 
   332 constdefs
   333   DynT_prop::"[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" 
   334                                               ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
   335  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
   336                      (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
   337 
   338 lemma DynT_propI: 
   339  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
   340   \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   341 proof (unfold DynT_prop_def)
   342   assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
   343      and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
   344      and            wf: "wf_prog G"
   345      and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   346   let ?invCls = "(invocation_class mode s a' statT)"
   347   let ?IntVir = "mode = IntVir"
   348   let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
   349                           (if \<exists>T. statT = ArrayT T
   350                                   then invCls = Object
   351                                   else G\<turnstile>Class invCls\<preceq>RefT statT)"
   352   show "?IntVir \<longrightarrow> ?Concl ?invCls"
   353   proof  
   354     assume modeIntVir: ?IntVir 
   355     with mode have not_Null: "a' \<noteq> Null" ..
   356     from statT_a' not_Null state_conform 
   357     obtain a obj 
   358       where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
   359                         "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
   360       by (blast dest: conforms_RefTD)
   361     show "?Concl ?invCls"
   362     proof (cases "tag obj")
   363       case CInst
   364       with modeIntVir obj_props
   365       show ?thesis 
   366 	by (auto dest!: widen_Array2 split add: split_if)
   367     next
   368       case Arr
   369       from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
   370       moreover from Arr have "obj_class obj = Object" 
   371 	by (blast dest: obj_class_Arr1)
   372       moreover note modeIntVir obj_props wf 
   373       ultimately show ?thesis by (auto dest!: widen_Array )
   374     qed
   375   qed
   376 qed
   377 
   378 lemma invocation_methd:
   379 "\<lbrakk>wf_prog G; statT \<noteq> NullT; 
   380  (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
   381  (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
   382  (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
   383  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
   384  dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
   385 \<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
   386 proof -
   387   assume         wf: "wf_prog G"
   388      and  not_NullT: "statT \<noteq> NullT"
   389      and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   390      and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
   391      and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
   392      and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   393      and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
   394                       = Some m"
   395   show ?thesis
   396   proof (cases statT)
   397     case NullT
   398     with not_NullT show ?thesis by simp
   399   next
   400     case IfaceT
   401     with statI_prop obtain I 
   402       where    statI: "statT = IfaceT I" and 
   403             is_iface: "is_iface G I"     and
   404           not_SuperM: "mode \<noteq> SuperM" by blast            
   405     
   406     show ?thesis 
   407     proof (cases mode)
   408       case Static
   409       with wf dynlookup statI is_iface 
   410       show ?thesis
   411 	by (auto simp add: invocation_declclass_def dynlookup_def 
   412                            dynimethd_def dynmethd_C_C 
   413 	            intro: dynmethd_declclass
   414 	            dest!: wf_imethdsD
   415                      dest: table_of_map_SomeI
   416                     split: split_if_asm)
   417     next	
   418       case SuperM
   419       with not_SuperM show ?thesis ..
   420     next
   421       case IntVir
   422       with wf dynlookup IfaceT invC_prop show ?thesis 
   423 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   424                            DynT_prop_def
   425 	            intro: methd_declclass dynmethd_declclass
   426 	            split: split_if_asm)
   427     qed
   428   next
   429     case ClassT
   430     show ?thesis
   431     proof (cases mode)
   432       case Static
   433       with wf ClassT dynlookup statC_prop 
   434       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   435                                intro: dynmethd_declclass)
   436     next
   437       case SuperM
   438       with wf ClassT dynlookup statC_prop 
   439       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   440                                intro: dynmethd_declclass)
   441     next
   442       case IntVir
   443       with wf ClassT dynlookup statC_prop invC_prop 
   444       show ?thesis
   445 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   446                            DynT_prop_def
   447 	            intro: dynmethd_declclass)
   448     qed
   449   next
   450     case ArrayT
   451     show ?thesis
   452     proof (cases mode)
   453       case Static
   454       with wf ArrayT dynlookup show ?thesis
   455 	by (auto simp add: invocation_declclass_def dynlookup_def 
   456                            dynimethd_def dynmethd_C_C
   457                     intro: dynmethd_declclass
   458                      dest: table_of_map_SomeI)
   459     next
   460       case SuperM
   461       with ArrayT statA_prop show ?thesis by blast
   462     next
   463       case IntVir
   464       with wf ArrayT dynlookup invC_prop show ?thesis
   465 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   466                            DynT_prop_def dynmethd_C_C
   467                     intro: dynmethd_declclass
   468                      dest: table_of_map_SomeI)
   469     qed
   470   qed
   471 qed
   472 
   473 lemma DynT_mheadsD: 
   474 "\<lbrakk>G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT; 
   475   wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
   476   (statDeclT,sm) \<in> mheads G C statT sig; 
   477   invC = invocation_class (invmode sm e) s a' statT;
   478   declC =invocation_declclass G (invmode sm e) s a' statT sig
   479  \<rbrakk> \<Longrightarrow> 
   480   \<exists> dm. 
   481   methd G declC sig = Some dm \<and> dynlookup G statT invC sig = Some dm  \<and> 
   482   G\<turnstile>resTy (mthd dm)\<preceq>resTy sm \<and> 
   483   wf_mdecl G declC (sig, mthd dm) \<and>
   484   declC = declclass dm \<and>
   485   is_static dm = is_static sm \<and>  
   486   is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
   487   (if invmode sm e = IntVir
   488       then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   489       else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   490             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
   491             statDeclT = ClassT (declclass dm))"
   492 proof -
   493   assume invC_prop: "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" 
   494      and        wf: "wf_prog G" 
   495      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   496      and        sm: "(statDeclT,sm) \<in> mheads G C statT sig" 
   497      and      invC: "invC = invocation_class (invmode sm e) s a' statT"
   498      and     declC: "declC = 
   499                     invocation_declclass G (invmode sm e) s a' statT sig"
   500   from wt_e wf have type_statT: "is_type G (RefT statT)"
   501     by (auto dest: ty_expr_is_type)
   502   from sm have not_Null: "statT \<noteq> NullT" by auto
   503   from type_statT 
   504   have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   505     by (auto)
   506   from type_statT wt_e 
   507   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   508                                         invmode sm e \<noteq> SuperM)"
   509     by (auto dest: invocationTypeExpr_noClassD)
   510   from wt_e
   511   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode sm e \<noteq> SuperM)"
   512     by (auto dest: invocationTypeExpr_noClassD)
   513   show ?thesis
   514   proof (cases "invmode sm e = IntVir")
   515     case True
   516     with invC_prop not_Null
   517     have invC_prop': " is_class G invC \<and> 
   518                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
   519                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
   520       by (auto simp add: DynT_prop_def) 
   521     from True 
   522     have "\<not> is_static sm"
   523       by (simp add: invmode_IntVir_eq member_is_static_simp)
   524     with invC_prop' not_Null
   525     have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
   526       by (cases statT) auto
   527     with sm wf type_statT obtain dm where
   528            dm: "dynlookup G statT invC sig = Some dm" and
   529       resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy sm"      and
   530        static: "is_static dm = is_static sm"
   531       by  - (drule dynamic_mheadsD,force+)
   532     with declC invC not_Null 
   533     have declC': "declC = (declclass dm)" 
   534       by (auto simp add: invocation_declclass_def)
   535     with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
   536     have dm': "methd G declC sig = Some dm"
   537       by - (drule invocation_methd,auto)
   538     from wf dm invC_prop' declC' type_statT 
   539     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   540       by (auto dest: dynlookup_declC)
   541     from wf dm' declC_prop declC' 
   542     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   543       by (auto dest: methd_wf_mdecl)
   544     from invC_prop' 
   545     have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
   546       by auto
   547     from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
   548          dm
   549     show ?thesis by auto
   550   next
   551     case False
   552     with type_statT wf invC not_Null wf_I wf_A
   553     have invC_prop': "is_class G invC \<and>  
   554                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   555                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object))"
   556         by (case_tac "statT") (auto simp add: invocation_class_def 
   557                                        split: inv_mode.splits)
   558     with not_Null wf
   559     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   560       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
   561                                             dynimethd_def)
   562     from sm wf wt_e not_Null False invC_prop' obtain "dm" where
   563                     dm: "methd G invC sig = Some dm"          and
   564 	eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
   565 	     eq_mheads:"sm=mhead (mthd dm) "
   566       by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
   567     then have static: "is_static dm = is_static sm" by - (auto)
   568     with declC invC dynlookup_static dm
   569     have declC': "declC = (declclass dm)"  
   570       by (auto simp add: invocation_declclass_def)
   571     from invC_prop' wf declC' dm 
   572     have dm': "methd G declC sig = Some dm"
   573       by (auto intro: methd_declclass)
   574     from dynlookup_static dm 
   575     have dm'': "dynlookup G statT invC sig = Some dm"
   576       by simp
   577     from wf dm invC_prop' declC' type_statT 
   578     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   579       by (auto dest: methd_declC )
   580     then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
   581     from wf dm' declC_prop declC' 
   582     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   583       by (auto dest: methd_wf_mdecl)
   584     from invC_prop' declC_prop declC_prop1
   585     have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   586                        \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
   587       by auto
   588     from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
   589          eq_declC_sm_dm eq_mheads static
   590     show ?thesis by auto
   591   qed
   592 qed
   593 
   594 corollary DynT_mheadsE [consumes 7]: 
   595 --{* Same as @{text DynT_mheadsD} but better suited for application in 
   596 typesafety proof   *}
   597  assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
   598      and wf: "wf_prog G" 
   599      and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   600      and mheads: "(statDeclT,sm) \<in> mheads G C statT sig"
   601      and mode: "mode=invmode sm e" 
   602      and invC: "invC = invocation_class mode s a' statT"
   603      and declC: "declC =invocation_declclass G mode s a' statT sig"
   604      and dm: "\<And> dm. \<lbrakk>methd G declC sig = Some dm; 
   605                       dynlookup G statT invC sig = Some dm; 
   606                       G\<turnstile>resTy (mthd dm)\<preceq>resTy sm; 
   607                       wf_mdecl G declC (sig, mthd dm);
   608                       declC = declclass dm;
   609                       is_static dm = is_static sm;  
   610                       is_class G invC; is_class G declC; G\<turnstile>invC\<preceq>\<^sub>C declC;  
   611                       (if invmode sm e = IntVir
   612                       then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   613                       else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   614                              \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and>
   615                              statDeclT = ClassT (declclass dm))\<rbrakk> \<Longrightarrow> P"
   616    shows "P"
   617 proof -
   618     from invC_compatible mode have "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" by simp 
   619     moreover note wf wt_e mheads
   620     moreover from invC mode 
   621     have "invC = invocation_class (invmode sm e) s a' statT" by simp
   622     moreover from declC mode 
   623     have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
   624     ultimately show ?thesis
   625       by (rule DynT_mheadsD [THEN exE,rule_format])
   626          (elim conjE,rule dm)
   627 qed
   628    
   629 
   630 lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
   631  isrtype G (statT);
   632  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
   633   mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   634                     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
   635  \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
   636 apply (case_tac "mode = IntVir")
   637 apply (drule conf_RefTD)
   638 apply (force intro!: conf_AddrI 
   639             simp add: obj_class_def split add: obj_tag.split_asm)
   640 apply  clarsimp
   641 apply  safe
   642 apply    (erule (1) widen.subcls [THEN conf_widen])
   643 apply    (erule wf_ws_prog)
   644 
   645 apply    (frule widen_Object) apply (erule wf_ws_prog)
   646 apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
   647 done
   648 
   649 lemma Ass_lemma:
   650 "\<lbrakk> G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2;
   651    G,s2\<turnstile>v\<Colon>\<preceq>eT;s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk>
   652 \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and>
   653       (normal (assign f v (Norm s2)) \<longrightarrow> G,store (assign f v (Norm s2))\<turnstile>v\<Colon>\<preceq>eT)"
   654 apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
   655 apply (drule eval_gext', clarsimp)
   656 apply (erule conf_gext)
   657 apply simp
   658 done
   659 
   660 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
   661     x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
   662 apply (auto split add: split_abrupt_if simp add: throw_def2)
   663 apply (erule conforms_xconf)
   664 apply (frule conf_RefTD)
   665 apply (auto elim: widen.subcls [THEN conf_widen])
   666 done
   667 
   668 lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
   669  (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
   670  \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
   671 apply (rule conforms_allocL)
   672 apply  (erule conforms_NormI)
   673 apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
   674 apply (auto intro!: conf_AddrI)
   675 done
   676 
   677 lemma Fin_lemma: 
   678 "\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L);
   679   dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
   680 \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   681 apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   682 done
   683 
   684 lemma FVar_lemma1: 
   685 "\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
   686   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; 
   687   statDeclC \<noteq> Object; 
   688   class G statDeclC = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; 
   689   inited statDeclC (globs s1); 
   690   (if static f then id else np a) x2 = None\<rbrakk> 
   691  \<Longrightarrow>  
   692   \<exists>obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
   693                   = Some obj \<and> 
   694   var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
   695           (Inl(fn,statDeclC)) = Some (type f)"
   696 apply (drule initedD)
   697 apply (frule subcls_is_class2, simp (no_asm_simp))
   698 apply (case_tac "static f")
   699 apply  clarsimp
   700 apply  (drule (1) rev_gext_objD, clarsimp)
   701 apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
   702 apply  (rule var_tys_Some_eq [THEN iffD2])
   703 apply  clarsimp
   704 apply  (erule fields_table_SomeI, simp (no_asm))
   705 apply clarsimp
   706 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   707 apply (auto dest!: widen_Array split add: obj_tag.split)
   708 apply (rule fields_table_SomeI)
   709 apply (auto elim!: fields_mono subcls_is_class2)
   710 done
   711 
   712 lemma FVar_lemma2: "error_free state
   713        \<Longrightarrow> error_free
   714            (assign
   715              (\<lambda>v. supd
   716                    (upd_gobj
   717                      (if static field then Inr statDeclC
   718                       else Inl (the_Addr a))
   719                      (Inl (fn, statDeclC)) v))
   720              w state)"
   721 proof -
   722   assume error_free: "error_free state"
   723   obtain a s where "state=(a,s)"
   724     by (cases state) simp
   725   with error_free
   726   show ?thesis
   727     by (cases a) auto
   728 qed
   729 
   730 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   731 declare split_if     [split del] split_if_asm     [split del] 
   732         option.split [split del] option.split_asm [split del]
   733 ML_setup {*
   734 simpset_ref() := simpset() delloop "split_all_tac";
   735 claset_ref () := claset () delSWrapper "split_all_tac"
   736 *}
   737 lemma FVar_lemma: 
   738 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
   739   G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
   740   table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
   741   wf_prog G;   
   742   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class statC; 
   743   statDeclC \<noteq> Object; class G statDeclC = Some y;   
   744   (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited statDeclC (globs s1)\<rbrakk> \<Longrightarrow>  
   745   G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
   746 apply (unfold assign_conforms_def)
   747 apply (drule sym)
   748 apply (clarsimp simp add: fvar_def2)
   749 apply (drule (9) FVar_lemma1)
   750 apply (clarsimp)
   751 apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   752 apply clarsimp
   753 apply (rule conjI)
   754 apply   clarsimp
   755 apply   (drule (1) rev_gext_objD)
   756 apply   (force elim!: conforms_upd_gobj)
   757 
   758 apply   (blast intro: FVar_lemma2)
   759 done
   760 declare split_paired_All [simp] split_paired_Ex [simp] 
   761 declare split_if     [split] split_if_asm     [split] 
   762         option.split [split] option.split_asm [split]
   763 ML_setup {*
   764 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
   765 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   766 *}
   767 
   768 
   769 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
   770  the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
   771 \<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
   772 apply (erule widen_Array_Array [THEN conf_widen])
   773 apply  (erule_tac [2] wf_ws_prog)
   774 apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   775 defer apply assumption
   776 apply (force intro: var_tys_Some_eq [THEN iffD2])
   777 done
   778 
   779 lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
   780 proof record_split
   781   fix tag values more
   782   show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
   783     by auto
   784 qed
   785  
   786 lemma AVar_lemma2: "error_free state 
   787        \<Longrightarrow> error_free
   788            (assign
   789              (\<lambda>v (x, s').
   790                  ((raise_if (\<not> G,s'\<turnstile>v fits T) ArrStore) x,
   791                   upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
   792              w state)"
   793 proof -
   794   assume error_free: "error_free state"
   795   obtain a s where "state=(a,s)"
   796     by (cases state) simp
   797   with error_free
   798   show ?thesis
   799     by (cases a) auto
   800 qed
   801 
   802 lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
   803   ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
   804   (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>v\<Colon>\<preceq>Ta \<and> s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)"
   805 apply (unfold assign_conforms_def)
   806 apply (drule sym)
   807 apply (clarsimp simp add: avar_def2)
   808 apply (drule (1) conf_gext)
   809 apply (drule conf_RefTD, clarsimp)
   810 apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
   811 defer
   812 apply   (rule obj_split)
   813 apply clarify
   814 apply (frule obj_ty_widenD)
   815 apply (auto dest!: widen_Class)
   816 apply   (force dest: AVar_lemma1)
   817 
   818 apply   (force elim!: fits_Array dest: gext_objD 
   819          intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
   820 done
   821 
   822 
   823 section "Call"
   824 
   825 lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   826   wf_mhead G P sig mh;
   827   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   828   G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
   829       [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   830 apply (unfold wf_mhead_def)
   831 apply clarify
   832 apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
   833 apply (drule wf_ws_prog)
   834 apply (erule (2) conf_list_widen)
   835 done
   836 
   837 
   838 lemma lconf_map_lname [simp]: 
   839   "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
   840    =
   841   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   842 apply (unfold lconf_def)
   843 apply (auto split add: lname.splits)
   844 done
   845 
   846 lemma wlconf_map_lname [simp]: 
   847   "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
   848    =
   849   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   850 apply (unfold wlconf_def)
   851 apply (auto split add: lname.splits)
   852 done
   853 
   854 lemma lconf_map_ename [simp]:
   855   "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
   856    =
   857   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   858 apply (unfold lconf_def)
   859 apply (auto split add: ename.splits)
   860 done
   861 
   862 lemma wlconf_map_ename [simp]:
   863   "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
   864    =
   865   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   866 apply (unfold wlconf_def)
   867 apply (auto split add: ename.splits)
   868 done
   869 
   870 
   871 
   872 lemma defval_conf1 [rule_format (no_asm), elim]: 
   873   "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
   874 apply (unfold conf_def)
   875 apply (induct "T")
   876 apply (auto intro: prim_ty.induct)
   877 done
   878 
   879 lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
   880 by (auto simp add: abrupt_if_def)
   881 
   882 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   883 declare split_if     [split del] split_if_asm     [split del] 
   884         option.split [split del] option.split_asm [split del]
   885 ML_setup {*
   886 simpset_ref() := simpset() delloop "split_all_tac";
   887 claset_ref () := claset () delSWrapper "split_all_tac"
   888 *}
   889 lemma conforms_init_lvars: 
   890 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   891   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
   892   (x, s)\<Colon>\<preceq>(G, L); 
   893   methd G declC sig = Some dm;  
   894   isrtype G statT;
   895   G\<turnstile>invC\<preceq>\<^sub>C declC; 
   896   G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
   897   invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
   898   invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
   899        (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   900     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
   901   invC  = invocation_class (invmode (mhd sm) e) s a' statT;
   902   declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
   903   x\<noteq>Some (Jump Ret) 
   904  \<rbrakk> \<Longrightarrow>  
   905   init_lvars G declC sig (invmode (mhd sm) e) a'  
   906   pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
   907                 (case k of
   908                    EName e \<Rightarrow> (case e of 
   909                                  VNam v 
   910                                   \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
   911                                         (pars (mthd dm)[\<mapsto>]parTs sig)) v
   912                                | Res \<Rightarrow> Some (resTy (mthd dm)))
   913                  | This \<Rightarrow> if (is_static (mthd sm)) 
   914                               then None else Some (Class declC)))"
   915 apply (simp add: init_lvars_def2)
   916 apply (rule conforms_set_locals)
   917 apply  (simp (no_asm_simp) split add: split_if)
   918 apply (drule  (4) DynT_conf)
   919 apply clarsimp
   920 (* apply intro *)
   921 apply (drule (3) conforms_init_lvars_lemma 
   922                  [where ?lvars="(lcls (mbody (mthd dm)))"])
   923 apply (case_tac "dm",simp)
   924 apply (rule conjI)
   925 apply (unfold wlconf_def, clarify)
   926 apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
   927 apply   (case_tac "is_static sm")
   928 apply     simp
   929 apply     simp
   930 
   931 apply   simp
   932 apply   (case_tac "is_static sm")
   933 apply     simp
   934 apply     (simp add: np_no_jump)
   935 done
   936 declare split_paired_All [simp] split_paired_Ex [simp] 
   937 declare split_if     [split] split_if_asm     [split] 
   938         option.split [split] option.split_asm [split]
   939 ML_setup {*
   940 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
   941 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   942 *}
   943 
   944 
   945 subsection "accessibility"
   946 
   947 text {* 
   948 \par
   949 *} (* dummy text command to break paragraph for latex;
   950               large paragraphs exhaust memory of debian pdflatex *)
   951 
   952 theorem dynamic_field_access_ok:
   953   assumes wf: "wf_prog G" and
   954     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   955    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   956    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   957     normal_s: "normal s" and
   958         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   959            f: "accfield G accC statC fn = Some f" and
   960         dynC: "if stat then dynC=declclass f  
   961                        else dynC=obj_class (lookup_obj (store s) a)" and
   962         stat: "if stat then (is_static f) else (\<not> is_static f)"
   963   shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<and>
   964          G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   965 proof (cases "stat")
   966   case True
   967   with stat have static: "(is_static f)" by simp
   968   from True dynC 
   969   have dynC': "dynC=declclass f" by simp
   970   with f
   971   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   972     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   973   moreover
   974   from wt_e wf have "is_class G statC"
   975     by (auto dest!: ty_expr_is_type)
   976   moreover note wf dynC'
   977   ultimately have
   978      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   979     by (auto dest: fields_declC)
   980   with dynC' f static wf
   981   show ?thesis
   982     by (auto dest: static_to_dynamic_accessible_from_static
   983             dest!: accfield_accessibleD )
   984 next
   985   case False
   986   with wf conform_a not_Null conform_s dynC
   987   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   988     "is_class G dynC"
   989     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   990               dest: obj_ty_obj_class1
   991           simp add: obj_ty_obj_class )
   992   with wf f
   993   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   994     by (auto simp add: accfield_def Let_def
   995                  dest: fields_mono
   996                 dest!: table_of_remap_SomeD)
   997   moreover
   998   from f subclseq
   999   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
  1000     by (auto intro!: static_to_dynamic_accessible_from 
  1001                dest: accfield_accessibleD)
  1002   ultimately show ?thesis
  1003     by blast
  1004 qed
  1005 
  1006 lemma error_free_field_access:
  1007   assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
  1008               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  1009          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
  1010             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
  1011            conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1012             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  1013               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
  1014                 wf: "wf_prog G"   
  1015   shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
  1016 proof -
  1017   from fvar
  1018   have store_s2': "store s2'=store s2"
  1019     by (cases s2) (simp add: fvar_def2)
  1020   with fvar conf_s2 
  1021   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1022     by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1023   from eval_init 
  1024   have initd_statDeclC_s1: "initd statDeclC s1"
  1025     by (rule init_yields_initd)
  1026   with eval_e store_s2'
  1027   have initd_statDeclC_s2': "initd statDeclC s2'"
  1028     by (auto dest: eval_gext intro: inited_gext)
  1029   show ?thesis
  1030   proof (cases "normal s2'")
  1031     case False
  1032     then show ?thesis 
  1033       by (auto simp add: check_field_access_def Let_def)
  1034   next
  1035     case True
  1036     with fvar store_s2' 
  1037     have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
  1038       by (cases s2) (auto simp add: fvar_def2)
  1039     from True fvar store_s2'
  1040     have "normal s2"
  1041       by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1042     with conf_a store_s2'
  1043     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1044       by simp
  1045     from conf_a' conf_s2' True initd_statDeclC_s2' 
  1046       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1047                                    True wt_e accfield ] 
  1048     show ?thesis
  1049       by  (cases "is_static f")
  1050           (auto dest!: initedD
  1051            simp add: check_field_access_def Let_def)
  1052   qed
  1053 qed
  1054 
  1055 lemma call_access_ok:
  1056   assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
  1057       and        wf: "wf_prog G" 
  1058       and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
  1059       and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
  1060       and      invC: "invC = invocation_class (invmode statM e) s a statT"
  1061   shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
  1062   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
  1063 proof -
  1064   from wt_e wf have type_statT: "is_type G (RefT statT)"
  1065     by (auto dest: ty_expr_is_type)
  1066   from statM have not_Null: "statT \<noteq> NullT" by auto
  1067   from type_statT wt_e 
  1068   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
  1069                                         invmode statM e \<noteq> SuperM)"
  1070     by (auto dest: invocationTypeExpr_noClassD)
  1071   from wt_e
  1072   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
  1073     by (auto dest: invocationTypeExpr_noClassD)
  1074   show ?thesis
  1075   proof (cases "invmode statM e = IntVir")
  1076     case True
  1077     with invC_prop not_Null
  1078     have invC_prop': "is_class G invC \<and>  
  1079                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
  1080                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
  1081       by (auto simp add: DynT_prop_def)
  1082     with True not_Null
  1083     have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1084      by (cases statT) (auto simp add: invmode_def) 
  1085     with statM type_statT wf 
  1086     show ?thesis
  1087       by - (rule dynlookup_access,auto)
  1088   next
  1089     case False
  1090     with type_statT wf invC not_Null wf_I wf_A
  1091     have invC_prop': " is_class G invC \<and>
  1092                       ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
  1093                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
  1094         by (case_tac "statT") (auto simp add: invocation_class_def 
  1095                                        split: inv_mode.splits)
  1096     with not_Null wf
  1097     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
  1098       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
  1099                                             dynimethd_def)
  1100    from statM wf wt_e not_Null False invC_prop' obtain dynM where
  1101                 "accmethd G accC invC sig = Some dynM" 
  1102      by (auto dest!: static_mheadsD)
  1103    from invC_prop' False not_Null wf_I
  1104    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1105      by (cases statT) (auto simp add: invmode_def) 
  1106    with statM type_statT wf 
  1107     show ?thesis
  1108       by - (rule dynlookup_access,auto)
  1109   qed
  1110 qed
  1111 
  1112 lemma error_free_call_access:
  1113   assumes
  1114    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
  1115         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
  1116        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
  1117                = {((statDeclT, statM), pTs')}" and
  1118      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1119       conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1120      invProp: "normal s3 \<Longrightarrow>
  1121                 G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
  1122           s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1123                         (invmode statM e) a vs s2" and
  1124         invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
  1125     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
  1126                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
  1127           wf: "wf_prog G"
  1128   shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
  1129    = s3"
  1130 proof (cases "normal s2")
  1131   case False
  1132   with s3 
  1133   have "abrupt s3 = abrupt s2"  
  1134     by (auto simp add: init_lvars_def2)
  1135   with False
  1136   show ?thesis
  1137     by (auto simp add: check_method_access_def Let_def)
  1138 next
  1139   case True
  1140   note normal_s2 = True
  1141   with eval_args
  1142   have normal_s1: "normal s1"
  1143     by (cases "normal s1") auto
  1144   with conf_a eval_args 
  1145   have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1146     by (auto dest: eval_gext intro: conf_gext)
  1147   show ?thesis
  1148   proof (cases "a=Null \<longrightarrow> (is_static statM)")
  1149     case False
  1150     then obtain "\<not> is_static statM" "a=Null" 
  1151       by blast
  1152     with normal_s2 s3
  1153     have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
  1154       by (auto simp add: init_lvars_def2)
  1155     then show ?thesis
  1156       by (auto simp add: check_method_access_def Let_def)
  1157   next
  1158     case True
  1159     from statM 
  1160     obtain
  1161       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1162       by (blast dest: max_spec2mheads)
  1163     from True normal_s2 s3
  1164     have "normal s3"
  1165       by (auto simp add: init_lvars_def2)
  1166     then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
  1167       by (rule invProp)
  1168     with wt_e statM' wf invC
  1169     obtain dynM where 
  1170       dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1171       acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1172                           in invC dyn_accessible_from accC"
  1173       by (force dest!: call_access_ok)
  1174     moreover
  1175     from s3 invC
  1176     have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
  1177       by (cases s2,cases "invmode statM e") 
  1178          (simp add: init_lvars_def2 del: invmode_Static_eq)+
  1179     ultimately
  1180     show ?thesis
  1181       by (auto simp add: check_method_access_def Let_def)
  1182   qed
  1183 qed
  1184 
  1185 lemma map_upds_eq_length_append_simp:
  1186   "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
  1187 proof (induct ps) 
  1188   case Nil thus ?case by simp
  1189 next
  1190   case (Cons p ps tab qs)
  1191   have "length (p#ps) = length qs" .
  1192   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1193     by (cases qs) auto
  1194   from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
  1195     by (rule Cons.hyps)
  1196   with qs show ?case 
  1197     by simp
  1198 qed
  1199 
  1200 lemma map_upds_upd_eq_length_simp:
  1201   "\<And> tab qs x y. length ps = length qs 
  1202                   \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
  1203 proof (induct "ps")
  1204   case Nil thus ?case by simp
  1205 next
  1206   case (Cons p ps tab qs x y)
  1207   have "length (p#ps) = length qs" .
  1208   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1209     by (cases qs) auto
  1210   from eq_length 
  1211   have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
  1212     by (rule Cons.hyps)
  1213   with qs show ?case
  1214     by simp
  1215 qed
  1216 
  1217 
  1218 lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
  1219 by simp
  1220 
  1221 lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) z"
  1222 by (simp add: fun_upd_def)
  1223 
  1224 lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
  1225 by (cases xs) simp+
  1226 
  1227 lemma map_upds_cong_ext: 
  1228  "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) z"
  1229 proof (induct xs)
  1230   case Nil thus ?case by simp
  1231 next
  1232   case (Cons x xs tab tab' ys)
  1233   have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
  1234     by (rule Cons.hyps) (rule map_upd_cong_ext)
  1235   thus ?case
  1236     by simp
  1237 qed
  1238    
  1239 lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
  1240   by simp
  1241 
  1242 
  1243 lemma map_upds_override_cong:
  1244 "\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
  1245  (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
  1246 proof (induct ws)
  1247   case Nil thus ?case by simp
  1248 next
  1249   case (Cons w ws tab tab' zs)
  1250   have x: "x \<in> set (w#ws)" .
  1251   show ?case
  1252   proof (cases "x=w")
  1253     case True thus ?thesis
  1254       by simp (rule map_upds_cong_ext, rule map_upd_override)
  1255   next
  1256     case False
  1257     with x have "x \<in> set ws"
  1258       by simp
  1259     with Cons.hyps show ?thesis
  1260       by simp
  1261   qed
  1262 qed
  1263 
  1264 lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
  1265  shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
  1266 proof (induct ps)
  1267   case Nil thus ?case by simp
  1268 next
  1269   case (Cons p ps tab qs)
  1270   have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
  1271           =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
  1272     by (rule Cons.hyps)
  1273   moreover
  1274   have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
  1275     by (cases qs) simp+
  1276   ultimately show ?case
  1277     by simp (rule map_upds_override_cong)
  1278 qed
  1279  
  1280 
  1281 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
  1282         length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
  1283 proof (induct ps)
  1284   case Nil thus ?case by simp
  1285 next
  1286   case (Cons p ps tab qs)
  1287   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1288     by (cases qs) auto
  1289   from eq_length
  1290   have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
  1291     by (rule Cons.hyps)
  1292   with qs show ?case 
  1293     by simp
  1294 qed
  1295   
  1296   
  1297 lemma map_upds_upds_eq_length_prefix_simp:
  1298   "\<And> tab qs. length ps = length qs
  1299               \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
  1300 proof (induct ps)
  1301   case Nil thus ?case by simp
  1302 next
  1303   case (Cons p ps tab qs)
  1304   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1305     by (cases qs) auto
  1306   from eq_length 
  1307   have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
  1308     by (rule Cons.hyps)
  1309   with qs 
  1310   show ?case by simp
  1311 qed
  1312 
  1313 lemma map_upd_cut_irrelevant:
  1314 "\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<rbrakk>
  1315     \<Longrightarrow> tab vn = Some el"
  1316 by (cases "tab' vn = None") (simp add: fun_upd_def)+
  1317 
  1318 lemma map_upd_Some_expand:
  1319 "\<lbrakk>tab vn = Some z\<rbrakk>
  1320     \<Longrightarrow> \<exists> z. (tab(x\<mapsto>y)) vn = Some z"
  1321 by (simp add: fun_upd_def)
  1322 
  1323 lemma map_upds_Some_expand:
  1324 "\<And> tab ys z. \<lbrakk>tab vn = Some z\<rbrakk>
  1325     \<Longrightarrow> \<exists> z. (tab(xs[\<mapsto>]ys)) vn = Some z"
  1326 proof (induct xs)
  1327   case Nil thus ?case by simp
  1328 next
  1329   case (Cons x xs tab ys z)
  1330   have "tab vn = Some z" .
  1331   then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
  1332     by (rule map_upd_Some_expand [of tab,elim_format]) blast
  1333   hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
  1334     by (rule Cons.hyps)
  1335   thus ?case
  1336     by simp
  1337 qed
  1338 
  1339 
  1340 lemma map_upd_Some_swap:
  1341  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
  1342 by (simp add: fun_upd_def)
  1343 
  1344 lemma map_upd_None_swap:
  1345  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
  1346 by (simp add: fun_upd_def)
  1347 
  1348 
  1349 lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
  1350 by (simp add: fun_upd_def)
  1351 
  1352 lemma map_eq_upds_eq: 
  1353   "\<And> tab tab' ys. 
  1354    tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
  1355 proof (induct xs)
  1356   case Nil thus ?case by simp 
  1357 next
  1358   case (Cons x xs tab tab' ys)
  1359   have "tab vn = tab' vn" .
  1360   hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
  1361     by (rule map_eq_upd_eq)
  1362   hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
  1363     by (rule Cons.hyps)
  1364   thus ?case 
  1365     by simp
  1366 qed
  1367 
  1368 lemma map_upd_in_expansion_map_swap:
  1369  "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1370                  \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
  1371 by (simp add: fun_upd_def)
  1372 
  1373 lemma map_upds_in_expansion_map_swap:
  1374  "\<And>tab tab' ys z. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1375                  \<Longrightarrow>  (tab'(xs[\<mapsto>]ys)) vn = Some z"
  1376 proof (induct xs)
  1377   case Nil thus ?case by simp
  1378 next
  1379   case (Cons x xs tab tab' ys z)
  1380   from Cons.prems obtain 
  1381     some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
  1382     tab_not_z: "tab vn \<noteq> Some z"
  1383     by simp
  1384   show ?case
  1385   proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
  1386     case True
  1387     with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
  1388       by (rule Cons.hyps)
  1389     thus ?thesis 
  1390       by simp
  1391   next
  1392     case False
  1393     hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
  1394     moreover
  1395     from tabx_z tab_not_z
  1396     have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
  1397       by (rule map_upd_in_expansion_map_swap)
  1398     ultimately
  1399     have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
  1400       by simp
  1401     hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
  1402       by (rule map_eq_upds_eq)
  1403     with some 
  1404     show ?thesis 
  1405       by simp
  1406   qed
  1407 qed
  1408    
  1409 lemma map_upds_Some_swap: 
  1410  assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1411     shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1412 proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
  1413   case True
  1414   then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
  1415     by (rule map_upd_Some_swap [elim_format]) blast
  1416   thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1417     by (rule map_upds_Some_expand)
  1418 next
  1419   case False
  1420   with r_u
  1421   have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1422     by (rule map_upds_in_expansion_map_swap)
  1423   thus ?thesis
  1424     by simp
  1425 qed
  1426  
  1427 lemma map_upds_Some_insert:
  1428   assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
  1429     shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1430 proof (cases "\<exists> z. tab vn = Some z")
  1431   case True
  1432   then obtain z' where "tab vn = Some z'" by blast
  1433   then obtain z'' where "(tab(u\<mapsto>v)) vn = Some z''"
  1434     by (rule map_upd_Some_expand [elim_format]) blast
  1435   thus ?thesis
  1436     by (rule map_upds_Some_expand)
  1437 next
  1438   case False
  1439   hence "tab vn \<noteq> Some z" by simp
  1440   with z
  1441   have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1442     by (rule map_upds_in_expansion_map_swap)
  1443   thus ?thesis ..
  1444 qed
  1445    
  1446 lemma map_upds_None_cut:
  1447 assumes expand_None: "(tab(xs[\<mapsto>]ys)) vn = None"
  1448   shows "tab vn = None"
  1449 proof (cases "tab vn = None")
  1450   case True thus ?thesis by simp
  1451 next
  1452   case False then obtain z where "tab vn = Some z" by blast
  1453   then obtain z' where "(tab(xs[\<mapsto>]ys)) vn = Some z'"
  1454     by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
  1455   with expand_None show ?thesis
  1456     by simp
  1457 qed
  1458     
  1459 
  1460 lemma map_upds_cut_irrelevant:
  1461 "\<And> tab tab' ys. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some el; (tab'(xs[\<mapsto>]ys)) vn = None\<rbrakk>
  1462                   \<Longrightarrow> tab vn = Some el"
  1463 proof  (induct "xs")
  1464   case Nil thus ?case by simp
  1465 next
  1466   case (Cons x xs tab tab' ys)
  1467   from Cons.prems
  1468   have "(tab(x\<mapsto>hd ys)) vn = Some el"
  1469     by - (rule Cons.hyps,auto)
  1470   moreover from Cons.prems 
  1471   have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
  1472     by simp
  1473   hence "(tab'(x\<mapsto>hd ys)) vn = None"
  1474     by (rule map_upds_None_cut)
  1475   ultimately show "tab vn = Some el" 
  1476     by (rule map_upd_cut_irrelevant)
  1477 qed
  1478    
  1479 lemma dom_vname_split:
  1480  "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
  1481    = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
  1482      dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
  1483   (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
  1484 proof 
  1485   show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
  1486   proof 
  1487     fix el 
  1488     assume el_in_list: "el \<in> ?List x xs y ys"
  1489     show "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1490     proof (cases el)
  1491       case This
  1492       with el_in_list show ?thesis by (simp add: dom_def)
  1493     next
  1494       case (EName en)
  1495       show ?thesis
  1496       proof (cases en)
  1497 	case Res
  1498 	with EName el_in_list show ?thesis by (simp add: dom_def)
  1499       next
  1500 	case (VNam vn)
  1501 	with EName el_in_list show ?thesis 
  1502 	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
  1503       qed
  1504     qed
  1505   qed
  1506 next
  1507   show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
  1508   proof 
  1509     fix el 
  1510     assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1511     show "el \<in> ?List x xs y ys"
  1512     proof (cases el)
  1513       case This
  1514       with el_in_hd_tl show ?thesis by (simp add: dom_def)
  1515     next
  1516       case (EName en)
  1517       show ?thesis
  1518       proof (cases en)
  1519 	case Res
  1520 	with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
  1521       next
  1522 	case (VNam vn)
  1523 	with EName el_in_hd_tl show ?thesis 
  1524 	  by (auto simp add: dom_def intro: map_upds_Some_expand 
  1525                                             map_upds_Some_insert)
  1526       qed
  1527     qed
  1528   qed
  1529 qed
  1530 
  1531 lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
  1532 by (auto simp add: dom_def fun_upd_def)
  1533 
  1534 lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
  1535 proof (induct xs)
  1536   case Nil thus ?case by (simp add: dom_def)
  1537 next
  1538   case (Cons x xs tab ys)
  1539   have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
  1540   moreover 
  1541   have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
  1542     by (rule dom_map_upd)
  1543   ultimately
  1544   show ?case
  1545     by simp
  1546 qed
  1547  
  1548 
  1549 
  1550 lemma dom_ename_case_None_simp:
  1551  "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
  1552   apply (auto simp add: dom_def image_def )
  1553   apply (case_tac "x")
  1554   apply auto
  1555   done
  1556 
  1557 lemma dom_ename_case_Some_simp:
  1558  "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
  1559   apply (auto simp add: dom_def image_def )
  1560   apply (case_tac "x")
  1561   apply auto
  1562   done
  1563 
  1564 lemma dom_lname_case_None_simp:
  1565   "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
  1566   apply (auto simp add: dom_def image_def )
  1567   apply (case_tac "x")
  1568   apply auto
  1569   done
  1570 
  1571 lemma dom_lname_case_Some_simp:
  1572  "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
  1573   apply (auto simp add: dom_def image_def)
  1574   apply (case_tac "x")
  1575   apply auto
  1576   done
  1577 
  1578 lemmas dom_lname_ename_case_simps =  
  1579      dom_ename_case_None_simp dom_ename_case_Some_simp 
  1580      dom_lname_case_None_simp dom_lname_case_Some_simp
  1581 
  1582 lemma image_comp: 
  1583  "f ` g ` A = (f \<circ> g) ` A"
  1584 by (auto simp add: image_def)
  1585 
  1586 lemma dom_locals_init_lvars: 
  1587   assumes m: "m=(mthd (the (methd G C sig)))"  
  1588   shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
  1589            = parameters m"
  1590 proof -
  1591   from m
  1592   have static_m': "is_static m = static m"
  1593     by simp
  1594   have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
  1595     by (simp add: dom_map_upds)
  1596   show ?thesis
  1597   proof (cases "static m")
  1598     case True
  1599     with static_m' dom_vnames m
  1600     show ?thesis
  1601       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1602                               dom_lname_ename_case_simps image_comp)
  1603   next
  1604     case False
  1605     with static_m' dom_vnames m
  1606     show ?thesis
  1607       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1608                               dom_lname_ename_case_simps image_comp)
  1609   qed
  1610 qed
  1611 
  1612 lemma da_e2_BinOp:
  1613   assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1614                   \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
  1615     and wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T"
  1616     and wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" 
  1617     and wt_binop: "wt_binop G binop e1T e2T" 
  1618     and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1619     and normal_s1: "normal s1"
  1620     and	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
  1621     and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
  1622     and wf: "wf_prog G"
  1623   shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1624          \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1625 proof -
  1626   note inj_term_simps [simp]
  1627   from da obtain E1 where
  1628     da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
  1629     by cases simp+
  1630   obtain E2 where
  1631     "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1632       \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1633   proof (cases "need_second_arg binop v1")
  1634     case False
  1635     obtain S where
  1636       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1637                   \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>Skip\<rangle>\<^sub>s\<guillemotright> S"
  1638       by (auto intro: da_Skip [simplified] assigned.select_convs)
  1639     thus ?thesis
  1640       using that by (simp add: False)
  1641   next
  1642     case True
  1643     from eval_e1 have 
  1644       s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1645       by (rule dom_locals_eval_mono_elim)
  1646     {
  1647       assume condAnd: "binop=CondAnd"
  1648       have ?thesis
  1649       proof -
  1650 	from da obtain E2' where
  1651 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1652              \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1653 	  by cases (simp add: condAnd)+
  1654 	moreover
  1655 	have "dom (locals (store s0)) 
  1656           \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1657 	proof -
  1658 	  from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
  1659 	    by simp
  1660 	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1661 	    by (auto dest: conf_Boolean)
  1662 	  with True condAnd
  1663 	  have v1: "v1=Bool True"
  1664 	    by simp
  1665 	  from eval_e1 normal_s1 
  1666 	  have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1667 	    by (rule assigns_if_good_approx' [elim_format])
  1668 	       (insert wt_e1, simp_all add: e1T v1)
  1669 	  with s0_s1 show ?thesis by (rule Un_least)
  1670 	qed
  1671 	ultimately
  1672 	show ?thesis
  1673 	  using that by (cases rule: da_weakenE) (simp add: True)
  1674       qed
  1675     }
  1676     moreover
  1677     { 
  1678       assume condOr: "binop=CondOr"
  1679       have ?thesis
  1680 	(* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
  1681       proof -
  1682 	from da obtain E2' where
  1683 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1684               \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1685 	  by cases (simp add: condOr)+
  1686 	moreover
  1687 	have "dom (locals (store s0)) 
  1688                      \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1689 	proof -
  1690 	  from condOr wt_binop have e1T: "e1T=PrimT Boolean"
  1691 	    by simp
  1692 	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1693 	    by (auto dest: conf_Boolean)
  1694 	  with True condOr
  1695 	  have v1: "v1=Bool False"
  1696 	    by simp
  1697 	  from eval_e1 normal_s1 
  1698 	  have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1699 	    by (rule assigns_if_good_approx' [elim_format])
  1700 	       (insert wt_e1, simp_all add: e1T v1)
  1701 	  with s0_s1 show ?thesis by (rule Un_least)
  1702 	qed
  1703 	ultimately
  1704 	show ?thesis
  1705 	  using that by (rule da_weakenE) (simp add: True)
  1706       qed
  1707     }
  1708     moreover
  1709     {
  1710       assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
  1711       have ?thesis
  1712       proof -
  1713 	from da notAndOr obtain E1' where
  1714           da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1715                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
  1716 	  and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
  1717 	  by cases simp+
  1718 	from eval_e1 wt_e1 da_e1 wf normal_s1 
  1719 	have "nrm E1' \<subseteq> dom (locals (store s1))"
  1720 	  by (cases rule: da_good_approxE') rules
  1721 	with da_e2 show ?thesis
  1722 	  using that by (rule da_weakenE) (simp add: True)
  1723       qed
  1724     }
  1725     ultimately show ?thesis
  1726       by (cases binop) auto
  1727   qed
  1728   thus ?thesis ..
  1729 qed
  1730 
  1731 section "main proof of type safety"
  1732     
  1733 lemma eval_type_sound:
  1734   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1735    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  1736    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  1737    and      wf: "wf_prog G" 
  1738    and conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1739   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1740          (error_free s0 = error_free s1)"
  1741 proof -
  1742   note inj_term_simps [simp]
  1743   let ?TypeSafeObj = "\<lambda> s0 s1 t v. 
  1744           \<forall>  L accC T A. s0\<Colon>\<preceq>(G,L) \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T
  1745                       \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A  
  1746                       \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1747                           \<and> (error_free s0 = error_free s1)"
  1748   from eval 
  1749   have "\<And> L accC T A. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  1750                       \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  1751         \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1752             \<and> (error_free s0 = error_free s1)"
  1753    (is "PROP ?TypeSafe s0 s1 t v"
  1754     is "\<And> L accC T A. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1755                  \<Longrightarrow> ?DefAss L accC s0 t A 
  1756                  \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1757                      ?ErrorFree s0 s1")
  1758   proof (induct)
  1759     case (Abrupt s t xc L accC T A) 
  1760     have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
  1761     then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1762       (normal (Some xc, s) 
  1763       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
  1764       (error_free (Some xc, s) = error_free (Some xc, s))"
  1765       by (simp)
  1766   next
  1767     case (Skip s L accC T A)
  1768     have "Norm s\<Colon>\<preceq>(G, L)" and  
  1769            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
  1770     then show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1771               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1772               (error_free (Norm s) = error_free (Norm s))"
  1773       by (simp)
  1774   next
  1775     case (Expr e s0 s1 v L accC T A)
  1776     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1777     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1778     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1779     moreover
  1780     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
  1781     then obtain eT 
  1782       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1783       by (rule wt_elim_cases) (blast)
  1784     moreover
  1785     from Expr.prems obtain E where
  1786       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
  1787       by (elim da_elim_cases) simp
  1788     ultimately 
  1789     obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1790       by (rule hyp [elim_format]) simp
  1791     with wt
  1792     show "s1\<Colon>\<preceq>(G, L) \<and>
  1793           (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1794           (error_free (Norm s0) = error_free s1)"
  1795       by (simp)
  1796   next
  1797     case (Lab c l s0 s1 L accC T A)
  1798     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
  1799     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1800     moreover
  1801     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
  1802     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1803       by (rule wt_elim_cases) (blast)
  1804     moreover from Lab.prems obtain C where
  1805      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
  1806       by (elim da_elim_cases) simp
  1807     ultimately
  1808     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1809            error_free_s1: "error_free s1" 
  1810       by (rule hyp [elim_format]) simp
  1811     from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
  1812       by (cases s1) (auto intro: conforms_absorb)
  1813     with wt error_free_s1
  1814     show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
  1815           (normal (abupd (absorb l) s1)
  1816            \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1817           (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
  1818       by (simp)
  1819   next
  1820     case (Comp c1 c2 s0 s1 s2 L accC T A)
  1821     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1822     have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1823     have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1824     have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
  1825     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1826     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
  1827     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1828                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1829       by (rule wt_elim_cases) (blast)
  1830     from Comp.prems
  1831     obtain C1 C2
  1832       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  1833                       dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and 
  1834             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>In1r c2\<guillemotright> C2" 
  1835       by (elim da_elim_cases) simp
  1836     from conf_s0 wt_c1 da_c1
  1837     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1838            error_free_s1: "error_free s1"
  1839       by (rule hyp_c1 [elim_format]) simp
  1840     show "s2\<Colon>\<preceq>(G, L) \<and>
  1841           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1842           (error_free (Norm s0) = error_free s2)"
  1843     proof (cases "normal s1")
  1844       case False
  1845       with eval_c2 have "s2=s1" by auto
  1846       with conf_s1 error_free_s1 False wt show ?thesis
  1847 	by simp
  1848     next
  1849       case True
  1850       obtain C2' where 
  1851 	"\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
  1852       proof -
  1853 	from eval_c1 wt_c1 da_c1 wf True
  1854 	have "nrm C1 \<subseteq> dom (locals (store s1))"
  1855 	  by (cases rule: da_good_approxE') rules
  1856 	with da_c2 show ?thesis
  1857 	  by (rule da_weakenE)
  1858       qed
  1859       with conf_s1 wt_c2 
  1860       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1861 	by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
  1862       thus ?thesis
  1863 	using wt by simp
  1864     qed
  1865   next
  1866     case (If b c1 c2 e s0 s1 s2 L accC T)
  1867     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1868     have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1869     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1870     have hyp_then_else: 
  1871             "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
  1872     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1873     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
  1874     then obtain 
  1875               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1876       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1877       (*
  1878                 wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1879                 wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
  1880       by (rule wt_elim_cases) (auto split add: split_if)
  1881     from If.prems obtain E C where
  1882       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  1883                                        \<guillemotright>In1l e\<guillemotright> E" and
  1884       da_then_else: 
  1885       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1886          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  1887           \<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C"
  1888      (*
  1889      da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1890                                       \<union> assigns_if True e) \<guillemotright>In1r c1\<guillemotright> C1" and
  1891      da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1892                                        \<union> assigns_if False e) \<guillemotright>In1r c2\<guillemotright> C2" *)
  1893       by (elim da_elim_cases) (cases "the_Bool b",auto)
  1894     from conf_s0 wt_e da_e  
  1895     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1896       by (rule hyp_e [elim_format]) simp
  1897     show "s2\<Colon>\<preceq>(G, L) \<and>
  1898            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1899            (error_free (Norm s0) = error_free s2)"
  1900     proof (cases "normal s1")
  1901       case False
  1902       with eval_then_else have "s2=s1" by auto
  1903       with conf_s1 error_free_s1 False wt show ?thesis
  1904 	by simp
  1905     next
  1906       case True
  1907       obtain C' where
  1908 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1909           (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
  1910       proof -
  1911 	from eval_e have 
  1912 	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1913 	  by (rule dom_locals_eval_mono_elim)
  1914         moreover
  1915 	from eval_e True wt_e 
  1916 	have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1917 	  by (rule assigns_if_good_approx')
  1918 	ultimately 
  1919 	have "dom (locals (store ((Norm s0)::state))) 
  1920                 \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1921 	  by (rule Un_least)
  1922 	with da_then_else show ?thesis
  1923 	  by (rule da_weakenE)
  1924       qed
  1925       with conf_s1 wt_then_else  
  1926       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1927 	by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
  1928       with wt show ?thesis
  1929 	by simp
  1930     qed
  1931     -- {* Note that we don't have to show that @{term b} really is a boolean 
  1932           value. With @{term the_Bool} we enforce to get a value of boolean 
  1933           type. So execution will be type safe, even if b would be
  1934           a string, for example. We might not expect such a behaviour to be
  1935           called type safe. To remedy the situation we would have to change
  1936           the evaulation rule, so that it only has a type safe evaluation if
  1937           we actually get a boolean value for the condition. That b is actually
  1938           a boolean value is part of @{term hyp_e}. See also Loop 
  1939        *}
  1940   next
  1941     case (Loop b c e l s0 s1 s2 s3 L accC T A)
  1942     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1943     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1944     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1945     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1946     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1947                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1948       by (rule wt_elim_cases) (blast)
  1949     have da:"\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1950             \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A".
  1951     then
  1952     obtain E C where
  1953       da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1954               \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E" and
  1955       da_c: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1956               \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1957                    \<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C" 
  1958       by (rule da_elim_cases) simp
  1959     from conf_s0 wt_e da_e 
  1960     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1961       by (rule hyp_e [elim_format]) simp
  1962     show "s3\<Colon>\<preceq>(G, L) \<and>
  1963           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1964           (error_free (Norm s0) = error_free s3)"
  1965     proof (cases "normal s1")
  1966       case True
  1967       note normal_s1 = this
  1968       show ?thesis
  1969       proof (cases "the_Bool b")
  1970 	case True
  1971 	with Loop.hyps  obtain
  1972           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  1973           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1974 	  by simp 
  1975 	have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
  1976 	  using Loop.hyps True by simp
  1977 	note hyp_c = this [rule_format]
  1978 	have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
  1979           s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1980 	  using Loop.hyps True by simp
  1981 	note hyp_w = this [rule_format]
  1982 	from eval_e have 
  1983 	  s0_s1: "dom (locals (store ((Norm s0)::state)))
  1984                     \<subseteq> dom (locals (store s1))"
  1985 	  by (rule dom_locals_eval_mono_elim)
  1986 	obtain C' where
  1987 	  "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
  1988 	proof -
  1989 	  note s0_s1
  1990           moreover
  1991 	  from eval_e normal_s1 wt_e 
  1992 	  have "assigns_if True e \<subseteq> dom (locals (store s1))"
  1993 	    by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
  1994 	  ultimately 
  1995 	  have "dom (locals (store ((Norm s0)::state))) 
  1996                  \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
  1997 	    by (rule Un_least)
  1998 	  with da_c show ?thesis
  1999 	    by (rule da_weakenE)
  2000 	qed
  2001 	with conf_s1 wt_c  
  2002 	obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2003 	  by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  2004 	from error_free_s2 
  2005 	have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
  2006 	  by simp
  2007 	from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  2008 	  by (cases s2) (auto intro: conforms_absorb)
  2009 	moreover note wt
  2010 	moreover
  2011 	obtain A' where 
  2012           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  2013               dom (locals(store (abupd (absorb (Cont l)) s2)))
  2014                 \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A'"
  2015 	proof -
  2016 	  note s0_s1
  2017 	  also from eval_c 
  2018 	  have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  2019 	    by (rule dom_locals_eval_mono_elim)
  2020 	  also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  2021 	    by simp
  2022 	  finally
  2023           have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
  2024 	  with da show ?thesis
  2025 	    by (rule da_weakenE)
  2026 	qed
  2027 	ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  2028 	  by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
  2029 	with wt show ?thesis
  2030 	  by simp
  2031       next
  2032 	case False
  2033 	with Loop.hyps have "s3=s1" by simp
  2034 	with conf_s1 error_free_s1 wt
  2035 	show ?thesis
  2036 	  by simp
  2037       qed
  2038     next
  2039       case False
  2040       have "s3=s1"
  2041       proof -
  2042 	from False obtain abr where abr: "abrupt s1 = Some abr"
  2043 	  by (cases s1) auto
  2044 	from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2045 	  by (rule eval_expression_no_jump 
  2046                [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified]) 
  2047              (simp_all add: wf)
  2048 	    
  2049 	show ?thesis
  2050 	proof (cases "the_Bool b")
  2051 	  case True  
  2052 	  with Loop.hyps obtain
  2053             eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  2054             eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  2055 	    by simp
  2056 	  from eval_c abr have "s2=s1" by auto
  2057 	  moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  2058 	    by (cases s1) (simp add: absorb_def)
  2059 	  ultimately show ?thesis
  2060 	    using eval_while abr
  2061 	    by auto
  2062 	next
  2063 	  case False
  2064 	  with Loop.hyps show ?thesis by simp
  2065 	qed
  2066       qed
  2067       with conf_s1 error_free_s1 wt
  2068       show ?thesis
  2069 	by simp
  2070     qed
  2071   next
  2072     case (Jmp j s L accC T A)
  2073     have "Norm s\<Colon>\<preceq>(G, L)" .
  2074     moreover
  2075     from Jmp.prems 
  2076     have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
  2077       by (elim da_elim_cases)
  2078     ultimately have "(Some (Jump j), s)\<Colon>\<preceq>(G, L)" by auto
  2079     then 
  2080     show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  2081            (normal (Some (Jump j), s) 
  2082            \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Jmp j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2083            (error_free (Norm s) = error_free (Some (Jump j), s))"
  2084       by simp
  2085   next
  2086     case (Throw a e s0 s1 L accC T A)
  2087     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  2088     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  2089     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2090     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
  2091     then obtain tn 
  2092       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  2093             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  2094       by (rule wt_elim_cases) (auto)
  2095     from Throw.prems obtain E where 
  2096       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2097              \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2098       by (elim da_elim_cases) simp
  2099     from conf_s0 wt_e da_e obtain
  2100       "s1\<Colon>\<preceq>(G, L)" and
  2101       "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  2102       error_free_s1: "error_free s1"
  2103       by (rule hyp [elim_format]) simp
  2104     with wf throwable
  2105     have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  2106       by (cases s1) (auto dest: Throw_lemma)
  2107     with wt error_free_s1
  2108     show "abupd (throw a) s1\<Colon>\<preceq>(G, L) \<and>
  2109             (normal (abupd (throw a) s1) \<longrightarrow>
  2110             G,L,store (abupd (throw a) s1)\<turnstile>In1r (Throw e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2111             (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  2112       by simp
  2113   next
  2114     case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T A)
  2115     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  2116     have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  2117     have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  2118     have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
  2119     have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  2120     then obtain 
  2121       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2122       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  2123       fresh_vn: "L(VName vn)=None"
  2124       by (rule wt_elim_cases) simp
  2125     from Try.prems obtain C1 C2 where
  2126       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2127                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1"  and
  2128       da_c2:
  2129        "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2130         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>In1r c2\<guillemotright> C2"
  2131       by (elim da_elim_cases) simp
  2132     from conf_s0 wt_c1 da_c1
  2133     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2134       by (rule hyp_c1 [elim_format]) simp
  2135     from conf_s1 sx_alloc wf 
  2136     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  2137       by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits)
  2138     from sx_alloc error_free_s1 
  2139     have error_free_s2: "error_free s2"
  2140       by (rule error_free_sxalloc)
  2141     show "s3\<Colon>\<preceq>(G, L) \<and>
  2142           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  2143           (error_free (Norm s0) = error_free s3)"
  2144     proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
  2145       case False
  2146       from sx_alloc wf
  2147       have eq_s2_s1: "s2=s1"
  2148 	by (rule sxalloc_type_sound [elim_format])
  2149 	   (insert False, auto split: option.splits abrupt.splits )
  2150       with False 
  2151       have "\<not>  G,s2\<turnstile>catch catchC"
  2152 	by (simp add: catch_def)
  2153       with Try
  2154       have "s3=s2"
  2155 	by simp
  2156       with wt conf_s1 error_free_s1 eq_s2_s1
  2157       show ?thesis
  2158 	by simp
  2159     next
  2160       case True
  2161       note exception_s1 = this
  2162       show ?thesis
  2163       proof (cases "G,s2\<turnstile>catch catchC") 
  2164 	case False
  2165 	with Try
  2166 	have "s3=s2"
  2167 	  by simp
  2168 	with wt conf_s2 error_free_s2 
  2169 	show ?thesis
  2170 	  by simp
  2171       next
  2172 	case True
  2173 	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  2174 	from True Try.hyps
  2175 	have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  2176 	  by simp
  2177 	note hyp_c2 = this [rule_format]
  2178 	from exception_s1 sx_alloc wf
  2179 	obtain a 
  2180 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  2181 	  by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
  2182 	with True
  2183 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  2184 	  by (cases s2) simp
  2185 	with xcpt_s2 conf_s2 wf
  2186 	have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  2187 	  by (auto dest: Try_lemma)
  2188 	moreover note wt_c2
  2189 	moreover
  2190 	obtain C2' where
  2191 	  "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2192           \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2193 	proof -
  2194 	  have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  2195                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  2196           proof -
  2197             have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  2198             hence "dom (locals (store ((Norm s0)::state))) 
  2199                     \<subseteq> dom (locals (store s1))"
  2200               by (rule dom_locals_eval_mono_elim)
  2201             also
  2202             from sx_alloc
  2203             have "\<dots> \<subseteq> dom (locals (store s2))"
  2204               by (rule dom_locals_sxalloc_mono)
  2205             also 
  2206             have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  2207               by (cases s2) (simp add: new_xcpt_var_def, blast) 
  2208             also
  2209             have "{VName vn} \<subseteq> \<dots>"
  2210               by (cases s2) simp
  2211             ultimately show ?thesis
  2212               by (rule Un_least)
  2213           qed
  2214 	  with da_c2 show ?thesis
  2215 	    by (rule da_weakenE)
  2216 	qed
  2217 	ultimately
  2218 	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  2219                error_free_s3: "error_free s3"
  2220 	  by (rule hyp_c2 [elim_format])
  2221              (cases s2, simp add: xcpt_s2 error_free_s2) 
  2222 	from conf_s3 fresh_vn 
  2223 	have "s3\<Colon>\<preceq>(G,L)"
  2224 	  by (blast intro: conforms_deallocL)
  2225 	with wt error_free_s3
  2226 	show ?thesis
  2227 	  by simp
  2228       qed
  2229     qed
  2230   next
  2231     case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
  2232     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  2233     have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  2234     have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
  2235                      then (x1, s1)
  2236                      else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  2237     have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
  2238     have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
  2239     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2240     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
  2241     then obtain
  2242       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2243       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  2244       by (rule wt_elim_cases) blast
  2245     from Fin.prems obtain C1 C2 where 
  2246       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2247                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
  2248       da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2249                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c2\<guillemotright> C2"
  2250       by (elim da_elim_cases) simp 
  2251     from conf_s0 wt_c1 da_c1   
  2252     obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  2253       by (rule hyp_c1 [elim_format]) simp
  2254     from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  2255       by (rule conforms_NormI)
  2256     moreover note wt_c2
  2257     moreover obtain C2'
  2258       where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2259                \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2260     proof -
  2261       from eval_c1
  2262       have "dom (locals (store ((Norm s0)::state))) 
  2263              \<subseteq> dom (locals (store (x1,s1)))"
  2264         by (rule dom_locals_eval_mono_elim)
  2265       hence "dom (locals (store ((Norm s0)::state))) 
  2266               \<subseteq> dom (locals (store ((Norm s1)::state)))"
  2267 	by simp
  2268       with da_c2 show ?thesis
  2269 	by (rule da_weakenE)
  2270     qed
  2271     ultimately
  2272     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2273       by (rule hyp_c2 [elim_format]) simp
  2274     from error_free_s1 s3 
  2275     have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  2276       by simp
  2277     show "s3\<Colon>\<preceq>(G, L) \<and>
  2278           (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  2279           (error_free (Norm s0) = error_free s3)"
  2280     proof (cases x1)
  2281       case None with conf_s2 s3' wt show ?thesis by auto
  2282     next
  2283       case (Some x) 
  2284       from eval_c2 have 
  2285 	"dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
  2286 	by (rule dom_locals_eval_mono_elim)
  2287       with Some eval_c2 wf conf_s1 conf_s2
  2288       have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  2289 	by (cases s2) (auto dest: Fin_lemma)
  2290       from Some error_free_s1
  2291       have "\<not> (\<exists> err. x=Error err)"
  2292 	by (simp add: error_free_def)
  2293       with error_free_s2
  2294       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
  2295 	by (cases s2) simp
  2296       with Some wt conf s3' show ?thesis
  2297 	by (cases s2) auto
  2298     qed
  2299   next
  2300     case (Init C c s0 s1 s2 s3 L accC T)
  2301     have     cls: "the (class G C) = c" .
  2302     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2303     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  2304     with cls
  2305     have cls_C: "class G C = Some c"
  2306       by - (erule wt_elim_cases,auto)
  2307     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2308           (error_free (Norm s0) = error_free s3)"
  2309     proof (cases "inited C (globs s0)")
  2310       case True
  2311       with Init.hyps have "s3 = Norm s0"
  2312 	by simp
  2313       with conf_s0 wt show ?thesis 
  2314 	by simp
  2315     next
  2316       case False
  2317       with Init.hyps obtain 
  2318            eval_init_super: 
  2319            "G\<turnstile>Norm ((init_class_obj G C) s0) 
  2320               \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  2321         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  2322 	s3: "s3 = (set_lvars (locals (store s1))) s2" 
  2323 	by simp
  2324       have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
  2325 	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  2326 	using False Init.hyps by simp
  2327       note hyp_init_super = this [rule_format] 
  2328       have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  2329 	using False Init.hyps by simp
  2330       note hyp_init_c = this [rule_format]
  2331       from conf_s0 wf cls_C False
  2332       have "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  2333 	by (auto dest: conforms_init_class_obj)
  2334       moreover from wf cls_C have
  2335 	wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  2336                          \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  2337 	by (cases "C=Object")
  2338            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  2339       moreover
  2340       obtain S where
  2341 	da_init_super:
  2342 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2343           \<turnstile> dom (locals (store ((Norm ((init_class_obj G C) s0))::state))) 
  2344                \<guillemotright>In1r (if C = Object then Skip else Init (super c))\<guillemotright> S"
  2345       proof (cases "C=Object")
  2346 	case True 
  2347 	with da_Skip show ?thesis
  2348 	  using that by (auto intro: assigned.select_convs)
  2349       next
  2350 	case False 
  2351 	with da_Init show ?thesis
  2352 	  by - (rule that, auto intro: assigned.select_convs)
  2353       qed
  2354       ultimately 
  2355       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2356 	by (rule hyp_init_super [elim_format]) simp
  2357       from eval_init_super wt_init_super wf
  2358       have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2359 	by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
  2360               auto)
  2361       with conf_s1
  2362       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  2363 	by (cases s1) (auto intro: conforms_set_locals)
  2364       moreover 
  2365       from error_free_s1
  2366       have error_free_empty: "error_free ((set_lvars empty) s1)"
  2367 	by simp
  2368       from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
  2369 	by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
  2370       moreover from cls_C wf obtain I
  2371 	where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
  2372 	by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
  2373        (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
  2374       then obtain I' where
  2375 	"\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
  2376             \<guillemotright>In1r (init c)\<guillemotright> I'"
  2377 	  by (rule da_weakenE) simp
  2378       ultimately
  2379       obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  2380 	by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
  2381       have "abrupt s2 \<noteq> Some (Jump Ret)"
  2382       proof -
  2383 	from s1_no_ret 
  2384 	have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
  2385 	  by simp
  2386 	moreover
  2387 	from cls_C wf have "jumpNestingOkS {} (init c)"
  2388 	  by (rule wf_prog_cdecl [THEN wf_cdeclE])
  2389 	ultimately 
  2390 	show ?thesis
  2391 	  using eval_init wt_init_c wf
  2392 	  by - (rule eval_statement_no_jump 
  2393                      [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
  2394       qed
  2395       with conf_s2 s3 conf_s1 eval_init
  2396       have "s3\<Colon>\<preceq>(G, L)"
  2397 	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  2398       moreover from error_free_s2 s3
  2399       have "error_free s3"
  2400 	by simp
  2401       moreover note wt
  2402       ultimately show ?thesis
  2403 	by simp
  2404     qed
  2405   next
  2406     case (NewC C a s0 s1 s2 L accC T A)
  2407     have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
  2408     have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
  2409     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
  2410     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2411     moreover
  2412     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  2413     then obtain is_cls_C: "is_class G C" and
  2414                        T: "T=Inl (Class C)"
  2415       by (rule wt_elim_cases) (auto dest: is_acc_classD)
  2416     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" by auto
  2417     moreover obtain I where 
  2418       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2419           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init C)\<guillemotright> I"
  2420       by (auto intro: da_Init [simplified] assigned.select_convs)
  2421      (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2422     ultimately 
  2423     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2424       by (rule hyp [elim_format]) simp 
  2425     from conf_s1 halloc wf is_cls_C
  2426     obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  2427                              "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  2428       by (cases s2) (auto dest!: halloc_type_sound)
  2429     from halloc error_free_s1 
  2430     have "error_free s2"
  2431       by (rule error_free_halloc)
  2432     with halloc_type_safe T
  2433     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2434           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (NewC C)\<succ>In1 (Addr a)\<Colon>\<preceq>T)  \<and>
  2435           (error_free (Norm s0) = error_free s2)"
  2436       by auto
  2437   next
  2438     case (NewA elT a e i s0 s1 s2 s3 L accC T A)
  2439     have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1" .
  2440     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  2441     have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
  2442     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>" .
  2443     have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
  2444     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2445     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T" .
  2446     then obtain
  2447       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
  2448       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  2449             elT: "is_type G elT" and
  2450            T: "T=Inl (elT.[])"
  2451       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  2452     from NewA.prems 
  2453     have da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2454                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2455       by (elim da_elim_cases) simp
  2456     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2457     proof -
  2458       note conf_s0 wt_init
  2459       moreover obtain I where
  2460 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2461          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
  2462       proof (cases "\<exists>C. elT = Class C")
  2463 	case True
  2464 	thus ?thesis
  2465 	  by - (rule that, (auto intro: da_Init [simplified] 
  2466                                         assigned.select_convs
  2467                               simp add: init_comp_ty_def))
  2468 	 (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2469       next
  2470 	case False
  2471 	thus ?thesis
  2472 	by - (rule that, (auto intro: da_Skip [simplified] 
  2473                                       assigned.select_convs
  2474                            simp add: init_comp_ty_def))
  2475          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
  2476       qed
  2477       ultimately show ?thesis
  2478 	by (rule hyp_init [elim_format]) auto
  2479     qed 
  2480     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2481     proof -
  2482       from eval_init 
  2483       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2484 	by (rule dom_locals_eval_mono_elim)
  2485       with da_e 
  2486       obtain A' where
  2487        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2488             \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2489 	by (rule da_weakenE)
  2490       with conf_s1 wt_size
  2491       show ?thesis
  2492 	by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
  2493     qed
  2494     from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  2495       by (cases s2) auto
  2496     with halloc wf elT 
  2497     have halloc_type_safe:
  2498           "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>elT.[])"
  2499       by (cases s3) (auto dest!: halloc_type_sound)
  2500     from halloc error_free_s2
  2501     have "error_free s3"
  2502       by (auto dest: error_free_halloc)
  2503     with halloc_type_safe T
  2504     show "s3\<Colon>\<preceq>(G, L) \<and> 
  2505           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New elT[e])\<succ>In1 (Addr a)\<Colon>\<preceq>T) \<and>
  2506           (error_free (Norm s0) = error_free s3) "
  2507       by simp
  2508   next
  2509     case (Cast castT e s0 s1 s2 v L accC T A)
  2510     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  2511     have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
  2512     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2513     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2514     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
  2515     then obtain eT
  2516       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2517               eT: "G\<turnstile>eT\<preceq>? castT" and 
  2518                T: "T=Inl castT"
  2519       by (rule wt_elim_cases) auto
  2520     from Cast.prems 
  2521     have "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2522                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2523       by (elim da_elim_cases) simp
  2524     with conf_s0 wt_e
  2525     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2526            v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2527       error_free_s1: "error_free s1"
  2528       by (rule hyp [elim_format]) simp
  2529     from conf_s1 s2 
  2530     have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  2531       by (cases s1) simp
  2532     from error_free_s1 s2
  2533     have error_free_s2: "error_free s2"
  2534       by simp
  2535     {
  2536       assume norm_s2: "normal s2"
  2537       have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
  2538       proof -
  2539 	from s2 norm_s2 have "normal s1"
  2540 	  by (cases s1) simp
  2541 	with v_ok 
  2542 	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  2543 	  by simp
  2544 	with eT wf s2 T norm_s2
  2545 	show ?thesis
  2546 	  by (cases s1) (auto dest: fits_conf)
  2547       qed
  2548     }
  2549     with conf_s2 error_free_s2
  2550     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2551            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
  2552            (error_free (Norm s0) = error_free s2)"
  2553       by blast
  2554   next
  2555     case (Inst instT b e s0 s1 v L accC T A)
  2556     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2557     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2558     from Inst.prems obtain eT
  2559     where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
  2560              T: "T=Inl (PrimT Boolean)" 
  2561       by (elim wt_elim_cases) simp
  2562     from Inst.prems 
  2563     have da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2564                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2565       by (elim da_elim_cases) simp
  2566     from conf_s0 wt_e da_e
  2567     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2568               v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>RefT eT" and
  2569       error_free_s1: "error_free s1"
  2570       by (rule hyp [elim_format]) simp
  2571     with T show ?case
  2572       by simp
  2573   next
  2574     case (Lit s v L accC T A)
  2575     then show ?case
  2576       by (auto elim!: wt_elim_cases 
  2577                intro: conf_litval simp add: empty_dt_def)
  2578   next
  2579     case (UnOp e s0 s1 unop v L accC T A)
  2580     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2581     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2582     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
  2583     then obtain eT
  2584       where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2585             wt_unop: "wt_unop unop eT" and
  2586                   T: "T=Inl (PrimT (unop_type unop))" 
  2587       by (auto elim!: wt_elim_cases)
  2588     from UnOp.prems obtain A where
  2589        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2590                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2591       by (elim da_elim_cases) simp
  2592     from conf_s0 wt_e da_e
  2593     obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2594                   wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2595          error_free_s1: "error_free s1"
  2596       by (rule hyp [elim_format]) simp
  2597     from wt_v T wt_unop
  2598     have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
  2599       by (cases unop) auto
  2600     with conf_s1 error_free_s1
  2601     show "s1\<Colon>\<preceq>(G, L) \<and>
  2602      (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
  2603      error_free (Norm s0) = error_free s1"
  2604       by simp
  2605   next
  2606     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T A)
  2607     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" .
  2608     have eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  2609                              else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
  2610     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
  2611     have hyp_e2: "PROP ?TypeSafe       s1  s2 
  2612                    (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
  2613                    (In1 v2)" .
  2614     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2615     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
  2616     then obtain e1T e2T where
  2617          wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
  2618          wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  2619       wt_binop: "wt_binop G binop e1T e2T" and
  2620              T: "T=Inl (PrimT (binop_type binop))"
  2621       by (elim wt_elim_cases) simp
  2622     have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
  2623       by simp
  2624     obtain S where
  2625       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2626                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
  2627       by (auto intro: da_Skip [simplified] assigned.select_convs)
  2628     have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
  2629                   \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A".
  2630     then obtain E1 where
  2631       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2632                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
  2633       by (elim da_elim_cases) simp+
  2634     from conf_s0 wt_e1 da_e1
  2635     obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2636                   wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  2637           error_free_s1: "error_free s1"
  2638       by (rule hyp_e1 [elim_format]) simp
  2639     from wt_binop T
  2640     have conf_v:
  2641       "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  2642       by (cases binop) auto
  2643     -- {* Note that we don't use the information that v1 really is compatible 
  2644           with the expected type e1T and v2 is compatible with e2T, 
  2645           because @{text eval_binop} will anyway produce an output of 
  2646           the right type.
  2647           So evaluating the addition of an integer with a string is type
  2648           safe. This is a little bit annoying since we may regard such a
  2649           behaviour as not type safe.
  2650           If we want to avoid this we can redefine @{text eval_binop} so that
  2651           it only produces a output of proper type if it is assigned to 
  2652           values of the expected types, and arbitrary if the inputs have 
  2653           unexpected types. The proof can easily be adapted since we
  2654           have the hypothesis that the values have a proper type.
  2655           This also applies to unary operations.
  2656        *}
  2657     from eval_e1 have 
  2658       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2659       by (rule dom_locals_eval_mono_elim)
  2660     show "s2\<Colon>\<preceq>(G, L) \<and>
  2661           (normal s2 \<longrightarrow>
  2662         G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  2663           error_free (Norm s0) = error_free s2"
  2664     proof (cases "normal s1")
  2665       case False
  2666       with eval_e2 have "s2=s1" by auto
  2667       with conf_s1 error_free_s1 False show ?thesis
  2668 	by auto
  2669     next
  2670       case True
  2671       note normal_s1 = this
  2672       show ?thesis 
  2673       proof (cases "need_second_arg binop v1")
  2674 	case False
  2675 	with normal_s1 eval_e2 have "s2=s1"
  2676 	  by (cases s1) (simp, elim eval_elim_cases,simp)
  2677 	with conf_s1 conf_v error_free_s1
  2678 	show ?thesis by simp
  2679       next
  2680 	case True
  2681 	note need_second_arg = this
  2682 	with hyp_e2 
  2683 	have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
  2684 	from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
  2685           wt_v1 [rule_format,OF normal_s1] wf
  2686 	obtain E2 where
  2687 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
  2688 	  by (rule da_e2_BinOp [elim_format]) 
  2689              (auto simp add: need_second_arg )
  2690 	with conf_s1 wt_e2 
  2691 	obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  2692 	  by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
  2693 	with conf_v show ?thesis by simp
  2694       qed
  2695     qed
  2696   next
  2697     case (Super s L accC T A)
  2698     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  2699     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  2700     then obtain C c where
  2701              C: "L This = Some (Class C)" and
  2702        neq_Obj: "C\<noteq>Object" and
  2703          cls_C: "class G C = Some c" and
  2704              T: "T=Inl (Class (super c))"
  2705       by (rule wt_elim_cases) auto
  2706     from Super.prems
  2707     obtain "This \<in> dom (locals s)"
  2708       by (elim da_elim_cases) simp
  2709     with conf_s C  have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  2710       by (auto dest: conforms_localD [THEN wlconfD])
  2711     with neq_Obj cls_C wf
  2712     have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  2713       by (auto intro: conf_widen
  2714                 dest: subcls_direct[THEN widen.subcls])
  2715     with T conf_s
  2716     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  2717            (normal (Norm s) \<longrightarrow> 
  2718               G,L,store (Norm s)\<turnstile>In1l Super\<succ>In1 (val_this s)\<Colon>\<preceq>T) \<and>
  2719            (error_free (Norm s) = error_free (Norm s))"
  2720       by simp
  2721   next
  2722     case (Acc upd s0 s1 w v L accC T A) 
  2723     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
  2724     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2725     from Acc.prems obtain vT where
  2726       wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
  2727          T: "T=Inl vT"
  2728       by (elim wt_elim_cases) simp
  2729     from Acc.prems obtain V where
  2730       da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2731                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
  2732       by (cases "\<exists> n. v=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
  2733     {
  2734       fix n assume lvar: "v=LVar n"
  2735       have "locals (store s1) n \<noteq> None"
  2736       proof -
  2737 	from Acc.prems lvar have 
  2738 	  "n \<in> dom (locals s0)"
  2739 	  by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
  2740 	also
  2741 	have "dom (locals s0) \<subseteq> dom (locals (store s1))"
  2742 	proof -
  2743 	  have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
  2744 	  thus ?thesis
  2745 	    by (rule dom_locals_eval_mono_elim) simp
  2746 	qed
  2747 	finally show ?thesis
  2748 	  by blast
  2749       qed
  2750     } note lvar_in_locals = this 
  2751     from conf_s0 wt_v da_v
  2752     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
  2753       and  conf_var: "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In2 v\<succ>In2 (w, upd)\<Colon>\<preceq>Inl vT)"
  2754       and  error_free_s1: "error_free s1"
  2755       by (rule hyp [elim_format]) simp
  2756     from lvar_in_locals conf_var T
  2757     have "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1l (Acc v)\<succ>In1 w\<Colon>\<preceq>T)"
  2758       by (cases "\<exists> n. v=LVar n") auto
  2759     with conf_s1 error_free_s1 show ?case
  2760       by simp
  2761   next
  2762     case (Ass e upd s0 s1 s2 v var w L accC T A)
  2763     have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" .
  2764     have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
  2765     have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" .
  2766     have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
  2767     have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2768     have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
  2769     then obtain varT eT where
  2770 	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  2771 	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2772 	  widen: "G\<turnstile>eT\<preceq>varT" and
  2773               T: "T=Inl eT"
  2774       by (rule wt_elim_cases) auto
  2775     show "assign upd v s2\<Colon>\<preceq>(G, L) \<and>
  2776            (normal (assign upd v s2) \<longrightarrow>
  2777             G,L,store (assign upd v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2778       (error_free (Norm s0) = error_free (assign upd v s2))"
  2779     proof (cases "\<exists> vn. var=LVar vn")
  2780       case False
  2781       with Ass.prems
  2782       obtain V E where
  2783 	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2784                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V" and
  2785 	da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  2786 	by (elim da_elim_cases) simp+
  2787       from conf_s0 wt_var da_var 
  2788       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2789 	and  conf_var: "normal s1 
  2790                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2791 	and  error_free_s1: "error_free s1"
  2792 	by (rule hyp_var [elim_format]) simp
  2793       show ?thesis
  2794       proof (cases "normal s1")
  2795 	case False
  2796 	with eval_e have "s2=s1" by auto
  2797 	with False have "assign upd v s2=s1"
  2798 	  by simp
  2799 	with conf_s1 error_free_s1 False show ?thesis
  2800 	  by auto
  2801       next
  2802 	case True
  2803 	note normal_s1=this
  2804 	obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2805                          \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2806 	proof -
  2807 	  from eval_var wt_var da_var wf normal_s1
  2808 	  have "nrm V \<subseteq>  dom (locals (store s1))"
  2809 	    by (cases rule: da_good_approxE') rules
  2810 	  with da_e show ?thesis
  2811 	    by (rule da_weakenE) 
  2812 	qed
  2813 	with conf_s1 wt_e 
  2814 	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2815           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2816           error_free_s2: "error_free s2"
  2817 	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2818 	show ?thesis 
  2819 	proof (cases "normal s2")
  2820 	  case False
  2821 	  with conf_s2 error_free_s2 
  2822 	  show ?thesis
  2823 	    by auto
  2824 	next
  2825 	  case True
  2826 	  from True conf_v
  2827 	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2828 	    by simp
  2829 	  with widen wf
  2830 	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2831 	    by (auto intro: conf_widen)
  2832 	  from normal_s1 conf_var
  2833 	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2834 	    by simp
  2835 	  then 
  2836 	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2837 	    by (simp add: rconf_def)
  2838 	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2839 	    eval_e T conf_s2 error_free_s2
  2840 	  show ?thesis
  2841 	    by (cases s1, cases s2) 
  2842 	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2843 	qed
  2844       qed
  2845     next
  2846       case True
  2847       then obtain vn where vn: "var=LVar vn"
  2848 	by blast
  2849       with Ass.prems
  2850       obtain E where
  2851 	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  2852 	           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2853 	by (elim da_elim_cases) simp+
  2854       from da.LVar vn obtain V where
  2855 	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2856                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V"
  2857 	by auto
  2858       obtain E' where
  2859 	da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2860                    \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> E'"
  2861       proof -
  2862 	have "dom (locals (store ((Norm s0)::state))) 
  2863                 \<subseteq> dom (locals (store (s1)))"
  2864 	  by (rule dom_locals_eval_mono_elim)
  2865 	with da_e show ?thesis
  2866 	  by (rule da_weakenE)
  2867       qed
  2868       from conf_s0 wt_var da_var 
  2869       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2870 	and  conf_var: "normal s1 
  2871                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2872 	and  error_free_s1: "error_free s1"
  2873 	by (rule hyp_var [elim_format]) simp
  2874       show ?thesis
  2875       proof (cases "normal s1")
  2876 	case False
  2877 	with eval_e have "s2=s1" by auto
  2878 	with False have "assign upd v s2=s1"
  2879 	  by simp
  2880 	with conf_s1 error_free_s1 False show ?thesis
  2881 	  by auto
  2882       next
  2883 	case True
  2884 	note normal_s1 = this
  2885 	from conf_s1 wt_e da_e'
  2886 	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2887           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2888           error_free_s2: "error_free s2"
  2889 	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2890 	show ?thesis 
  2891 	proof (cases "normal s2")
  2892 	  case False
  2893 	  with conf_s2 error_free_s2 
  2894 	  show ?thesis
  2895 	    by auto
  2896 	next
  2897 	  case True
  2898 	  from True conf_v
  2899 	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2900 	    by simp
  2901 	  with widen wf
  2902 	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2903 	    by (auto intro: conf_widen)
  2904 	  from normal_s1 conf_var
  2905 	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2906 	    by simp
  2907 	  then 
  2908 	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2909 	    by (simp add: rconf_def)
  2910 	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2911 	    eval_e T conf_s2 error_free_s2
  2912 	  show ?thesis
  2913 	    by (cases s1, cases s2) 
  2914 	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2915 	qed
  2916       qed
  2917     qed
  2918   next
  2919 -- {* 
  2920 \par
  2921 *} (* dummy text command to break paragraph for latex;
  2922               large paragraphs exhaust memory of debian pdflatex *)
  2923     case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A)
  2924     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  2925     have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  2926     have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
  2927     have hyp_if: "PROP ?TypeSafe s1 s2 
  2928                        (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  2929     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2930     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  2931     then obtain T1 T2 statT where
  2932       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  2933       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  2934       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  2935       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  2936       T    : "T=Inl statT"
  2937       by (rule wt_elim_cases) auto
  2938     with Cond.prems obtain E0 E1 E2 where
  2939          da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2940                   \<turnstile> dom (locals (store ((Norm s0)::state))) 
  2941                       \<guillemotright>In1l e0\<guillemotright> E0" and
  2942          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2943                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2944                          \<union> assigns_if True e0) \<guillemotright>In1l e1\<guillemotright> E1" and
  2945          da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2946                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2947                         \<union> assigns_if False e0) \<guillemotright>In1l e2\<guillemotright> E2"
  2948        by (elim da_elim_cases) simp+
  2949     from conf_s0 wt_e0 da_e0  
  2950     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  2951       by (rule hyp_e0 [elim_format]) simp
  2952     show "s2\<Colon>\<preceq>(G, L) \<and>
  2953            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2954            (error_free (Norm s0) = error_free s2)"
  2955     proof (cases "normal s1")
  2956       case False
  2957       with eval_e1_e2 have "s2=s1" by auto
  2958       with conf_s1 error_free_s1 False show ?thesis
  2959 	by auto
  2960     next
  2961       case True
  2962       have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  2963                     \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2964       proof -
  2965 	from eval_e0 have 
  2966 	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2967 	  by (rule dom_locals_eval_mono_elim)
  2968         moreover
  2969 	from eval_e0 True wt_e0 
  2970 	have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2971 	  by (rule assigns_if_good_approx') 
  2972 	ultimately show ?thesis by (rule Un_least)
  2973       qed 
  2974       show ?thesis
  2975       proof (cases "the_Bool b")
  2976 	case True
  2977 	with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  2978 	  by simp
  2979 	from da_e1 s0_s1 True obtain E1' where
  2980 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  2981 	  by - (rule da_weakenE,auto)
  2982 	with conf_s1 wt_e1
  2983 	obtain 
  2984 	  "s2\<Colon>\<preceq>(G, L)"
  2985 	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  2986 	  "error_free s2"            
  2987 	  by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  2988 	moreover
  2989 	from statT  
  2990 	have "G\<turnstile>T1\<preceq>statT"
  2991 	  by auto
  2992 	ultimately show ?thesis
  2993 	  using T wf by auto
  2994       next
  2995 	case False
  2996 	with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  2997 	  by simp
  2998 	from da_e2 s0_s1 False obtain E2' where
  2999 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  3000 	  by - (rule da_weakenE,auto)
  3001 	with conf_s1 wt_e2
  3002 	obtain 
  3003 	  "s2\<Colon>\<preceq>(G, L)"
  3004 	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  3005 	  "error_free s2"            
  3006 	  by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  3007 	moreover
  3008 	from statT  
  3009 	have "G\<turnstile>T2\<preceq>statT"
  3010 	  by auto
  3011 	ultimately show ?thesis
  3012 	  using T wf by auto
  3013       qed
  3014     qed
  3015   next
  3016     case (Call invDeclC a accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  3017            v vs L accC T A)
  3018     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  3019     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  3020     have invDeclC: "invDeclC 
  3021                       = invocation_declclass G mode (store s2) a statT 
  3022                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
  3023     have init_lvars: 
  3024            "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2".
  3025     have check: "s3' =
  3026        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" .
  3027     have eval_methd: 
  3028            "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  3029     have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  3030     have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  3031     have hyp_methd: "PROP ?TypeSafe s3' s4 
  3032                (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  3033     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3034     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3035                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  3036     from wt obtain pTs statDeclT statM where
  3037                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  3038               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  3039                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  3040                          = {((statDeclT,statM),pTs')}" and
  3041                  mode: "mode = invmode statM e" and
  3042                     T: "T =Inl (resTy statM)" and
  3043         eq_accC_accC': "accC=accC'"
  3044       by (rule wt_elim_cases) fastsimp+
  3045     from Call.prems obtain E where
  3046       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3047                \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3048       da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 args\<guillemotright> A" 
  3049       by (elim da_elim_cases) simp
  3050     from conf_s0 wt_e da_e  
  3051     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3052            conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  3053            error_free_s1: "error_free s1" 
  3054       by (rule hyp_e [elim_format]) simp
  3055     { 
  3056       assume abnormal_s2: "\<not> normal s2"
  3057       have "set_lvars (locals (store s2)) s4 = s2"
  3058       proof -
  3059 	from abnormal_s2 init_lvars 
  3060 	obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  3061              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  3062                                             mode a vs s2)" 
  3063 	  by (auto simp add: init_lvars_def2)
  3064 	moreover
  3065 	from keep_abrupt abnormal_s2 check
  3066 	have eq_s3'_s3: "s3'=s3" 
  3067 	  by (auto simp add: check_method_access_def Let_def)
  3068 	moreover
  3069 	from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  3070 	have "s4=s3'"
  3071 	  by auto
  3072 	ultimately show
  3073 	  "set_lvars (locals (store s2)) s4 = s2"
  3074 	  by (cases s2,cases s3) (simp add: init_lvars_def2)
  3075       qed
  3076     } note propagate_abnormal_s2 = this
  3077     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  3078            (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  3079              G,L,store ((set_lvars (locals (store s2))) s4)
  3080                \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3081            (error_free (Norm s0) =
  3082                 error_free ((set_lvars (locals (store s2))) s4))"
  3083     proof (cases "normal s1")
  3084       case False
  3085       with eval_args have "s2=s1" by auto
  3086       with False propagate_abnormal_s2 conf_s1 error_free_s1 
  3087       show ?thesis
  3088 	by auto
  3089     next
  3090       case True
  3091       note normal_s1 = this
  3092       obtain A' where 
  3093 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  3094       proof -
  3095 	from eval_e wt_e da_e wf normal_s1
  3096 	have "nrm E \<subseteq>  dom (locals (store s1))"
  3097 	  by (cases rule: da_good_approxE') rules
  3098 	with da_args show ?thesis
  3099 	  by (rule da_weakenE) 
  3100       qed
  3101       with conf_s1 wt_args 
  3102       obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3103               conf_args: "normal s2 
  3104                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  3105           error_free_s2: "error_free s2" 
  3106 	by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  3107       from error_free_s2 init_lvars
  3108       have error_free_s3: "error_free s3"
  3109 	by (auto simp add: init_lvars_def2)
  3110       from statM 
  3111       obtain
  3112 	statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  3113 	pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  3114 	by (blast dest: max_spec2mheads)
  3115       from check
  3116       have eq_store_s3'_s3: "store s3'=store s3"
  3117 	by (cases s3) (simp add: check_method_access_def Let_def)
  3118       obtain invC
  3119 	where invC: "invC = invocation_class mode (store s2) a statT"
  3120 	by simp
  3121       with init_lvars
  3122       have invC': "invC = (invocation_class mode (store s3) a statT)"
  3123 	by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  3124       show ?thesis
  3125       proof (cases "normal s2")
  3126 	case False
  3127 	with propagate_abnormal_s2 conf_s2 error_free_s2
  3128 	show ?thesis
  3129 	  by auto
  3130       next
  3131 	case True
  3132 	note normal_s2 = True
  3133 	with normal_s1 conf_a eval_args 
  3134 	have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  3135 	  by (auto dest: eval_gext intro: conf_gext)
  3136 	show ?thesis
  3137 	proof (cases "a=Null \<longrightarrow> is_static statM")
  3138 	  case False
  3139 	  then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  3140 	    by blast
  3141 	  with normal_s2 init_lvars mode
  3142 	  obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  3143                      "store s3 = store (init_lvars G invDeclC 
  3144                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2)"
  3145 	    by (auto simp add: init_lvars_def2)
  3146 	  moreover
  3147 	  from np check
  3148 	  have eq_s3'_s3: "s3'=s3" 
  3149 	    by (auto simp add: check_method_access_def Let_def)
  3150 	  moreover
  3151 	  from eq_s3'_s3 np eval_methd
  3152 	  have "s4=s3'"
  3153 	    by auto
  3154 	  ultimately have
  3155 	    "set_lvars (locals (store s2)) s4 
  3156             = (Some (Xcpt (Std NullPointer)),store s2)"
  3157 	    by (cases s2,cases s3) (simp add: init_lvars_def2)
  3158 	  with conf_s2 error_free_s2
  3159 	  show ?thesis
  3160 	    by (cases s2) (auto dest: conforms_NormI)
  3161 	next
  3162 	  case True
  3163 	  with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  3164 	    by (auto dest!: Null_staticD)
  3165 	  with conf_s2 conf_a_s2 wf invC  
  3166 	  have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  3167 	    by (cases s2) (auto intro: DynT_propI)
  3168 	  with wt_e statM' invC mode wf 
  3169 	  obtain dynM where 
  3170             dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3171             acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  3172                             in invC dyn_accessible_from accC"
  3173 	    by (force dest!: call_access_ok)
  3174 	  with invC' check eq_accC_accC'
  3175 	  have eq_s3'_s3: "s3'=s3"
  3176 	    by (auto simp add: check_method_access_def Let_def)
  3177 	  from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  3178 	  obtain 
  3179 	    wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  3180 	      dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3181             iscls_invDeclC: "is_class G invDeclC" and
  3182 	         invDeclC': "invDeclC = declclass dynM" and
  3183 	      invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  3184 	     resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  3185 	    is_static_eq: "is_static dynM = is_static statM" and
  3186 	    involved_classes_prop:
  3187              "(if invmode statM e = IntVir
  3188                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  3189                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  3190                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  3191                       statDeclT = ClassT invDeclC)"
  3192 	    by (cases rule: DynT_mheadsE) simp
  3193 	  obtain L' where 
  3194 	   L':"L'=(\<lambda> k. 
  3195                  (case k of
  3196                     EName e
  3197                     \<Rightarrow> (case e of 
  3198                           VNam v 
  3199                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  3200                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  3201                         | Res \<Rightarrow> Some (resTy dynM))
  3202                   | This \<Rightarrow> if is_static statM 
  3203                             then None else Some (Class invDeclC)))"
  3204 	    by simp
  3205 	  from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  3206             wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  3207 	  have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  3208 	    apply - 
  3209                (* FIXME confomrs_init_lvars should be 
  3210                   adjusted to be more directy applicable *)
  3211 	    apply (drule conforms_init_lvars [of G invDeclC 
  3212                     "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  3213                     L statT invC a "(statDeclT,statM)" e])
  3214 	    apply (rule wf)
  3215 	    apply (rule conf_args,assumption)
  3216 	    apply (simp add: pTs_widen)
  3217 	    apply (cases s2,simp)
  3218 	    apply (rule dynM')
  3219 	    apply (force dest: ty_expr_is_type)
  3220 	    apply (rule invC_widen)
  3221 	    apply (force intro: conf_gext dest: eval_gext)
  3222 	    apply simp
  3223 	    apply simp
  3224 	    apply (simp add: invC)
  3225 	    apply (simp add: invDeclC)
  3226 	    apply (simp add: normal_s2)
  3227 	    apply (cases s2, simp add: L' init_lvars
  3228 	                     cong add: lname.case_cong ename.case_cong)
  3229 	    done
  3230 	  with eq_s3'_s3 
  3231 	  have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  3232 	  moreover
  3233 	  from  is_static_eq wf_dynM L'
  3234 	  obtain mthdT where
  3235 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3236                \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  3237 	    mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  3238 	    by - (drule wf_mdecl_bodyD,
  3239                  auto simp add: callee_lcl_def  
  3240                       cong add: lname.case_cong ename.case_cong)
  3241 	  with dynM' iscls_invDeclC invDeclC'
  3242 	  have
  3243 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3244                \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  3245 	    by (auto intro: wt.Methd)
  3246 	  moreover
  3247 	  obtain M where 
  3248 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  3249 	       \<turnstile> dom (locals (store s3')) 
  3250 	          \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  3251 	  proof -
  3252 	    from wf_dynM
  3253 	    obtain M' where
  3254 	      da_body: 
  3255 	      "\<lparr>prg=G, cls=invDeclC
  3256                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  3257                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  3258               res: "Result \<in> nrm M'"
  3259 	      by (rule wf_mdeclE) rules
  3260 	    from da_body is_static_eq L' have
  3261 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3262                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  3263 	      by (simp add: callee_lcl_def  
  3264                   cong add: lname.case_cong ename.case_cong)
  3265 	    moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  3266 	    proof -
  3267 	      from is_static_eq 
  3268 	      have "(invmode (mthd dynM) e) = (invmode statM e)"
  3269 		by (simp add: invmode_def)
  3270 	      with init_lvars dynM' is_static_eq normal_s2 mode 
  3271 	      have "parameters (mthd dynM) = dom (locals (store s3))"
  3272 		using dom_locals_init_lvars 
  3273                   [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
  3274 		by simp
  3275 	      also from check
  3276 	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  3277 		by (simp add:  eq_s3'_s3)
  3278 	      finally show ?thesis .
  3279 	    qed
  3280 	    ultimately obtain M2 where
  3281 	      da:
  3282 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3283                 \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  3284               M2: "nrm M' \<subseteq> nrm M2"
  3285 	      by (rule da_weakenE)
  3286 	    from res M2 have "Result \<in> nrm M2"
  3287 	      by blast
  3288 	    moreover from wf_dynM
  3289 	    have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  3290 	      by (rule wf_mdeclE)
  3291 	    ultimately
  3292 	    obtain M3 where
  3293 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  3294                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  3295 	      using da
  3296 	      by (rules intro: da.Body assigned.select_convs)
  3297 	    from _ this [simplified]
  3298 	    show ?thesis
  3299 	      by (rule da.Methd [simplified,elim_format])
  3300 	         (auto intro: dynM')
  3301 	  qed
  3302 	  ultimately obtain  
  3303 	    conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  3304 	    conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  3305 	    error_free_s4: "error_free s4"
  3306 	    by (rule hyp_methd [elim_format]) 
  3307                (simp add: error_free_s3 eq_s3'_s3)
  3308 	  from init_lvars eval_methd eq_s3'_s3 
  3309 	  have "store s2\<le>|store s4"
  3310 	    by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  3311 	  moreover
  3312 	  have "abrupt s4 \<noteq> Some (Jump Ret)"
  3313 	  proof -
  3314 	    from normal_s2 init_lvars
  3315 	    have "abrupt s3 \<noteq> Some (Jump Ret)"
  3316 	      by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  3317 	    with check
  3318 	    have "abrupt s3' \<noteq> Some (Jump Ret)"
  3319 	      by (cases s3) (auto simp add: check_method_access_def Let_def)
  3320 	    with eval_methd
  3321 	    show ?thesis
  3322 	      by (rule Methd_no_jump)
  3323 	  qed
  3324 	  ultimately 
  3325 	  have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  3326 	    using conf_s2 conf_s4
  3327 	    by (cases s2,cases s4) (auto intro: conforms_return)
  3328 	  moreover 
  3329 	  from conf_Res mthdT_widen resTy_widen wf
  3330 	  have "normal s4 
  3331                   \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3332 	    by (auto dest: widen_trans)
  3333 	  then
  3334 	  have "normal ((set_lvars (locals (store s2))) s4)
  3335              \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3336 	    by (cases s4) auto
  3337 	  moreover note error_free_s4 T
  3338 	  ultimately 
  3339 	  show ?thesis
  3340 	    by simp
  3341 	qed
  3342       qed
  3343     qed
  3344   next
  3345     case (Methd D s0 s1 sig v L accC T A)
  3346     have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  3347     have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  3348     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3349     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
  3350     then obtain m bodyT where
  3351       D: "is_class G D" and
  3352       m: "methd G D sig = Some m" and
  3353       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  3354                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  3355       T: "T=Inl bodyT"
  3356       by (rule wt_elim_cases) auto
  3357     moreover
  3358     from Methd.prems m have 
  3359        da_body: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3360                    \<turnstile> (dom (locals (store ((Norm s0)::state))))
  3361                        \<guillemotright>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<guillemotright> A"
  3362       by - (erule da_elim_cases,simp)
  3363     ultimately
  3364     show "s1\<Colon>\<preceq>(G, L) \<and> 
  3365            (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3366            (error_free (Norm s0) = error_free s1)"
  3367       using hyp [of _ _ "(Inl bodyT)"] conf_s0 
  3368       by (auto simp add: Let_def body_def)
  3369   next
  3370     case (Body D c s0 s1 s2 s3 L accC T A)
  3371     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  3372     have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  3373     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
  3374     have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
  3375     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3376     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
  3377     then obtain bodyT where
  3378          iscls_D: "is_class G D" and
  3379             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
  3380          resultT: "L Result = Some bodyT" and
  3381       isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  3382                T: "T=Inl bodyT"
  3383       by (rule wt_elim_cases) auto
  3384     from Body.prems obtain C where
  3385       da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3386                    \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1r c\<guillemotright> C" and
  3387       jmpOk: "jumpNestingOkS {Ret} c" and
  3388       res: "Result \<in> nrm C"
  3389       by (elim da_elim_cases) simp
  3390     note conf_s0
  3391     moreover from iscls_D 
  3392     have "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init D\<Colon>\<surd>" by auto
  3393     moreover obtain I where 
  3394       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3395           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init D)\<guillemotright> I"
  3396       by (auto intro: da_Init [simplified] assigned.select_convs)
  3397     ultimately obtain
  3398       conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1:  "error_free s1"
  3399        by (rule hyp_init [elim_format]) simp
  3400     obtain C' where da_C': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3401                              \<turnstile> (dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'"
  3402                and nrm_C': "nrm C \<subseteq> nrm C'"
  3403     proof -
  3404       from eval_init 
  3405       have "(dom (locals (store ((Norm s0)::state)))) 
  3406                      \<subseteq> (dom (locals (store s1)))"
  3407 	by (rule dom_locals_eval_mono_elim)
  3408       with da_c show ?thesis by (rule da_weakenE)
  3409     qed
  3410     from conf_s1 wt_c da_C' 
  3411     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3412       by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  3413     from conf_s2
  3414     have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  3415       by (cases s2) (auto intro: conforms_absorb)
  3416     moreover
  3417     from error_free_s2
  3418     have "error_free (abupd (absorb Ret) s2)"
  3419       by simp
  3420     moreover have "abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump Ret)"
  3421       by (cases s3) (simp add: absorb_def)
  3422     moreover have "s3=s2"
  3423     proof -
  3424       from iscls_D
  3425       have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
  3426 	by auto
  3427       from eval_init wf
  3428       have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  3429 	by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  3430       from eval_c _ wt_c wf
  3431       have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  3432 	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  3433       moreover 
  3434       have "s3 =
  3435                 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  3436                         abrupt s2 = Some (Jump (Cont l))
  3437                  then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
  3438       ultimately show ?thesis 
  3439 	by force
  3440     qed
  3441     moreover
  3442     {
  3443       assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
  3444       have "Result \<in> dom (locals (store s2))"
  3445       proof -
  3446 	from normal_upd_s2
  3447 	have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  3448 	  by (cases s2) (simp add: absorb_def)
  3449 	thus ?thesis
  3450 	proof 
  3451 	  assume "normal s2"
  3452 	  with eval_c wt_c da_C' wf res nrm_C'
  3453 	  show ?thesis
  3454 	    by (cases rule: da_good_approxE') blast
  3455 	next
  3456 	  assume "abrupt s2 = Some (Jump Ret)"
  3457 	  with conf_s2 show ?thesis
  3458 	    by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  3459 	qed 
  3460       qed
  3461     }
  3462     moreover note T resultT
  3463     ultimately
  3464     show "abupd (absorb Ret) s3\<Colon>\<preceq>(G, L) \<and>
  3465            (normal (abupd (absorb Ret) s3) \<longrightarrow>
  3466              G,L,store (abupd (absorb Ret) s3)
  3467              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  3468           (error_free (Norm s0) = error_free (abupd (absorb Ret) s3)) "
  3469       by (cases s2) (auto intro: conforms_locals)
  3470   next
  3471     case (LVar s vn L accC T)
  3472     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and 
  3473              wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
  3474     then obtain vnT where
  3475       vnT: "L vn = Some vnT" and
  3476         T: "T=Inl vnT"
  3477       by (auto elim!: wt_elim_cases)
  3478     from conf_s vnT
  3479     have conf_fst: "locals s vn \<noteq> None \<longrightarrow> G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  3480      by (auto elim: conforms_localD [THEN wlconfD]  
  3481               simp add: lvar_def) 
  3482     moreover
  3483     from conf_s conf_fst vnT 
  3484     have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  3485       by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
  3486     moreover note conf_s T
  3487     ultimately 
  3488     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  3489                  (normal (Norm s) \<longrightarrow>
  3490                     G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  3491                  (error_free (Norm s) = error_free (Norm s))"
  3492       by (simp add: lvar_def) 
  3493   next
  3494     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T A)
  3495     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  3496     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  3497     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  3498     have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  3499     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  3500     have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
  3501     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3502     have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  3503     then obtain statC f where
  3504                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  3505             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  3506        eq_accC_accC': "accC=accC'" and
  3507                 stat: "stat=is_static f" and
  3508 	           T: "T=(Inl (type f))"
  3509       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  3510     from FVar.prems eq_accC_accC'
  3511     have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3512                  \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> A"
  3513       by (elim da_elim_cases) simp
  3514     note conf_s0
  3515     moreover
  3516     from wf wt_e 
  3517     have iscls_statC: "is_class G statC"
  3518       by (auto dest: ty_expr_is_type type_is_class)
  3519     with wf accfield 
  3520     have iscls_statDeclC: "is_class G statDeclC"
  3521       by (auto dest!: accfield_fields dest: fields_declC)
  3522     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  3523       by simp
  3524     moreover obtain I where 
  3525       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3526         \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init statDeclC)\<guillemotright> I"
  3527       by (auto intro: da_Init [simplified] assigned.select_convs)
  3528     ultimately 
  3529     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  3530       by (rule hyp_init [elim_format]) simp
  3531     obtain A' where 
  3532       "\<lparr>prg=G, cls=accC, lcl=L\<rparr> \<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e\<guillemotright> A'"
  3533     proof -
  3534       from eval_init
  3535       have "(dom (locals (store ((Norm s0)::state)))) 
  3536 	       \<subseteq> (dom (locals (store s1)))"
  3537 	by (rule dom_locals_eval_mono_elim)
  3538       with da_e show ?thesis
  3539 	by (rule da_weakenE)
  3540     qed
  3541     with conf_s1 wt_e 
  3542     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3543                   conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  3544            error_free_s2: "error_free s2"
  3545       by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  3546     from fvar 
  3547     have store_s2': "store s2'=store s2"
  3548       by (cases s2) (simp add: fvar_def2)
  3549     with fvar conf_s2 
  3550     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3551       by (cases s2,cases stat) (auto simp add: fvar_def2)
  3552     from eval_init 
  3553     have initd_statDeclC_s1: "initd statDeclC s1"
  3554       by (rule init_yields_initd)
  3555     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  3556     have eq_s3_s2': "s3=s2'"  
  3557       by (auto dest!: error_free_field_access)
  3558     have conf_v: "normal s2' \<Longrightarrow> 
  3559            G,store s2'\<turnstile>fst v\<Colon>\<preceq>type f \<and> store s2'\<le>|snd v\<preceq>type f\<Colon>\<preceq>(G, L)"
  3560     proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  3561       assume normal: "normal s2'"
  3562       obtain vv vf x2 store2 store2'
  3563 	where  v: "v=(vv,vf)" and
  3564               s2: "s2=(x2,store2)" and
  3565          store2': "store s2' = store2'"
  3566 	by (cases v,cases s2,cases s2') blast
  3567       from iscls_statDeclC obtain c
  3568 	where c: "class G statDeclC = Some c"
  3569 	by auto
  3570       have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  3571       proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  3572                                statC G c L "store s1"])
  3573 	from v normal s2 fvar stat store2' 
  3574 	show "((vv, vf), Norm store2') = 
  3575                fvar statDeclC (static f) fn a (x2, store2)"
  3576 	  by (auto simp add: member_is_static_simp)
  3577 	from accfield iscls_statC wf
  3578 	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  3579 	  by (auto dest!: accfield_fields dest: fields_declC)
  3580 	from accfield
  3581 	show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
  3582 	  by (auto dest!: accfield_fields)
  3583 	from wf show "wf_prog G" .
  3584 	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  3585 	  by auto
  3586 	from fld wf iscls_statC
  3587 	show "statDeclC \<noteq> Object "
  3588 	  by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  3589 	from c show "class G statDeclC = Some c" .
  3590 	from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3591 	from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  3592 	from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  3593 	  by simp
  3594       qed
  3595       with v s2 store2'  
  3596       show ?thesis
  3597 	by simp
  3598     qed
  3599     from fvar error_free_s2
  3600     have "error_free s2'"
  3601       by (cases s2)
  3602          (auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
  3603     with conf_v T conf_s2' eq_s3_s2'
  3604     show "s3\<Colon>\<preceq>(G, L) \<and>
  3605           (normal s3 
  3606            \<longrightarrow> G,L,store s3\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3607           (error_free (Norm s0) = error_free s3)"
  3608       by auto
  3609   next
  3610     case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T A)
  3611     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
  3612     have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
  3613     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
  3614     have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
  3615     have avar: "(v, s2') = avar G i a s2" .
  3616     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3617     have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
  3618     then obtain elemT
  3619        where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  3620              wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  3621                  T: "T= Inl elemT"
  3622       by (rule wt_elim_cases) auto
  3623     from AVar.prems obtain E1 where
  3624       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3625                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e1\<guillemotright> E1" and
  3626       da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>In1l e2\<guillemotright> A" 
  3627       by (elim da_elim_cases) simp
  3628     from conf_s0 wt_e1 da_e1  
  3629     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3630             conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  3631             error_free_s1: "error_free s1"
  3632       by (rule hyp_e1 [elim_format]) simp
  3633     show "s2'\<Colon>\<preceq>(G, L) \<and>
  3634            (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3635            (error_free (Norm s0) = error_free s2') "
  3636     proof (cases "normal s1")
  3637       case False
  3638       moreover
  3639       from False eval_e2 have eq_s2_s1: "s2=s1" by auto
  3640       moreover
  3641       from eq_s2_s1 False have  "\<not> normal s2" by simp
  3642       then have "snd (avar G i a s2) = s2"
  3643 	by (cases s2) (simp add: avar_def2)
  3644       with avar have "s2'=s2"
  3645 	by (cases "(avar G i a s2)") simp
  3646       ultimately show ?thesis
  3647 	using conf_s1 error_free_s1
  3648 	by auto
  3649     next
  3650       case True
  3651       obtain A' where 
  3652 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  3653       proof -
  3654 	from eval_e1 wt_e1 da_e1 wf True
  3655 	have "nrm E1 \<subseteq> dom (locals (store s1))"
  3656 	  by (cases rule: da_good_approxE') rules
  3657 	with da_e2 show ?thesis
  3658 	  by (rule da_weakenE)
  3659       qed
  3660       with conf_s1 wt_e2
  3661       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3662 	by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  3663       from avar 
  3664       have "store s2'=store s2"
  3665 	by (cases s2) (simp add: avar_def2)
  3666       with avar conf_s2 
  3667       have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3668 	by (cases s2) (auto simp add: avar_def2)
  3669       from avar error_free_s2
  3670       have error_free_s2': "error_free s2'"
  3671 	by (cases s2) (auto simp add: avar_def2 )
  3672       have "normal s2' \<Longrightarrow> 
  3673         G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3674       proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  3675 	assume normal: "normal s2'"
  3676 	show ?thesis
  3677 	proof -
  3678 	  obtain vv vf x1 store1 x2 store2 store2'
  3679 	    where  v: "v=(vv,vf)" and
  3680                   s1: "s1=(x1,store1)" and
  3681                   s2: "s2=(x2,store2)" and
  3682 	     store2': "store2'=store s2'"
  3683 	    by (cases v,cases s1, cases s2, cases s2') blast 
  3684 	  have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3685 	  proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  3686                                   OF wf])
  3687 	    from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  3688 	      by simp
  3689 	    from v normal s2 store2' avar 
  3690 	    show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  3691 	      by auto
  3692 	    from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3693 	    from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  3694 	    from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  3695 	  qed
  3696 	  with v s1 s2 store2' 
  3697 	  show ?thesis
  3698 	    by simp
  3699 	qed
  3700       qed
  3701       with conf_s2' error_free_s2' T 
  3702       show ?thesis 
  3703 	by auto
  3704     qed
  3705   next
  3706     case (Nil s0 L accC T)
  3707     then show ?case
  3708       by (auto elim!: wt_elim_cases)
  3709   next
  3710     case (Cons e es s0 s1 s2 v vs L accC T A)
  3711     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  3712     have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
  3713     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  3714     have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
  3715     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3716     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
  3717     then obtain eT esT where
  3718        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  3719        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  3720        T: "T=Inr (eT#esT)"
  3721       by (rule wt_elim_cases) blast
  3722     from Cons.prems obtain E where
  3723       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3724                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3725       da_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 es\<guillemotright> A" 
  3726       by (elim da_elim_cases) simp
  3727     from conf_s0 wt_e da_e 
  3728     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  3729       conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  3730       by (rule hyp_e [elim_format]) simp
  3731     show 
  3732       "s2\<Colon>\<preceq>(G, L) \<and> 
  3733       (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  3734       (error_free (Norm s0) = error_free s2)"
  3735     proof (cases "normal s1")
  3736       case False
  3737       with eval_es have "s2=s1" by auto
  3738       with False conf_s1 error_free_s1
  3739       show ?thesis
  3740 	by auto
  3741     next
  3742       case True
  3743       obtain A' where 
  3744 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  3745       proof -
  3746 	from eval_e wt_e da_e wf True
  3747 	have "nrm E \<subseteq> dom (locals (store s1))"
  3748 	  by (cases rule: da_good_approxE') rules
  3749 	with da_es show ?thesis
  3750 	  by (rule da_weakenE)
  3751       qed
  3752       with conf_s1 wt_es
  3753       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  3754            error_free_s2: "error_free s2" and
  3755            conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  3756 	by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  3757       moreover
  3758       from True eval_es conf_v 
  3759       have conf_v': "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  3760 	apply clarify
  3761 	apply (rule conf_gext)
  3762 	apply (auto dest: eval_gext)
  3763 	done
  3764       ultimately show ?thesis using T by simp
  3765     qed
  3766   qed
  3767   then show ?thesis .
  3768 qed
  3769 
  3770 text {* 
  3771 
  3772 
  3773 *} (* dummy text command to break paragraph for latex;
  3774               large paragraphs exhaust memory of debian pdflatex *)
  3775 
  3776 corollary eval_type_soundE [consumes 5]:
  3777   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  3778   and     conf: "s0\<Colon>\<preceq>(G, L)"
  3779   and       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>t\<Colon>T"
  3780   and       da: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile> dom (locals (snd s0)) \<guillemotright>t\<guillemotright> A"
  3781   and       wf: "wf_prog G"
  3782   and     elim: "\<lbrakk>s1\<Colon>\<preceq>(G, L); normal s1 \<Longrightarrow> G,L,snd s1\<turnstile>t\<succ>v\<Colon>\<preceq>T; 
  3783                   error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
  3784   shows "P"
  3785 using eval wt da wf conf
  3786 by (rule eval_type_sound [elim_format]) (rules intro: elim) 
  3787 
  3788  
  3789 corollary eval_ts: 
  3790  "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T;
  3791    \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1l e\<guillemotright>A\<rbrakk> 
  3792 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  3793      (error_free s = error_free s')"
  3794 apply (drule (4) eval_type_sound)
  3795 apply clarsimp
  3796 done
  3797 
  3798 corollary evals_ts: 
  3799 "\<lbrakk>G\<turnstile>s \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>es\<Colon>\<doteq>Ts;
  3800   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In3 es\<guillemotright>A\<rbrakk> 
  3801 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  3802      (error_free s = error_free s')" 
  3803 apply (drule (4) eval_type_sound)
  3804 apply clarsimp
  3805 done
  3806 
  3807 corollary evar_ts: 
  3808 "\<lbrakk>G\<turnstile>s \<midarrow>v=\<succ>vf\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>v\<Colon>=T;
  3809  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In2 v\<guillemotright>A\<rbrakk> \<Longrightarrow>  
  3810   s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  3811   (error_free s = error_free s')"
  3812 apply (drule (4) eval_type_sound)
  3813 apply clarsimp
  3814 done
  3815 
  3816 theorem exec_ts: 
  3817 "\<lbrakk>G\<turnstile>s \<midarrow>c\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  3818  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1r c\<guillemotright>A\<rbrakk> 
  3819  \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  3820 apply (drule (4) eval_type_sound)
  3821 apply clarsimp
  3822 done
  3823 
  3824 lemma wf_eval_Fin: 
  3825   assumes wf:    "wf_prog G" 
  3826     and   wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)"
  3827     and   da_c1: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store (Norm s0)))\<guillemotright>In1r c1\<guillemotright>A"
  3828     and conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" 
  3829     and eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" 
  3830     and eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" 
  3831     and      s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  3832   shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
  3833 proof -
  3834   from eval_c1 wt_c1 da_c1 wf conf_s0
  3835   have "error_free (x1,s1)"
  3836     by (auto dest: eval_type_sound)
  3837   with eval_c1 eval_c2 s3
  3838   show ?thesis
  3839     by - (rule eval.Fin, auto simp add: error_free_def)
  3840 qed
  3841 
  3842 subsection "Ideas for the future"
  3843 
  3844 text {* In the type soundness proof and the correctness proof of 
  3845 definite assignment we perform induction on the evaluation relation with the 
  3846 further preconditions that the term is welltyped and definitely assigned. During
  3847 the proofs we have to establish the welltypedness and definite assignment of 
  3848 the subterms to be able to apply the induction hypothesis. So large parts of
  3849 both proofs are the same work in propagating welltypedness and definite 
  3850 assignment. So we can derive a new induction rule for induction on the 
  3851 evaluation of a wellformed term, were these propagations is already done, once
  3852 and forever. 
  3853 Then we can do the proofs with this rule and can enjoy the time we have saved.
  3854 Here is a first and incomplete sketch of such a rule.*}
  3855 theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab 
  3856                                 Comp If]:
  3857   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  3858    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  3859    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  3860    and      wf: "wf_prog G" 
  3861    and  abrupt: "\<And> s t abr L accC T A. 
  3862                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
  3863                    \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
  3864                   \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
  3865    and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
  3866    and    expr: "\<And> e s0 s1 v L accC eT E.
  3867                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
  3868                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3869                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E;
  3870                   P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1\<rbrakk> 
  3871                  \<Longrightarrow>  P L accC (Norm s0) \<langle>Expr e\<rangle>\<^sub>s \<diamondsuit> s1"
  3872    and     lab: "\<And> c l s0 s1 L accC C.
  3873                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  3874                   \<lparr>prg=G,cls=accC, lcl=L\<rparr>
  3875                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
  3876                   P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1\<rbrakk>
  3877                   \<Longrightarrow> P L accC (Norm s0) \<langle>l\<bullet> c\<rangle>\<^sub>s \<diamondsuit> (abupd (absorb l) s1)"
  3878    and    comp: "\<And> c1 c2 s0 s1 s2 L accC C1.
  3879                  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;G\<turnstile>s1 \<midarrow>c2 \<rightarrow> s2;
  3880                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>;
  3881                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>;
  3882                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3883                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1;
  3884                   P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1;
  3885                   \<And> Q. \<lbrakk>normal s1; 
  3886                          \<And> C2.\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3887                                   \<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2;
  3888                                P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
  3889                         \<rbrakk> \<Longrightarrow> Q 
  3890                   \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3891     and    if: "\<And> b c1 c2 e s0 s1 s2 L accC E.
  3892                 \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
  3893                  G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
  3894                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
  3895                  \<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>;
  3896                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3897                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E;
  3898                  P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1;
  3899                  \<And> Q. \<lbrakk>normal s1;
  3900                         \<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  3901                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  3902                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  3903                               \<rbrakk> \<Longrightarrow> Q
  3904                        \<rbrakk> \<Longrightarrow> Q
  3905                 \<rbrakk> \<Longrightarrow> P L accC (Norm s0) \<langle>If(e) c1 Else c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3906    shows "P L accC s0 t v s1"  
  3907 proof -
  3908   note inj_term_simps [simp]
  3909   from eval 
  3910   show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  3911                        \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  3912         \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
  3913   proof (induct)
  3914     case Abrupt with abrupt show ?case .
  3915   next
  3916     case Skip from skip show ?case by simp
  3917   next
  3918     case (Expr e s0 s1 v L accC T A) 
  3919     from Expr.prems obtain eT where 
  3920       "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
  3921       by (elim wt_elim_cases) 
  3922     moreover
  3923     from Expr.prems obtain E where
  3924       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E"
  3925       by (elim da_elim_cases) simp
  3926     moreover from calculation
  3927     have "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1"
  3928       by (rule Expr.hyps) 
  3929     ultimately show ?case
  3930       by (rule expr)
  3931   next
  3932     case (Lab c l s0 s1 L accC T A)
  3933     from Lab.prems 
  3934     have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  3935       by (elim wt_elim_cases)
  3936     moreover
  3937     from Lab.prems obtain C where
  3938       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C"
  3939       by (elim da_elim_cases) simp
  3940     moreover from calculation
  3941     have "P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1"
  3942       by (rule  Lab.hyps)  
  3943     ultimately show ?case
  3944       by (rule lab)
  3945   next
  3946     case (Comp c1 c2 s0 s1 s2 L accC T A) 
  3947     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  3948     have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  3949     from Comp.prems obtain 
  3950       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  3951       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  3952       by (elim wt_elim_cases) 
  3953     from Comp.prems
  3954     obtain C1 C2
  3955       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  3956                       dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and 
  3957             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2" 
  3958       by (elim da_elim_cases) simp
  3959     from wt_c1 da_c1
  3960     have P_c1: "P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1"
  3961       by (rule Comp.hyps)
  3962     {
  3963       fix Q
  3964       assume normal_s1: "normal s1"
  3965       assume elim: "\<And> C2'. 
  3966                     \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright>C2';
  3967                        P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
  3968       have Q
  3969       proof -
  3970 	obtain C2' where 
  3971 	  da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  3972 	proof -
  3973 	  from eval_c1 wt_c1 da_c1 wf normal_s1
  3974 	  have "nrm C1 \<subseteq> dom (locals (store s1))"
  3975 	    by (cases rule: da_good_approxE') rules
  3976 	  with da_c2 show ?thesis
  3977 	    by (rule da_weakenE)
  3978 	qed
  3979 	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  3980 	  by (rule Comp.hyps)
  3981 	with da show ?thesis
  3982 	  using elim by rules
  3983       qed
  3984     }
  3985     with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
  3986     show ?case
  3987       by (rule comp) rules+
  3988   next
  3989     case (If b c1 c2 e s0 s1 s2 L accC T A)
  3990     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  3991     have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  3992     from If.prems
  3993     obtain 
  3994               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  3995       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  3996       by (elim wt_elim_cases) (auto split add: split_if)
  3997     from If.prems obtain E C where
  3998       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  3999                                        \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  4000       da_then_else: 
  4001       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  4002          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  4003           \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C"
  4004       by (elim da_elim_cases) (cases "the_Bool b",auto)
  4005     from wt_e da_e
  4006     have P_e: "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1"
  4007       by (rule If.hyps)
  4008     {
  4009       fix Q
  4010       assume normal_s1: "normal s1"
  4011       assume elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  4012                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  4013                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  4014                               \<rbrakk> \<Longrightarrow> Q"
  4015       have Q
  4016       proof -
  4017 	obtain C' where
  4018 	  da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  4019                 (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
  4020 	proof -
  4021 	  from eval_e have 
  4022 	    "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  4023 	    by (rule dom_locals_eval_mono_elim)
  4024           moreover
  4025 	  from eval_e normal_s1 wt_e 
  4026 	  have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4027 	    by (rule assigns_if_good_approx')
  4028 	  ultimately 
  4029 	  have "dom (locals (store ((Norm s0)::state))) 
  4030             \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4031 	    by (rule Un_least)
  4032 	  with da_then_else show ?thesis
  4033 	    by (rule da_weakenE)
  4034 	qed
  4035 	with wt_then_else
  4036 	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  4037 	  by (rule If.hyps)
  4038 	with da show ?thesis using elim by rules
  4039       qed
  4040     }
  4041     with eval_e eval_then_else wt_e wt_then_else da_e P_e
  4042     show ?case
  4043       by (rule if) rules+
  4044   next
  4045     oops
  4046 
  4047 end