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