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