src/HOL/Bali/TypeSafe.thy
author schirmer
Tue Jul 16 20:25:21 2002 +0200 (2002-07-16)
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13601 fd3e3d6b37b2
permissions -rw-r--r--
Added conditional and (&&) and or (||).
     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 = Eval + WellForm + 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       .
    29   next
    30     case New
    31     then show ?case
    32       by (auto split: split_if_asm)
    33   qed
    34   with eqs 
    35   show ?thesis
    36     by simp
    37 qed
    38 
    39 lemma error_free_sxalloc:
    40   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
    41   shows "error_free s1"
    42 proof -
    43   from sxalloc error_free_s0
    44   obtain abrupt0 store0 abrupt1 store1
    45     where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
    46           sxalloc': "G\<turnstile>(abrupt0,store0) \<midarrow>sxalloc\<rightarrow> (abrupt1,store1)" and
    47           error_free_s0': "error_free (abrupt0,store0)"
    48     by (cases s0,cases s1) auto
    49   from sxalloc' error_free_s0'
    50   have "error_free (abrupt1,store1)"
    51   proof (induct)
    52   qed (auto)
    53   with eqs 
    54   show ?thesis 
    55     by simp
    56 qed
    57 
    58 lemma error_free_check_field_access_eq:
    59  "error_free (check_field_access G accC statDeclC fn stat a s)
    60  \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
    61 apply (cases s)
    62 apply (auto simp add: check_field_access_def Let_def error_free_def 
    63                       abrupt_if_def 
    64             split: split_if_asm)
    65 done
    66 
    67 lemma error_free_check_method_access_eq:
    68 "error_free (check_method_access G accC statT mode sig a' s)
    69  \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
    70 apply (cases s)
    71 apply (auto simp add: check_method_access_def Let_def error_free_def 
    72                       abrupt_if_def 
    73             split: split_if_asm)
    74 done
    75 
    76 lemma error_free_FVar_lemma: 
    77      "error_free s 
    78        \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
    79   by (case_tac s) (auto split: split_if) 
    80 
    81 lemma error_free_init_lvars [simp,intro]:
    82 "error_free s \<Longrightarrow> 
    83   error_free (init_lvars G C sig mode a pvs s)"
    84 by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
    85 
    86 lemma error_free_LVar_lemma:   
    87 "error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
    88 by (cases s) simp
    89 
    90 lemma error_free_throw [simp,intro]:
    91   "error_free s \<Longrightarrow> error_free (abupd (throw x) s)"
    92 by (cases s) (simp add: throw_def)
    93 
    94 
    95 section "result conformance"
    96 
    97 constdefs
    98   assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
    99           ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
   100 "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
   101  (\<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>
   102  (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
   103 
   104   rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
   105           ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_"                               [71,71,71,71,71,71] 70)
   106   "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
   107     \<equiv> case T of
   108         Inl T  \<Rightarrow> if (\<exists>vf. t=In2 vf)
   109                   then G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T \<and> s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L)
   110                   else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
   111       | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
   112 
   113 lemma rconf_In1 [simp]: 
   114  "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
   115 apply (unfold rconf_def)
   116 apply (simp (no_asm))
   117 done
   118 
   119 lemma rconf_In2 [simp]: 
   120  "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))"
   121 apply (unfold rconf_def)
   122 apply (simp (no_asm))
   123 done
   124 
   125 lemma rconf_In3 [simp]: 
   126  "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"
   127 apply (unfold rconf_def)
   128 apply (simp (no_asm))
   129 done
   130 
   131 section "fits and conf"
   132 
   133 (* unused *)
   134 lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
   135 apply (unfold fits_def)
   136 apply clarify
   137 apply (erule swap, simp (no_asm_use))
   138 apply (drule conf_RefTD)
   139 apply auto
   140 done
   141 
   142 lemma fits_conf: 
   143   "\<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'"
   144 apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
   145 apply (force dest: conf_RefTD intro: conf_AddrI)
   146 done
   147 
   148 lemma fits_Array: 
   149  "\<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'"
   150 apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
   151 apply (force dest: conf_RefTD intro: conf_AddrI)
   152 done
   153 
   154 
   155 
   156 section "gext"
   157 
   158 lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   159 apply (simp (no_asm_simp) only: split_tupled_all)
   160 apply (erule halloc.induct)
   161 apply  (auto dest!: new_AddrD)
   162 done
   163 
   164 lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   165 apply (simp (no_asm_simp) only: split_tupled_all)
   166 apply (erule sxalloc.induct)
   167 apply   (auto dest!: halloc_gext)
   168 done
   169 
   170 lemma eval_gext_lemma [rule_format (no_asm)]: 
   171  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
   172     In1 v \<Rightarrow> True  
   173   | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
   174   | In3 vs \<Rightarrow> True)"
   175 apply (erule eval_induct)
   176 prefer 26 
   177   apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
   178 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
   179  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
   180             check_field_access_def check_method_access_def Let_def
   181  split del: split_if_asm split add: sum3.split)
   182 (* 6 subgoals *)
   183 apply force+
   184 done
   185 
   186 lemma evar_gext_f: 
   187   "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
   188 apply (drule eval_gext_lemma [THEN conjunct2])
   189 apply auto
   190 done
   191 
   192 lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
   193 
   194 lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2"
   195 apply (drule eval_gext)
   196 apply auto
   197 done
   198 
   199 lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
   200 apply (erule eval_cases , auto split del: split_if_asm)
   201 apply (case_tac "inited C (globs s1)")
   202 apply  (clarsimp split del: split_if_asm)+
   203 apply (drule eval_gext')+
   204 apply (drule init_class_obj_inited)
   205 apply (erule inited_gext)
   206 apply (simp (no_asm_use))
   207 done
   208 
   209 
   210 section "Lemmas"
   211 
   212 lemma obj_ty_obj_class1: 
   213  "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
   214 apply (case_tac "tag obj")
   215 apply (auto simp add: obj_ty_def obj_class_def)
   216 done
   217 
   218 lemma oconf_init_obj: 
   219  "\<lbrakk>wf_prog G;  
   220  (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
   221 \<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   222 apply (auto intro!: oconf_init_obj_lemma unique_fields)
   223 done
   224 
   225 (*
   226 lemma obj_split: "P obj = (\<forall> oi vs. obj = \<lparr>tag=oi,values=vs\<rparr> \<longrightarrow> ?P \<lparr>tag=oi,values=vs\<rparr>)"
   227 apply auto
   228 apply (case_tac "obj")
   229 apply auto
   230 *)
   231 
   232 lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
   233   wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   234                         | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   235   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   236 apply (unfold init_obj_def)
   237 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   238             simp add: obj.update_defs)
   239 done
   240 
   241 lemma conforms_init_class_obj: 
   242  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   243   (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
   244 apply (rule not_initedD [THEN conforms_newG])
   245 apply    (auto)
   246 done
   247 
   248 
   249 lemma fst_init_lvars[simp]: 
   250  "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
   251   (if is_static m then x else (np a') x)"
   252 apply (simp (no_asm) add: init_lvars_def2)
   253 done
   254 
   255 
   256 lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
   257   is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
   258 apply (simp (no_asm_simp) only: split_tupled_all)
   259 apply (case_tac "aa")
   260 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
   261        intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
   262 done
   263 
   264 lemma halloc_type_sound: 
   265 "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
   266   T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
   267   (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
   268 apply (auto elim!: halloc_conforms)
   269 apply (case_tac "aa")
   270 apply (subst obj_ty_eq)
   271 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   272 done
   273 
   274 lemma sxalloc_type_sound: 
   275  "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> case fst s1 of  
   276   None \<Rightarrow> s2 = s1 | Some x \<Rightarrow>  
   277   (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))"
   278 apply (simp (no_asm_simp) only: split_tupled_all)
   279 apply (erule sxalloc.induct)
   280 apply   auto
   281 apply (rule halloc_conforms [THEN conforms_xconf])
   282 apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   283 done
   284 
   285 lemma wt_init_comp_ty: 
   286 "is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
   287 apply (unfold init_comp_ty_def)
   288 apply (clarsimp simp add: accessible_in_RefT_simp 
   289                           is_acc_type_def is_acc_class_def)
   290 done
   291 
   292 
   293 declare fun_upd_same [simp]
   294 
   295 declare fun_upd_apply [simp del]
   296 
   297 
   298 constdefs
   299   DynT_prop::"[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" 
   300                                               ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
   301  "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
   302                      (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
   303 
   304 lemma DynT_propI: 
   305  "\<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> 
   306   \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   307 proof (unfold DynT_prop_def)
   308   assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
   309      and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
   310      and            wf: "wf_prog G"
   311      and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   312   let ?invCls = "(invocation_class mode s a' statT)"
   313   let ?IntVir = "mode = IntVir"
   314   let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
   315                           (if \<exists>T. statT = ArrayT T
   316                                   then invCls = Object
   317                                   else G\<turnstile>Class invCls\<preceq>RefT statT)"
   318   show "?IntVir \<longrightarrow> ?Concl ?invCls"
   319   proof  
   320     assume modeIntVir: ?IntVir 
   321     with mode have not_Null: "a' \<noteq> Null" ..
   322     from statT_a' not_Null state_conform 
   323     obtain a obj 
   324       where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
   325                         "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
   326       by (blast dest: conforms_RefTD)
   327     show "?Concl ?invCls"
   328     proof (cases "tag obj")
   329       case CInst
   330       with modeIntVir obj_props
   331       show ?thesis 
   332 	by (auto dest!: widen_Array2 split add: split_if)
   333     next
   334       case Arr
   335       from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
   336       moreover from Arr have "obj_class obj = Object" 
   337 	by (blast dest: obj_class_Arr1)
   338       moreover note modeIntVir obj_props wf 
   339       ultimately show ?thesis by (auto dest!: widen_Array )
   340     qed
   341   qed
   342 qed
   343 
   344 lemma invocation_methd:
   345 "\<lbrakk>wf_prog G; statT \<noteq> NullT; 
   346  (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
   347  (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
   348  (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
   349  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
   350  dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
   351 \<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
   352 proof -
   353   assume         wf: "wf_prog G"
   354      and  not_NullT: "statT \<noteq> NullT"
   355      and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   356      and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
   357      and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
   358      and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   359      and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
   360                       = Some m"
   361   show ?thesis
   362   proof (cases statT)
   363     case NullT
   364     with not_NullT show ?thesis by simp
   365   next
   366     case IfaceT
   367     with statI_prop obtain I 
   368       where    statI: "statT = IfaceT I" and 
   369             is_iface: "is_iface G I"     and
   370           not_SuperM: "mode \<noteq> SuperM" by blast            
   371     
   372     show ?thesis 
   373     proof (cases mode)
   374       case Static
   375       with wf dynlookup statI is_iface 
   376       show ?thesis
   377 	by (auto simp add: invocation_declclass_def dynlookup_def 
   378                            dynimethd_def dynmethd_C_C 
   379 	            intro: dynmethd_declclass
   380 	            dest!: wf_imethdsD
   381                      dest: table_of_map_SomeI
   382                     split: split_if_asm)
   383     next	
   384       case SuperM
   385       with not_SuperM show ?thesis ..
   386     next
   387       case IntVir
   388       with wf dynlookup IfaceT invC_prop show ?thesis 
   389 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   390                            DynT_prop_def
   391 	            intro: methd_declclass dynmethd_declclass
   392 	            split: split_if_asm)
   393     qed
   394   next
   395     case ClassT
   396     show ?thesis
   397     proof (cases mode)
   398       case Static
   399       with wf ClassT dynlookup statC_prop 
   400       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   401                                intro: dynmethd_declclass)
   402     next
   403       case SuperM
   404       with wf ClassT dynlookup statC_prop 
   405       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   406                                intro: dynmethd_declclass)
   407     next
   408       case IntVir
   409       with wf ClassT dynlookup statC_prop invC_prop 
   410       show ?thesis
   411 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   412                            DynT_prop_def
   413 	            intro: dynmethd_declclass)
   414     qed
   415   next
   416     case ArrayT
   417     show ?thesis
   418     proof (cases mode)
   419       case Static
   420       with wf ArrayT dynlookup show ?thesis
   421 	by (auto simp add: invocation_declclass_def dynlookup_def 
   422                            dynimethd_def dynmethd_C_C
   423                     intro: dynmethd_declclass
   424                      dest: table_of_map_SomeI)
   425     next
   426       case SuperM
   427       with ArrayT statA_prop show ?thesis by blast
   428     next
   429       case IntVir
   430       with wf ArrayT dynlookup invC_prop show ?thesis
   431 	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   432                            DynT_prop_def dynmethd_C_C
   433                     intro: dynmethd_declclass
   434                      dest: table_of_map_SomeI)
   435     qed
   436   qed
   437 qed
   438 
   439 lemma DynT_mheadsD: 
   440 "\<lbrakk>G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT; 
   441   wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
   442   (statDeclT,sm) \<in> mheads G C statT sig; 
   443   invC = invocation_class (invmode sm e) s a' statT;
   444   declC =invocation_declclass G (invmode sm e) s a' statT sig
   445  \<rbrakk> \<Longrightarrow> 
   446   \<exists> dm. 
   447   methd G declC sig = Some dm \<and> dynlookup G statT invC sig = Some dm  \<and> 
   448   G\<turnstile>resTy (mthd dm)\<preceq>resTy sm \<and> 
   449   wf_mdecl G declC (sig, mthd dm) \<and>
   450   declC = declclass dm \<and>
   451   is_static dm = is_static sm \<and>  
   452   is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
   453   (if invmode sm e = IntVir
   454       then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   455       else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   456             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
   457             statDeclT = ClassT (declclass dm))"
   458 proof -
   459   assume invC_prop: "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" 
   460      and        wf: "wf_prog G" 
   461      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   462      and        sm: "(statDeclT,sm) \<in> mheads G C statT sig" 
   463      and      invC: "invC = invocation_class (invmode sm e) s a' statT"
   464      and     declC: "declC = 
   465                     invocation_declclass G (invmode sm e) s a' statT sig"
   466   from wt_e wf have type_statT: "is_type G (RefT statT)"
   467     by (auto dest: ty_expr_is_type)
   468   from sm have not_Null: "statT \<noteq> NullT" by auto
   469   from type_statT 
   470   have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   471     by (auto)
   472   from type_statT wt_e 
   473   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   474                                         invmode sm e \<noteq> SuperM)"
   475     by (auto dest: invocationTypeExpr_noClassD)
   476   from wt_e
   477   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode sm e \<noteq> SuperM)"
   478     by (auto dest: invocationTypeExpr_noClassD)
   479   show ?thesis
   480   proof (cases "invmode sm e = IntVir")
   481     case True
   482     with invC_prop not_Null
   483     have invC_prop': " is_class G invC \<and> 
   484                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
   485                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
   486       by (auto simp add: DynT_prop_def) 
   487     from True 
   488     have "\<not> is_static sm"
   489       by (simp add: invmode_IntVir_eq member_is_static_simp)
   490     with invC_prop' not_Null
   491     have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
   492       by (cases statT) auto
   493     with sm wf type_statT obtain dm where
   494            dm: "dynlookup G statT invC sig = Some dm" and
   495       resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy sm"      and
   496        static: "is_static dm = is_static sm"
   497       by  - (drule dynamic_mheadsD,force+)
   498     with declC invC not_Null 
   499     have declC': "declC = (declclass dm)" 
   500       by (auto simp add: invocation_declclass_def)
   501     with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
   502     have dm': "methd G declC sig = Some dm"
   503       by - (drule invocation_methd,auto)
   504     from wf dm invC_prop' declC' type_statT 
   505     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   506       by (auto dest: dynlookup_declC)
   507     from wf dm' declC_prop declC' 
   508     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   509       by (auto dest: methd_wf_mdecl)
   510     from invC_prop' 
   511     have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
   512       by auto
   513     from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
   514          dm
   515     show ?thesis by auto
   516   next
   517     case False
   518     with type_statT wf invC not_Null wf_I wf_A
   519     have invC_prop': "is_class G invC \<and>  
   520                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   521                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object))"
   522         by (case_tac "statT") (auto simp add: invocation_class_def 
   523                                        split: inv_mode.splits)
   524     with not_Null wf
   525     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   526       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
   527                                             dynimethd_def)
   528     from sm wf wt_e not_Null False invC_prop' obtain "dm" where
   529                     dm: "methd G invC sig = Some dm"          and
   530 	eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
   531 	     eq_mheads:"sm=mhead (mthd dm) "
   532       by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
   533     then have static: "is_static dm = is_static sm" by - (auto)
   534     with declC invC dynlookup_static dm
   535     have declC': "declC = (declclass dm)"  
   536       by (auto simp add: invocation_declclass_def)
   537     from invC_prop' wf declC' dm 
   538     have dm': "methd G declC sig = Some dm"
   539       by (auto intro: methd_declclass)
   540     from dynlookup_static dm 
   541     have dm'': "dynlookup G statT invC sig = Some dm"
   542       by simp
   543     from wf dm invC_prop' declC' type_statT 
   544     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   545       by (auto dest: methd_declC )
   546     then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
   547     from wf dm' declC_prop declC' 
   548     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   549       by (auto dest: methd_wf_mdecl)
   550     from invC_prop' declC_prop declC_prop1
   551     have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   552                        \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
   553       by auto
   554     from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
   555          eq_declC_sm_dm eq_mheads static
   556     show ?thesis by auto
   557   qed
   558 qed   
   559 
   560 lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
   561  isrtype G (statT);
   562  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
   563   mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   564                     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
   565  \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
   566 apply (case_tac "mode = IntVir")
   567 apply (drule conf_RefTD)
   568 apply (force intro!: conf_AddrI 
   569             simp add: obj_class_def split add: obj_tag.split_asm)
   570 apply  clarsimp
   571 apply  safe
   572 apply    (erule (1) widen.subcls [THEN conf_widen])
   573 apply    (erule wf_ws_prog)
   574 
   575 apply    (frule widen_Object) apply (erule wf_ws_prog)
   576 apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
   577 done
   578 
   579 lemma Ass_lemma:
   580 "\<lbrakk> G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2;
   581    G,s2\<turnstile>v\<Colon>\<preceq>eT;s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk>
   582 \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and>
   583       (normal (assign f v (Norm s2)) \<longrightarrow> G,store (assign f v (Norm s2))\<turnstile>v\<Colon>\<preceq>eT)"
   584 apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
   585 apply (drule eval_gext', clarsimp)
   586 apply (erule conf_gext)
   587 apply simp
   588 done
   589 
   590 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
   591     x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
   592 apply (auto split add: split_abrupt_if simp add: throw_def2)
   593 apply (erule conforms_xconf)
   594 apply (frule conf_RefTD)
   595 apply (auto elim: widen.subcls [THEN conf_widen])
   596 done
   597 
   598 lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
   599  (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
   600  \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
   601 apply (rule conforms_allocL)
   602 apply  (erule conforms_NormI)
   603 apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
   604 apply (auto intro!: conf_AddrI)
   605 done
   606 
   607 lemma Fin_lemma: 
   608 "\<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)\<rbrakk> 
   609 \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   610 apply (force elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   611 done
   612 
   613 lemma FVar_lemma1: 
   614 "\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
   615   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; 
   616   statDeclC \<noteq> Object; 
   617   class G statDeclC = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; 
   618   inited statDeclC (globs s1); 
   619   (if static f then id else np a) x2 = None\<rbrakk> 
   620  \<Longrightarrow>  
   621   \<exists>obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
   622                   = Some obj \<and> 
   623   var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
   624           (Inl(fn,statDeclC)) = Some (type f)"
   625 apply (drule initedD)
   626 apply (frule subcls_is_class2, simp (no_asm_simp))
   627 apply (case_tac "static f")
   628 apply  clarsimp
   629 apply  (drule (1) rev_gext_objD, clarsimp)
   630 apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
   631 apply  (rule var_tys_Some_eq [THEN iffD2])
   632 apply  clarsimp
   633 apply  (erule fields_table_SomeI, simp (no_asm))
   634 apply clarsimp
   635 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   636 apply (auto dest!: widen_Array split add: obj_tag.split)
   637 apply (rotate_tac -1) (* to front: tag obja = CInst pid_field_type to enable
   638                          conditional rewrite *)
   639 apply (rule fields_table_SomeI)
   640 apply (auto elim!: fields_mono subcls_is_class2)
   641 done
   642 
   643 lemma FVar_lemma2: "error_free state
   644        \<Longrightarrow> error_free
   645            (assign
   646              (\<lambda>v. supd
   647                    (upd_gobj
   648                      (if static field then Inr statDeclC
   649                       else Inl (the_Addr a))
   650                      (Inl (fn, statDeclC)) v))
   651              w state)"
   652 proof -
   653   assume error_free: "error_free state"
   654   obtain a s where "state=(a,s)"
   655     by (cases state) simp
   656   with error_free
   657   show ?thesis
   658     by (cases a) auto
   659 qed
   660 
   661 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   662 declare split_if     [split del] split_if_asm     [split del] 
   663         option.split [split del] option.split_asm [split del]
   664 ML_setup {*
   665 simpset_ref() := simpset() delloop "split_all_tac";
   666 claset_ref () := claset () delSWrapper "split_all_tac"
   667 *}
   668 lemma FVar_lemma: 
   669 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
   670   G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
   671   table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
   672   wf_prog G;   
   673   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class statC; 
   674   statDeclC \<noteq> Object; class G statDeclC = Some y;   
   675   (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited statDeclC (globs s1)\<rbrakk> \<Longrightarrow>  
   676   G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
   677 apply (unfold assign_conforms_def)
   678 apply (drule sym)
   679 apply (clarsimp simp add: fvar_def2)
   680 apply (drule (9) FVar_lemma1)
   681 apply (clarsimp)
   682 apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   683 apply clarsimp
   684 apply (rule conjI)
   685 apply   clarsimp
   686 apply   (drule (1) rev_gext_objD)
   687 apply   (force elim!: conforms_upd_gobj)
   688 
   689 apply   (blast intro: FVar_lemma2)
   690 done
   691 declare split_paired_All [simp] split_paired_Ex [simp] 
   692 declare split_if     [split] split_if_asm     [split] 
   693         option.split [split] option.split_asm [split]
   694 ML_setup {*
   695 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
   696 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   697 *}
   698 
   699 
   700 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
   701  the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
   702 \<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
   703 apply (erule widen_Array_Array [THEN conf_widen])
   704 apply  (erule_tac [2] wf_ws_prog)
   705 apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   706 defer apply assumption
   707 apply (force intro: var_tys_Some_eq [THEN iffD2])
   708 done
   709 
   710 lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
   711 proof record_split
   712   fix tag values more
   713   show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
   714     by auto
   715 qed
   716  
   717 lemma AVar_lemma2: "error_free state 
   718        \<Longrightarrow> error_free
   719            (assign
   720              (\<lambda>v (x, s').
   721                  ((raise_if (\<not> G,s'\<turnstile>v fits T) ArrStore) x,
   722                   upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
   723              w state)"
   724 proof -
   725   assume error_free: "error_free state"
   726   obtain a s where "state=(a,s)"
   727     by (cases state) simp
   728   with error_free
   729   show ?thesis
   730     by (cases a) auto
   731 qed
   732 
   733 lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
   734   ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
   735   (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)"
   736 apply (unfold assign_conforms_def)
   737 apply (drule sym)
   738 apply (clarsimp simp add: avar_def2)
   739 apply (drule (1) conf_gext)
   740 apply (drule conf_RefTD, clarsimp)
   741 apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
   742 defer
   743 apply   (rule obj_split)
   744 apply clarify
   745 apply (frule obj_ty_widenD)
   746 apply (auto dest!: widen_Class)
   747 apply   (force dest: AVar_lemma1)
   748 
   749 apply   (force elim!: fits_Array dest: gext_objD 
   750          intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
   751 done
   752 
   753 section "Call"
   754 
   755 lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   756   wf_mhead G P sig mh; 
   757   Ball (set lvars) (split (\<lambda>vn. is_type G)); 
   758   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   759   G,s\<turnstile>init_vals (table_of lvars)(pars mh[\<mapsto>]pvs)
   760       [\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   761 apply (unfold wf_mhead_def)
   762 apply clarify
   763 apply (erule (2) Ball_set_table [THEN lconf_init_vals, THEN lconf_ext_list])
   764 apply (drule wf_ws_prog)
   765 apply (erule (2) conf_list_widen)
   766 done
   767 
   768 
   769 lemma lconf_map_lname [simp]: 
   770   "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
   771    =
   772   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   773 apply (unfold lconf_def)
   774 apply safe
   775 apply (case_tac "n")
   776 apply (force split add: lname.split)+
   777 done
   778 
   779 lemma lconf_map_ename [simp]:
   780   "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
   781    =
   782   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   783 apply (unfold lconf_def)
   784 apply safe
   785 apply (force split add: ename.split)+
   786 done
   787 
   788 
   789 lemma defval_conf1 [rule_format (no_asm), elim]: 
   790   "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
   791 apply (unfold conf_def)
   792 apply (induct "T")
   793 apply (auto intro: prim_ty.induct)
   794 done
   795 
   796 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   797 declare split_if     [split del] split_if_asm     [split del] 
   798         option.split [split del] option.split_asm [split del]
   799 ML_setup {*
   800 simpset_ref() := simpset() delloop "split_all_tac";
   801 claset_ref () := claset () delSWrapper "split_all_tac"
   802 *}
   803 lemma conforms_init_lvars: 
   804 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   805   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
   806   (x, s)\<Colon>\<preceq>(G, L); 
   807   methd G declC sig = Some dm;  
   808   isrtype G statT;
   809   G\<turnstile>invC\<preceq>\<^sub>C declC; 
   810   G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
   811   invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
   812   invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
   813        (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   814     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
   815   invC  = invocation_class (invmode (mhd sm) e) s a' statT;
   816   declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
   817   Ball (set (lcls (mbody (mthd dm)))) 
   818        (split (\<lambda>vn. is_type G)) 
   819  \<rbrakk> \<Longrightarrow>  
   820   init_lvars G declC sig (invmode (mhd sm) e) a'  
   821   pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
   822                 (case k of
   823                    EName e \<Rightarrow> (case e of 
   824                                  VNam v 
   825                                   \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
   826                                         (pars (mthd dm)[\<mapsto>]parTs sig)) v
   827                                | Res \<Rightarrow> Some (resTy (mthd dm)))
   828                  | This \<Rightarrow> if (is_static (mthd sm)) 
   829                               then None else Some (Class declC)))"
   830 apply (simp add: init_lvars_def2)
   831 apply (rule conforms_set_locals)
   832 apply  (simp (no_asm_simp) split add: split_if)
   833 apply (drule  (4) DynT_conf)
   834 apply clarsimp
   835 (* apply intro *)
   836 apply (drule (4) conforms_init_lvars_lemma)
   837 apply (case_tac "dm",simp)
   838 apply (rule conjI)
   839 apply (unfold lconf_def, clarify)
   840 apply (rule defval_conf1)
   841 apply (clarsimp simp add: wf_mhead_def is_acc_type_def)
   842 apply (case_tac "is_static sm")
   843 apply simp_all
   844 done
   845 declare split_paired_All [simp] split_paired_Ex [simp] 
   846 declare split_if     [split] split_if_asm     [split] 
   847         option.split [split] option.split_asm [split]
   848 ML_setup {*
   849 claset_ref()  := claset() addSbefore ("split_all_tac", split_all_tac);
   850 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   851 *}
   852 
   853 
   854 
   855 subsection "accessibility"
   856 
   857 text {* 
   858 \par
   859 *} (* dummy text command to break paragraph for latex;
   860               large paragraphs exhaust memory of debian pdflatex *)
   861 
   862 (* #### stat raus und gleich is_static f schreiben *) 
   863 theorem dynamic_field_access_ok:
   864   assumes wf: "wf_prog G" and
   865     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   866    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   867    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   868     normal_s: "normal s" and
   869         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   870            f: "accfield G accC statC fn = Some f" and
   871         dynC: "if stat then dynC=declclass f  
   872                        else dynC=obj_class (lookup_obj (store s) a)" and
   873         stat: "if stat then (is_static f) else (\<not> is_static f)"
   874   shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   875      G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   876 proof (cases "stat")
   877   case True
   878   with stat have static: "(is_static f)" by simp
   879   from True dynC 
   880   have dynC': "dynC=declclass f" by simp
   881   with f
   882   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   883     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   884   moreover
   885   from wt_e wf have "is_class G statC"
   886     by (auto dest!: ty_expr_is_type)
   887   moreover note wf dynC'
   888   ultimately have
   889      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   890     by (auto dest: fields_declC)
   891   with dynC' f static wf
   892   show ?thesis
   893     by (auto dest: static_to_dynamic_accessible_from_static
   894             dest!: accfield_accessibleD )
   895 next
   896   case False
   897   with wf conform_a not_Null conform_s dynC
   898   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   899     "is_class G dynC"
   900     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   901               dest: obj_ty_obj_class1
   902           simp add: obj_ty_obj_class )
   903   with wf f
   904   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   905     by (auto simp add: accfield_def Let_def
   906                  dest: fields_mono
   907                 dest!: table_of_remap_SomeD)
   908   moreover
   909   from f subclseq
   910   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   911     by (auto intro!: static_to_dynamic_accessible_from 
   912                dest: accfield_accessibleD)
   913   ultimately show ?thesis
   914     by blast
   915 qed
   916 
   917 (*
   918 theorem dynamic_field_access_ok:
   919   (assumes wf: "wf_prog G" and
   920      not_Null: "\<not> is_static f \<longrightarrow> a\<noteq>Null" and
   921     conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   922     conform_s: "s\<Colon>\<preceq>(G, L)" and 
   923      normal_s: "normal s" and
   924          wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   925             f: "accfield G accC statC fn = Some f" and
   926          dynC: "if is_static f 
   927                    then dynC=declclass f  
   928                    else dynC=obj_class (lookup_obj (store s) a)" 
   929   ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   930      G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   931 proof (cases "is_static f")
   932   case True
   933   from True dynC 
   934   have dynC': "dynC=declclass f" by simp
   935   with f
   936   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   937     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   938   moreover
   939   from wt_e wf have "is_class G statC"
   940     by (auto dest!: ty_expr_is_type)
   941   moreover note wf dynC'
   942   ultimately have
   943      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   944     by (auto dest: fields_declC)
   945   with dynC' f True wf
   946   show ?thesis
   947     by (auto dest: static_to_dynamic_accessible_from_static
   948             dest!: accfield_accessibleD )
   949 next
   950   case False
   951   with wf conform_a not_Null conform_s dynC
   952   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   953     "is_class G dynC"
   954     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   955               dest: obj_ty_obj_class1
   956           simp add: obj_ty_obj_class )
   957   with wf f
   958   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   959     by (auto simp add: accfield_def Let_def
   960                  dest: fields_mono
   961                 dest!: table_of_remap_SomeD)
   962   moreover
   963   from f subclseq
   964   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   965     by (auto intro!: static_to_dynamic_accessible_from 
   966                dest: accfield_accessibleD)
   967   ultimately show ?thesis
   968     by blast
   969 qed
   970 *)
   971 
   972 
   973 (* ### Einsetzen in case FVar des TypeSoundness Proofs *)
   974 (*
   975 lemma FVar_check_error_free:
   976 (assumes fvar: "(v, s2') = fvar statDeclC stat fn a s2" and 
   977         check: "s3 = check_field_access G accC statDeclC fn stat a s2'" and
   978        conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
   979       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   980     initd_statDeclC_s2: "initd statDeclC s2" and
   981     wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   982     accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   983     stat: "stat=is_static f" and
   984       wf: "wf_prog G"
   985 )  "s3=s2'"
   986 proof -
   987   from fvar 
   988   have store_s2': "store s2'=store s2"
   989     by (cases s2) (simp add: fvar_def2)
   990   with fvar conf_s2 
   991   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
   992     by (cases s2,cases stat) (auto simp add: fvar_def2)
   993   from initd_statDeclC_s2 store_s2' 
   994   have initd_statDeclC_s2': "initd statDeclC s2"
   995     by simp
   996   show ?thesis
   997   proof (cases "normal s2'")
   998     case False
   999     with check show ?thesis 
  1000       by (auto simp add: check_field_access_def Let_def)
  1001   next
  1002     case True
  1003     with fvar store_s2' 
  1004     have not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" 
  1005       by (cases s2) (auto simp add: fvar_def2)
  1006     from True fvar store_s2'
  1007     have "normal s2"
  1008       by (cases s2,cases stat) (auto simp add: fvar_def2)
  1009     with conf_a store_s2'
  1010     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1011       by simp 
  1012     from conf_a' conf_s2'  check True initd_statDeclC_s2' 
  1013       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1014                                    True wt_e accfield ] stat
  1015     show ?thesis
  1016       by (cases stat)
  1017          (auto dest!: initedD
  1018            simp add: check_field_access_def Let_def)
  1019   qed
  1020 qed
  1021 *)
  1022 
  1023 lemma error_free_field_access:
  1024   assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
  1025               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  1026          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
  1027             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
  1028            conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1029             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  1030               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
  1031                 wf: "wf_prog G"   
  1032   shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
  1033 proof -
  1034   from fvar
  1035   have store_s2': "store s2'=store s2"
  1036     by (cases s2) (simp add: fvar_def2)
  1037   with fvar conf_s2 
  1038   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1039     by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1040   from eval_init 
  1041   have initd_statDeclC_s1: "initd statDeclC s1"
  1042     by (rule init_yields_initd)
  1043   with eval_e store_s2'
  1044   have initd_statDeclC_s2': "initd statDeclC s2'"
  1045     by (auto dest: eval_gext intro: inited_gext)
  1046   show ?thesis
  1047   proof (cases "normal s2'")
  1048     case False
  1049     then show ?thesis 
  1050       by (auto simp add: check_field_access_def Let_def)
  1051   next
  1052     case True
  1053     with fvar store_s2' 
  1054     have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
  1055       by (cases s2) (auto simp add: fvar_def2)
  1056     from True fvar store_s2'
  1057     have "normal s2"
  1058       by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1059     with conf_a store_s2'
  1060     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1061       by simp
  1062     from conf_a' conf_s2' True initd_statDeclC_s2' 
  1063       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1064                                    True wt_e accfield ] 
  1065     show ?thesis
  1066       by  (cases "is_static f")
  1067           (auto dest!: initedD
  1068            simp add: check_field_access_def Let_def)
  1069   qed
  1070 qed
  1071 
  1072 lemma call_access_ok:
  1073   assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
  1074       and        wf: "wf_prog G" 
  1075       and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
  1076       and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
  1077       and      invC: "invC = invocation_class (invmode statM e) s a statT"
  1078   shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
  1079   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
  1080 proof -
  1081   from wt_e wf have type_statT: "is_type G (RefT statT)"
  1082     by (auto dest: ty_expr_is_type)
  1083   from statM have not_Null: "statT \<noteq> NullT" by auto
  1084   from type_statT wt_e 
  1085   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
  1086                                         invmode statM e \<noteq> SuperM)"
  1087     by (auto dest: invocationTypeExpr_noClassD)
  1088   from wt_e
  1089   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
  1090     by (auto dest: invocationTypeExpr_noClassD)
  1091   show ?thesis
  1092   proof (cases "invmode statM e = IntVir")
  1093     case True
  1094     with invC_prop not_Null
  1095     have invC_prop': "is_class G invC \<and>  
  1096                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
  1097                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
  1098       by (auto simp add: DynT_prop_def)
  1099     with True not_Null
  1100     have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1101      by (cases statT) (auto simp add: invmode_def) 
  1102     with statM type_statT wf 
  1103     show ?thesis
  1104       by - (rule dynlookup_access,auto)
  1105   next
  1106     case False
  1107     with type_statT wf invC not_Null wf_I wf_A
  1108     have invC_prop': " is_class G invC \<and>
  1109                       ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
  1110                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
  1111         by (case_tac "statT") (auto simp add: invocation_class_def 
  1112                                        split: inv_mode.splits)
  1113     with not_Null wf
  1114     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
  1115       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
  1116                                             dynimethd_def)
  1117    from statM wf wt_e not_Null False invC_prop' obtain dynM where
  1118                 "accmethd G accC invC sig = Some dynM" 
  1119      by (auto dest!: static_mheadsD)
  1120    from invC_prop' False not_Null wf_I
  1121    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1122      by (cases statT) (auto simp add: invmode_def) 
  1123    with statM type_statT wf 
  1124     show ?thesis
  1125       by - (rule dynlookup_access,auto)
  1126   qed
  1127 qed
  1128 
  1129 lemma error_free_call_access:
  1130   assumes
  1131    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
  1132         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
  1133        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
  1134                = {((statDeclT, statM), pTs')}" and
  1135      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1136       conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1137      invProp: "normal s3 \<Longrightarrow>
  1138                 G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
  1139           s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1140                         (invmode statM e) a vs s2" and
  1141         invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
  1142     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
  1143                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
  1144           wf: "wf_prog G"
  1145   shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
  1146    = s3"
  1147 proof (cases "normal s2")
  1148   case False
  1149   with s3 
  1150   have "abrupt s3 = abrupt s2"  
  1151     by (auto simp add: init_lvars_def2)
  1152   with False
  1153   show ?thesis
  1154     by (auto simp add: check_method_access_def Let_def)
  1155 next
  1156   case True
  1157   note normal_s2 = True
  1158   with eval_args
  1159   have normal_s1: "normal s1"
  1160     by (cases "normal s1") auto
  1161   with conf_a eval_args 
  1162   have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1163     by (auto dest: eval_gext intro: conf_gext)
  1164   show ?thesis
  1165   proof (cases "a=Null \<longrightarrow> (is_static statM)")
  1166     case False
  1167     then obtain "\<not> is_static statM" "a=Null" 
  1168       by blast
  1169     with normal_s2 s3
  1170     have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
  1171       by (auto simp add: init_lvars_def2)
  1172     then show ?thesis
  1173       by (auto simp add: check_method_access_def Let_def)
  1174   next
  1175     case True
  1176     from statM 
  1177     obtain
  1178       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1179       by (blast dest: max_spec2mheads)
  1180     from True normal_s2 s3
  1181     have "normal s3"
  1182       by (auto simp add: init_lvars_def2)
  1183     then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
  1184       by (rule invProp)
  1185     with wt_e statM' wf invC
  1186     obtain dynM where 
  1187       dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1188       acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1189                           in invC dyn_accessible_from accC"
  1190       by (force dest!: call_access_ok)
  1191     moreover
  1192     from s3 invC
  1193     have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
  1194       by (cases s2,cases "invmode statM e") 
  1195          (simp add: init_lvars_def2 del: invmode_Static_eq)+
  1196     ultimately
  1197     show ?thesis
  1198       by (auto simp add: check_method_access_def Let_def)
  1199   qed
  1200 qed
  1201 
  1202 section "main proof of type safety"
  1203 
  1204 lemma eval_type_sound:
  1205   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1206             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
  1207             wf: "wf_prog G" and 
  1208        conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1209   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1210          (error_free s0 = error_free s1)"
  1211 proof -
  1212   from eval 
  1213   have "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>  
  1214         \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1215             \<and> (error_free s0 = error_free s1)"
  1216    (is "PROP ?TypeSafe s0 s1 t v"
  1217     is "\<And> L accC T. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1218                  \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1219                      ?ErrorFree s0 s1")
  1220   proof (induct)
  1221     case (Abrupt s t xc L accC T) 
  1222     have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
  1223     then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1224       (normal (Some xc, s) 
  1225       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
  1226       (error_free (Some xc, s) = error_free (Some xc, s))"
  1227       by (simp)
  1228   next
  1229     case (Skip s L accC T)
  1230     have "Norm s\<Colon>\<preceq>(G, L)" and  
  1231            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
  1232     then show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1233               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1234               (error_free (Norm s) = error_free (Norm s))"
  1235       by (simp)
  1236   next
  1237     case (Expr e s0 s1 v L accC T)
  1238     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1239     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1240     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1241     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
  1242     then obtain eT 
  1243       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1244       by (rule wt_elim_cases) (blast)
  1245     with conf_s0 hyp 
  1246     obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1247       by (blast)
  1248     with wt
  1249     show "s1\<Colon>\<preceq>(G, L) \<and>
  1250           (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1251           (error_free (Norm s0) = error_free s1)"
  1252       by (simp)
  1253   next
  1254     case (Lab c l s0 s1 L accC T)
  1255     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
  1256     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1257     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
  1258     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1259       by (rule wt_elim_cases) (blast)
  1260     with conf_s0 hyp
  1261     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1262            error_free_s1: "error_free s1" 
  1263       by (blast)
  1264     from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
  1265       by (cases s1) (auto intro: conforms_absorb)
  1266     with wt error_free_s1
  1267     show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
  1268           (normal (abupd (absorb l) s1)
  1269            \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1270           (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
  1271       by (simp)
  1272   next
  1273     case (Comp c1 c2 s0 s1 s2 L accC T)
  1274     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1275     have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1276     have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1277     have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
  1278     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1279     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
  1280     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1281                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1282       by (rule wt_elim_cases) (blast)
  1283     with conf_s0 hyp_c1 hyp_c2
  1284     obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1285       by (blast)
  1286     with wt
  1287     show "s2\<Colon>\<preceq>(G, L) \<and>
  1288           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1289           (error_free (Norm s0) = error_free s2)"
  1290       by (simp)
  1291   next
  1292     case (If b c1 c2 e s0 s1 s2 L accC T)
  1293     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1294     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1295     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1296     have hyp_then_else: 
  1297             "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
  1298     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1299     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
  1300     then obtain "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
  1301                 "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1302       by (rule wt_elim_cases) (auto split add: split_if)
  1303     with conf_s0 hyp_e hyp_then_else
  1304     obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1305       by (blast)
  1306     with wt
  1307     show "s2\<Colon>\<preceq>(G, L) \<and>
  1308            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1309            (error_free (Norm s0) = error_free s2)"
  1310       by (simp)
  1311   next
  1312     case (Loop b c e l s0 s1 s2 s3 L accC T)
  1313     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1314     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1315     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1316     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1317     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1318                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1319       by (rule wt_elim_cases) (blast)
  1320     from conf_s0 wt_e hyp_e
  1321     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1322       by blast
  1323     show "s3\<Colon>\<preceq>(G, L) \<and>
  1324           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1325           (error_free (Norm s0) = error_free s3)"
  1326     proof (cases "normal s1 \<and> the_Bool b")
  1327       case True
  1328       from Loop True have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" by auto
  1329       from Loop True have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1330 	by auto
  1331       from Loop True have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>"
  1332 	by (auto)
  1333       from Loop True have hyp_w: "PROP ?TypeSafe (abupd (absorb (Cont l)) s2)
  1334                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1335 	by (auto)
  1336       from conf_s1 error_free_s1 wt_c hyp_c
  1337       obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1338 	by blast
  1339       from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1340 	by (cases s2) (auto intro: conforms_absorb)
  1341       moreover
  1342       from error_free_s2 have "error_free (abupd (absorb (Cont l)) s2)"
  1343 	by simp
  1344       moreover note wt hyp_w
  1345       ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  1346 	by blast
  1347       with wt 
  1348       show ?thesis
  1349 	by (simp)
  1350     next
  1351       case False
  1352       with Loop have "s3=s1" by simp
  1353       with conf_s1 error_free_s1 wt
  1354       show ?thesis
  1355 	by (simp)
  1356     qed
  1357   next
  1358     case (Do j s L accC T)
  1359     have "Norm s\<Colon>\<preceq>(G, L)" .
  1360     then 
  1361     show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  1362            (normal (Some (Jump j), s) 
  1363            \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Do j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1364            (error_free (Norm s) = error_free (Some (Jump j), s))"
  1365       by simp
  1366   next
  1367     case (Throw a e s0 s1 L accC T)
  1368     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  1369     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  1370     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1371     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
  1372     then obtain tn 
  1373       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  1374             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  1375       by (rule wt_elim_cases) (auto)
  1376     from conf_s0 wt_e hyp obtain
  1377       "s1\<Colon>\<preceq>(G, L)" and
  1378       "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  1379       error_free_s1: "error_free s1"
  1380       by force
  1381     with wf throwable
  1382     have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  1383       by (cases s1) (auto dest: Throw_lemma)
  1384     with wt error_free_s1
  1385     show "abupd (throw a) s1\<Colon>\<preceq>(G, L) \<and>
  1386             (normal (abupd (throw a) s1) \<longrightarrow>
  1387             G,L,store (abupd (throw a) s1)\<turnstile>In1r (Throw e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1388             (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  1389       by simp
  1390   next
  1391     case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
  1392     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1393     have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1394     have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1395     have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
  1396     have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  1397     then obtain 
  1398       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1399       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  1400       fresh_vn: "L(VName vn)=None"
  1401       by (rule wt_elim_cases) (auto)
  1402     with conf_s0 hyp_c1
  1403     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1404       by blast
  1405     from conf_s1 sx_alloc wf 
  1406     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  1407       by (auto dest: sxalloc_type_sound split: option.splits)
  1408     from sx_alloc error_free_s1 
  1409     have error_free_s2: "error_free s2"
  1410       by (rule error_free_sxalloc)
  1411     show "s3\<Colon>\<preceq>(G, L) \<and>
  1412           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  1413           (error_free (Norm s0) = error_free s3)"
  1414     proof (cases "normal s1")  
  1415       case True
  1416       with sx_alloc wf 
  1417       have eq_s2_s1: "s2=s1"
  1418 	by (auto dest: sxalloc_type_sound split: option.splits)
  1419       with True 
  1420       have "\<not>  G,s2\<turnstile>catch catchC"
  1421 	by (simp add: catch_def)
  1422       with Try
  1423       have "s3=s2"
  1424 	by simp
  1425       with wt conf_s1 error_free_s1 eq_s2_s1
  1426       show ?thesis
  1427 	by simp
  1428     next
  1429       case False
  1430       note exception_s1 = this
  1431       show ?thesis
  1432       proof (cases "G,s2\<turnstile>catch catchC") 
  1433 	case False
  1434 	with Try
  1435 	have "s3=s2"
  1436 	  by simp
  1437 	with wt conf_s2 error_free_s2 
  1438 	show ?thesis
  1439 	  by simp
  1440       next
  1441 	case True
  1442 	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  1443 	from True Try 
  1444 	have hyp_c2: "PROP ?TypeSafe (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1445 	  by auto
  1446 	from exception_s1 sx_alloc wf
  1447 	obtain a 
  1448 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  1449 	  by (auto dest!: sxalloc_type_sound split: option.splits)
  1450 	with True
  1451 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  1452 	  by (cases s2) simp
  1453 	with xcpt_s2 conf_s2 wf
  1454 	have "Norm (lupd(VName vn\<mapsto>Addr a) (store s2))
  1455               \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1456 	  by (auto dest: Try_lemma)
  1457 	with hyp_c2 wt_c2 xcpt_s2 error_free_s2
  1458 	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  1459                error_free_s3: "error_free s3"
  1460 	  by (cases s2) auto
  1461 	from conf_s3 fresh_vn 
  1462 	have "s3\<Colon>\<preceq>(G,L)"
  1463 	  by (blast intro: conforms_deallocL)
  1464 	with wt error_free_s3
  1465 	show ?thesis
  1466 	  by simp
  1467       qed
  1468     qed
  1469   next
  1470     case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
  1471     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  1472     have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  1473     have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
  1474                      then (x1, s1)
  1475                      else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  1476     have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
  1477     have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
  1478     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1479     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
  1480     then obtain
  1481       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1482       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1483       by (rule wt_elim_cases) blast
  1484     from conf_s0 wt_c1 hyp_c1  
  1485     obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  1486       by blast
  1487     from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  1488       by (rule conforms_NormI)
  1489     with wt_c2 hyp_c2
  1490     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1491       by blast
  1492     from error_free_s1 s3 
  1493     have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  1494       by simp
  1495     show "s3\<Colon>\<preceq>(G, L) \<and>
  1496           (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1497           (error_free (Norm s0) = error_free s3)"
  1498     proof (cases x1)
  1499       case None with conf_s2 s3' wt show ?thesis by auto
  1500     next
  1501       case (Some x) 
  1502       with c2 wf conf_s1 conf_s2
  1503       have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  1504 	by (cases s2) (auto dest: Fin_lemma)
  1505       from Some error_free_s1
  1506       have "\<not> (\<exists> err. x=Error err)"
  1507 	by (simp add: error_free_def)
  1508       with error_free_s2
  1509       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
  1510 	by (cases s2) simp
  1511       with Some wt conf s3' show ?thesis
  1512 	by (cases s2) auto
  1513     qed
  1514   next
  1515     case (Init C c s0 s1 s2 s3 L accC T)
  1516     have     cls: "the (class G C) = c" .
  1517     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1518     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  1519     with cls
  1520     have cls_C: "class G C = Some c"
  1521       by - (erule wt_elim_cases,auto)
  1522     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1523           (error_free (Norm s0) = error_free s3)"
  1524     proof (cases "inited C (globs s0)")
  1525       case True
  1526       with Init have "s3 = Norm s0"
  1527 	by simp
  1528       with conf_s0 wt show ?thesis 
  1529 	by simp
  1530     next
  1531       case False
  1532       with Init 
  1533       have "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1534               \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  1535         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  1536 	s3: "s3 = (set_lvars (locals (store s1))) s2" 
  1537 	by auto
  1538       from False Init 
  1539       have hyp_init_super: 
  1540              "PROP ?TypeSafe (Norm ((init_class_obj G C) s0)) s1
  1541 	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  1542 	by auto
  1543       with False Init (* without chaining hyp_init_super, the simplifier will
  1544                           loop! *)
  1545       have hyp_init_c:
  1546 	"PROP ?TypeSafe ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  1547 	by auto
  1548       from conf_s0 wf cls_C False
  1549       have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1550 	by (auto dest: conforms_init_class_obj)
  1551       from wf cls_C have
  1552 	wt_super:"\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1553                    \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1554 	by (cases "C=Object")
  1555            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1556       with conf_s0' hyp_init_super
  1557       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1558 	by blast 
  1559       then
  1560       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1561 	by (cases s1) (auto dest: conforms_set_locals )
  1562       moreover from error_free_s1
  1563       have "error_free ((set_lvars empty) s1)"
  1564 	by simp
  1565       moreover note hyp_init_c wf cls_C 
  1566       ultimately
  1567       obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  1568 	by (auto dest!: wf_prog_cdecl wf_cdecl_wt_init)
  1569       with s3 conf_s1 eval_init
  1570       have "s3\<Colon>\<preceq>(G, L)"
  1571 	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  1572       moreover from error_free_s2 s3
  1573       have "error_free s3"
  1574 	by simp
  1575       moreover note wt
  1576       ultimately show ?thesis
  1577 	by simp
  1578     qed
  1579   next
  1580     case (NewC C a s0 s1 s2 L accC T)
  1581     have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
  1582     have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
  1583     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
  1584     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1585     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  1586     then obtain is_cls_C: "is_class G C" and
  1587                        T: "T=Inl (Class C)"
  1588       by (rule wt_elim_cases) (auto dest: is_acc_classD)
  1589     with conf_s0 hyp
  1590     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1591       by auto
  1592     from conf_s1 halloc wf is_cls_C
  1593     obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  1594                              "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  1595       by (cases s2) (auto dest!: halloc_type_sound)
  1596     from halloc error_free_s1 
  1597     have "error_free s2"
  1598       by (rule error_free_halloc)
  1599     with halloc_type_safe T
  1600     show "s2\<Colon>\<preceq>(G, L) \<and> 
  1601           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (NewC C)\<succ>In1 (Addr a)\<Colon>\<preceq>T)  \<and>
  1602           (error_free (Norm s0) = error_free s2)"
  1603       by auto
  1604   next
  1605     case (NewA T a e i s0 s1 s2 s3 L accC Ta)
  1606     have "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1" .
  1607     have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  1608     have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1609     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
  1610     have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
  1611     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1612     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
  1613     then obtain
  1614       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
  1615       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  1616             T: "is_type G T" and
  1617            Ta: "Ta=Inl (T.[])"
  1618       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  1619     from conf_s0 wt_init hyp_init
  1620     obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  1621       by blast
  1622     with wt_size hyp_size
  1623     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1624       by blast
  1625     from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  1626       by (cases s2) auto
  1627     with halloc wf T 
  1628     have halloc_type_safe:
  1629           "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>T.[])"
  1630       by (cases s3) (auto dest!: halloc_type_sound)
  1631     from halloc error_free_s2
  1632     have "error_free s3"
  1633       by (auto dest: error_free_halloc)
  1634     with halloc_type_safe Ta
  1635     show "s3\<Colon>\<preceq>(G, L) \<and> 
  1636           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New T[e])\<succ>In1 (Addr a)\<Colon>\<preceq>Ta) \<and>
  1637           (error_free (Norm s0) = error_free s3) "
  1638       by simp
  1639   next
  1640     case (Cast castT e s0 s1 s2 v L accC T)
  1641     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1642     have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
  1643     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1644     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1645     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
  1646     then obtain eT
  1647       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1648               eT: "G\<turnstile>eT\<preceq>? castT" and 
  1649                T: "T=Inl castT"
  1650       by (rule wt_elim_cases) auto
  1651     with conf_s0 hyp
  1652     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1653       by blast
  1654     from conf_s1 s2 
  1655     have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  1656       by (cases s1) simp
  1657     from error_free_s1 s2
  1658     have error_free_s2: "error_free s2"
  1659       by simp
  1660     {
  1661       assume norm_s2: "normal s2"
  1662       have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
  1663       proof -
  1664 	from s2 norm_s2 have "normal s1"
  1665 	  by (cases s1) simp
  1666 	with wt_e conf_s0 hyp 
  1667 	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  1668 	  by force
  1669 	with eT wf s2 T norm_s2
  1670 	show ?thesis
  1671 	  by (cases s1) (auto dest: fits_conf)
  1672       qed
  1673     }
  1674     with conf_s2 error_free_s2
  1675     show "s2\<Colon>\<preceq>(G, L) \<and> 
  1676            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
  1677            (error_free (Norm s0) = error_free s2)"
  1678       by blast
  1679   next
  1680     case (Inst T b e s0 s1 v L accC T')
  1681     then show ?case
  1682       by (auto elim!: wt_elim_cases)
  1683   next
  1684     case (Lit s v L accC T)
  1685     then show ?case
  1686       by (auto elim!: wt_elim_cases 
  1687                intro: conf_litval simp add: empty_dt_def)
  1688   next
  1689     case (UnOp e s0 s1 unop v L accC T)
  1690     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1691     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1692     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
  1693     then obtain eT
  1694       where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1695             wt_unop: "wt_unop unop eT" and
  1696                   T: "T=Inl (PrimT (unop_type unop))" 
  1697       by (auto elim!: wt_elim_cases)
  1698     from conf_s0 wt_e 
  1699     obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  1700                   wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  1701          error_free_s1: "error_free s1"
  1702       by (auto dest!: hyp)
  1703     from wt_v T wt_unop
  1704     have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
  1705       by (cases unop) auto
  1706     with conf_s1 error_free_s1
  1707     show "s1\<Colon>\<preceq>(G, L) \<and>
  1708      (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
  1709      error_free (Norm s0) = error_free s1"
  1710       by simp
  1711   next
  1712     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
  1713     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
  1714     have hyp_e2: "PROP ?TypeSafe       s1  s2 
  1715                    (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
  1716                    (In1 v2)" .
  1717     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1718     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
  1719     then obtain e1T e2T where
  1720          wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
  1721          wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  1722       wt_binop: "wt_binop G binop e1T e2T" and
  1723              T: "T=Inl (PrimT (binop_type binop))"
  1724       by (auto elim!: wt_elim_cases)
  1725     have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
  1726       by simp
  1727     from conf_s0 wt_e1 
  1728     obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  1729                   wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  1730           error_free_s1: "error_free s1"
  1731       by (auto dest!: hyp_e1)
  1732     from conf_s1 wt_e2 wt_Skip error_free_s1
  1733     obtain      conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
  1734           error_free_s2: "error_free s2"
  1735       by (cases "need_second_arg binop v1")
  1736          (auto dest!: hyp_e2 )
  1737     from wt_binop T
  1738     have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  1739       by (cases binop) auto
  1740     with conf_s2 conf_s1 error_free_s2 error_free_s1
  1741     show "s2\<Colon>\<preceq>(G, L) \<and>
  1742           (normal s2 \<longrightarrow>
  1743         G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  1744           error_free (Norm s0) = error_free s2"
  1745       by simp
  1746   next
  1747     case (Super s L accC T)
  1748     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  1749     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  1750     then obtain C c where
  1751              C: "L This = Some (Class C)" and
  1752        neq_Obj: "C\<noteq>Object" and
  1753          cls_C: "class G C = Some c" and
  1754              T: "T=Inl (Class (super c))"
  1755       by (rule wt_elim_cases) auto
  1756     from C conf_s have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  1757       by (blast intro: conforms_localD [THEN lconfD])
  1758     with neq_Obj cls_C wf
  1759     have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  1760       by (auto intro: conf_widen
  1761                 dest: subcls_direct[THEN widen.subcls])
  1762     with T conf_s
  1763     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1764            (normal (Norm s) \<longrightarrow> 
  1765               G,L,store (Norm s)\<turnstile>In1l Super\<succ>In1 (val_this s)\<Colon>\<preceq>T) \<and>
  1766            (error_free (Norm s) = error_free (Norm s))"
  1767       by simp
  1768   next
  1769     case (Acc f s0 s1 v va L accC T)
  1770     then show ?case
  1771       by (force elim!: wt_elim_cases)
  1772   next
  1773     case (Ass e f s0 s1 s2 v var w L accC T)
  1774     have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> s1" .
  1775     have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
  1776     have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,f))" .
  1777     have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
  1778     have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1779     have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
  1780     then obtain varT eT where
  1781 	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  1782 	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1783 	  widen: "G\<turnstile>eT\<preceq>varT" and
  1784               T: "T=Inl eT"
  1785       by (rule wt_elim_cases) auto
  1786     from conf_s0 wt_var hyp_var
  1787     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1788       by blast
  1789     with wt_e hyp_e
  1790     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1791       by blast
  1792     show "assign f v s2\<Colon>\<preceq>(G, L) \<and>
  1793            (normal (assign f v s2) \<longrightarrow>
  1794             G,L,store (assign f v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1795             (error_free (Norm s0) = error_free (assign f v s2))"
  1796     proof (cases "normal s1")
  1797       case False
  1798       with eval_e 
  1799       have "s2=s1"
  1800 	by auto
  1801       with False conf_s1 error_free_s1
  1802       show ?thesis
  1803 	by auto
  1804     next
  1805       case True
  1806       note normal_s1=this
  1807       show ?thesis 
  1808       proof (cases "normal s2")
  1809 	case False
  1810 	with conf_s2 error_free_s2 
  1811 	show ?thesis
  1812 	  by auto
  1813       next
  1814 	case True
  1815 	from True normal_s1 conf_s1 wt_e hyp_e
  1816 	have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1817 	  by force
  1818 	with widen wf
  1819 	have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1820 	  by (auto intro: conf_widen)
  1821 	from conf_s0 normal_s1 wt_var hyp_var
  1822 	have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, f)\<Colon>\<preceq>Inl varT"
  1823 	  by blast
  1824 	then 
  1825 	have conf_assign:  "store s1\<le>|f\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1826 	  by auto
  1827 	from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1828 	  eval_e T conf_s2 error_free_s2
  1829 	show ?thesis
  1830 	  by (cases s1, cases s2) 
  1831 	     (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1832       qed
  1833     qed
  1834   next
  1835     case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
  1836     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  1837     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  1838     have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
  1839     have hyp_if: "PROP ?TypeSafe s1 s2 
  1840                        (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  1841     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1842     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  1843     then obtain T1 T2 statT where
  1844       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  1845       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  1846       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  1847       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  1848       T    : "T=Inl statT"
  1849       by (rule wt_elim_cases) auto
  1850     with wt_e0 conf_s0 hyp_e0
  1851     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  1852       by blast
  1853     with wt_e1 wt_e2 statT hyp_if
  1854     obtain dynT where
  1855       conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2" and
  1856       conf_res: 
  1857           "(normal s2 \<longrightarrow>
  1858         G,L,store s2\<turnstile>In1l (if the_Bool b then e1 else e2)\<succ>In1 v\<Colon>\<preceq>Inl dynT)" and
  1859       dynT: "dynT = (if the_Bool b then T1 else T2)"
  1860       by (cases "the_Bool b") force+
  1861     from statT dynT  
  1862     have "G\<turnstile>dynT\<preceq>statT"
  1863       by (cases "the_Bool b") auto
  1864     with conf_s2 conf_res error_free_s2 T wf
  1865     show "s2\<Colon>\<preceq>(G, L) \<and>
  1866            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1867            (error_free (Norm s0) = error_free s2)"
  1868       by (auto)
  1869   next
  1870     case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1871            v vs L accC T)
  1872     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
  1873     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  1874     have invDeclC: "invDeclC 
  1875                       = invocation_declclass G mode (store s2) a' statT 
  1876                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
  1877     have init_lvars: 
  1878            "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2".
  1879     have check: "s3' =
  1880        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
  1881     have eval_methd: 
  1882            "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  1883     have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
  1884     have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  1885     have hyp_methd: "PROP ?TypeSafe s3' s4 
  1886                (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  1887     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1888     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1889                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  1890     from wt obtain pTs statDeclT statM where
  1891                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  1892               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  1893                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  1894                          = {((statDeclT,statM),pTs')}" and
  1895                  mode: "mode = invmode statM e" and
  1896                     T: "T =Inl (resTy statM)" and
  1897         eq_accC_accC': "accC=accC'"
  1898       by (rule wt_elim_cases) auto
  1899     from conf_s0 wt_e hyp_e 
  1900     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1901            conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
  1902            error_free_s1: "error_free s1" 
  1903       by force
  1904     with wt_args hyp_args
  1905     obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1906             conf_args: "normal s2 
  1907                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  1908         error_free_s2: "error_free s2" 
  1909       by force
  1910     from error_free_s2 init_lvars
  1911     have error_free_s3: "error_free s3"
  1912       by (auto simp add: init_lvars_def2)
  1913     from statM 
  1914     obtain
  1915       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1916       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1917       by (blast dest: max_spec2mheads)
  1918     from check
  1919     have eq_store_s3'_s3: "store s3'=store s3"
  1920       by (cases s3) (simp add: check_method_access_def Let_def)
  1921     obtain invC
  1922       where invC: "invC = invocation_class mode (store s2) a' statT"
  1923       by simp
  1924     with init_lvars
  1925     have invC': "invC = (invocation_class mode (store s3) a' statT)"
  1926       by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1927     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  1928              (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  1929                G,L,store ((set_lvars (locals (store s2))) s4)
  1930                \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1931              (error_free (Norm s0) =
  1932                 error_free ((set_lvars (locals (store s2))) s4))"
  1933     proof (cases "normal s2")
  1934       case False
  1935       with init_lvars 
  1936       obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1937              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1938                                             mode a' vs s2)" 
  1939 	by (auto simp add: init_lvars_def2)
  1940       moreover
  1941       from keep_abrupt False check
  1942       have eq_s3'_s3: "s3'=s3" 
  1943 	by (auto simp add: check_method_access_def Let_def)
  1944       moreover
  1945       from eq_s3'_s3 False keep_abrupt eval_methd
  1946       have "s4=s3'"
  1947 	by auto
  1948       ultimately have
  1949 	"set_lvars (locals (store s2)) s4 = s2"
  1950 	by (cases s2,cases s4) (simp add: init_lvars_def2)
  1951       with False conf_s2 error_free_s2
  1952       show ?thesis
  1953 	by auto
  1954     next
  1955       case True
  1956       note normal_s2 = True
  1957       with eval_args
  1958       have normal_s1: "normal s1"
  1959 	by (cases "normal s1") auto
  1960       with conf_a' eval_args 
  1961       have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
  1962 	by (auto dest: eval_gext intro: conf_gext)
  1963       show ?thesis
  1964       proof (cases "a'=Null \<longrightarrow> is_static statM")
  1965 	case False
  1966 	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
  1967 	  by blast
  1968 	with normal_s2 init_lvars mode
  1969 	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1970                    "store s3 = store (init_lvars G invDeclC 
  1971                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
  1972 	  by (auto simp add: init_lvars_def2)
  1973 	moreover
  1974 	from np check
  1975 	have eq_s3'_s3: "s3'=s3" 
  1976 	  by (auto simp add: check_method_access_def Let_def)
  1977 	moreover
  1978 	from eq_s3'_s3 np eval_methd
  1979 	have "s4=s3'"
  1980 	  by auto
  1981 	ultimately have
  1982 	  "set_lvars (locals (store s2)) s4 
  1983            = (Some (Xcpt (Std NullPointer)),store s2)"
  1984 	  by (cases s2,cases s4) (simp add: init_lvars_def2)
  1985 	with conf_s2 error_free_s2
  1986 	show ?thesis
  1987 	  by (cases s2) (auto dest: conforms_NormI)
  1988       next
  1989 	case True
  1990 	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
  1991 	  by (auto dest!: Null_staticD)
  1992 	with conf_s2 conf_a'_s2 wf invC  
  1993 	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1994 	  by (cases s2) (auto intro: DynT_propI)
  1995 	with wt_e statM' invC mode wf 
  1996 	obtain dynM where 
  1997           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1998           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1999                           in invC dyn_accessible_from accC"
  2000 	  by (force dest!: call_access_ok)
  2001 	with invC' check eq_accC_accC'
  2002 	have eq_s3'_s3: "s3'=s3"
  2003 	  by (auto simp add: check_method_access_def Let_def)
  2004 	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  2005 	obtain 
  2006 	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  2007 	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  2008            iscls_invDeclC: "is_class G invDeclC" and
  2009 	        invDeclC': "invDeclC = declclass dynM" and
  2010 	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  2011 	    resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  2012 	   is_static_eq: "is_static dynM = is_static statM" and
  2013 	   involved_classes_prop:
  2014              "(if invmode statM e = IntVir
  2015                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  2016                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  2017                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  2018                       statDeclT = ClassT invDeclC)"
  2019 	  by (auto dest: DynT_mheadsD)
  2020 	obtain L' where 
  2021 	   L':"L'=(\<lambda> k. 
  2022                  (case k of
  2023                     EName e
  2024                     \<Rightarrow> (case e of 
  2025                           VNam v 
  2026                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  2027                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  2028                         | Res \<Rightarrow> Some (resTy dynM))
  2029                   | This \<Rightarrow> if is_static statM 
  2030                             then None else Some (Class invDeclC)))"
  2031 	  by simp
  2032 	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  2033              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
  2034 	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  2035 	  apply - 
  2036              (* FIXME confomrs_init_lvars should be 
  2037                 adjusted to be more directy applicable *)
  2038 	  apply (drule conforms_init_lvars [of G invDeclC 
  2039                   "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  2040                   L statT invC a' "(statDeclT,statM)" e])
  2041 	  apply (rule wf)
  2042 	  apply (rule conf_args,assumption)
  2043 	  apply (simp add: pTs_widen)
  2044 	  apply (cases s2,simp)
  2045 	  apply (rule dynM')
  2046 	  apply (force dest: ty_expr_is_type)
  2047 	  apply (rule invC_widen)
  2048 	  apply (force intro: conf_gext dest: eval_gext)
  2049 	  apply simp
  2050 	  apply simp
  2051 	  apply (simp add: invC)
  2052 	  apply (simp add: invDeclC)
  2053 	  apply (force dest: wf_mdeclD1 is_acc_typeD)
  2054 	  apply (cases s2, simp add: L' init_lvars
  2055 	                      cong add: lname.case_cong ename.case_cong)
  2056 	  done 
  2057 	from  is_static_eq wf_dynM L'
  2058 	obtain mthdT where
  2059 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  2060             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  2061 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  2062 	  by - (drule wf_mdecl_bodyD,
  2063                 auto simp: cong add: lname.case_cong ename.case_cong)
  2064 	with dynM' iscls_invDeclC invDeclC'
  2065 	have
  2066 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  2067             \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  2068 	  by (auto intro: wt.Methd)
  2069 	with eq_s3'_s3 conf_s3 error_free_s3 
  2070              hyp_methd [of L' invDeclC "Inl mthdT"]
  2071 	obtain  conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  2072 	       conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  2073 	  error_free_s4: "error_free s4"
  2074 	  by auto
  2075 	from init_lvars eval_methd eq_s3'_s3 
  2076 	have "store s2\<le>|store s4"
  2077 	  by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  2078 	with conf_s2 conf_s4
  2079 	have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  2080 	  by (cases s2,cases s4) (auto intro: conforms_return)
  2081 	moreover 
  2082 	from conf_Res mthdT_widen resTy_widen wf
  2083 	have "normal s4 
  2084              \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  2085 	  by (auto dest: widen_trans)
  2086 	then
  2087 	have "normal ((set_lvars (locals (store s2))) s4)
  2088              \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  2089 	  by (cases s4) auto
  2090 	moreover note error_free_s4 T
  2091 	ultimately 
  2092 	show ?thesis
  2093 	  by simp
  2094       qed
  2095     qed
  2096   next
  2097     case (Methd D s0 s1 sig v L accC T)
  2098     have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  2099     have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  2100     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2101     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
  2102     then obtain m bodyT where
  2103       D: "is_class G D" and
  2104       m: "methd G D sig = Some m" and
  2105       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  2106                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  2107       T: "T=Inl bodyT"
  2108       by (rule wt_elim_cases) auto
  2109     with hyp [of _ _ "(Inl bodyT)"] conf_s0 
  2110     show "s1\<Colon>\<preceq>(G, L) \<and> 
  2111            (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2112            (error_free (Norm s0) = error_free s1)"
  2113       by (auto simp add: Let_def body_def)
  2114   next
  2115     case (Body D c s0 s1 s2 L accC T)
  2116     have "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  2117     have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  2118     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
  2119     have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
  2120     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2121     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
  2122     then obtain bodyT where
  2123          iscls_D: "is_class G D" and
  2124             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
  2125          resultT: "L Result = Some bodyT" and
  2126       isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  2127                T: "T=Inl bodyT"
  2128       by (rule wt_elim_cases) auto
  2129     from conf_s0 iscls_D hyp_init
  2130     obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  2131       by auto
  2132     with wt_c hyp_c
  2133     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2134       by blast
  2135     from conf_s2
  2136     have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  2137       by (cases s2) (auto intro: conforms_absorb)
  2138     moreover
  2139     from error_free_s2
  2140     have "error_free (abupd (absorb Ret) s2)"
  2141       by simp
  2142     moreover note T resultT
  2143     ultimately
  2144     show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
  2145            (normal (abupd (absorb Ret) s2) \<longrightarrow>
  2146              G,L,store (abupd (absorb Ret) s2)
  2147              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  2148           (error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
  2149       by (cases s2) (auto intro: conforms_locals)
  2150   next
  2151     case (LVar s vn L accC T)
  2152     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and 
  2153              wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
  2154     then obtain vnT where
  2155       vnT: "L vn = Some vnT" and
  2156         T: "T=Inl vnT"
  2157       by (auto elim!: wt_elim_cases)
  2158     from conf_s vnT
  2159     have conf_fst: "G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  2160       by (auto elim: conforms_localD [THEN lconfD]  
  2161                simp add: lvar_def)
  2162     moreover
  2163     from conf_s conf_fst vnT 
  2164     have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  2165       by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
  2166     moreover note conf_s T
  2167     ultimately 
  2168     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  2169                  (normal (Norm s) \<longrightarrow>
  2170                     G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  2171                  (error_free (Norm s) = error_free (Norm s))"
  2172       by simp 
  2173   next
  2174     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
  2175     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  2176     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  2177     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  2178     have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  2179     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  2180     have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
  2181     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2182     have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  2183     then obtain statC f where
  2184                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  2185             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  2186        eq_accC_accC': "accC=accC'" and
  2187                 stat: "stat=is_static f" and
  2188 	           T: "T=(Inl (type f))"
  2189       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  2190     from wf wt_e 
  2191     have iscls_statC: "is_class G statC"
  2192       by (auto dest: ty_expr_is_type type_is_class)
  2193     with wf accfield 
  2194     have iscls_statDeclC: "is_class G statDeclC"
  2195       by (auto dest!: accfield_fields dest: fields_declC)
  2196     with conf_s0 hyp_init
  2197     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2198       by auto
  2199     from conf_s1 wt_e hyp_e
  2200     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  2201                   conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" 
  2202       by force
  2203     from conf_s1 wt_e error_free_s1 hyp_e
  2204     have error_free_s2: "error_free s2"
  2205       by auto
  2206     from fvar 
  2207     have store_s2': "store s2'=store s2"
  2208       by (cases s2) (simp add: fvar_def2)
  2209     with fvar conf_s2 
  2210     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  2211       by (cases s2,cases stat) (auto simp add: fvar_def2)
  2212     from eval_init 
  2213     have initd_statDeclC_s1: "initd statDeclC s1"
  2214       by (rule init_yields_initd)
  2215     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  2216     have eq_s3_s2': "s3=s2'"  
  2217       by (auto dest!: error_free_field_access)
  2218     have conf_v: "normal s2' \<Longrightarrow> 
  2219            G,store s2'\<turnstile>fst v\<Colon>\<preceq>type f \<and> store s2'\<le>|snd v\<preceq>type f\<Colon>\<preceq>(G, L)"
  2220     proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  2221       assume normal: "normal s2'"
  2222       obtain vv vf x2 store2 store2'
  2223 	where  v: "v=(vv,vf)" and
  2224               s2: "s2=(x2,store2)" and
  2225          store2': "store s2' = store2'"
  2226 	by (cases v,cases s2,cases s2') blast
  2227       from iscls_statDeclC obtain c
  2228 	where c: "class G statDeclC = Some c"
  2229 	by auto
  2230       have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  2231       proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  2232                                statC G c L "store s1"])
  2233 	from v normal s2 fvar stat store2' 
  2234 	show "((vv, vf), Norm store2') = 
  2235                fvar statDeclC (static f) fn a (x2, store2)"
  2236 	  by (auto simp add: member_is_static_simp)
  2237 	from accfield iscls_statC wf
  2238 	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  2239 	  by (auto dest!: accfield_fields dest: fields_declC)
  2240 	from accfield
  2241 	show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
  2242 	  by (auto dest!: accfield_fields)
  2243 	from wf show "wf_prog G" .
  2244 	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  2245 	  by auto
  2246 	from fld wf iscls_statC
  2247 	show "statDeclC \<noteq> Object "
  2248 	  by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  2249 	from c show "class G statDeclC = Some c" .
  2250 	from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  2251 	from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  2252 	from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  2253 	  by simp
  2254       qed
  2255       with v s2 store2'  
  2256       show ?thesis
  2257 	by simp
  2258     qed
  2259     from fvar error_free_s2
  2260     have "error_free s2'"
  2261       by (cases s2)
  2262          (auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
  2263     with conf_v T conf_s2' eq_s3_s2'
  2264     show "s3\<Colon>\<preceq>(G, L) \<and>
  2265           (normal s3 
  2266            \<longrightarrow> G,L,store s3\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<succ>In2 v\<Colon>\<preceq>T) \<and>
  2267           (error_free (Norm s0) = error_free s3)"
  2268       by auto
  2269   next
  2270     case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
  2271     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
  2272     have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
  2273     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
  2274     have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
  2275     have avar: "(v, s2') = avar G i a s2" .
  2276     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2277     have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
  2278     then obtain elemT
  2279        where wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  2280              wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  2281                  T: "T= Inl elemT"
  2282       by (rule wt_elim_cases) auto
  2283     from  conf_s0 wt_e1 hyp_e1 
  2284     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2285             conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  2286             error_free_s1: "error_free s1"
  2287       by force
  2288     from conf_s1 error_free_s1 wt_e2 hyp_e2
  2289     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2290       by blast
  2291     from avar 
  2292     have "store s2'=store s2"
  2293       by (cases s2) (simp add: avar_def2)
  2294     with avar conf_s2 
  2295     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  2296       by (cases s2) (auto simp add: avar_def2)
  2297     from avar error_free_s2
  2298     have error_free_s2': "error_free s2'"
  2299       by (cases s2) (auto simp add: avar_def2 )
  2300     have "normal s2' \<Longrightarrow> 
  2301            G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  2302     proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  2303       assume normal: "normal s2'"
  2304       show ?thesis
  2305       proof -
  2306 	obtain vv vf x1 store1 x2 store2 store2'
  2307 	   where  v: "v=(vv,vf)" and
  2308                  s1: "s1=(x1,store1)" and
  2309                  s2: "s2=(x2,store2)" and
  2310 	    store2': "store2'=store s2'"
  2311 	  by (cases v,cases s1, cases s2, cases s2') blast 
  2312 	have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  2313 	proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  2314                                  OF wf])
  2315 	  from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  2316 	    by simp
  2317 	  from v normal s2 store2' avar 
  2318 	  show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  2319 	    by auto
  2320 	  from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  2321 	  from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  2322 	  from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  2323 	qed
  2324 	with v s1 s2 store2' 
  2325 	show ?thesis
  2326 	  by simp
  2327       qed
  2328     qed
  2329     with conf_s2' error_free_s2' T 
  2330     show "s2'\<Colon>\<preceq>(G, L) \<and>
  2331            (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  2332            (error_free (Norm s0) = error_free s2') "
  2333       by auto
  2334   next
  2335     case (Nil s0 L accC T)
  2336     then show ?case
  2337       by (auto elim!: wt_elim_cases)
  2338   next
  2339     case (Cons e es s0 s1 s2 v vs L accC T)
  2340     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  2341     have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
  2342     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2343     have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
  2344     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2345     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
  2346     then obtain eT esT where
  2347        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2348        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  2349        T: "T=Inr (eT#esT)"
  2350       by (rule wt_elim_cases) blast
  2351     from hyp_e [OF conf_s0 wt_e]
  2352     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  2353       conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  2354       by auto
  2355     from eval_es conf_v 
  2356     have conf_v': "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2357       apply clarify
  2358       apply (rule conf_gext)
  2359       apply (auto dest: eval_gext)
  2360       done
  2361     from hyp_es [OF conf_s1 wt_es] error_free_s1 
  2362     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2363            error_free_s2: "error_free s2" and
  2364            conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  2365       by auto
  2366     with conf_v' T
  2367     show 
  2368       "s2\<Colon>\<preceq>(G, L) \<and> 
  2369       (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  2370       (error_free (Norm s0) = error_free s2) "
  2371       by auto
  2372   qed
  2373   then show ?thesis .
  2374 qed
  2375 
  2376 text {* 
  2377 
  2378 
  2379 *} (* dummy text command to break paragraph for latex;
  2380               large paragraphs exhaust memory of debian pdflatex *)
  2381  
  2382 corollary eval_ts: 
  2383  "\<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\<rbrakk> 
  2384 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  2385      (error_free s = error_free s')"
  2386 apply (drule (3) eval_type_sound)
  2387 apply clarsimp
  2388 done
  2389 
  2390 corollary evals_ts: 
  2391 "\<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\<rbrakk> 
  2392 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  2393      (error_free s = error_free s')" 
  2394 apply (drule (3) eval_type_sound)
  2395 apply clarsimp
  2396 done
  2397 
  2398 corollary evar_ts: 
  2399 "\<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\<rbrakk> \<Longrightarrow>  
  2400   s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  2401   (error_free s = error_free s')"
  2402 apply (drule (3) eval_type_sound)
  2403 apply clarsimp
  2404 done
  2405 
  2406 theorem exec_ts: 
  2407 "\<lbrakk>G\<turnstile>s \<midarrow>s0\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0\<Colon>\<surd>\<rbrakk> 
  2408  \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  2409 apply (drule (3) eval_type_sound)
  2410 apply clarsimp
  2411 done
  2412 
  2413 lemma wf_eval_Fin: 
  2414   assumes wf:    "wf_prog G" and
  2415           wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
  2416         conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
  2417         eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
  2418         eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
  2419             s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  2420   shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
  2421 proof -
  2422   from eval_c1 wt_c1 wf conf_s0
  2423   have "error_free (x1,s1)"
  2424     by (auto dest: eval_type_sound)
  2425   with eval_c1 eval_c2 s3
  2426   show ?thesis
  2427     by - (rule eval.Fin, auto simp add: error_free_def)
  2428 qed
  2429 
  2430 end