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