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