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