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