src/HOL/Bali/TypeSafe.thy
author wenzelm
Thu Jan 05 22:29:55 2006 +0100 (2006-01-05)
changeset 18585 5d379fe2eb74
parent 18576 8d98b7711e47
child 19796 d86e7b1fc472
permissions -rw-r--r--
replaced swap by contrapos_np;
     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 imports DefiniteAssignmentCorrect Conform begin
     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 contrapos_np, 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             )
   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 change_simpset (fn ss => ss delloop "split_all_tac");
   734 change_claset (fn cs => cs 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 change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   764 change_simpset (fn ss => ss 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 change_simpset (fn ss => ss delloop "split_all_tac");
   882 change_claset (fn cs => cs 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 change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac));
   936 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   937 *}
   938 
   939 
   940 subsection "accessibility"
   941 
   942 theorem dynamic_field_access_ok:
   943   assumes wf: "wf_prog G" and
   944     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   945    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   946    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   947     normal_s: "normal s" and
   948         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   949            f: "accfield G accC statC fn = Some f" and
   950         dynC: "if stat then dynC=declclass f  
   951                        else dynC=obj_class (lookup_obj (store s) a)" and
   952         stat: "if stat then (is_static f) else (\<not> is_static f)"
   953   shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<and>
   954          G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   955 proof (cases "stat")
   956   case True
   957   with stat have static: "(is_static f)" by simp
   958   from True dynC 
   959   have dynC': "dynC=declclass f" by simp
   960   with f
   961   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   962     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   963   moreover
   964   from wt_e wf have "is_class G statC"
   965     by (auto dest!: ty_expr_is_type)
   966   moreover note wf dynC'
   967   ultimately have
   968      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   969     by (auto dest: fields_declC)
   970   with dynC' f static wf
   971   show ?thesis
   972     by (auto dest: static_to_dynamic_accessible_from_static
   973             dest!: accfield_accessibleD )
   974 next
   975   case False
   976   with wf conform_a not_Null conform_s dynC
   977   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   978     "is_class G dynC"
   979     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   980               dest: obj_ty_obj_class1
   981           simp add: obj_ty_obj_class )
   982   with wf f
   983   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   984     by (auto simp add: accfield_def Let_def
   985                  dest: fields_mono
   986                 dest!: table_of_remap_SomeD)
   987   moreover
   988   from f subclseq
   989   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   990     by (auto intro!: static_to_dynamic_accessible_from 
   991                dest: accfield_accessibleD)
   992   ultimately show ?thesis
   993     by blast
   994 qed
   995 
   996 lemma error_free_field_access:
   997   assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
   998               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   999          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
  1000             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
  1001            conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1002             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  1003               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
  1004                 wf: "wf_prog G"   
  1005   shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
  1006 proof -
  1007   from fvar
  1008   have store_s2': "store s2'=store s2"
  1009     by (cases s2) (simp add: fvar_def2)
  1010   with fvar conf_s2 
  1011   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1012     by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1013   from eval_init 
  1014   have initd_statDeclC_s1: "initd statDeclC s1"
  1015     by (rule init_yields_initd)
  1016   with eval_e store_s2'
  1017   have initd_statDeclC_s2': "initd statDeclC s2'"
  1018     by (auto dest: eval_gext intro: inited_gext)
  1019   show ?thesis
  1020   proof (cases "normal s2'")
  1021     case False
  1022     then show ?thesis 
  1023       by (auto simp add: check_field_access_def Let_def)
  1024   next
  1025     case True
  1026     with fvar store_s2' 
  1027     have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
  1028       by (cases s2) (auto simp add: fvar_def2)
  1029     from True fvar store_s2'
  1030     have "normal s2"
  1031       by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1032     with conf_a store_s2'
  1033     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1034       by simp
  1035     from conf_a' conf_s2' True initd_statDeclC_s2' 
  1036       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1037                                    True wt_e accfield ] 
  1038     show ?thesis
  1039       by  (cases "is_static f")
  1040           (auto dest!: initedD
  1041            simp add: check_field_access_def Let_def)
  1042   qed
  1043 qed
  1044 
  1045 lemma call_access_ok:
  1046   assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
  1047       and        wf: "wf_prog G" 
  1048       and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
  1049       and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
  1050       and      invC: "invC = invocation_class (invmode statM e) s a statT"
  1051   shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
  1052   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
  1053 proof -
  1054   from wt_e wf have type_statT: "is_type G (RefT statT)"
  1055     by (auto dest: ty_expr_is_type)
  1056   from statM have not_Null: "statT \<noteq> NullT" by auto
  1057   from type_statT wt_e 
  1058   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
  1059                                         invmode statM e \<noteq> SuperM)"
  1060     by (auto dest: invocationTypeExpr_noClassD)
  1061   from wt_e
  1062   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
  1063     by (auto dest: invocationTypeExpr_noClassD)
  1064   show ?thesis
  1065   proof (cases "invmode statM e = IntVir")
  1066     case True
  1067     with invC_prop not_Null
  1068     have invC_prop': "is_class G invC \<and>  
  1069                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
  1070                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
  1071       by (auto simp add: DynT_prop_def)
  1072     with True not_Null
  1073     have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1074      by (cases statT) (auto simp add: invmode_def) 
  1075     with statM type_statT wf 
  1076     show ?thesis
  1077       by - (rule dynlookup_access,auto)
  1078   next
  1079     case False
  1080     with type_statT wf invC not_Null wf_I wf_A
  1081     have invC_prop': " is_class G invC \<and>
  1082                       ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
  1083                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
  1084         by (case_tac "statT") (auto simp add: invocation_class_def 
  1085                                        split: inv_mode.splits)
  1086     with not_Null wf
  1087     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
  1088       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
  1089                                             dynimethd_def)
  1090    from statM wf wt_e not_Null False invC_prop' obtain dynM where
  1091                 "accmethd G accC invC sig = Some dynM" 
  1092      by (auto dest!: static_mheadsD)
  1093    from invC_prop' False not_Null wf_I
  1094    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1095      by (cases statT) (auto simp add: invmode_def) 
  1096    with statM type_statT wf 
  1097     show ?thesis
  1098       by - (rule dynlookup_access,auto)
  1099   qed
  1100 qed
  1101 
  1102 lemma error_free_call_access:
  1103   assumes
  1104    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
  1105         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
  1106        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
  1107                = {((statDeclT, statM), pTs')}" and
  1108      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1109       conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1110      invProp: "normal s3 \<Longrightarrow>
  1111                 G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
  1112           s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1113                         (invmode statM e) a vs s2" and
  1114         invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
  1115     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
  1116                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
  1117           wf: "wf_prog G"
  1118   shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
  1119    = s3"
  1120 proof (cases "normal s2")
  1121   case False
  1122   with s3 
  1123   have "abrupt s3 = abrupt s2"  
  1124     by (auto simp add: init_lvars_def2)
  1125   with False
  1126   show ?thesis
  1127     by (auto simp add: check_method_access_def Let_def)
  1128 next
  1129   case True
  1130   note normal_s2 = True
  1131   with eval_args
  1132   have normal_s1: "normal s1"
  1133     by (cases "normal s1") auto
  1134   with conf_a eval_args 
  1135   have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1136     by (auto dest: eval_gext intro: conf_gext)
  1137   show ?thesis
  1138   proof (cases "a=Null \<longrightarrow> (is_static statM)")
  1139     case False
  1140     then obtain "\<not> is_static statM" "a=Null" 
  1141       by blast
  1142     with normal_s2 s3
  1143     have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
  1144       by (auto simp add: init_lvars_def2)
  1145     then show ?thesis
  1146       by (auto simp add: check_method_access_def Let_def)
  1147   next
  1148     case True
  1149     from statM 
  1150     obtain
  1151       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1152       by (blast dest: max_spec2mheads)
  1153     from True normal_s2 s3
  1154     have "normal s3"
  1155       by (auto simp add: init_lvars_def2)
  1156     then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
  1157       by (rule invProp)
  1158     with wt_e statM' wf invC
  1159     obtain dynM where 
  1160       dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1161       acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1162                           in invC dyn_accessible_from accC"
  1163       by (force dest!: call_access_ok)
  1164     moreover
  1165     from s3 invC
  1166     have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
  1167       by (cases s2,cases "invmode statM e") 
  1168          (simp add: init_lvars_def2 del: invmode_Static_eq)+
  1169     ultimately
  1170     show ?thesis
  1171       by (auto simp add: check_method_access_def Let_def)
  1172   qed
  1173 qed
  1174 
  1175 lemma map_upds_eq_length_append_simp:
  1176   "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
  1177 proof (induct ps) 
  1178   case Nil thus ?case by simp
  1179 next
  1180   case (Cons p ps tab qs)
  1181   have "length (p#ps) = length qs" .
  1182   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1183     by (cases qs) auto
  1184   from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
  1185     by (rule Cons.hyps)
  1186   with qs show ?case 
  1187     by simp
  1188 qed
  1189 
  1190 lemma map_upds_upd_eq_length_simp:
  1191   "\<And> tab qs x y. length ps = length qs 
  1192                   \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
  1193 proof (induct "ps")
  1194   case Nil thus ?case by simp
  1195 next
  1196   case (Cons p ps tab qs x y)
  1197   have "length (p#ps) = length qs" .
  1198   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1199     by (cases qs) auto
  1200   from eq_length 
  1201   have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
  1202     by (rule Cons.hyps)
  1203   with qs show ?case
  1204     by simp
  1205 qed
  1206 
  1207 
  1208 lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
  1209 by simp
  1210 
  1211 lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) z"
  1212 by (simp add: fun_upd_def)
  1213 
  1214 lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
  1215 by (cases xs) simp+
  1216 
  1217 lemma map_upds_cong_ext: 
  1218  "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) z"
  1219 proof (induct xs)
  1220   case Nil thus ?case by simp
  1221 next
  1222   case (Cons x xs tab tab' ys)
  1223   note Hyps = this
  1224   show ?case
  1225   proof (cases ys)
  1226     case Nil
  1227     thus ?thesis by simp
  1228   next
  1229     case (Cons y ys')
  1230     have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
  1231       by (iprover intro: Hyps map_upd_cong_ext)
  1232     with Cons show ?thesis
  1233       by simp
  1234   qed
  1235 qed
  1236    
  1237 lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
  1238   by simp
  1239 
  1240 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
  1241         length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
  1242 proof (induct ps)
  1243   case Nil thus ?case by simp
  1244 next
  1245   case (Cons p ps tab qs)
  1246   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1247     by (cases qs) auto
  1248   from eq_length
  1249   have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
  1250     by (rule Cons.hyps)
  1251   with qs show ?case 
  1252     by simp
  1253 qed
  1254   
  1255   
  1256 lemma map_upds_upds_eq_length_prefix_simp:
  1257   "\<And> tab qs. length ps = length qs
  1258               \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
  1259 proof (induct ps)
  1260   case Nil thus ?case by simp
  1261 next
  1262   case (Cons p ps tab qs)
  1263   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1264     by (cases qs) auto
  1265   from eq_length 
  1266   have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
  1267     by (rule Cons.hyps)
  1268   with qs 
  1269   show ?case by simp
  1270 qed
  1271 
  1272 lemma map_upd_cut_irrelevant:
  1273 "\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<rbrakk>
  1274     \<Longrightarrow> tab vn = Some el"
  1275 by (cases "tab' vn = None") (simp add: fun_upd_def)+
  1276 
  1277 lemma map_upd_Some_expand:
  1278 "\<lbrakk>tab vn = Some z\<rbrakk>
  1279     \<Longrightarrow> \<exists> z. (tab(x\<mapsto>y)) vn = Some z"
  1280 by (simp add: fun_upd_def)
  1281 
  1282 lemma map_upds_Some_expand:
  1283 "\<And> tab ys z. \<lbrakk>tab vn = Some z\<rbrakk>
  1284     \<Longrightarrow> \<exists> z. (tab(xs[\<mapsto>]ys)) vn = Some z"
  1285 proof (induct xs)
  1286   case Nil thus ?case by simp
  1287 next
  1288   case (Cons x xs tab ys z)
  1289   have z: "tab vn = Some z" .
  1290   show ?case
  1291   proof (cases ys)
  1292     case Nil
  1293     with z show ?thesis by simp
  1294   next
  1295     case (Cons y ys')
  1296     have ys: "ys = y#ys'".
  1297     from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
  1298       by (rule map_upd_Some_expand [of tab,elim_format]) blast
  1299     hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
  1300       by (rule Cons.hyps)
  1301     with ys show ?thesis
  1302       by simp
  1303   qed
  1304 qed
  1305 
  1306 
  1307 lemma map_upd_Some_swap:
  1308  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
  1309 by (simp add: fun_upd_def)
  1310 
  1311 lemma map_upd_None_swap:
  1312  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
  1313 by (simp add: fun_upd_def)
  1314 
  1315 
  1316 lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
  1317 by (simp add: fun_upd_def)
  1318 
  1319 lemma map_upd_in_expansion_map_swap:
  1320  "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1321                  \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
  1322 by (simp add: fun_upd_def)
  1323 
  1324 lemma map_upds_in_expansion_map_swap:
  1325  "\<And>tab tab' ys z. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1326                  \<Longrightarrow>  (tab'(xs[\<mapsto>]ys)) vn = Some z"
  1327 proof (induct xs)
  1328   case Nil thus ?case by simp
  1329 next
  1330   case (Cons x xs tab tab' ys z)
  1331   have some: "(tab(x # xs[\<mapsto>]ys)) vn = Some z" .
  1332   have tab_not_z: "tab vn \<noteq> Some z".
  1333   show ?case
  1334   proof (cases "ys")
  1335     case Nil with some tab_not_z show ?thesis by simp
  1336   next
  1337     case (Cons y tl)
  1338     have ys: "ys = y#tl".
  1339     show ?thesis
  1340     proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
  1341       case True
  1342       with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
  1343 	by (fastsimp intro: Cons.hyps)
  1344       with ys show ?thesis 
  1345 	by simp
  1346     next
  1347       case False
  1348       hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
  1349       moreover
  1350       from tabx_z tab_not_z
  1351       have "(tab'(x\<mapsto>y)) vn = Some z" 
  1352 	by (rule map_upd_in_expansion_map_swap)
  1353       ultimately
  1354       have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
  1355 	by simp
  1356       hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
  1357 	by (rule map_upds_cong_ext)
  1358       with some ys
  1359       show ?thesis 
  1360 	by simp
  1361     qed
  1362   qed
  1363 qed
  1364    
  1365 lemma map_upds_Some_swap: 
  1366  assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1367     shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1368 proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
  1369   case True
  1370   then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
  1371     by (rule map_upd_Some_swap [elim_format]) blast
  1372   thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1373     by (rule map_upds_Some_expand)
  1374 next
  1375   case False
  1376   with r_u
  1377   have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1378     by (rule map_upds_in_expansion_map_swap)
  1379   thus ?thesis
  1380     by simp
  1381 qed
  1382  
  1383 lemma map_upds_Some_insert:
  1384   assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
  1385     shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1386 proof (cases "\<exists> z. tab vn = Some z")
  1387   case True
  1388   then obtain z' where "tab vn = Some z'" by blast
  1389   then obtain z'' where "(tab(u\<mapsto>v)) vn = Some z''"
  1390     by (rule map_upd_Some_expand [elim_format]) blast
  1391   thus ?thesis
  1392     by (rule map_upds_Some_expand)
  1393 next
  1394   case False
  1395   hence "tab vn \<noteq> Some z" by simp
  1396   with z
  1397   have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1398     by (rule map_upds_in_expansion_map_swap)
  1399   thus ?thesis ..
  1400 qed
  1401    
  1402 lemma map_upds_None_cut:
  1403 assumes expand_None: "(tab(xs[\<mapsto>]ys)) vn = None"
  1404   shows "tab vn = None"
  1405 proof (cases "tab vn = None")
  1406   case True thus ?thesis by simp
  1407 next
  1408   case False then obtain z where "tab vn = Some z" by blast
  1409   then obtain z' where "(tab(xs[\<mapsto>]ys)) vn = Some z'"
  1410     by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
  1411   with expand_None show ?thesis
  1412     by simp
  1413 qed
  1414     
  1415 
  1416 lemma map_upds_cut_irrelevant:
  1417 "\<And> tab tab' ys. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some el; (tab'(xs[\<mapsto>]ys)) vn = None\<rbrakk>
  1418                   \<Longrightarrow> tab vn = Some el"
  1419 proof  (induct "xs")
  1420   case Nil thus ?case by simp
  1421 next
  1422   case (Cons x xs tab tab' ys)
  1423   have tab_vn: "(tab(x # xs[\<mapsto>]ys)) vn = Some el".
  1424   have tab'_vn: "(tab'(x # xs[\<mapsto>]ys)) vn = None".
  1425   show ?case
  1426   proof (cases ys)
  1427     case Nil
  1428     with tab_vn show ?thesis by simp
  1429   next
  1430     case (Cons y tl)
  1431     have ys: "ys=y#tl".
  1432     with tab_vn tab'_vn 
  1433     have "(tab(x\<mapsto>y)) vn = Some el"
  1434       by - (rule Cons.hyps,auto)
  1435     moreover from tab'_vn ys
  1436     have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
  1437       by simp
  1438     hence "(tab'(x\<mapsto>y)) vn = None"
  1439       by (rule map_upds_None_cut)
  1440     ultimately show "tab vn = Some el" 
  1441       by (rule map_upd_cut_irrelevant)
  1442   qed
  1443 qed
  1444 
  1445    
  1446 lemma dom_vname_split:
  1447  "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
  1448    = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
  1449      dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
  1450   (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
  1451 proof 
  1452   show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
  1453   proof 
  1454     fix el 
  1455     assume el_in_list: "el \<in> ?List x xs y ys"
  1456     show "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1457     proof (cases el)
  1458       case This
  1459       with el_in_list show ?thesis by (simp add: dom_def)
  1460     next
  1461       case (EName en)
  1462       show ?thesis
  1463       proof (cases en)
  1464 	case Res
  1465 	with EName el_in_list show ?thesis by (simp add: dom_def)
  1466       next
  1467 	case (VNam vn)
  1468 	with EName el_in_list show ?thesis 
  1469 	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
  1470       qed
  1471     qed
  1472   qed
  1473 next
  1474   show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
  1475   proof (rule subsetI)
  1476     fix el 
  1477     assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1478     show "el \<in> ?List x xs y ys"
  1479     proof (cases el)
  1480       case This
  1481       with el_in_hd_tl show ?thesis by (simp add: dom_def)
  1482     next
  1483       case (EName en)
  1484       show ?thesis
  1485       proof (cases en)
  1486 	case Res
  1487 	with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
  1488       next
  1489 	case (VNam vn)
  1490 	with EName el_in_hd_tl show ?thesis 
  1491 	  by (auto simp add: dom_def intro: map_upds_Some_expand 
  1492                                             map_upds_Some_insert)
  1493       qed
  1494     qed
  1495   qed
  1496 qed
  1497 
  1498 lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
  1499 by (auto simp add: dom_def fun_upd_def)
  1500 
  1501 lemma dom_map_upds: "\<And> tab ys. length xs = length ys 
  1502   \<Longrightarrow> dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
  1503 proof (induct xs)
  1504   case Nil thus ?case by (simp add: dom_def)
  1505 next
  1506   case (Cons x xs tab ys)
  1507   note Hyp = Cons.hyps
  1508   have len: "length (x#xs)=length ys".
  1509   show ?case
  1510   proof (cases ys)
  1511     case Nil with len show ?thesis by simp
  1512   next
  1513     case (Cons y tl)
  1514     with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
  1515       by - (rule Hyp,simp)
  1516     moreover 
  1517     have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
  1518       by (rule dom_map_upd)
  1519     ultimately
  1520     show ?thesis using Cons
  1521       by simp
  1522   qed
  1523 qed
  1524  
  1525 lemma dom_ename_case_None_simp:
  1526  "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
  1527   apply (auto simp add: dom_def image_def )
  1528   apply (case_tac "x")
  1529   apply auto
  1530   done
  1531 
  1532 lemma dom_ename_case_Some_simp:
  1533  "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
  1534   apply (auto simp add: dom_def image_def )
  1535   apply (case_tac "x")
  1536   apply auto
  1537   done
  1538 
  1539 lemma dom_lname_case_None_simp:
  1540   "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
  1541   apply (auto simp add: dom_def image_def )
  1542   apply (case_tac "x")
  1543   apply auto
  1544   done
  1545 
  1546 lemma dom_lname_case_Some_simp:
  1547  "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
  1548   apply (auto simp add: dom_def image_def)
  1549   apply (case_tac "x")
  1550   apply auto
  1551   done
  1552 
  1553 lemmas dom_lname_ename_case_simps =  
  1554      dom_ename_case_None_simp dom_ename_case_Some_simp 
  1555      dom_lname_case_None_simp dom_lname_case_Some_simp
  1556 
  1557 lemma image_comp: 
  1558  "f ` g ` A = (f \<circ> g) ` A"
  1559 by (auto simp add: image_def)
  1560 
  1561 
  1562 lemma dom_locals_init_lvars: 
  1563   assumes m: "m=(mthd (the (methd G C sig)))"  
  1564   assumes len: "length (pars m) = length pvs"
  1565   shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
  1566            = parameters m"
  1567 proof -
  1568   from m
  1569   have static_m': "is_static m = static m"
  1570     by simp
  1571   from len
  1572   have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
  1573     by (simp add: dom_map_upds)
  1574   show ?thesis
  1575   proof (cases "static m")
  1576     case True
  1577     with static_m' dom_vnames m
  1578     show ?thesis
  1579       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1580                               dom_lname_ename_case_simps image_comp)
  1581   next
  1582     case False
  1583     with static_m' dom_vnames m
  1584     show ?thesis
  1585       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1586                               dom_lname_ename_case_simps image_comp)
  1587   qed
  1588 qed
  1589 
  1590 
  1591 lemma da_e2_BinOp:
  1592   assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1593                   \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
  1594     and wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T"
  1595     and wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" 
  1596     and wt_binop: "wt_binop G binop e1T e2T" 
  1597     and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1598     and normal_s1: "normal s1"
  1599     and	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
  1600     and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
  1601     and wf: "wf_prog G"
  1602   shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1603          \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1604 proof -
  1605   note inj_term_simps [simp]
  1606   from da obtain E1 where
  1607     da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
  1608     by cases simp+
  1609   obtain E2 where
  1610     "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1611       \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1612   proof (cases "need_second_arg binop v1")
  1613     case False
  1614     obtain S where
  1615       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1616                   \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>Skip\<rangle>\<^sub>s\<guillemotright> S"
  1617       by (auto intro: da_Skip [simplified] assigned.select_convs)
  1618     thus ?thesis
  1619       using that by (simp add: False)
  1620   next
  1621     case True
  1622     from eval_e1 have 
  1623       s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1624       by (rule dom_locals_eval_mono_elim)
  1625     {
  1626       assume condAnd: "binop=CondAnd"
  1627       have ?thesis
  1628       proof -
  1629 	from da obtain E2' where
  1630 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1631              \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1632 	  by cases (simp add: condAnd)+
  1633 	moreover
  1634 	have "dom (locals (store s0)) 
  1635           \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1636 	proof -
  1637 	  from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
  1638 	    by simp
  1639 	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1640 	    by (auto dest: conf_Boolean)
  1641 	  with True condAnd
  1642 	  have v1: "v1=Bool True"
  1643 	    by simp
  1644 	  from eval_e1 normal_s1 
  1645 	  have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1646 	    by (rule assigns_if_good_approx' [elim_format])
  1647 	       (insert wt_e1, simp_all add: e1T v1)
  1648 	  with s0_s1 show ?thesis by (rule Un_least)
  1649 	qed
  1650 	ultimately
  1651 	show ?thesis
  1652 	  using that by (cases rule: da_weakenE) (simp add: True)
  1653       qed
  1654     }
  1655     moreover
  1656     { 
  1657       assume condOr: "binop=CondOr"
  1658       have ?thesis
  1659 	(* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
  1660       proof -
  1661 	from da obtain E2' where
  1662 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1663               \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1664 	  by cases (simp add: condOr)+
  1665 	moreover
  1666 	have "dom (locals (store s0)) 
  1667                      \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1668 	proof -
  1669 	  from condOr wt_binop have e1T: "e1T=PrimT Boolean"
  1670 	    by simp
  1671 	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1672 	    by (auto dest: conf_Boolean)
  1673 	  with True condOr
  1674 	  have v1: "v1=Bool False"
  1675 	    by simp
  1676 	  from eval_e1 normal_s1 
  1677 	  have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1678 	    by (rule assigns_if_good_approx' [elim_format])
  1679 	       (insert wt_e1, simp_all add: e1T v1)
  1680 	  with s0_s1 show ?thesis by (rule Un_least)
  1681 	qed
  1682 	ultimately
  1683 	show ?thesis
  1684 	  using that by (rule da_weakenE) (simp add: True)
  1685       qed
  1686     }
  1687     moreover
  1688     {
  1689       assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
  1690       have ?thesis
  1691       proof -
  1692 	from da notAndOr obtain E1' where
  1693           da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1694                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
  1695 	  and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
  1696 	  by cases simp+
  1697 	from eval_e1 wt_e1 da_e1 wf normal_s1 
  1698 	have "nrm E1' \<subseteq> dom (locals (store s1))"
  1699 	  by (cases rule: da_good_approxE') iprover
  1700 	with da_e2 show ?thesis
  1701 	  using that by (rule da_weakenE) (simp add: True)
  1702       qed
  1703     }
  1704     ultimately show ?thesis
  1705       by (cases binop) auto
  1706   qed
  1707   thus ?thesis ..
  1708 qed
  1709 
  1710 section "main proof of type safety"
  1711     
  1712 lemma eval_type_sound:
  1713   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1714    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  1715    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  1716    and      wf: "wf_prog G" 
  1717    and conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1718   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1719          (error_free s0 = error_free s1)"
  1720 proof -
  1721   note inj_term_simps [simp]
  1722   let ?TypeSafeObj = "\<lambda> s0 s1 t v. 
  1723           \<forall>  L accC T A. s0\<Colon>\<preceq>(G,L) \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T
  1724                       \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A  
  1725                       \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1726                           \<and> (error_free s0 = error_free s1)"
  1727   from eval 
  1728   have "\<And> L accC T A. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  1729                       \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  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    (is "PROP ?TypeSafe s0 s1 t v"
  1733     is "\<And> L accC T A. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1734                  \<Longrightarrow> ?DefAss L accC s0 t A 
  1735                  \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1736                      ?ErrorFree s0 s1")
  1737   proof (induct)
  1738     case (Abrupt s t xc L accC T A) 
  1739     have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
  1740     then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1741       (normal (Some xc, s) 
  1742       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
  1743       (error_free (Some xc, s) = error_free (Some xc, s))"
  1744       by (simp)
  1745   next
  1746     case (Skip s L accC T A)
  1747     have "Norm s\<Colon>\<preceq>(G, L)" and  
  1748            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
  1749     then show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1750               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1751               (error_free (Norm s) = error_free (Norm s))"
  1752       by (simp)
  1753   next
  1754     case (Expr e s0 s1 v L accC T A)
  1755     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1756     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1757     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1758     moreover
  1759     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
  1760     then obtain eT 
  1761       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1762       by (rule wt_elim_cases) (blast)
  1763     moreover
  1764     from Expr.prems obtain E where
  1765       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
  1766       by (elim da_elim_cases) simp
  1767     ultimately 
  1768     obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1769       by (rule hyp [elim_format]) simp
  1770     with wt
  1771     show "s1\<Colon>\<preceq>(G, L) \<and>
  1772           (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1773           (error_free (Norm s0) = error_free s1)"
  1774       by (simp)
  1775   next
  1776     case (Lab c l s0 s1 L accC T A)
  1777     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
  1778     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1779     moreover
  1780     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
  1781     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1782       by (rule wt_elim_cases) (blast)
  1783     moreover from Lab.prems obtain C where
  1784      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
  1785       by (elim da_elim_cases) simp
  1786     ultimately
  1787     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1788            error_free_s1: "error_free s1" 
  1789       by (rule hyp [elim_format]) simp
  1790     from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
  1791       by (cases s1) (auto intro: conforms_absorb)
  1792     with wt error_free_s1
  1793     show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
  1794           (normal (abupd (absorb l) s1)
  1795            \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1796           (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
  1797       by (simp)
  1798   next
  1799     case (Comp c1 c2 s0 s1 s2 L accC T A)
  1800     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1801     have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1802     have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1803     have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
  1804     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1805     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
  1806     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1807                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1808       by (rule wt_elim_cases) (blast)
  1809     from Comp.prems
  1810     obtain C1 C2
  1811       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  1812                       dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and 
  1813             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>In1r c2\<guillemotright> C2" 
  1814       by (elim da_elim_cases) simp
  1815     from conf_s0 wt_c1 da_c1
  1816     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1817            error_free_s1: "error_free s1"
  1818       by (rule hyp_c1 [elim_format]) simp
  1819     show "s2\<Colon>\<preceq>(G, L) \<and>
  1820           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1821           (error_free (Norm s0) = error_free s2)"
  1822     proof (cases "normal s1")
  1823       case False
  1824       with eval_c2 have "s2=s1" by auto
  1825       with conf_s1 error_free_s1 False wt show ?thesis
  1826 	by simp
  1827     next
  1828       case True
  1829       obtain C2' where 
  1830 	"\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
  1831       proof -
  1832 	from eval_c1 wt_c1 da_c1 wf True
  1833 	have "nrm C1 \<subseteq> dom (locals (store s1))"
  1834 	  by (cases rule: da_good_approxE') iprover
  1835 	with da_c2 show ?thesis
  1836 	  by (rule da_weakenE)
  1837       qed
  1838       with conf_s1 wt_c2 
  1839       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1840 	by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
  1841       thus ?thesis
  1842 	using wt by simp
  1843     qed
  1844   next
  1845     case (If b c1 c2 e s0 s1 s2 L accC T)
  1846     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1847     have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1848     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1849     have hyp_then_else: 
  1850             "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
  1851     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1852     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
  1853     then obtain 
  1854               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1855       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1856       (*
  1857                 wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1858                 wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
  1859       by (rule wt_elim_cases) (auto split add: split_if)
  1860     from If.prems obtain E C where
  1861       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  1862                                        \<guillemotright>In1l e\<guillemotright> E" and
  1863       da_then_else: 
  1864       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1865          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  1866           \<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C"
  1867      (*
  1868      da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1869                                       \<union> assigns_if True e) \<guillemotright>In1r c1\<guillemotright> C1" and
  1870      da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1871                                        \<union> assigns_if False e) \<guillemotright>In1r c2\<guillemotright> C2" *)
  1872       by (elim da_elim_cases) (cases "the_Bool b",auto)
  1873     from conf_s0 wt_e da_e  
  1874     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1875       by (rule hyp_e [elim_format]) simp
  1876     show "s2\<Colon>\<preceq>(G, L) \<and>
  1877            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1878            (error_free (Norm s0) = error_free s2)"
  1879     proof (cases "normal s1")
  1880       case False
  1881       with eval_then_else have "s2=s1" by auto
  1882       with conf_s1 error_free_s1 False wt show ?thesis
  1883 	by simp
  1884     next
  1885       case True
  1886       obtain C' where
  1887 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1888           (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
  1889       proof -
  1890 	from eval_e have 
  1891 	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1892 	  by (rule dom_locals_eval_mono_elim)
  1893         moreover
  1894 	from eval_e True wt_e 
  1895 	have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1896 	  by (rule assigns_if_good_approx')
  1897 	ultimately 
  1898 	have "dom (locals (store ((Norm s0)::state))) 
  1899                 \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1900 	  by (rule Un_least)
  1901 	with da_then_else show ?thesis
  1902 	  by (rule da_weakenE)
  1903       qed
  1904       with conf_s1 wt_then_else  
  1905       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1906 	by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
  1907       with wt show ?thesis
  1908 	by simp
  1909     qed
  1910     -- {* Note that we don't have to show that @{term b} really is a boolean 
  1911           value. With @{term the_Bool} we enforce to get a value of boolean 
  1912           type. So execution will be type safe, even if b would be
  1913           a string, for example. We might not expect such a behaviour to be
  1914           called type safe. To remedy the situation we would have to change
  1915           the evaulation rule, so that it only has a type safe evaluation if
  1916           we actually get a boolean value for the condition. That b is actually
  1917           a boolean value is part of @{term hyp_e}. See also Loop 
  1918        *}
  1919   next
  1920     case (Loop b c e l s0 s1 s2 s3 L accC T A)
  1921     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1922     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1923     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1924     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1925     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1926                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1927       by (rule wt_elim_cases) (blast)
  1928     have da:"\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1929             \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A".
  1930     then
  1931     obtain E C where
  1932       da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1933               \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E" and
  1934       da_c: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1935               \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1936                    \<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C" 
  1937       by (rule da_elim_cases) simp
  1938     from conf_s0 wt_e da_e 
  1939     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1940       by (rule hyp_e [elim_format]) simp
  1941     show "s3\<Colon>\<preceq>(G, L) \<and>
  1942           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1943           (error_free (Norm s0) = error_free s3)"
  1944     proof (cases "normal s1")
  1945       case True
  1946       note normal_s1 = this
  1947       show ?thesis
  1948       proof (cases "the_Bool b")
  1949 	case True
  1950 	with Loop.hyps  obtain
  1951           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  1952           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1953 	  by simp 
  1954 	have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
  1955 	  using Loop.hyps True by simp
  1956 	note hyp_c = this [rule_format]
  1957 	have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
  1958           s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1959 	  using Loop.hyps True by simp
  1960 	note hyp_w = this [rule_format]
  1961 	from eval_e have 
  1962 	  s0_s1: "dom (locals (store ((Norm s0)::state)))
  1963                     \<subseteq> dom (locals (store s1))"
  1964 	  by (rule dom_locals_eval_mono_elim)
  1965 	obtain C' where
  1966 	  "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
  1967 	proof -
  1968 	  note s0_s1
  1969           moreover
  1970 	  from eval_e normal_s1 wt_e 
  1971 	  have "assigns_if True e \<subseteq> dom (locals (store s1))"
  1972 	    by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
  1973 	  ultimately 
  1974 	  have "dom (locals (store ((Norm s0)::state))) 
  1975                  \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
  1976 	    by (rule Un_least)
  1977 	  with da_c show ?thesis
  1978 	    by (rule da_weakenE)
  1979 	qed
  1980 	with conf_s1 wt_c  
  1981 	obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1982 	  by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  1983 	from error_free_s2 
  1984 	have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
  1985 	  by simp
  1986 	from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1987 	  by (cases s2) (auto intro: conforms_absorb)
  1988 	moreover note wt
  1989 	moreover
  1990 	obtain A' where 
  1991           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1992               dom (locals(store (abupd (absorb (Cont l)) s2)))
  1993                 \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A'"
  1994 	proof -
  1995 	  note s0_s1
  1996 	  also from eval_c 
  1997 	  have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  1998 	    by (rule dom_locals_eval_mono_elim)
  1999 	  also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  2000 	    by simp
  2001 	  finally
  2002           have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
  2003 	  with da show ?thesis
  2004 	    by (rule da_weakenE)
  2005 	qed
  2006 	ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  2007 	  by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
  2008 	with wt show ?thesis
  2009 	  by simp
  2010       next
  2011 	case False
  2012 	with Loop.hyps have "s3=s1" by simp
  2013 	with conf_s1 error_free_s1 wt
  2014 	show ?thesis
  2015 	  by simp
  2016       qed
  2017     next
  2018       case False
  2019       have "s3=s1"
  2020       proof -
  2021 	from False obtain abr where abr: "abrupt s1 = Some abr"
  2022 	  by (cases s1) auto
  2023 	from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2024 	  by (rule eval_expression_no_jump 
  2025                [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified]) 
  2026              (simp_all add: wf)
  2027 	    
  2028 	show ?thesis
  2029 	proof (cases "the_Bool b")
  2030 	  case True  
  2031 	  with Loop.hyps obtain
  2032             eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  2033             eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  2034 	    by simp
  2035 	  from eval_c abr have "s2=s1" by auto
  2036 	  moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  2037 	    by (cases s1) (simp add: absorb_def)
  2038 	  ultimately show ?thesis
  2039 	    using eval_while abr
  2040 	    by auto
  2041 	next
  2042 	  case False
  2043 	  with Loop.hyps show ?thesis by simp
  2044 	qed
  2045       qed
  2046       with conf_s1 error_free_s1 wt
  2047       show ?thesis
  2048 	by simp
  2049     qed
  2050   next
  2051     case (Jmp j s L accC T A)
  2052     have "Norm s\<Colon>\<preceq>(G, L)" .
  2053     moreover
  2054     from Jmp.prems 
  2055     have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
  2056       by (elim da_elim_cases)
  2057     ultimately have "(Some (Jump j), s)\<Colon>\<preceq>(G, L)" by auto
  2058     then 
  2059     show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  2060            (normal (Some (Jump j), s) 
  2061            \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Jmp j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2062            (error_free (Norm s) = error_free (Some (Jump j), s))"
  2063       by simp
  2064   next
  2065     case (Throw a e s0 s1 L accC T A)
  2066     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  2067     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  2068     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2069     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
  2070     then obtain tn 
  2071       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  2072             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  2073       by (rule wt_elim_cases) (auto)
  2074     from Throw.prems obtain E where 
  2075       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2076              \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2077       by (elim da_elim_cases) simp
  2078     from conf_s0 wt_e da_e obtain
  2079       "s1\<Colon>\<preceq>(G, L)" and
  2080       "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  2081       error_free_s1: "error_free s1"
  2082       by (rule hyp [elim_format]) simp
  2083     with wf throwable
  2084     have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  2085       by (cases s1) (auto dest: Throw_lemma)
  2086     with wt error_free_s1
  2087     show "abupd (throw a) s1\<Colon>\<preceq>(G, L) \<and>
  2088             (normal (abupd (throw a) s1) \<longrightarrow>
  2089             G,L,store (abupd (throw a) s1)\<turnstile>In1r (Throw e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2090             (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  2091       by simp
  2092   next
  2093     case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T A)
  2094     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  2095     have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  2096     have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  2097     have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
  2098     have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  2099     then obtain 
  2100       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2101       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  2102       fresh_vn: "L(VName vn)=None"
  2103       by (rule wt_elim_cases) simp
  2104     from Try.prems obtain C1 C2 where
  2105       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2106                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1"  and
  2107       da_c2:
  2108        "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2109         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>In1r c2\<guillemotright> C2"
  2110       by (elim da_elim_cases) simp
  2111     from conf_s0 wt_c1 da_c1
  2112     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2113       by (rule hyp_c1 [elim_format]) simp
  2114     from conf_s1 sx_alloc wf 
  2115     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  2116       by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits)
  2117     from sx_alloc error_free_s1 
  2118     have error_free_s2: "error_free s2"
  2119       by (rule error_free_sxalloc)
  2120     show "s3\<Colon>\<preceq>(G, L) \<and>
  2121           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  2122           (error_free (Norm s0) = error_free s3)"
  2123     proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
  2124       case False
  2125       from sx_alloc wf
  2126       have eq_s2_s1: "s2=s1"
  2127 	by (rule sxalloc_type_sound [elim_format])
  2128 	   (insert False, auto split: option.splits abrupt.splits )
  2129       with False 
  2130       have "\<not>  G,s2\<turnstile>catch catchC"
  2131 	by (simp add: catch_def)
  2132       with Try
  2133       have "s3=s2"
  2134 	by simp
  2135       with wt conf_s1 error_free_s1 eq_s2_s1
  2136       show ?thesis
  2137 	by simp
  2138     next
  2139       case True
  2140       note exception_s1 = this
  2141       show ?thesis
  2142       proof (cases "G,s2\<turnstile>catch catchC") 
  2143 	case False
  2144 	with Try
  2145 	have "s3=s2"
  2146 	  by simp
  2147 	with wt conf_s2 error_free_s2 
  2148 	show ?thesis
  2149 	  by simp
  2150       next
  2151 	case True
  2152 	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  2153 	from True Try.hyps
  2154 	have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  2155 	  by simp
  2156 	note hyp_c2 = this [rule_format]
  2157 	from exception_s1 sx_alloc wf
  2158 	obtain a 
  2159 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  2160 	  by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
  2161 	with True
  2162 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  2163 	  by (cases s2) simp
  2164 	with xcpt_s2 conf_s2 wf
  2165 	have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  2166 	  by (auto dest: Try_lemma)
  2167 	moreover note wt_c2
  2168 	moreover
  2169 	obtain C2' where
  2170 	  "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2171           \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2172 	proof -
  2173 	  have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  2174                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  2175           proof -
  2176             have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  2177             hence "dom (locals (store ((Norm s0)::state))) 
  2178                     \<subseteq> dom (locals (store s1))"
  2179               by (rule dom_locals_eval_mono_elim)
  2180             also
  2181             from sx_alloc
  2182             have "\<dots> \<subseteq> dom (locals (store s2))"
  2183               by (rule dom_locals_sxalloc_mono)
  2184             also 
  2185             have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  2186               by (cases s2) (simp add: new_xcpt_var_def, blast) 
  2187             also
  2188             have "{VName vn} \<subseteq> \<dots>"
  2189               by (cases s2) simp
  2190             ultimately show ?thesis
  2191               by (rule Un_least)
  2192           qed
  2193 	  with da_c2 show ?thesis
  2194 	    by (rule da_weakenE)
  2195 	qed
  2196 	ultimately
  2197 	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  2198                error_free_s3: "error_free s3"
  2199 	  by (rule hyp_c2 [elim_format])
  2200              (cases s2, simp add: xcpt_s2 error_free_s2) 
  2201 	from conf_s3 fresh_vn 
  2202 	have "s3\<Colon>\<preceq>(G,L)"
  2203 	  by (blast intro: conforms_deallocL)
  2204 	with wt error_free_s3
  2205 	show ?thesis
  2206 	  by simp
  2207       qed
  2208     qed
  2209   next
  2210     case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
  2211     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  2212     have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  2213     have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
  2214                      then (x1, s1)
  2215                      else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  2216     have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
  2217     have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
  2218     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2219     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
  2220     then obtain
  2221       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2222       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  2223       by (rule wt_elim_cases) blast
  2224     from Fin.prems obtain C1 C2 where 
  2225       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2226                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
  2227       da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2228                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c2\<guillemotright> C2"
  2229       by (elim da_elim_cases) simp 
  2230     from conf_s0 wt_c1 da_c1   
  2231     obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  2232       by (rule hyp_c1 [elim_format]) simp
  2233     from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  2234       by (rule conforms_NormI)
  2235     moreover note wt_c2
  2236     moreover obtain C2'
  2237       where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2238                \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2239     proof -
  2240       from eval_c1
  2241       have "dom (locals (store ((Norm s0)::state))) 
  2242              \<subseteq> dom (locals (store (x1,s1)))"
  2243         by (rule dom_locals_eval_mono_elim)
  2244       hence "dom (locals (store ((Norm s0)::state))) 
  2245               \<subseteq> dom (locals (store ((Norm s1)::state)))"
  2246 	by simp
  2247       with da_c2 show ?thesis
  2248 	by (rule da_weakenE)
  2249     qed
  2250     ultimately
  2251     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2252       by (rule hyp_c2 [elim_format]) simp
  2253     from error_free_s1 s3 
  2254     have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  2255       by simp
  2256     show "s3\<Colon>\<preceq>(G, L) \<and>
  2257           (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  2258           (error_free (Norm s0) = error_free s3)"
  2259     proof (cases x1)
  2260       case None with conf_s2 s3' wt show ?thesis by auto
  2261     next
  2262       case (Some x) 
  2263       from eval_c2 have 
  2264 	"dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
  2265 	by (rule dom_locals_eval_mono_elim)
  2266       with Some eval_c2 wf conf_s1 conf_s2
  2267       have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  2268 	by (cases s2) (auto dest: Fin_lemma)
  2269       from Some error_free_s1
  2270       have "\<not> (\<exists> err. x=Error err)"
  2271 	by (simp add: error_free_def)
  2272       with error_free_s2
  2273       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
  2274 	by (cases s2) simp
  2275       with Some wt conf s3' show ?thesis
  2276 	by (cases s2) auto
  2277     qed
  2278   next
  2279     case (Init C c s0 s1 s2 s3 L accC T)
  2280     have     cls: "the (class G C) = c" .
  2281     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2282     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  2283     with cls
  2284     have cls_C: "class G C = Some c"
  2285       by - (erule wt_elim_cases,auto)
  2286     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2287           (error_free (Norm s0) = error_free s3)"
  2288     proof (cases "inited C (globs s0)")
  2289       case True
  2290       with Init.hyps have "s3 = Norm s0"
  2291 	by simp
  2292       with conf_s0 wt show ?thesis 
  2293 	by simp
  2294     next
  2295       case False
  2296       with Init.hyps obtain 
  2297            eval_init_super: 
  2298            "G\<turnstile>Norm ((init_class_obj G C) s0) 
  2299               \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  2300         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  2301 	s3: "s3 = (set_lvars (locals (store s1))) s2" 
  2302 	by simp
  2303       have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
  2304 	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  2305 	using False Init.hyps by simp
  2306       note hyp_init_super = this [rule_format] 
  2307       have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  2308 	using False Init.hyps by simp
  2309       note hyp_init_c = this [rule_format]
  2310       from conf_s0 wf cls_C False
  2311       have "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  2312 	by (auto dest: conforms_init_class_obj)
  2313       moreover from wf cls_C have
  2314 	wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  2315                          \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  2316 	by (cases "C=Object")
  2317            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  2318       moreover
  2319       obtain S where
  2320 	da_init_super:
  2321 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2322           \<turnstile> dom (locals (store ((Norm ((init_class_obj G C) s0))::state))) 
  2323                \<guillemotright>In1r (if C = Object then Skip else Init (super c))\<guillemotright> S"
  2324       proof (cases "C=Object")
  2325 	case True 
  2326 	with da_Skip show ?thesis
  2327 	  using that by (auto intro: assigned.select_convs)
  2328       next
  2329 	case False 
  2330 	with da_Init show ?thesis
  2331 	  by - (rule that, auto intro: assigned.select_convs)
  2332       qed
  2333       ultimately 
  2334       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2335 	by (rule hyp_init_super [elim_format]) simp
  2336       from eval_init_super wt_init_super wf
  2337       have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2338 	by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
  2339               auto)
  2340       with conf_s1
  2341       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  2342 	by (cases s1) (auto intro: conforms_set_locals)
  2343       moreover 
  2344       from error_free_s1
  2345       have error_free_empty: "error_free ((set_lvars empty) s1)"
  2346 	by simp
  2347       from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
  2348 	by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
  2349       moreover from cls_C wf obtain I
  2350 	where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
  2351 	by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
  2352        (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
  2353       then obtain I' where
  2354 	"\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
  2355             \<guillemotright>In1r (init c)\<guillemotright> I'"
  2356 	  by (rule da_weakenE) simp
  2357       ultimately
  2358       obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  2359 	by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
  2360       have "abrupt s2 \<noteq> Some (Jump Ret)"
  2361       proof -
  2362 	from s1_no_ret 
  2363 	have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
  2364 	  by simp
  2365 	moreover
  2366 	from cls_C wf have "jumpNestingOkS {} (init c)"
  2367 	  by (rule wf_prog_cdecl [THEN wf_cdeclE])
  2368 	ultimately 
  2369 	show ?thesis
  2370 	  using eval_init wt_init_c wf
  2371 	  by - (rule eval_statement_no_jump 
  2372                      [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
  2373       qed
  2374       with conf_s2 s3 conf_s1 eval_init
  2375       have "s3\<Colon>\<preceq>(G, L)"
  2376 	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  2377       moreover from error_free_s2 s3
  2378       have "error_free s3"
  2379 	by simp
  2380       moreover note wt
  2381       ultimately show ?thesis
  2382 	by simp
  2383     qed
  2384   next
  2385     case (NewC C a s0 s1 s2 L accC T A)
  2386     have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
  2387     have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
  2388     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
  2389     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2390     moreover
  2391     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  2392     then obtain is_cls_C: "is_class G C" and
  2393                        T: "T=Inl (Class C)"
  2394       by (rule wt_elim_cases) (auto dest: is_acc_classD)
  2395     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" by auto
  2396     moreover obtain I where 
  2397       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2398           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init C)\<guillemotright> I"
  2399       by (auto intro: da_Init [simplified] assigned.select_convs)
  2400      (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2401     ultimately 
  2402     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2403       by (rule hyp [elim_format]) simp 
  2404     from conf_s1 halloc wf is_cls_C
  2405     obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  2406                              "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  2407       by (cases s2) (auto dest!: halloc_type_sound)
  2408     from halloc error_free_s1 
  2409     have "error_free s2"
  2410       by (rule error_free_halloc)
  2411     with halloc_type_safe T
  2412     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2413           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (NewC C)\<succ>In1 (Addr a)\<Colon>\<preceq>T)  \<and>
  2414           (error_free (Norm s0) = error_free s2)"
  2415       by auto
  2416   next
  2417     case (NewA elT a e i s0 s1 s2 s3 L accC T A)
  2418     have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1" .
  2419     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  2420     have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
  2421     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>" .
  2422     have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
  2423     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2424     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T" .
  2425     then obtain
  2426       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
  2427       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  2428             elT: "is_type G elT" and
  2429            T: "T=Inl (elT.[])"
  2430       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  2431     from NewA.prems 
  2432     have da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2433                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2434       by (elim da_elim_cases) simp
  2435     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2436     proof -
  2437       note conf_s0 wt_init
  2438       moreover obtain I where
  2439 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2440          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
  2441       proof (cases "\<exists>C. elT = Class C")
  2442 	case True
  2443 	thus ?thesis
  2444 	  by - (rule that, (auto intro: da_Init [simplified] 
  2445                                         assigned.select_convs
  2446                               simp add: init_comp_ty_def))
  2447 	 (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2448       next
  2449 	case False
  2450 	thus ?thesis
  2451 	by - (rule that, (auto intro: da_Skip [simplified] 
  2452                                       assigned.select_convs
  2453                            simp add: init_comp_ty_def))
  2454          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
  2455       qed
  2456       ultimately show ?thesis
  2457 	by (rule hyp_init [elim_format]) auto
  2458     qed 
  2459     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2460     proof -
  2461       from eval_init 
  2462       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2463 	by (rule dom_locals_eval_mono_elim)
  2464       with da_e 
  2465       obtain A' where
  2466        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2467             \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2468 	by (rule da_weakenE)
  2469       with conf_s1 wt_size
  2470       show ?thesis
  2471 	by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
  2472     qed
  2473     from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  2474       by (cases s2) auto
  2475     with halloc wf elT 
  2476     have halloc_type_safe:
  2477           "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>elT.[])"
  2478       by (cases s3) (auto dest!: halloc_type_sound)
  2479     from halloc error_free_s2
  2480     have "error_free s3"
  2481       by (auto dest: error_free_halloc)
  2482     with halloc_type_safe T
  2483     show "s3\<Colon>\<preceq>(G, L) \<and> 
  2484           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New elT[e])\<succ>In1 (Addr a)\<Colon>\<preceq>T) \<and>
  2485           (error_free (Norm s0) = error_free s3) "
  2486       by simp
  2487   next
  2488     case (Cast castT e s0 s1 s2 v L accC T A)
  2489     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  2490     have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
  2491     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2492     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2493     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
  2494     then obtain eT
  2495       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2496               eT: "G\<turnstile>eT\<preceq>? castT" and 
  2497                T: "T=Inl castT"
  2498       by (rule wt_elim_cases) auto
  2499     from Cast.prems 
  2500     have "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2501                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2502       by (elim da_elim_cases) simp
  2503     with conf_s0 wt_e
  2504     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2505            v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2506       error_free_s1: "error_free s1"
  2507       by (rule hyp [elim_format]) simp
  2508     from conf_s1 s2 
  2509     have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  2510       by (cases s1) simp
  2511     from error_free_s1 s2
  2512     have error_free_s2: "error_free s2"
  2513       by simp
  2514     {
  2515       assume norm_s2: "normal s2"
  2516       have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
  2517       proof -
  2518 	from s2 norm_s2 have "normal s1"
  2519 	  by (cases s1) simp
  2520 	with v_ok 
  2521 	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  2522 	  by simp
  2523 	with eT wf s2 T norm_s2
  2524 	show ?thesis
  2525 	  by (cases s1) (auto dest: fits_conf)
  2526       qed
  2527     }
  2528     with conf_s2 error_free_s2
  2529     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2530            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
  2531            (error_free (Norm s0) = error_free s2)"
  2532       by blast
  2533   next
  2534     case (Inst instT b e s0 s1 v L accC T A)
  2535     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2536     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2537     from Inst.prems obtain eT
  2538     where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
  2539              T: "T=Inl (PrimT Boolean)" 
  2540       by (elim wt_elim_cases) simp
  2541     from Inst.prems 
  2542     have da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2543                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2544       by (elim da_elim_cases) simp
  2545     from conf_s0 wt_e da_e
  2546     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2547               v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>RefT eT" and
  2548       error_free_s1: "error_free s1"
  2549       by (rule hyp [elim_format]) simp
  2550     with T show ?case
  2551       by simp
  2552   next
  2553     case (Lit s v L accC T A)
  2554     then show ?case
  2555       by (auto elim!: wt_elim_cases 
  2556                intro: conf_litval simp add: empty_dt_def)
  2557   next
  2558     case (UnOp e s0 s1 unop v L accC T A)
  2559     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2560     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2561     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
  2562     then obtain eT
  2563       where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2564             wt_unop: "wt_unop unop eT" and
  2565                   T: "T=Inl (PrimT (unop_type unop))" 
  2566       by (auto elim!: wt_elim_cases)
  2567     from UnOp.prems obtain A where
  2568        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2569                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2570       by (elim da_elim_cases) simp
  2571     from conf_s0 wt_e da_e
  2572     obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2573                   wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2574          error_free_s1: "error_free s1"
  2575       by (rule hyp [elim_format]) simp
  2576     from wt_v T wt_unop
  2577     have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
  2578       by (cases unop) auto
  2579     with conf_s1 error_free_s1
  2580     show "s1\<Colon>\<preceq>(G, L) \<and>
  2581      (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
  2582      error_free (Norm s0) = error_free s1"
  2583       by simp
  2584   next
  2585     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T A)
  2586     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" .
  2587     have eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  2588                              else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
  2589     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
  2590     have hyp_e2: "PROP ?TypeSafe       s1  s2 
  2591                    (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
  2592                    (In1 v2)" .
  2593     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2594     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
  2595     then obtain e1T e2T where
  2596          wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
  2597          wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  2598       wt_binop: "wt_binop G binop e1T e2T" and
  2599              T: "T=Inl (PrimT (binop_type binop))"
  2600       by (elim wt_elim_cases) simp
  2601     have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
  2602       by simp
  2603     obtain S where
  2604       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2605                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
  2606       by (auto intro: da_Skip [simplified] assigned.select_convs)
  2607     have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
  2608                   \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A".
  2609     then obtain E1 where
  2610       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2611                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
  2612       by (elim da_elim_cases) simp+
  2613     from conf_s0 wt_e1 da_e1
  2614     obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2615                   wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  2616           error_free_s1: "error_free s1"
  2617       by (rule hyp_e1 [elim_format]) simp
  2618     from wt_binop T
  2619     have conf_v:
  2620       "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  2621       by (cases binop) auto
  2622     -- {* Note that we don't use the information that v1 really is compatible 
  2623           with the expected type e1T and v2 is compatible with e2T, 
  2624           because @{text eval_binop} will anyway produce an output of 
  2625           the right type.
  2626           So evaluating the addition of an integer with a string is type
  2627           safe. This is a little bit annoying since we may regard such a
  2628           behaviour as not type safe.
  2629           If we want to avoid this we can redefine @{text eval_binop} so that
  2630           it only produces a output of proper type if it is assigned to 
  2631           values of the expected types, and arbitrary if the inputs have 
  2632           unexpected types. The proof can easily be adapted since we
  2633           have the hypothesis that the values have a proper type.
  2634           This also applies to unary operations.
  2635        *}
  2636     from eval_e1 have 
  2637       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2638       by (rule dom_locals_eval_mono_elim)
  2639     show "s2\<Colon>\<preceq>(G, L) \<and>
  2640           (normal s2 \<longrightarrow>
  2641         G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  2642           error_free (Norm s0) = error_free s2"
  2643     proof (cases "normal s1")
  2644       case False
  2645       with eval_e2 have "s2=s1" by auto
  2646       with conf_s1 error_free_s1 False show ?thesis
  2647 	by auto
  2648     next
  2649       case True
  2650       note normal_s1 = this
  2651       show ?thesis 
  2652       proof (cases "need_second_arg binop v1")
  2653 	case False
  2654 	with normal_s1 eval_e2 have "s2=s1"
  2655 	  by (cases s1) (simp, elim eval_elim_cases,simp)
  2656 	with conf_s1 conf_v error_free_s1
  2657 	show ?thesis by simp
  2658       next
  2659 	case True
  2660 	note need_second_arg = this
  2661 	with hyp_e2 
  2662 	have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
  2663 	from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
  2664           wt_v1 [rule_format,OF normal_s1] wf
  2665 	obtain E2 where
  2666 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
  2667 	  by (rule da_e2_BinOp [elim_format]) 
  2668              (auto simp add: need_second_arg )
  2669 	with conf_s1 wt_e2 
  2670 	obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  2671 	  by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
  2672 	with conf_v show ?thesis by simp
  2673       qed
  2674     qed
  2675   next
  2676     case (Super s L accC T A)
  2677     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  2678     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  2679     then obtain C c where
  2680              C: "L This = Some (Class C)" and
  2681        neq_Obj: "C\<noteq>Object" and
  2682          cls_C: "class G C = Some c" and
  2683              T: "T=Inl (Class (super c))"
  2684       by (rule wt_elim_cases) auto
  2685     from Super.prems
  2686     obtain "This \<in> dom (locals s)"
  2687       by (elim da_elim_cases) simp
  2688     with conf_s C  have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  2689       by (auto dest: conforms_localD [THEN wlconfD])
  2690     with neq_Obj cls_C wf
  2691     have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  2692       by (auto intro: conf_widen
  2693                 dest: subcls_direct[THEN widen.subcls])
  2694     with T conf_s
  2695     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  2696            (normal (Norm s) \<longrightarrow> 
  2697               G,L,store (Norm s)\<turnstile>In1l Super\<succ>In1 (val_this s)\<Colon>\<preceq>T) \<and>
  2698            (error_free (Norm s) = error_free (Norm s))"
  2699       by simp
  2700   next
  2701     case (Acc upd s0 s1 w v L accC T A) 
  2702     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
  2703     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2704     from Acc.prems obtain vT where
  2705       wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
  2706          T: "T=Inl vT"
  2707       by (elim wt_elim_cases) simp
  2708     from Acc.prems obtain V where
  2709       da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2710                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
  2711       by (cases "\<exists> n. v=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
  2712     {
  2713       fix n assume lvar: "v=LVar n"
  2714       have "locals (store s1) n \<noteq> None"
  2715       proof -
  2716 	from Acc.prems lvar have 
  2717 	  "n \<in> dom (locals s0)"
  2718 	  by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
  2719 	also
  2720 	have "dom (locals s0) \<subseteq> dom (locals (store s1))"
  2721 	proof -
  2722 	  have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
  2723 	  thus ?thesis
  2724 	    by (rule dom_locals_eval_mono_elim) simp
  2725 	qed
  2726 	finally show ?thesis
  2727 	  by blast
  2728       qed
  2729     } note lvar_in_locals = this 
  2730     from conf_s0 wt_v da_v
  2731     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
  2732       and  conf_var: "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In2 v\<succ>In2 (w, upd)\<Colon>\<preceq>Inl vT)"
  2733       and  error_free_s1: "error_free s1"
  2734       by (rule hyp [elim_format]) simp
  2735     from lvar_in_locals conf_var T
  2736     have "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1l (Acc v)\<succ>In1 w\<Colon>\<preceq>T)"
  2737       by (cases "\<exists> n. v=LVar n") auto
  2738     with conf_s1 error_free_s1 show ?case
  2739       by simp
  2740   next
  2741     case (Ass e upd s0 s1 s2 v var w L accC T A)
  2742     have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" .
  2743     have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
  2744     have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" .
  2745     have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
  2746     have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2747     have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
  2748     then obtain varT eT where
  2749 	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  2750 	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2751 	  widen: "G\<turnstile>eT\<preceq>varT" and
  2752               T: "T=Inl eT"
  2753       by (rule wt_elim_cases) auto
  2754     show "assign upd v s2\<Colon>\<preceq>(G, L) \<and>
  2755            (normal (assign upd v s2) \<longrightarrow>
  2756             G,L,store (assign upd v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2757       (error_free (Norm s0) = error_free (assign upd v s2))"
  2758     proof (cases "\<exists> vn. var=LVar vn")
  2759       case False
  2760       with Ass.prems
  2761       obtain V E where
  2762 	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2763                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V" and
  2764 	da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  2765 	by (elim da_elim_cases) simp+
  2766       from conf_s0 wt_var da_var 
  2767       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2768 	and  conf_var: "normal s1 
  2769                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2770 	and  error_free_s1: "error_free s1"
  2771 	by (rule hyp_var [elim_format]) simp
  2772       show ?thesis
  2773       proof (cases "normal s1")
  2774 	case False
  2775 	with eval_e have "s2=s1" by auto
  2776 	with False have "assign upd v s2=s1"
  2777 	  by simp
  2778 	with conf_s1 error_free_s1 False show ?thesis
  2779 	  by auto
  2780       next
  2781 	case True
  2782 	note normal_s1=this
  2783 	obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2784                          \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2785 	proof -
  2786 	  from eval_var wt_var da_var wf normal_s1
  2787 	  have "nrm V \<subseteq>  dom (locals (store s1))"
  2788 	    by (cases rule: da_good_approxE') iprover
  2789 	  with da_e show ?thesis
  2790 	    by (rule da_weakenE) 
  2791 	qed
  2792 	with conf_s1 wt_e 
  2793 	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2794           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2795           error_free_s2: "error_free s2"
  2796 	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2797 	show ?thesis 
  2798 	proof (cases "normal s2")
  2799 	  case False
  2800 	  with conf_s2 error_free_s2 
  2801 	  show ?thesis
  2802 	    by auto
  2803 	next
  2804 	  case True
  2805 	  from True conf_v
  2806 	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2807 	    by simp
  2808 	  with widen wf
  2809 	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2810 	    by (auto intro: conf_widen)
  2811 	  from normal_s1 conf_var
  2812 	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2813 	    by simp
  2814 	  then 
  2815 	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2816 	    by (simp add: rconf_def)
  2817 	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2818 	    eval_e T conf_s2 error_free_s2
  2819 	  show ?thesis
  2820 	    by (cases s1, cases s2) 
  2821 	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2822 	qed
  2823       qed
  2824     next
  2825       case True
  2826       then obtain vn where vn: "var=LVar vn"
  2827 	by blast
  2828       with Ass.prems
  2829       obtain E where
  2830 	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  2831 	           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2832 	by (elim da_elim_cases) simp+
  2833       from da.LVar vn obtain V where
  2834 	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2835                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V"
  2836 	by auto
  2837       obtain E' where
  2838 	da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2839                    \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> E'"
  2840       proof -
  2841 	have "dom (locals (store ((Norm s0)::state))) 
  2842                 \<subseteq> dom (locals (store (s1)))"
  2843 	  by (rule dom_locals_eval_mono_elim)
  2844 	with da_e show ?thesis
  2845 	  by (rule da_weakenE)
  2846       qed
  2847       from conf_s0 wt_var da_var 
  2848       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2849 	and  conf_var: "normal s1 
  2850                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2851 	and  error_free_s1: "error_free s1"
  2852 	by (rule hyp_var [elim_format]) simp
  2853       show ?thesis
  2854       proof (cases "normal s1")
  2855 	case False
  2856 	with eval_e have "s2=s1" by auto
  2857 	with False have "assign upd v s2=s1"
  2858 	  by simp
  2859 	with conf_s1 error_free_s1 False show ?thesis
  2860 	  by auto
  2861       next
  2862 	case True
  2863 	note normal_s1 = this
  2864 	from conf_s1 wt_e da_e'
  2865 	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2866           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2867           error_free_s2: "error_free s2"
  2868 	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2869 	show ?thesis 
  2870 	proof (cases "normal s2")
  2871 	  case False
  2872 	  with conf_s2 error_free_s2 
  2873 	  show ?thesis
  2874 	    by auto
  2875 	next
  2876 	  case True
  2877 	  from True conf_v
  2878 	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2879 	    by simp
  2880 	  with widen wf
  2881 	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2882 	    by (auto intro: conf_widen)
  2883 	  from normal_s1 conf_var
  2884 	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2885 	    by simp
  2886 	  then 
  2887 	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2888 	    by (simp add: rconf_def)
  2889 	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2890 	    eval_e T conf_s2 error_free_s2
  2891 	  show ?thesis
  2892 	    by (cases s1, cases s2) 
  2893 	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2894 	qed
  2895       qed
  2896     qed
  2897   next
  2898     case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A)
  2899     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  2900     have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  2901     have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
  2902     have hyp_if: "PROP ?TypeSafe s1 s2 
  2903                        (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  2904     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2905     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  2906     then obtain T1 T2 statT where
  2907       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  2908       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  2909       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  2910       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  2911       T    : "T=Inl statT"
  2912       by (rule wt_elim_cases) auto
  2913     with Cond.prems obtain E0 E1 E2 where
  2914          da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2915                   \<turnstile> dom (locals (store ((Norm s0)::state))) 
  2916                       \<guillemotright>In1l e0\<guillemotright> E0" and
  2917          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2918                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2919                          \<union> assigns_if True e0) \<guillemotright>In1l e1\<guillemotright> E1" and
  2920          da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2921                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2922                         \<union> assigns_if False e0) \<guillemotright>In1l e2\<guillemotright> E2"
  2923        by (elim da_elim_cases) simp+
  2924     from conf_s0 wt_e0 da_e0  
  2925     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  2926       by (rule hyp_e0 [elim_format]) simp
  2927     show "s2\<Colon>\<preceq>(G, L) \<and>
  2928            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2929            (error_free (Norm s0) = error_free s2)"
  2930     proof (cases "normal s1")
  2931       case False
  2932       with eval_e1_e2 have "s2=s1" by auto
  2933       with conf_s1 error_free_s1 False show ?thesis
  2934 	by auto
  2935     next
  2936       case True
  2937       have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  2938                     \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2939       proof -
  2940 	from eval_e0 have 
  2941 	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2942 	  by (rule dom_locals_eval_mono_elim)
  2943         moreover
  2944 	from eval_e0 True wt_e0 
  2945 	have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2946 	  by (rule assigns_if_good_approx') 
  2947 	ultimately show ?thesis by (rule Un_least)
  2948       qed 
  2949       show ?thesis
  2950       proof (cases "the_Bool b")
  2951 	case True
  2952 	with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  2953 	  by simp
  2954 	from da_e1 s0_s1 True obtain E1' where
  2955 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  2956 	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
  2957 	with conf_s1 wt_e1
  2958 	obtain 
  2959 	  "s2\<Colon>\<preceq>(G, L)"
  2960 	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  2961 	  "error_free s2"            
  2962 	  by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  2963 	moreover
  2964 	from statT  
  2965 	have "G\<turnstile>T1\<preceq>statT"
  2966 	  by auto
  2967 	ultimately show ?thesis
  2968 	  using T wf by auto
  2969       next
  2970 	case False
  2971 	with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  2972 	  by simp
  2973 	from da_e2 s0_s1 False obtain E2' where
  2974 	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  2975 	  by - (rule da_weakenE, auto iff del: Un_subset_iff)
  2976 	with conf_s1 wt_e2
  2977 	obtain 
  2978 	  "s2\<Colon>\<preceq>(G, L)"
  2979 	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  2980 	  "error_free s2"            
  2981 	  by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  2982 	moreover
  2983 	from statT  
  2984 	have "G\<turnstile>T2\<preceq>statT"
  2985 	  by auto
  2986 	ultimately show ?thesis
  2987 	  using T wf by auto
  2988       qed
  2989     qed
  2990   next
  2991     case (Call invDeclC a accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  2992            v vs L accC T A)
  2993     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  2994     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  2995     have invDeclC: "invDeclC 
  2996                       = invocation_declclass G mode (store s2) a statT 
  2997                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
  2998     have init_lvars: 
  2999            "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2".
  3000     have check: "s3' =
  3001        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" .
  3002     have eval_methd: 
  3003            "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  3004     have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  3005     have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  3006     have hyp_methd: "PROP ?TypeSafe s3' s4 
  3007                (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  3008     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3009     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3010                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  3011     from wt obtain pTs statDeclT statM where
  3012                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  3013               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  3014                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  3015                          = {((statDeclT,statM),pTs')}" and
  3016                  mode: "mode = invmode statM e" and
  3017                     T: "T =Inl (resTy statM)" and
  3018         eq_accC_accC': "accC=accC'"
  3019       by (rule wt_elim_cases) fastsimp+
  3020     from Call.prems obtain E where
  3021       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3022                \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3023       da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 args\<guillemotright> A" 
  3024       by (elim da_elim_cases) simp
  3025     from conf_s0 wt_e da_e  
  3026     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3027            conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  3028            error_free_s1: "error_free s1" 
  3029       by (rule hyp_e [elim_format]) simp
  3030     { 
  3031       assume abnormal_s2: "\<not> normal s2"
  3032       have "set_lvars (locals (store s2)) s4 = s2"
  3033       proof -
  3034 	from abnormal_s2 init_lvars 
  3035 	obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  3036              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  3037                                             mode a vs s2)" 
  3038 	  by (auto simp add: init_lvars_def2)
  3039 	moreover
  3040 	from keep_abrupt abnormal_s2 check
  3041 	have eq_s3'_s3: "s3'=s3" 
  3042 	  by (auto simp add: check_method_access_def Let_def)
  3043 	moreover
  3044 	from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  3045 	have "s4=s3'"
  3046 	  by auto
  3047 	ultimately show
  3048 	  "set_lvars (locals (store s2)) s4 = s2"
  3049 	  by (cases s2,cases s3) (simp add: init_lvars_def2)
  3050       qed
  3051     } note propagate_abnormal_s2 = this
  3052     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  3053            (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  3054              G,L,store ((set_lvars (locals (store s2))) s4)
  3055                \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3056            (error_free (Norm s0) =
  3057                 error_free ((set_lvars (locals (store s2))) s4))"
  3058     proof (cases "normal s1")
  3059       case False
  3060       with eval_args have "s2=s1" by auto
  3061       with False propagate_abnormal_s2 conf_s1 error_free_s1 
  3062       show ?thesis
  3063 	by auto
  3064     next
  3065       case True
  3066       note normal_s1 = this
  3067       obtain A' where 
  3068 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  3069       proof -
  3070 	from eval_e wt_e da_e wf normal_s1
  3071 	have "nrm E \<subseteq>  dom (locals (store s1))"
  3072 	  by (cases rule: da_good_approxE') iprover
  3073 	with da_args show ?thesis
  3074 	  by (rule da_weakenE) 
  3075       qed
  3076       with conf_s1 wt_args 
  3077       obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3078               conf_args: "normal s2 
  3079                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  3080           error_free_s2: "error_free s2" 
  3081 	by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  3082       from error_free_s2 init_lvars
  3083       have error_free_s3: "error_free s3"
  3084 	by (auto simp add: init_lvars_def2)
  3085       from statM 
  3086       obtain
  3087 	statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  3088 	pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  3089 	by (blast dest: max_spec2mheads)
  3090       from check
  3091       have eq_store_s3'_s3: "store s3'=store s3"
  3092 	by (cases s3) (simp add: check_method_access_def Let_def)
  3093       obtain invC
  3094 	where invC: "invC = invocation_class mode (store s2) a statT"
  3095 	by simp
  3096       with init_lvars
  3097       have invC': "invC = (invocation_class mode (store s3) a statT)"
  3098 	by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  3099       show ?thesis
  3100       proof (cases "normal s2")
  3101 	case False
  3102 	with propagate_abnormal_s2 conf_s2 error_free_s2
  3103 	show ?thesis
  3104 	  by auto
  3105       next
  3106 	case True
  3107 	note normal_s2 = True
  3108 	with normal_s1 conf_a eval_args 
  3109 	have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  3110 	  by (auto dest: eval_gext intro: conf_gext)
  3111 	show ?thesis
  3112 	proof (cases "a=Null \<longrightarrow> is_static statM")
  3113 	  case False
  3114 	  then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  3115 	    by blast
  3116 	  with normal_s2 init_lvars mode
  3117 	  obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  3118                      "store s3 = store (init_lvars G invDeclC 
  3119                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2)"
  3120 	    by (auto simp add: init_lvars_def2)
  3121 	  moreover
  3122 	  from np check
  3123 	  have eq_s3'_s3: "s3'=s3" 
  3124 	    by (auto simp add: check_method_access_def Let_def)
  3125 	  moreover
  3126 	  from eq_s3'_s3 np eval_methd
  3127 	  have "s4=s3'"
  3128 	    by auto
  3129 	  ultimately have
  3130 	    "set_lvars (locals (store s2)) s4 
  3131             = (Some (Xcpt (Std NullPointer)),store s2)"
  3132 	    by (cases s2,cases s3) (simp add: init_lvars_def2)
  3133 	  with conf_s2 error_free_s2
  3134 	  show ?thesis
  3135 	    by (cases s2) (auto dest: conforms_NormI)
  3136 	next
  3137 	  case True
  3138 	  with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  3139 	    by (auto dest!: Null_staticD)
  3140 	  with conf_s2 conf_a_s2 wf invC  
  3141 	  have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  3142 	    by (cases s2) (auto intro: DynT_propI)
  3143 	  with wt_e statM' invC mode wf 
  3144 	  obtain dynM where 
  3145             dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3146             acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  3147                             in invC dyn_accessible_from accC"
  3148 	    by (force dest!: call_access_ok)
  3149 	  with invC' check eq_accC_accC'
  3150 	  have eq_s3'_s3: "s3'=s3"
  3151 	    by (auto simp add: check_method_access_def Let_def)
  3152 	  from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  3153 	  obtain 
  3154 	    wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  3155 	      dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3156             iscls_invDeclC: "is_class G invDeclC" and
  3157 	         invDeclC': "invDeclC = declclass dynM" and
  3158 	      invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  3159 	     resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  3160 	    is_static_eq: "is_static dynM = is_static statM" and
  3161 	    involved_classes_prop:
  3162              "(if invmode statM e = IntVir
  3163                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  3164                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  3165                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  3166                       statDeclT = ClassT invDeclC)"
  3167 	    by (cases rule: DynT_mheadsE) simp
  3168 	  obtain L' where 
  3169 	   L':"L'=(\<lambda> k. 
  3170                  (case k of
  3171                     EName e
  3172                     \<Rightarrow> (case e of 
  3173                           VNam v 
  3174                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  3175                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  3176                         | Res \<Rightarrow> Some (resTy dynM))
  3177                   | This \<Rightarrow> if is_static statM 
  3178                             then None else Some (Class invDeclC)))"
  3179 	    by simp
  3180 	  from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  3181             wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  3182 	  have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  3183 	    apply - 
  3184                (* FIXME confomrs_init_lvars should be 
  3185                   adjusted to be more directy applicable *)
  3186 	    apply (drule conforms_init_lvars [of G invDeclC 
  3187                     "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  3188                     L statT invC a "(statDeclT,statM)" e])
  3189 	    apply (rule wf)
  3190 	    apply (rule conf_args,assumption)
  3191 	    apply (simp add: pTs_widen)
  3192 	    apply (cases s2,simp)
  3193 	    apply (rule dynM')
  3194 	    apply (force dest: ty_expr_is_type)
  3195 	    apply (rule invC_widen)
  3196 	    apply (force intro: conf_gext dest: eval_gext)
  3197 	    apply simp
  3198 	    apply simp
  3199 	    apply (simp add: invC)
  3200 	    apply (simp add: invDeclC)
  3201 	    apply (simp add: normal_s2)
  3202 	    apply (cases s2, simp add: L' init_lvars
  3203 	                     cong add: lname.case_cong ename.case_cong)
  3204 	    done
  3205 	  with eq_s3'_s3 
  3206 	  have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  3207 	  moreover
  3208 	  from  is_static_eq wf_dynM L'
  3209 	  obtain mthdT where
  3210 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3211                \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  3212 	    mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  3213 	    by - (drule wf_mdecl_bodyD,
  3214                  auto simp add: callee_lcl_def  
  3215                       cong add: lname.case_cong ename.case_cong)
  3216 	  with dynM' iscls_invDeclC invDeclC'
  3217 	  have
  3218 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3219                \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  3220 	    by (auto intro: wt.Methd)
  3221 	  moreover
  3222 	  obtain M where 
  3223 	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  3224 	       \<turnstile> dom (locals (store s3')) 
  3225 	          \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  3226 	  proof -
  3227 	    from wf_dynM
  3228 	    obtain M' where
  3229 	      da_body: 
  3230 	      "\<lparr>prg=G, cls=invDeclC
  3231                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  3232                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  3233               res: "Result \<in> nrm M'"
  3234 	      by (rule wf_mdeclE) iprover
  3235 	    from da_body is_static_eq L' have
  3236 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3237                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  3238 	      by (simp add: callee_lcl_def  
  3239                   cong add: lname.case_cong ename.case_cong)
  3240 	    moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  3241 	    proof -
  3242 	      from is_static_eq 
  3243 	      have "(invmode (mthd dynM) e) = (invmode statM e)"
  3244 		by (simp add: invmode_def)
  3245 	      moreover
  3246 	      have "length (pars (mthd dynM)) = length vs" 
  3247 	      proof -
  3248 		from normal_s2 conf_args
  3249 		have "length vs = length pTs"
  3250 		  by (simp add: list_all2_def)
  3251 		also from pTs_widen
  3252 		have "\<dots> = length pTs'"
  3253 		  by (simp add: widens_def list_all2_def)
  3254 		also from wf_dynM
  3255 		have "\<dots> = length (pars (mthd dynM))"
  3256 		  by (simp add: wf_mdecl_def wf_mhead_def)
  3257 		finally show ?thesis ..
  3258 	      qed
  3259 	      moreover note init_lvars dynM' is_static_eq normal_s2 mode 
  3260 	      ultimately
  3261 	      have "parameters (mthd dynM) = dom (locals (store s3))"
  3262 		using dom_locals_init_lvars 
  3263                   [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
  3264 		by simp
  3265 	      also from check
  3266 	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  3267 		by (simp add:  eq_s3'_s3)
  3268 	      finally show ?thesis .
  3269 	    qed
  3270 	    ultimately obtain M2 where
  3271 	      da:
  3272 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3273                 \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  3274               M2: "nrm M' \<subseteq> nrm M2"
  3275 	      by (rule da_weakenE)
  3276 	    from res M2 have "Result \<in> nrm M2"
  3277 	      by blast
  3278 	    moreover from wf_dynM
  3279 	    have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  3280 	      by (rule wf_mdeclE)
  3281 	    ultimately
  3282 	    obtain M3 where
  3283 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  3284                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  3285 	      using da
  3286 	      by (iprover intro: da.Body assigned.select_convs)
  3287 	    from _ this [simplified]
  3288 	    show ?thesis
  3289 	      by (rule da.Methd [simplified,elim_format])
  3290 	         (auto intro: dynM')
  3291 	  qed
  3292 	  ultimately obtain  
  3293 	    conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  3294 	    conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  3295 	    error_free_s4: "error_free s4"
  3296 	    by (rule hyp_methd [elim_format]) 
  3297                (simp add: error_free_s3 eq_s3'_s3)
  3298 	  from init_lvars eval_methd eq_s3'_s3 
  3299 	  have "store s2\<le>|store s4"
  3300 	    by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  3301 	  moreover
  3302 	  have "abrupt s4 \<noteq> Some (Jump Ret)"
  3303 	  proof -
  3304 	    from normal_s2 init_lvars
  3305 	    have "abrupt s3 \<noteq> Some (Jump Ret)"
  3306 	      by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  3307 	    with check
  3308 	    have "abrupt s3' \<noteq> Some (Jump Ret)"
  3309 	      by (cases s3) (auto simp add: check_method_access_def Let_def)
  3310 	    with eval_methd
  3311 	    show ?thesis
  3312 	      by (rule Methd_no_jump)
  3313 	  qed
  3314 	  ultimately 
  3315 	  have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  3316 	    using conf_s2 conf_s4
  3317 	    by (cases s2,cases s4) (auto intro: conforms_return)
  3318 	  moreover 
  3319 	  from conf_Res mthdT_widen resTy_widen wf
  3320 	  have "normal s4 
  3321                   \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3322 	    by (auto dest: widen_trans)
  3323 	  then
  3324 	  have "normal ((set_lvars (locals (store s2))) s4)
  3325              \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3326 	    by (cases s4) auto
  3327 	  moreover note error_free_s4 T
  3328 	  ultimately 
  3329 	  show ?thesis
  3330 	    by simp
  3331 	qed
  3332       qed
  3333     qed
  3334   next
  3335     case (Methd D s0 s1 sig v L accC T A)
  3336     have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  3337     have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  3338     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3339     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
  3340     then obtain m bodyT where
  3341       D: "is_class G D" and
  3342       m: "methd G D sig = Some m" and
  3343       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  3344                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  3345       T: "T=Inl bodyT"
  3346       by (rule wt_elim_cases) auto
  3347     moreover
  3348     from Methd.prems m have 
  3349        da_body: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3350                    \<turnstile> (dom (locals (store ((Norm s0)::state))))
  3351                        \<guillemotright>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<guillemotright> A"
  3352       by - (erule da_elim_cases,simp)
  3353     ultimately
  3354     show "s1\<Colon>\<preceq>(G, L) \<and> 
  3355            (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3356            (error_free (Norm s0) = error_free s1)"
  3357       using hyp [of _ _ "(Inl bodyT)"] conf_s0 
  3358       by (auto simp add: Let_def body_def)
  3359   next
  3360     case (Body D c s0 s1 s2 s3 L accC T A)
  3361     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  3362     have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  3363     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
  3364     have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
  3365     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3366     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
  3367     then obtain bodyT where
  3368          iscls_D: "is_class G D" and
  3369             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
  3370          resultT: "L Result = Some bodyT" and
  3371       isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  3372                T: "T=Inl bodyT"
  3373       by (rule wt_elim_cases) auto
  3374     from Body.prems obtain C where
  3375       da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3376                    \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1r c\<guillemotright> C" and
  3377       jmpOk: "jumpNestingOkS {Ret} c" and
  3378       res: "Result \<in> nrm C"
  3379       by (elim da_elim_cases) simp
  3380     note conf_s0
  3381     moreover from iscls_D 
  3382     have "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init D\<Colon>\<surd>" by auto
  3383     moreover obtain I where 
  3384       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3385           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init D)\<guillemotright> I"
  3386       by (auto intro: da_Init [simplified] assigned.select_convs)
  3387     ultimately obtain
  3388       conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1:  "error_free s1"
  3389        by (rule hyp_init [elim_format]) simp
  3390     obtain C' where da_C': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3391                              \<turnstile> (dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'"
  3392                and nrm_C': "nrm C \<subseteq> nrm C'"
  3393     proof -
  3394       from eval_init 
  3395       have "(dom (locals (store ((Norm s0)::state)))) 
  3396                      \<subseteq> (dom (locals (store s1)))"
  3397 	by (rule dom_locals_eval_mono_elim)
  3398       with da_c show ?thesis by (rule da_weakenE)
  3399     qed
  3400     from conf_s1 wt_c da_C' 
  3401     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3402       by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  3403     from conf_s2
  3404     have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  3405       by (cases s2) (auto intro: conforms_absorb)
  3406     moreover
  3407     from error_free_s2
  3408     have "error_free (abupd (absorb Ret) s2)"
  3409       by simp
  3410     moreover have "abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump Ret)"
  3411       by (cases s3) (simp add: absorb_def)
  3412     moreover have "s3=s2"
  3413     proof -
  3414       from iscls_D
  3415       have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
  3416 	by auto
  3417       from eval_init wf
  3418       have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  3419 	by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  3420       from eval_c _ wt_c wf
  3421       have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  3422 	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  3423       moreover 
  3424       have "s3 =
  3425                 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  3426                         abrupt s2 = Some (Jump (Cont l))
  3427                  then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
  3428       ultimately show ?thesis 
  3429 	by force
  3430     qed
  3431     moreover
  3432     {
  3433       assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
  3434       have "Result \<in> dom (locals (store s2))"
  3435       proof -
  3436 	from normal_upd_s2
  3437 	have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  3438 	  by (cases s2) (simp add: absorb_def)
  3439 	thus ?thesis
  3440 	proof 
  3441 	  assume "normal s2"
  3442 	  with eval_c wt_c da_C' wf res nrm_C'
  3443 	  show ?thesis
  3444 	    by (cases rule: da_good_approxE') blast
  3445 	next
  3446 	  assume "abrupt s2 = Some (Jump Ret)"
  3447 	  with conf_s2 show ?thesis
  3448 	    by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  3449 	qed 
  3450       qed
  3451     }
  3452     moreover note T resultT
  3453     ultimately
  3454     show "abupd (absorb Ret) s3\<Colon>\<preceq>(G, L) \<and>
  3455            (normal (abupd (absorb Ret) s3) \<longrightarrow>
  3456              G,L,store (abupd (absorb Ret) s3)
  3457              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  3458           (error_free (Norm s0) = error_free (abupd (absorb Ret) s3)) "
  3459       by (cases s2) (auto intro: conforms_locals)
  3460   next
  3461     case (LVar s vn L accC T)
  3462     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and 
  3463              wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
  3464     then obtain vnT where
  3465       vnT: "L vn = Some vnT" and
  3466         T: "T=Inl vnT"
  3467       by (auto elim!: wt_elim_cases)
  3468     from conf_s vnT
  3469     have conf_fst: "locals s vn \<noteq> None \<longrightarrow> G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  3470      by (auto elim: conforms_localD [THEN wlconfD]  
  3471               simp add: lvar_def) 
  3472     moreover
  3473     from conf_s conf_fst vnT 
  3474     have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  3475       by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
  3476     moreover note conf_s T
  3477     ultimately 
  3478     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  3479                  (normal (Norm s) \<longrightarrow>
  3480                     G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  3481                  (error_free (Norm s) = error_free (Norm s))"
  3482       by (simp add: lvar_def) 
  3483   next
  3484     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T A)
  3485     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  3486     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  3487     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  3488     have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  3489     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  3490     have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
  3491     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3492     have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  3493     then obtain statC f where
  3494                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  3495             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  3496        eq_accC_accC': "accC=accC'" and
  3497                 stat: "stat=is_static f" and
  3498 	           T: "T=(Inl (type f))"
  3499       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  3500     from FVar.prems eq_accC_accC'
  3501     have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3502                  \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> A"
  3503       by (elim da_elim_cases) simp
  3504     note conf_s0
  3505     moreover
  3506     from wf wt_e 
  3507     have iscls_statC: "is_class G statC"
  3508       by (auto dest: ty_expr_is_type type_is_class)
  3509     with wf accfield 
  3510     have iscls_statDeclC: "is_class G statDeclC"
  3511       by (auto dest!: accfield_fields dest: fields_declC)
  3512     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  3513       by simp
  3514     moreover obtain I where 
  3515       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3516         \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init statDeclC)\<guillemotright> I"
  3517       by (auto intro: da_Init [simplified] assigned.select_convs)
  3518     ultimately 
  3519     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  3520       by (rule hyp_init [elim_format]) simp
  3521     obtain A' where 
  3522       "\<lparr>prg=G, cls=accC, lcl=L\<rparr> \<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e\<guillemotright> A'"
  3523     proof -
  3524       from eval_init
  3525       have "(dom (locals (store ((Norm s0)::state)))) 
  3526 	       \<subseteq> (dom (locals (store s1)))"
  3527 	by (rule dom_locals_eval_mono_elim)
  3528       with da_e show ?thesis
  3529 	by (rule da_weakenE)
  3530     qed
  3531     with conf_s1 wt_e 
  3532     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3533                   conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  3534            error_free_s2: "error_free s2"
  3535       by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  3536     from fvar 
  3537     have store_s2': "store s2'=store s2"
  3538       by (cases s2) (simp add: fvar_def2)
  3539     with fvar conf_s2 
  3540     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3541       by (cases s2,cases stat) (auto simp add: fvar_def2)
  3542     from eval_init 
  3543     have initd_statDeclC_s1: "initd statDeclC s1"
  3544       by (rule init_yields_initd)
  3545     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  3546     have eq_s3_s2': "s3=s2'"  
  3547       by (auto dest!: error_free_field_access)
  3548     have conf_v: "normal s2' \<Longrightarrow> 
  3549            G,store s2'\<turnstile>fst v\<Colon>\<preceq>type f \<and> store s2'\<le>|snd v\<preceq>type f\<Colon>\<preceq>(G, L)"
  3550     proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  3551       assume normal: "normal s2'"
  3552       obtain vv vf x2 store2 store2'
  3553 	where  v: "v=(vv,vf)" and
  3554               s2: "s2=(x2,store2)" and
  3555          store2': "store s2' = store2'"
  3556 	by (cases v,cases s2,cases s2') blast
  3557       from iscls_statDeclC obtain c
  3558 	where c: "class G statDeclC = Some c"
  3559 	by auto
  3560       have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  3561       proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  3562                                statC G c L "store s1"])
  3563 	from v normal s2 fvar stat store2' 
  3564 	show "((vv, vf), Norm store2') = 
  3565                fvar statDeclC (static f) fn a (x2, store2)"
  3566 	  by (auto simp add: member_is_static_simp)
  3567 	from accfield iscls_statC wf
  3568 	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  3569 	  by (auto dest!: accfield_fields dest: fields_declC)
  3570 	from accfield
  3571 	show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
  3572 	  by (auto dest!: accfield_fields)
  3573 	from wf show "wf_prog G" .
  3574 	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  3575 	  by auto
  3576 	from fld wf iscls_statC
  3577 	show "statDeclC \<noteq> Object "
  3578 	  by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  3579 	from c show "class G statDeclC = Some c" .
  3580 	from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3581 	from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  3582 	from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  3583 	  by simp
  3584       qed
  3585       with v s2 store2'  
  3586       show ?thesis
  3587 	by simp
  3588     qed
  3589     from fvar error_free_s2
  3590     have "error_free s2'"
  3591       by (cases s2)
  3592          (auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
  3593     with conf_v T conf_s2' eq_s3_s2'
  3594     show "s3\<Colon>\<preceq>(G, L) \<and>
  3595           (normal s3 
  3596            \<longrightarrow> G,L,store s3\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3597           (error_free (Norm s0) = error_free s3)"
  3598       by auto
  3599   next
  3600     case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T A)
  3601     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
  3602     have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
  3603     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
  3604     have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
  3605     have avar: "(v, s2') = avar G i a s2" .
  3606     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3607     have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
  3608     then obtain elemT
  3609        where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  3610              wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  3611                  T: "T= Inl elemT"
  3612       by (rule wt_elim_cases) auto
  3613     from AVar.prems obtain E1 where
  3614       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3615                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e1\<guillemotright> E1" and
  3616       da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>In1l e2\<guillemotright> A" 
  3617       by (elim da_elim_cases) simp
  3618     from conf_s0 wt_e1 da_e1  
  3619     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3620             conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  3621             error_free_s1: "error_free s1"
  3622       by (rule hyp_e1 [elim_format]) simp
  3623     show "s2'\<Colon>\<preceq>(G, L) \<and>
  3624            (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3625            (error_free (Norm s0) = error_free s2') "
  3626     proof (cases "normal s1")
  3627       case False
  3628       moreover
  3629       from False eval_e2 have eq_s2_s1: "s2=s1" by auto
  3630       moreover
  3631       from eq_s2_s1 False have  "\<not> normal s2" by simp
  3632       then have "snd (avar G i a s2) = s2"
  3633 	by (cases s2) (simp add: avar_def2)
  3634       with avar have "s2'=s2"
  3635 	by (cases "(avar G i a s2)") simp
  3636       ultimately show ?thesis
  3637 	using conf_s1 error_free_s1
  3638 	by auto
  3639     next
  3640       case True
  3641       obtain A' where 
  3642 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  3643       proof -
  3644 	from eval_e1 wt_e1 da_e1 wf True
  3645 	have "nrm E1 \<subseteq> dom (locals (store s1))"
  3646 	  by (cases rule: da_good_approxE') iprover
  3647 	with da_e2 show ?thesis
  3648 	  by (rule da_weakenE)
  3649       qed
  3650       with conf_s1 wt_e2
  3651       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3652 	by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  3653       from avar 
  3654       have "store s2'=store s2"
  3655 	by (cases s2) (simp add: avar_def2)
  3656       with avar conf_s2 
  3657       have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3658 	by (cases s2) (auto simp add: avar_def2)
  3659       from avar error_free_s2
  3660       have error_free_s2': "error_free s2'"
  3661 	by (cases s2) (auto simp add: avar_def2 )
  3662       have "normal s2' \<Longrightarrow> 
  3663         G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3664       proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  3665 	assume normal: "normal s2'"
  3666 	show ?thesis
  3667 	proof -
  3668 	  obtain vv vf x1 store1 x2 store2 store2'
  3669 	    where  v: "v=(vv,vf)" and
  3670                   s1: "s1=(x1,store1)" and
  3671                   s2: "s2=(x2,store2)" and
  3672 	     store2': "store2'=store s2'"
  3673 	    by (cases v,cases s1, cases s2, cases s2') blast 
  3674 	  have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3675 	  proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  3676                                   OF wf])
  3677 	    from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  3678 	      by simp
  3679 	    from v normal s2 store2' avar 
  3680 	    show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  3681 	      by auto
  3682 	    from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3683 	    from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  3684 	    from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  3685 	  qed
  3686 	  with v s1 s2 store2' 
  3687 	  show ?thesis
  3688 	    by simp
  3689 	qed
  3690       qed
  3691       with conf_s2' error_free_s2' T 
  3692       show ?thesis 
  3693 	by auto
  3694     qed
  3695   next
  3696     case (Nil s0 L accC T)
  3697     then show ?case
  3698       by (auto elim!: wt_elim_cases)
  3699   next
  3700     case (Cons e es s0 s1 s2 v vs L accC T A)
  3701     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  3702     have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
  3703     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  3704     have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
  3705     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  3706     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
  3707     then obtain eT esT where
  3708        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  3709        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  3710        T: "T=Inr (eT#esT)"
  3711       by (rule wt_elim_cases) blast
  3712     from Cons.prems obtain E where
  3713       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3714                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3715       da_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 es\<guillemotright> A" 
  3716       by (elim da_elim_cases) simp
  3717     from conf_s0 wt_e da_e 
  3718     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  3719       conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  3720       by (rule hyp_e [elim_format]) simp
  3721     show 
  3722       "s2\<Colon>\<preceq>(G, L) \<and> 
  3723       (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  3724       (error_free (Norm s0) = error_free s2)"
  3725     proof (cases "normal s1")
  3726       case False
  3727       with eval_es have "s2=s1" by auto
  3728       with False conf_s1 error_free_s1
  3729       show ?thesis
  3730 	by auto
  3731     next
  3732       case True
  3733       obtain A' where 
  3734 	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  3735       proof -
  3736 	from eval_e wt_e da_e wf True
  3737 	have "nrm E \<subseteq> dom (locals (store s1))"
  3738 	  by (cases rule: da_good_approxE') iprover
  3739 	with da_es show ?thesis
  3740 	  by (rule da_weakenE)
  3741       qed
  3742       with conf_s1 wt_es
  3743       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  3744            error_free_s2: "error_free s2" and
  3745            conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  3746 	by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  3747       moreover
  3748       from True eval_es conf_v 
  3749       have conf_v': "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  3750 	apply clarify
  3751 	apply (rule conf_gext)
  3752 	apply (auto dest: eval_gext)
  3753 	done
  3754       ultimately show ?thesis using T by simp
  3755     qed
  3756   qed
  3757   then show ?thesis .
  3758 qed
  3759 
  3760 text {* 
  3761 
  3762 
  3763 *} (* dummy text command to break paragraph for latex;
  3764               large paragraphs exhaust memory of debian pdflatex *)
  3765 
  3766 corollary eval_type_soundE [consumes 5]:
  3767   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  3768   and     conf: "s0\<Colon>\<preceq>(G, L)"
  3769   and       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>t\<Colon>T"
  3770   and       da: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile> dom (locals (snd s0)) \<guillemotright>t\<guillemotright> A"
  3771   and       wf: "wf_prog G"
  3772   and     elim: "\<lbrakk>s1\<Colon>\<preceq>(G, L); normal s1 \<Longrightarrow> G,L,snd s1\<turnstile>t\<succ>v\<Colon>\<preceq>T; 
  3773                   error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
  3774   shows "P"
  3775 using eval wt da wf conf
  3776 by (rule eval_type_sound [elim_format]) (iprover intro: elim) 
  3777 
  3778  
  3779 corollary eval_ts: 
  3780  "\<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;
  3781    \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1l e\<guillemotright>A\<rbrakk> 
  3782 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  3783      (error_free s = error_free s')"
  3784 apply (drule (4) eval_type_sound)
  3785 apply clarsimp
  3786 done
  3787 
  3788 corollary evals_ts: 
  3789 "\<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;
  3790   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In3 es\<guillemotright>A\<rbrakk> 
  3791 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  3792      (error_free s = error_free s')" 
  3793 apply (drule (4) eval_type_sound)
  3794 apply clarsimp
  3795 done
  3796 
  3797 corollary evar_ts: 
  3798 "\<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;
  3799  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In2 v\<guillemotright>A\<rbrakk> \<Longrightarrow>  
  3800   s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  3801   (error_free s = error_free s')"
  3802 apply (drule (4) eval_type_sound)
  3803 apply clarsimp
  3804 done
  3805 
  3806 theorem exec_ts: 
  3807 "\<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>;
  3808  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1r c\<guillemotright>A\<rbrakk> 
  3809  \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  3810 apply (drule (4) eval_type_sound)
  3811 apply clarsimp
  3812 done
  3813 
  3814 lemma wf_eval_Fin: 
  3815   assumes wf:    "wf_prog G" 
  3816     and   wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)"
  3817     and   da_c1: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store (Norm s0)))\<guillemotright>In1r c1\<guillemotright>A"
  3818     and conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" 
  3819     and eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" 
  3820     and eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" 
  3821     and      s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  3822   shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
  3823 proof -
  3824   from eval_c1 wt_c1 da_c1 wf conf_s0
  3825   have "error_free (x1,s1)"
  3826     by (auto dest: eval_type_sound)
  3827   with eval_c1 eval_c2 s3
  3828   show ?thesis
  3829     by - (rule eval.Fin, auto simp add: error_free_def)
  3830 qed
  3831 
  3832 subsection "Ideas for the future"
  3833 
  3834 text {* In the type soundness proof and the correctness proof of 
  3835 definite assignment we perform induction on the evaluation relation with the 
  3836 further preconditions that the term is welltyped and definitely assigned. During
  3837 the proofs we have to establish the welltypedness and definite assignment of 
  3838 the subterms to be able to apply the induction hypothesis. So large parts of
  3839 both proofs are the same work in propagating welltypedness and definite 
  3840 assignment. So we can derive a new induction rule for induction on the 
  3841 evaluation of a wellformed term, were these propagations is already done, once
  3842 and forever. 
  3843 Then we can do the proofs with this rule and can enjoy the time we have saved.
  3844 Here is a first and incomplete sketch of such a rule.*}
  3845 theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab 
  3846                                 Comp If]:
  3847   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  3848    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  3849    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  3850    and      wf: "wf_prog G" 
  3851    and  abrupt: "\<And> s t abr L accC T A. 
  3852                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
  3853                    \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
  3854                   \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
  3855    and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
  3856    and    expr: "\<And> e s0 s1 v L accC eT E.
  3857                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
  3858                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3859                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E;
  3860                   P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1\<rbrakk> 
  3861                  \<Longrightarrow>  P L accC (Norm s0) \<langle>Expr e\<rangle>\<^sub>s \<diamondsuit> s1"
  3862    and     lab: "\<And> c l s0 s1 L accC C.
  3863                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  3864                   \<lparr>prg=G,cls=accC, lcl=L\<rparr>
  3865                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
  3866                   P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1\<rbrakk>
  3867                   \<Longrightarrow> P L accC (Norm s0) \<langle>l\<bullet> c\<rangle>\<^sub>s \<diamondsuit> (abupd (absorb l) s1)"
  3868    and    comp: "\<And> c1 c2 s0 s1 s2 L accC C1.
  3869                  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;G\<turnstile>s1 \<midarrow>c2 \<rightarrow> s2;
  3870                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>;
  3871                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>;
  3872                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3873                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1;
  3874                   P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1;
  3875                   \<And> Q. \<lbrakk>normal s1; 
  3876                          \<And> C2.\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3877                                   \<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2;
  3878                                P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
  3879                         \<rbrakk> \<Longrightarrow> Q 
  3880                   \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3881     and    if: "\<And> b c1 c2 e s0 s1 s2 L accC E.
  3882                 \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
  3883                  G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
  3884                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
  3885                  \<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>;
  3886                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3887                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E;
  3888                  P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1;
  3889                  \<And> Q. \<lbrakk>normal s1;
  3890                         \<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  3891                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  3892                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  3893                               \<rbrakk> \<Longrightarrow> Q
  3894                        \<rbrakk> \<Longrightarrow> Q
  3895                 \<rbrakk> \<Longrightarrow> P L accC (Norm s0) \<langle>If(e) c1 Else c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3896    shows "P L accC s0 t v s1"  
  3897 proof -
  3898   note inj_term_simps [simp]
  3899   from eval 
  3900   show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  3901                        \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  3902         \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
  3903   proof (induct)
  3904     case Abrupt with abrupt show ?case .
  3905   next
  3906     case Skip from skip show ?case by simp
  3907   next
  3908     case (Expr e s0 s1 v L accC T A) 
  3909     from Expr.prems obtain eT where 
  3910       "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
  3911       by (elim wt_elim_cases) 
  3912     moreover
  3913     from Expr.prems obtain E where
  3914       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E"
  3915       by (elim da_elim_cases) simp
  3916     moreover from calculation
  3917     have "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1"
  3918       by (rule Expr.hyps) 
  3919     ultimately show ?case
  3920       by (rule expr)
  3921   next
  3922     case (Lab c l s0 s1 L accC T A)
  3923     from Lab.prems 
  3924     have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  3925       by (elim wt_elim_cases)
  3926     moreover
  3927     from Lab.prems obtain C where
  3928       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C"
  3929       by (elim da_elim_cases) simp
  3930     moreover from calculation
  3931     have "P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1"
  3932       by (rule  Lab.hyps)  
  3933     ultimately show ?case
  3934       by (rule lab)
  3935   next
  3936     case (Comp c1 c2 s0 s1 s2 L accC T A) 
  3937     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  3938     have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  3939     from Comp.prems obtain 
  3940       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  3941       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  3942       by (elim wt_elim_cases) 
  3943     from Comp.prems
  3944     obtain C1 C2
  3945       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  3946                       dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and 
  3947             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2" 
  3948       by (elim da_elim_cases) simp
  3949     from wt_c1 da_c1
  3950     have P_c1: "P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1"
  3951       by (rule Comp.hyps)
  3952     {
  3953       fix Q
  3954       assume normal_s1: "normal s1"
  3955       assume elim: "\<And> C2'. 
  3956                     \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright>C2';
  3957                        P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
  3958       have Q
  3959       proof -
  3960 	obtain C2' where 
  3961 	  da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  3962 	proof -
  3963 	  from eval_c1 wt_c1 da_c1 wf normal_s1
  3964 	  have "nrm C1 \<subseteq> dom (locals (store s1))"
  3965 	    by (cases rule: da_good_approxE') iprover
  3966 	  with da_c2 show ?thesis
  3967 	    by (rule da_weakenE)
  3968 	qed
  3969 	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  3970 	  by (rule Comp.hyps)
  3971 	with da show ?thesis
  3972 	  using elim by iprover
  3973       qed
  3974     }
  3975     with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
  3976     show ?case
  3977       by (rule comp) iprover+
  3978   next
  3979     case (If b c1 c2 e s0 s1 s2 L accC T A)
  3980     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  3981     have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  3982     from If.prems
  3983     obtain 
  3984               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  3985       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  3986       by (elim wt_elim_cases) (auto split add: split_if)
  3987     from If.prems obtain E C where
  3988       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  3989                                        \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  3990       da_then_else: 
  3991       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3992          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  3993           \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C"
  3994       by (elim da_elim_cases) (cases "the_Bool b",auto)
  3995     from wt_e da_e
  3996     have P_e: "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1"
  3997       by (rule If.hyps)
  3998     {
  3999       fix Q
  4000       assume normal_s1: "normal s1"
  4001       assume elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  4002                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  4003                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  4004                               \<rbrakk> \<Longrightarrow> Q"
  4005       have Q
  4006       proof -
  4007 	obtain C' where
  4008 	  da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  4009                 (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
  4010 	proof -
  4011 	  from eval_e have 
  4012 	    "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  4013 	    by (rule dom_locals_eval_mono_elim)
  4014           moreover
  4015 	  from eval_e normal_s1 wt_e 
  4016 	  have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4017 	    by (rule assigns_if_good_approx')
  4018 	  ultimately 
  4019 	  have "dom (locals (store ((Norm s0)::state))) 
  4020             \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4021 	    by (rule Un_least)
  4022 	  with da_then_else show ?thesis
  4023 	    by (rule da_weakenE)
  4024 	qed
  4025 	with wt_then_else
  4026 	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  4027 	  by (rule If.hyps)
  4028 	with da show ?thesis using elim by iprover
  4029       qed
  4030     }
  4031     with eval_e eval_then_else wt_e wt_then_else da_e P_e
  4032     show ?case
  4033       by (rule if) iprover+
  4034   next
  4035     oops
  4036 
  4037 end