src/HOL/Bali/TypeSafe.thy
author wenzelm
Mon Feb 25 20:48:14 2002 +0100 (2002-02-25)
changeset 12937 0c4fd7529467
parent 12925 99131847fb93
child 13337 f75dfc606ac7
permissions -rw-r--r--
clarified syntax of ``long'' statements: fixes/assumes/shows;
     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 24 
   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 
   858 (* #### stat raus und gleich is_static f schreiben *) 
   859 theorem dynamic_field_access_ok:
   860   assumes wf: "wf_prog G" and
   861     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   862    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   863    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   864     normal_s: "normal s" and
   865         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   866            f: "accfield G accC statC fn = Some f" and
   867         dynC: "if stat then dynC=declclass f  
   868                        else dynC=obj_class (lookup_obj (store s) a)" and
   869         stat: "if stat then (is_static f) else (\<not> is_static f)"
   870   shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   871      G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   872 proof (cases "stat")
   873   case True
   874   with stat have static: "(is_static f)" by simp
   875   from True dynC 
   876   have dynC': "dynC=declclass f" by simp
   877   with f
   878   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   879     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   880   moreover
   881   from wt_e wf have "is_class G statC"
   882     by (auto dest!: ty_expr_is_type)
   883   moreover note wf dynC'
   884   ultimately have
   885      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   886     by (auto dest: fields_declC)
   887   with dynC' f static wf
   888   show ?thesis
   889     by (auto dest: static_to_dynamic_accessible_from_static
   890             dest!: accfield_accessibleD )
   891 next
   892   case False
   893   with wf conform_a not_Null conform_s dynC
   894   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   895     "is_class G dynC"
   896     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   897               dest: obj_ty_obj_class1
   898           simp add: obj_ty_obj_class )
   899   with wf f
   900   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   901     by (auto simp add: accfield_def Let_def
   902                  dest: fields_mono
   903                 dest!: table_of_remap_SomeD)
   904   moreover
   905   from f subclseq
   906   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   907     by (auto intro!: static_to_dynamic_accessible_from 
   908                dest: accfield_accessibleD)
   909   ultimately show ?thesis
   910     by blast
   911 qed
   912 
   913 (*
   914 theorem dynamic_field_access_ok:
   915   (assumes wf: "wf_prog G" and
   916      not_Null: "\<not> is_static f \<longrightarrow> a\<noteq>Null" and
   917     conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   918     conform_s: "s\<Colon>\<preceq>(G, L)" and 
   919      normal_s: "normal s" and
   920          wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   921             f: "accfield G accC statC fn = Some f" and
   922          dynC: "if is_static f 
   923                    then dynC=declclass f  
   924                    else dynC=obj_class (lookup_obj (store s) a)" 
   925   ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   926      G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   927 proof (cases "is_static f")
   928   case True
   929   from True dynC 
   930   have dynC': "dynC=declclass f" by simp
   931   with f
   932   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   933     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   934   moreover
   935   from wt_e wf have "is_class G statC"
   936     by (auto dest!: ty_expr_is_type)
   937   moreover note wf dynC'
   938   ultimately have
   939      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   940     by (auto dest: fields_declC)
   941   with dynC' f True wf
   942   show ?thesis
   943     by (auto dest: static_to_dynamic_accessible_from_static
   944             dest!: accfield_accessibleD )
   945 next
   946   case False
   947   with wf conform_a not_Null conform_s dynC
   948   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   949     "is_class G dynC"
   950     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   951               dest: obj_ty_obj_class1
   952           simp add: obj_ty_obj_class )
   953   with wf f
   954   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   955     by (auto simp add: accfield_def Let_def
   956                  dest: fields_mono
   957                 dest!: table_of_remap_SomeD)
   958   moreover
   959   from f subclseq
   960   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   961     by (auto intro!: static_to_dynamic_accessible_from 
   962                dest: accfield_accessibleD)
   963   ultimately show ?thesis
   964     by blast
   965 qed
   966 *)
   967 
   968 
   969 (* ### Einsetzen in case FVar des TypeSoundness Proofs *)
   970 (*
   971 lemma FVar_check_error_free:
   972 (assumes fvar: "(v, s2') = fvar statDeclC stat fn a s2" and 
   973         check: "s3 = check_field_access G accC statDeclC fn stat a s2'" and
   974        conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
   975       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   976     initd_statDeclC_s2: "initd statDeclC s2" and
   977     wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   978     accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   979     stat: "stat=is_static f" and
   980       wf: "wf_prog G"
   981 )  "s3=s2'"
   982 proof -
   983   from fvar 
   984   have store_s2': "store s2'=store s2"
   985     by (cases s2) (simp add: fvar_def2)
   986   with fvar conf_s2 
   987   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
   988     by (cases s2,cases stat) (auto simp add: fvar_def2)
   989   from initd_statDeclC_s2 store_s2' 
   990   have initd_statDeclC_s2': "initd statDeclC s2"
   991     by simp
   992   show ?thesis
   993   proof (cases "normal s2'")
   994     case False
   995     with check show ?thesis 
   996       by (auto simp add: check_field_access_def Let_def)
   997   next
   998     case True
   999     with fvar store_s2' 
  1000     have not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" 
  1001       by (cases s2) (auto simp add: fvar_def2)
  1002     from True fvar store_s2'
  1003     have "normal s2"
  1004       by (cases s2,cases stat) (auto simp add: fvar_def2)
  1005     with conf_a store_s2'
  1006     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1007       by simp 
  1008     from conf_a' conf_s2'  check True initd_statDeclC_s2' 
  1009       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1010                                    True wt_e accfield ] stat
  1011     show ?thesis
  1012       by (cases stat)
  1013          (auto dest!: initedD
  1014            simp add: check_field_access_def Let_def)
  1015   qed
  1016 qed
  1017 *)
  1018 
  1019 lemma error_free_field_access:
  1020   assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
  1021               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  1022          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
  1023             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
  1024            conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1025             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  1026               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
  1027                 wf: "wf_prog G"   
  1028   shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
  1029 proof -
  1030   from fvar
  1031   have store_s2': "store s2'=store s2"
  1032     by (cases s2) (simp add: fvar_def2)
  1033   with fvar conf_s2 
  1034   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1035     by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1036   from eval_init 
  1037   have initd_statDeclC_s1: "initd statDeclC s1"
  1038     by (rule init_yields_initd)
  1039   with eval_e store_s2'
  1040   have initd_statDeclC_s2': "initd statDeclC s2'"
  1041     by (auto dest: eval_gext intro: inited_gext)
  1042   show ?thesis
  1043   proof (cases "normal s2'")
  1044     case False
  1045     then show ?thesis 
  1046       by (auto simp add: check_field_access_def Let_def)
  1047   next
  1048     case True
  1049     with fvar store_s2' 
  1050     have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
  1051       by (cases s2) (auto simp add: fvar_def2)
  1052     from True fvar store_s2'
  1053     have "normal s2"
  1054       by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1055     with conf_a store_s2'
  1056     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1057       by simp
  1058     from conf_a' conf_s2' True initd_statDeclC_s2' 
  1059       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1060                                    True wt_e accfield ] 
  1061     show ?thesis
  1062       by  (cases "is_static f")
  1063           (auto dest!: initedD
  1064            simp add: check_field_access_def Let_def)
  1065   qed
  1066 qed
  1067 
  1068 lemma call_access_ok:
  1069   assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
  1070       and        wf: "wf_prog G" 
  1071       and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
  1072       and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
  1073       and      invC: "invC = invocation_class (invmode statM e) s a statT"
  1074   shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
  1075   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
  1076 proof -
  1077   from wt_e wf have type_statT: "is_type G (RefT statT)"
  1078     by (auto dest: ty_expr_is_type)
  1079   from statM have not_Null: "statT \<noteq> NullT" by auto
  1080   from type_statT wt_e 
  1081   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
  1082                                         invmode statM e \<noteq> SuperM)"
  1083     by (auto dest: invocationTypeExpr_noClassD)
  1084   from wt_e
  1085   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
  1086     by (auto dest: invocationTypeExpr_noClassD)
  1087   show ?thesis
  1088   proof (cases "invmode statM e = IntVir")
  1089     case True
  1090     with invC_prop not_Null
  1091     have invC_prop': "is_class G invC \<and>  
  1092                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
  1093                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
  1094       by (auto simp add: DynT_prop_def)
  1095     with True not_Null
  1096     have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1097      by (cases statT) (auto simp add: invmode_def) 
  1098     with statM type_statT wf 
  1099     show ?thesis
  1100       by - (rule dynlookup_access,auto)
  1101   next
  1102     case False
  1103     with type_statT wf invC not_Null wf_I wf_A
  1104     have invC_prop': " is_class G invC \<and>
  1105                       ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
  1106                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
  1107         by (case_tac "statT") (auto simp add: invocation_class_def 
  1108                                        split: inv_mode.splits)
  1109     with not_Null wf
  1110     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
  1111       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
  1112                                             dynimethd_def)
  1113    from statM wf wt_e not_Null False invC_prop' obtain dynM where
  1114                 "accmethd G accC invC sig = Some dynM" 
  1115      by (auto dest!: static_mheadsD)
  1116    from invC_prop' False not_Null wf_I
  1117    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1118      by (cases statT) (auto simp add: invmode_def) 
  1119    with statM type_statT wf 
  1120     show ?thesis
  1121       by - (rule dynlookup_access,auto)
  1122   qed
  1123 qed
  1124 
  1125 lemma error_free_call_access:
  1126   assumes
  1127    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
  1128         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
  1129        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
  1130                = {((statDeclT, statM), pTs')}" and
  1131      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1132       conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1133      invProp: "normal s3 \<Longrightarrow>
  1134                 G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
  1135           s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1136                         (invmode statM e) a vs s2" and
  1137         invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
  1138     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
  1139                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
  1140           wf: "wf_prog G"
  1141   shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
  1142    = s3"
  1143 proof (cases "normal s2")
  1144   case False
  1145   with s3 
  1146   have "abrupt s3 = abrupt s2"  
  1147     by (auto simp add: init_lvars_def2)
  1148   with False
  1149   show ?thesis
  1150     by (auto simp add: check_method_access_def Let_def)
  1151 next
  1152   case True
  1153   note normal_s2 = True
  1154   with eval_args
  1155   have normal_s1: "normal s1"
  1156     by (cases "normal s1") auto
  1157   with conf_a eval_args 
  1158   have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1159     by (auto dest: eval_gext intro: conf_gext)
  1160   show ?thesis
  1161   proof (cases "a=Null \<longrightarrow> (is_static statM)")
  1162     case False
  1163     then obtain "\<not> is_static statM" "a=Null" 
  1164       by blast
  1165     with normal_s2 s3
  1166     have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
  1167       by (auto simp add: init_lvars_def2)
  1168     then show ?thesis
  1169       by (auto simp add: check_method_access_def Let_def)
  1170   next
  1171     case True
  1172     from statM 
  1173     obtain
  1174       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1175       by (blast dest: max_spec2mheads)
  1176     from True normal_s2 s3
  1177     have "normal s3"
  1178       by (auto simp add: init_lvars_def2)
  1179     then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
  1180       by (rule invProp)
  1181     with wt_e statM' wf invC
  1182     obtain dynM where 
  1183       dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1184       acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1185                           in invC dyn_accessible_from accC"
  1186       by (force dest!: call_access_ok)
  1187     moreover
  1188     from s3 invC
  1189     have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
  1190       by (cases s2,cases "invmode statM e") 
  1191          (simp add: init_lvars_def2 del: invmode_Static_eq)+
  1192     ultimately
  1193     show ?thesis
  1194       by (auto simp add: check_method_access_def Let_def)
  1195   qed
  1196 qed
  1197 
  1198 section "main proof of type safety"
  1199 
  1200 lemma eval_type_sound:
  1201   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1202             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
  1203             wf: "wf_prog G" and 
  1204        conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1205   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1206          (error_free s0 = error_free s1)"
  1207 proof -
  1208   from eval 
  1209   have "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>  
  1210         \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1211             \<and> (error_free s0 = error_free s1)"
  1212    (is "PROP ?TypeSafe s0 s1 t v"
  1213     is "\<And> L accC T. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1214                  \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1215                      ?ErrorFree s0 s1")
  1216   proof (induct)
  1217     case (Abrupt s t xc L accC T) 
  1218     have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
  1219     then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1220       (normal (Some xc, s) 
  1221       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
  1222       (error_free (Some xc, s) = error_free (Some xc, s))"
  1223       by (simp)
  1224   next
  1225     case (Skip s L accC T)
  1226     have "Norm s\<Colon>\<preceq>(G, L)" and  
  1227            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
  1228     then show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1229               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1230               (error_free (Norm s) = error_free (Norm s))"
  1231       by (simp)
  1232   next
  1233     case (Expr e s0 s1 v L accC T)
  1234     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1235     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1236     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1237     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
  1238     then obtain eT 
  1239       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1240       by (rule wt_elim_cases) (blast)
  1241     with conf_s0 hyp 
  1242     obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1243       by (blast)
  1244     with wt
  1245     show "s1\<Colon>\<preceq>(G, L) \<and>
  1246           (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1247           (error_free (Norm s0) = error_free s1)"
  1248       by (simp)
  1249   next
  1250     case (Lab c l s0 s1 L accC T)
  1251     have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
  1252     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1253     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
  1254     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1255       by (rule wt_elim_cases) (blast)
  1256     with conf_s0 hyp
  1257     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1258            error_free_s1: "error_free s1" 
  1259       by (blast)
  1260     from conf_s1 have "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L)"
  1261       by (cases s1) (auto intro: conforms_absorb)
  1262     with wt error_free_s1
  1263     show "abupd (absorb (Break l)) s1\<Colon>\<preceq>(G, L) \<and>
  1264           (normal (abupd (absorb (Break l)) s1)
  1265            \<longrightarrow> G,L,store (abupd (absorb (Break l)) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1266           (error_free (Norm s0) = error_free (abupd (absorb (Break l)) s1))"
  1267       by (simp)
  1268   next
  1269     case (Comp c1 c2 s0 s1 s2 L accC T)
  1270     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1271     have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1272     have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1273     have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
  1274     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1275     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T" .
  1276     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1277                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1278       by (rule wt_elim_cases) (blast)
  1279     with conf_s0 hyp_c1 hyp_c2
  1280     obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1281       by (blast)
  1282     with wt
  1283     show "s2\<Colon>\<preceq>(G, L) \<and>
  1284           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1285           (error_free (Norm s0) = error_free s2)"
  1286       by (simp)
  1287   next
  1288     case (If b c1 c2 e s0 s1 s2 L accC T)
  1289     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1290     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1291     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1292     have hyp_then_else: 
  1293             "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
  1294     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1295     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
  1296     then obtain "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
  1297                 "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1298       by (rule wt_elim_cases) (auto split add: split_if)
  1299     with conf_s0 hyp_e hyp_then_else
  1300     obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1301       by (blast)
  1302     with wt
  1303     show "s2\<Colon>\<preceq>(G, L) \<and>
  1304            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1305            (error_free (Norm s0) = error_free s2)"
  1306       by (simp)
  1307   next
  1308     case (Loop b c e l s0 s1 s2 s3 L accC T)
  1309     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1310     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1311     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1312     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1313     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1314                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1315       by (rule wt_elim_cases) (blast)
  1316     from conf_s0 wt_e hyp_e
  1317     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1318       by blast
  1319     show "s3\<Colon>\<preceq>(G, L) \<and>
  1320           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1321           (error_free (Norm s0) = error_free s3)"
  1322     proof (cases "normal s1 \<and> the_Bool b")
  1323       case True
  1324       from Loop True have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" by auto
  1325       from Loop True have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1326 	by auto
  1327       from Loop True have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>"
  1328 	by (auto)
  1329       from Loop True have hyp_w: "PROP ?TypeSafe (abupd (absorb (Cont l)) s2)
  1330                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1331 	by (auto)
  1332       from conf_s1 error_free_s1 wt_c hyp_c
  1333       obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1334 	by blast
  1335       from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1336 	by (cases s2) (auto intro: conforms_absorb)
  1337       moreover
  1338       from error_free_s2 have "error_free (abupd (absorb (Cont l)) s2)"
  1339 	by simp
  1340       moreover note wt hyp_w
  1341       ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  1342 	by blast
  1343       with wt 
  1344       show ?thesis
  1345 	by (simp)
  1346     next
  1347       case False
  1348       with Loop have "s3=s1" by simp
  1349       with conf_s1 error_free_s1 wt
  1350       show ?thesis
  1351 	by (simp)
  1352     qed
  1353   next
  1354     case (Do j s L accC T)
  1355     have "Norm s\<Colon>\<preceq>(G, L)" .
  1356     then 
  1357     show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  1358            (normal (Some (Jump j), s) 
  1359            \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Do j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1360            (error_free (Norm s) = error_free (Some (Jump j), s))"
  1361       by simp
  1362   next
  1363     case (Throw a e s0 s1 L accC T)
  1364     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  1365     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  1366     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1367     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T" .
  1368     then obtain tn 
  1369       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  1370             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  1371       by (rule wt_elim_cases) (auto)
  1372     from conf_s0 wt_e hyp obtain
  1373       "s1\<Colon>\<preceq>(G, L)" and
  1374       "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  1375       error_free_s1: "error_free s1"
  1376       by force
  1377     with wf throwable
  1378     have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  1379       by (cases s1) (auto dest: Throw_lemma)
  1380     with wt error_free_s1
  1381     show "abupd (throw a) s1\<Colon>\<preceq>(G, L) \<and>
  1382             (normal (abupd (throw a) s1) \<longrightarrow>
  1383             G,L,store (abupd (throw a) s1)\<turnstile>In1r (Throw e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1384             (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  1385       by simp
  1386   next
  1387     case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
  1388     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1389     have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1390     have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1391     have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
  1392     have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  1393     then obtain 
  1394       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1395       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  1396       fresh_vn: "L(VName vn)=None"
  1397       by (rule wt_elim_cases) (auto)
  1398     with conf_s0 hyp_c1
  1399     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1400       by blast
  1401     from conf_s1 sx_alloc wf 
  1402     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  1403       by (auto dest: sxalloc_type_sound split: option.splits)
  1404     from sx_alloc error_free_s1 
  1405     have error_free_s2: "error_free s2"
  1406       by (rule error_free_sxalloc)
  1407     show "s3\<Colon>\<preceq>(G, L) \<and>
  1408           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  1409           (error_free (Norm s0) = error_free s3)"
  1410     proof (cases "normal s1")  
  1411       case True
  1412       with sx_alloc wf 
  1413       have eq_s2_s1: "s2=s1"
  1414 	by (auto dest: sxalloc_type_sound split: option.splits)
  1415       with True 
  1416       have "\<not>  G,s2\<turnstile>catch catchC"
  1417 	by (simp add: catch_def)
  1418       with Try
  1419       have "s3=s2"
  1420 	by simp
  1421       with wt conf_s1 error_free_s1 eq_s2_s1
  1422       show ?thesis
  1423 	by simp
  1424     next
  1425       case False
  1426       note exception_s1 = this
  1427       show ?thesis
  1428       proof (cases "G,s2\<turnstile>catch catchC") 
  1429 	case False
  1430 	with Try
  1431 	have "s3=s2"
  1432 	  by simp
  1433 	with wt conf_s2 error_free_s2 
  1434 	show ?thesis
  1435 	  by simp
  1436       next
  1437 	case True
  1438 	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  1439 	from True Try 
  1440 	have hyp_c2: "PROP ?TypeSafe (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1441 	  by auto
  1442 	from exception_s1 sx_alloc wf
  1443 	obtain a 
  1444 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  1445 	  by (auto dest!: sxalloc_type_sound split: option.splits)
  1446 	with True
  1447 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  1448 	  by (cases s2) simp
  1449 	with xcpt_s2 conf_s2 wf
  1450 	have "Norm (lupd(VName vn\<mapsto>Addr a) (store s2))
  1451               \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1452 	  by (auto dest: Try_lemma)
  1453 	with hyp_c2 wt_c2 xcpt_s2 error_free_s2
  1454 	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  1455                error_free_s3: "error_free s3"
  1456 	  by (cases s2) auto
  1457 	from conf_s3 fresh_vn 
  1458 	have "s3\<Colon>\<preceq>(G,L)"
  1459 	  by (blast intro: conforms_deallocL)
  1460 	with wt error_free_s3
  1461 	show ?thesis
  1462 	  by simp
  1463       qed
  1464     qed
  1465   next
  1466     case (Fin c1 c2 s0 s1 s2 x1 L accC T)
  1467     have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  1468     have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  1469     have  hyp_c1: "PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
  1470     have  hyp_c2: "PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>" .
  1471     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1472     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
  1473     then obtain
  1474       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1475       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1476       by (rule wt_elim_cases) blast
  1477     from conf_s0 wt_c1 hyp_c1  
  1478     obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  1479       by blast
  1480     from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  1481       by (rule conforms_NormI)
  1482     with wt_c2 hyp_c2
  1483     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1484       by blast
  1485     show "abupd (abrupt_if (x1 \<noteq> None) x1) s2\<Colon>\<preceq>(G, L) \<and>
  1486           (normal (abupd (abrupt_if (x1 \<noteq> None) x1) s2) 
  1487            \<longrightarrow> G,L,store (abupd (abrupt_if (x1 \<noteq> None) x1) s2)
  1488                \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1489           (error_free (Norm s0) =
  1490               error_free (abupd (abrupt_if (x1 \<noteq> None) x1) s2))"
  1491     proof (cases x1)
  1492       case None with conf_s2 wt show ?thesis by auto
  1493     next
  1494       case (Some x) 
  1495       with c2 wf conf_s1 conf_s2
  1496       have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  1497 	by (cases s2) (auto dest: Fin_lemma)
  1498       from Some error_free_s1
  1499       have "\<not> (\<exists> err. x=Error err)"
  1500 	by (simp add: error_free_def)
  1501       with error_free_s2
  1502       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
  1503 	by (cases s2) simp
  1504       with Some wt conf show ?thesis
  1505 	by (cases s2) auto
  1506     qed
  1507   next
  1508     case (Init C c s0 s1 s2 s3 L accC T)
  1509     have     cls: "the (class G C) = c" .
  1510     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1511     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  1512     with cls
  1513     have cls_C: "class G C = Some c"
  1514       by - (erule wt_elim_cases,auto)
  1515     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1516           (error_free (Norm s0) = error_free s3)"
  1517     proof (cases "inited C (globs s0)")
  1518       case True
  1519       with Init have "s3 = Norm s0"
  1520 	by simp
  1521       with conf_s0 wt show ?thesis 
  1522 	by simp
  1523     next
  1524       case False
  1525       with Init 
  1526       have "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1527               \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  1528         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  1529 	s3: "s3 = (set_lvars (locals (store s1))) s2" 
  1530 	by auto
  1531       from False Init 
  1532       have hyp_init_super: 
  1533              "PROP ?TypeSafe (Norm ((init_class_obj G C) s0)) s1
  1534 	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  1535 	by auto
  1536       with False Init (* without chaining hyp_init_super, the simplifier will
  1537                           loop! *)
  1538       have hyp_init_c:
  1539 	"PROP ?TypeSafe ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  1540 	by auto
  1541       from conf_s0 wf cls_C False
  1542       have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1543 	by (auto dest: conforms_init_class_obj)
  1544       from wf cls_C have
  1545 	wt_super:"\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1546                    \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1547 	by (cases "C=Object")
  1548            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1549       with conf_s0' hyp_init_super
  1550       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1551 	by blast 
  1552       then
  1553       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1554 	by (cases s1) (auto dest: conforms_set_locals )
  1555       moreover from error_free_s1
  1556       have "error_free ((set_lvars empty) s1)"
  1557 	by simp
  1558       moreover note hyp_init_c wf cls_C 
  1559       ultimately
  1560       obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  1561 	by (auto dest!: wf_prog_cdecl wf_cdecl_wt_init)
  1562       with s3 conf_s1 eval_init
  1563       have "s3\<Colon>\<preceq>(G, L)"
  1564 	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  1565       moreover from error_free_s2 s3
  1566       have "error_free s3"
  1567 	by simp
  1568       moreover note wt
  1569       ultimately show ?thesis
  1570 	by simp
  1571     qed
  1572   next
  1573     case (NewC C a s0 s1 s2 L accC T)
  1574     have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
  1575     have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
  1576     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
  1577     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1578     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  1579     then obtain is_cls_C: "is_class G C" and
  1580                        T: "T=Inl (Class C)"
  1581       by (rule wt_elim_cases) (auto dest: is_acc_classD)
  1582     with conf_s0 hyp
  1583     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1584       by auto
  1585     from conf_s1 halloc wf is_cls_C
  1586     obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  1587                              "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  1588       by (cases s2) (auto dest!: halloc_type_sound)
  1589     from halloc error_free_s1 
  1590     have "error_free s2"
  1591       by (rule error_free_halloc)
  1592     with halloc_type_safe T
  1593     show "s2\<Colon>\<preceq>(G, L) \<and> 
  1594           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (NewC C)\<succ>In1 (Addr a)\<Colon>\<preceq>T)  \<and>
  1595           (error_free (Norm s0) = error_free s2)"
  1596       by auto
  1597   next
  1598     case (NewA T a e i s0 s1 s2 s3 L accC Ta)
  1599     have "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1" .
  1600     have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  1601     have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1602     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
  1603     have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
  1604     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1605     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
  1606     then obtain
  1607       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
  1608       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  1609             T: "is_type G T" and
  1610            Ta: "Ta=Inl (T.[])"
  1611       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  1612     from conf_s0 wt_init hyp_init
  1613     obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  1614       by blast
  1615     with wt_size hyp_size
  1616     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1617       by blast
  1618     from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  1619       by (cases s2) auto
  1620     with halloc wf T 
  1621     have halloc_type_safe:
  1622           "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>T.[])"
  1623       by (cases s3) (auto dest!: halloc_type_sound)
  1624     from halloc error_free_s2
  1625     have "error_free s3"
  1626       by (auto dest: error_free_halloc)
  1627     with halloc_type_safe Ta
  1628     show "s3\<Colon>\<preceq>(G, L) \<and> 
  1629           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New T[e])\<succ>In1 (Addr a)\<Colon>\<preceq>Ta) \<and>
  1630           (error_free (Norm s0) = error_free s3) "
  1631       by simp
  1632   next
  1633     case (Cast castT e s0 s1 s2 v L accC T)
  1634     have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1635     have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
  1636     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1637     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1638     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T" .
  1639     then obtain eT
  1640       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1641               eT: "G\<turnstile>eT\<preceq>? castT" and 
  1642                T: "T=Inl castT"
  1643       by (rule wt_elim_cases) auto
  1644     with conf_s0 hyp
  1645     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1646       by blast
  1647     from conf_s1 s2 
  1648     have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  1649       by (cases s1) simp
  1650     from error_free_s1 s2
  1651     have error_free_s2: "error_free s2"
  1652       by simp
  1653     {
  1654       assume norm_s2: "normal s2"
  1655       have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
  1656       proof -
  1657 	from s2 norm_s2 have "normal s1"
  1658 	  by (cases s1) simp
  1659 	with wt_e conf_s0 hyp 
  1660 	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  1661 	  by force
  1662 	with eT wf s2 T norm_s2
  1663 	show ?thesis
  1664 	  by (cases s1) (auto dest: fits_conf)
  1665       qed
  1666     }
  1667     with conf_s2 error_free_s2
  1668     show "s2\<Colon>\<preceq>(G, L) \<and> 
  1669            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
  1670            (error_free (Norm s0) = error_free s2)"
  1671       by blast
  1672   next
  1673     case (Inst T b e s0 s1 v L accC T')
  1674     then show ?case
  1675       by (auto elim!: wt_elim_cases)
  1676   next
  1677     case (Lit s v L accC T)
  1678     then show ?case
  1679       by (auto elim!: wt_elim_cases 
  1680                intro: conf_litval simp add: empty_dt_def)
  1681   next
  1682     case (Super s L accC T)
  1683     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  1684     have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  1685     then obtain C c where
  1686              C: "L This = Some (Class C)" and
  1687        neq_Obj: "C\<noteq>Object" and
  1688          cls_C: "class G C = Some c" and
  1689              T: "T=Inl (Class (super c))"
  1690       by (rule wt_elim_cases) auto
  1691     from C conf_s have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  1692       by (blast intro: conforms_localD [THEN lconfD])
  1693     with neq_Obj cls_C wf
  1694     have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  1695       by (auto intro: conf_widen
  1696                 dest: subcls_direct[THEN widen.subcls])
  1697     with T conf_s
  1698     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1699            (normal (Norm s) \<longrightarrow> 
  1700               G,L,store (Norm s)\<turnstile>In1l Super\<succ>In1 (val_this s)\<Colon>\<preceq>T) \<and>
  1701            (error_free (Norm s) = error_free (Norm s))"
  1702       by simp
  1703   next
  1704     case (Acc f s0 s1 v va L accC T)
  1705     then show ?case
  1706       by (force elim!: wt_elim_cases)
  1707   next
  1708     case (Ass e f s0 s1 s2 v var w L accC T)
  1709     have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> s1" .
  1710     have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
  1711     have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,f))" .
  1712     have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
  1713     have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1714     have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
  1715     then obtain varT eT where
  1716 	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  1717 	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1718 	  widen: "G\<turnstile>eT\<preceq>varT" and
  1719               T: "T=Inl eT"
  1720       by (rule wt_elim_cases) auto
  1721     from conf_s0 wt_var hyp_var
  1722     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1723       by blast
  1724     with wt_e hyp_e
  1725     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1726       by blast
  1727     show "assign f v s2\<Colon>\<preceq>(G, L) \<and>
  1728            (normal (assign f v s2) \<longrightarrow>
  1729             G,L,store (assign f v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1730             (error_free (Norm s0) = error_free (assign f v s2))"
  1731     proof (cases "normal s1")
  1732       case False
  1733       with eval_e 
  1734       have "s2=s1"
  1735 	by auto
  1736       with False conf_s1 error_free_s1
  1737       show ?thesis
  1738 	by auto
  1739     next
  1740       case True
  1741       note normal_s1=this
  1742       show ?thesis 
  1743       proof (cases "normal s2")
  1744 	case False
  1745 	with conf_s2 error_free_s2 
  1746 	show ?thesis
  1747 	  by auto
  1748       next
  1749 	case True
  1750 	from True normal_s1 conf_s1 wt_e hyp_e
  1751 	have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1752 	  by force
  1753 	with widen wf
  1754 	have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1755 	  by (auto intro: conf_widen)
  1756 	from conf_s0 normal_s1 wt_var hyp_var
  1757 	have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, f)\<Colon>\<preceq>Inl varT"
  1758 	  by blast
  1759 	then 
  1760 	have conf_assign:  "store s1\<le>|f\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1761 	  by auto
  1762 	from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1763 	  eval_e T conf_s2 error_free_s2
  1764 	show ?thesis
  1765 	  by (cases s1, cases s2) 
  1766 	     (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1767       qed
  1768     qed
  1769   next
  1770     case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
  1771     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  1772     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  1773     have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
  1774     have hyp_if: "PROP ?TypeSafe s1 s2 
  1775                        (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  1776     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1777     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  1778     then obtain T1 T2 statT where
  1779       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  1780       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  1781       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  1782       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  1783       T    : "T=Inl statT"
  1784       by (rule wt_elim_cases) auto
  1785     with wt_e0 conf_s0 hyp_e0
  1786     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  1787       by blast
  1788     with wt_e1 wt_e2 statT hyp_if
  1789     obtain dynT where
  1790       conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2" and
  1791       conf_res: 
  1792           "(normal s2 \<longrightarrow>
  1793         G,L,store s2\<turnstile>In1l (if the_Bool b then e1 else e2)\<succ>In1 v\<Colon>\<preceq>Inl dynT)" and
  1794       dynT: "dynT = (if the_Bool b then T1 else T2)"
  1795       by (cases "the_Bool b") force+
  1796     from statT dynT  
  1797     have "G\<turnstile>dynT\<preceq>statT"
  1798       by (cases "the_Bool b") auto
  1799     with conf_s2 conf_res error_free_s2 T wf
  1800     show "s2\<Colon>\<preceq>(G, L) \<and>
  1801            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1802            (error_free (Norm s0) = error_free s2)"
  1803       by (auto)
  1804   next
  1805     case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1806            v vs L accC T)
  1807     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
  1808     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  1809     have invDeclC: "invDeclC 
  1810                       = invocation_declclass G mode (store s2) a' statT 
  1811                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
  1812     have init_lvars: 
  1813            "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2".
  1814     have check: "s3' =
  1815        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
  1816     have eval_methd: 
  1817            "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  1818     have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
  1819     have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  1820     have hyp_methd: "PROP ?TypeSafe s3' s4 
  1821                      (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  1822     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1823     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1824                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  1825     from wt obtain pTs statDeclT statM where
  1826                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  1827               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  1828                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  1829                          = {((statDeclT,statM),pTs')}" and
  1830                  mode: "mode = invmode statM e" and
  1831                     T: "T =Inl (resTy statM)" and
  1832         eq_accC_accC': "accC=accC'"
  1833       by (rule wt_elim_cases) auto
  1834     from conf_s0 wt_e hyp_e 
  1835     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1836            conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
  1837            error_free_s1: "error_free s1" 
  1838       by force
  1839     with wt_args hyp_args
  1840     obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1841             conf_args: "normal s2 
  1842                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  1843         error_free_s2: "error_free s2" 
  1844       by force
  1845     from error_free_s2 init_lvars
  1846     have error_free_s3: "error_free s3"
  1847       by (auto simp add: init_lvars_def2)
  1848     from statM 
  1849     obtain
  1850       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1851       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1852       by (blast dest: max_spec2mheads)
  1853     from check
  1854     have eq_store_s3'_s3: "store s3'=store s3"
  1855       by (cases s3) (simp add: check_method_access_def Let_def)
  1856     obtain invC
  1857       where invC: "invC = invocation_class mode (store s2) a' statT"
  1858       by simp
  1859     with init_lvars
  1860     have invC': "invC = (invocation_class mode (store s3) a' statT)"
  1861       by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1862     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  1863              (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  1864                G,L,store ((set_lvars (locals (store s2))) s4)
  1865                \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1866              (error_free (Norm s0) =
  1867                 error_free ((set_lvars (locals (store s2))) s4))"
  1868     proof (cases "normal s2")
  1869       case False
  1870       with init_lvars 
  1871       obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1872              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1873                                             mode a' vs s2)" 
  1874 	by (auto simp add: init_lvars_def2)
  1875       moreover
  1876       from keep_abrupt False check
  1877       have eq_s3'_s3: "s3'=s3" 
  1878 	by (auto simp add: check_method_access_def Let_def)
  1879       moreover
  1880       from eq_s3'_s3 False keep_abrupt eval_methd
  1881       have "s4=s3'"
  1882 	by auto
  1883       ultimately have
  1884 	"set_lvars (locals (store s2)) s4 = s2"
  1885 	by (cases s2,cases s4) (simp add: init_lvars_def2)
  1886       with False conf_s2 error_free_s2
  1887       show ?thesis
  1888 	by auto
  1889     next
  1890       case True
  1891       note normal_s2 = True
  1892       with eval_args
  1893       have normal_s1: "normal s1"
  1894 	by (cases "normal s1") auto
  1895       with conf_a' eval_args 
  1896       have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
  1897 	by (auto dest: eval_gext intro: conf_gext)
  1898       show ?thesis
  1899       proof (cases "a'=Null \<longrightarrow> is_static statM")
  1900 	case False
  1901 	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
  1902 	  by blast
  1903 	with normal_s2 init_lvars mode
  1904 	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1905                    "store s3 = store (init_lvars G invDeclC 
  1906                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
  1907 	  by (auto simp add: init_lvars_def2)
  1908 	moreover
  1909 	from np check
  1910 	have eq_s3'_s3: "s3'=s3" 
  1911 	  by (auto simp add: check_method_access_def Let_def)
  1912 	moreover
  1913 	from eq_s3'_s3 np eval_methd
  1914 	have "s4=s3'"
  1915 	  by auto
  1916 	ultimately have
  1917 	  "set_lvars (locals (store s2)) s4 
  1918            = (Some (Xcpt (Std NullPointer)),store s2)"
  1919 	  by (cases s2,cases s4) (simp add: init_lvars_def2)
  1920 	with conf_s2 error_free_s2
  1921 	show ?thesis
  1922 	  by (cases s2) (auto dest: conforms_NormI)
  1923       next
  1924 	case True
  1925 	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
  1926 	  by (auto dest!: Null_staticD)
  1927 	with conf_s2 conf_a'_s2 wf invC  
  1928 	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1929 	  by (cases s2) (auto intro: DynT_propI)
  1930 	with wt_e statM' invC mode wf 
  1931 	obtain dynM where 
  1932           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1933           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1934                           in invC dyn_accessible_from accC"
  1935 	  by (force dest!: call_access_ok)
  1936 	with invC' check eq_accC_accC'
  1937 	have eq_s3'_s3: "s3'=s3"
  1938 	  by (auto simp add: check_method_access_def Let_def)
  1939 	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1940 	obtain 
  1941 	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1942 	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1943            iscls_invDeclC: "is_class G invDeclC" and
  1944 	        invDeclC': "invDeclC = declclass dynM" and
  1945 	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1946 	    resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1947 	   is_static_eq: "is_static dynM = is_static statM" and
  1948 	   involved_classes_prop:
  1949              "(if invmode statM e = IntVir
  1950                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1951                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1952                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1953                       statDeclT = ClassT invDeclC)"
  1954 	  by (auto dest: DynT_mheadsD)
  1955 	obtain L' where 
  1956 	   L':"L'=(\<lambda> k. 
  1957                  (case k of
  1958                     EName e
  1959                     \<Rightarrow> (case e of 
  1960                           VNam v 
  1961                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  1962                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  1963                         | Res \<Rightarrow> Some (resTy dynM))
  1964                   | This \<Rightarrow> if is_static statM 
  1965                             then None else Some (Class invDeclC)))"
  1966 	  by simp
  1967 	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1968              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
  1969 	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1970 	  apply - 
  1971              (* FIXME confomrs_init_lvars should be 
  1972                 adjusted to be more directy applicable *)
  1973 	  apply (drule conforms_init_lvars [of G invDeclC 
  1974                   "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1975                   L statT invC a' "(statDeclT,statM)" e])
  1976 	  apply (rule wf)
  1977 	  apply (rule conf_args,assumption)
  1978 	  apply (simp add: pTs_widen)
  1979 	  apply (cases s2,simp)
  1980 	  apply (rule dynM')
  1981 	  apply (force dest: ty_expr_is_type)
  1982 	  apply (rule invC_widen)
  1983 	  apply (force intro: conf_gext dest: eval_gext)
  1984 	  apply simp
  1985 	  apply simp
  1986 	  apply (simp add: invC)
  1987 	  apply (simp add: invDeclC)
  1988 	  apply (force dest: wf_mdeclD1 is_acc_typeD)
  1989 	  apply (cases s2, simp add: L' init_lvars
  1990 	                      cong add: lname.case_cong ename.case_cong)
  1991 	  done 
  1992 	from  is_static_eq wf_dynM L'
  1993 	obtain mthdT where
  1994 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1995             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  1996 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1997 	  by - (drule wf_mdecl_bodyD,
  1998                 simp cong add: lname.case_cong ename.case_cong)
  1999 	with dynM' iscls_invDeclC invDeclC'
  2000 	have
  2001 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  2002             \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  2003 	  by (auto intro: wt.Methd)
  2004 	with eq_s3'_s3 conf_s3 error_free_s3 
  2005              hyp_methd [of L' invDeclC "Inl mthdT"]
  2006 	obtain  conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  2007 	       conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  2008 	  error_free_s4: "error_free s4"
  2009 	  by auto
  2010 	from init_lvars eval_methd eq_s3'_s3 
  2011 	have "store s2\<le>|store s4"
  2012 	  by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  2013 	with conf_s2 conf_s4
  2014 	have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  2015 	  by (cases s2,cases s4) (auto intro: conforms_return)
  2016 	moreover 
  2017 	from conf_Res mthdT_widen resTy_widen wf
  2018 	have "normal s4 
  2019              \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  2020 	  by (auto dest: widen_trans)
  2021 	then
  2022 	have "normal ((set_lvars (locals (store s2))) s4)
  2023              \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  2024 	  by (cases s4) auto
  2025 	moreover note error_free_s4 T
  2026 	ultimately 
  2027 	show ?thesis
  2028 	  by simp
  2029       qed
  2030     qed
  2031   next
  2032     case (Methd D s0 s1 sig v L accC T)
  2033     have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  2034     have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  2035     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2036     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T" .
  2037     then obtain m bodyT where
  2038       D: "is_class G D" and
  2039       m: "methd G D sig = Some m" and
  2040       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  2041                    \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  2042       T: "T=Inl bodyT"
  2043       by (rule wt_elim_cases) auto
  2044     with hyp [of _ _ "(Inl bodyT)"] conf_s0 
  2045     show "s1\<Colon>\<preceq>(G, L) \<and> 
  2046            (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2047            (error_free (Norm s0) = error_free s1)"
  2048       by (auto simp add: Let_def body_def)
  2049   next
  2050     case (Body D c s0 s1 s2 L accC T)
  2051     have "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  2052     have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  2053     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
  2054     have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
  2055     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2056     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T" .
  2057     then obtain bodyT where
  2058          iscls_D: "is_class G D" and
  2059             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
  2060          resultT: "L Result = Some bodyT" and
  2061       isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  2062                T: "T=Inl bodyT"
  2063       by (rule wt_elim_cases) auto
  2064     from conf_s0 iscls_D hyp_init
  2065     obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  2066       by auto
  2067     with wt_c hyp_c
  2068     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2069       by blast
  2070     from conf_s2
  2071     have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  2072       by (cases s2) (auto intro: conforms_absorb)
  2073     moreover
  2074     from error_free_s2
  2075     have "error_free (abupd (absorb Ret) s2)"
  2076       by simp
  2077     moreover note T resultT
  2078     ultimately
  2079     show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
  2080            (normal (abupd (absorb Ret) s2) \<longrightarrow>
  2081              G,L,store (abupd (absorb Ret) s2)
  2082               \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  2083           (error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
  2084       by (cases s2) (auto intro: conforms_locals)
  2085   next
  2086     case (LVar s vn L accC T)
  2087     have conf_s: "Norm s\<Colon>\<preceq>(G, L)" and 
  2088              wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T" .
  2089     then obtain vnT where
  2090       vnT: "L vn = Some vnT" and
  2091         T: "T=Inl vnT"
  2092       by (auto elim!: wt_elim_cases)
  2093     from conf_s vnT
  2094     have conf_fst: "G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  2095       by (auto elim: conforms_localD [THEN lconfD]  
  2096                simp add: lvar_def)
  2097     moreover
  2098     from conf_s conf_fst vnT 
  2099     have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  2100       by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
  2101     moreover note conf_s T
  2102     ultimately 
  2103     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  2104                  (normal (Norm s) \<longrightarrow>
  2105                     G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  2106                  (error_free (Norm s) = error_free (Norm s))"
  2107       by simp 
  2108   next
  2109     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
  2110     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  2111     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  2112     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  2113     have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  2114     have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  2115     have hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 a)" .
  2116     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2117     have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  2118     then obtain statC f where
  2119                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  2120             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  2121        eq_accC_accC': "accC=accC'" and
  2122                 stat: "stat=is_static f" and
  2123 	           T: "T=(Inl (type f))"
  2124       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  2125     from wf wt_e 
  2126     have iscls_statC: "is_class G statC"
  2127       by (auto dest: ty_expr_is_type type_is_class)
  2128     with wf accfield 
  2129     have iscls_statDeclC: "is_class G statDeclC"
  2130       by (auto dest!: accfield_fields dest: fields_declC)
  2131     with conf_s0 hyp_init
  2132     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2133       by auto
  2134     from conf_s1 wt_e hyp_e
  2135     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  2136                   conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" 
  2137       by force
  2138     from conf_s1 wt_e error_free_s1 hyp_e
  2139     have error_free_s2: "error_free s2"
  2140       by auto
  2141     from fvar 
  2142     have store_s2': "store s2'=store s2"
  2143       by (cases s2) (simp add: fvar_def2)
  2144     with fvar conf_s2 
  2145     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  2146       by (cases s2,cases stat) (auto simp add: fvar_def2)
  2147     from eval_init 
  2148     have initd_statDeclC_s1: "initd statDeclC s1"
  2149       by (rule init_yields_initd)
  2150     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  2151     have eq_s3_s2': "s3=s2'"  
  2152       by (auto dest!: error_free_field_access)
  2153     have conf_v: "normal s2' \<Longrightarrow> 
  2154            G,store s2'\<turnstile>fst v\<Colon>\<preceq>type f \<and> store s2'\<le>|snd v\<preceq>type f\<Colon>\<preceq>(G, L)"
  2155     proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  2156       assume normal: "normal s2'"
  2157       obtain vv vf x2 store2 store2'
  2158 	where  v: "v=(vv,vf)" and
  2159               s2: "s2=(x2,store2)" and
  2160          store2': "store s2' = store2'"
  2161 	by (cases v,cases s2,cases s2') blast
  2162       from iscls_statDeclC obtain c
  2163 	where c: "class G statDeclC = Some c"
  2164 	by auto
  2165       have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  2166       proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  2167                                statC G c L "store s1"])
  2168 	from v normal s2 fvar stat store2' 
  2169 	show "((vv, vf), Norm store2') = 
  2170                fvar statDeclC (static f) fn a (x2, store2)"
  2171 	  by (auto simp add: member_is_static_simp)
  2172 	from accfield iscls_statC wf
  2173 	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  2174 	  by (auto dest!: accfield_fields dest: fields_declC)
  2175 	from accfield
  2176 	show fld: "table_of (fields G statC) (fn, statDeclC) = Some f"
  2177 	  by (auto dest!: accfield_fields)
  2178 	from wf show "wf_prog G" .
  2179 	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  2180 	  by auto
  2181 	from fld wf iscls_statC
  2182 	show "statDeclC \<noteq> Object "
  2183 	  by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  2184 	from c show "class G statDeclC = Some c" .
  2185 	from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  2186 	from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  2187 	from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  2188 	  by simp
  2189       qed
  2190       with v s2 store2'  
  2191       show ?thesis
  2192 	by simp
  2193     qed
  2194     from fvar error_free_s2
  2195     have "error_free s2'"
  2196       by (cases s2)
  2197          (auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
  2198     with conf_v T conf_s2' eq_s3_s2'
  2199     show "s3\<Colon>\<preceq>(G, L) \<and>
  2200           (normal s3 
  2201            \<longrightarrow> G,L,store s3\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<succ>In2 v\<Colon>\<preceq>T) \<and>
  2202           (error_free (Norm s0) = error_free s3)"
  2203       by auto
  2204   next
  2205     case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
  2206     have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
  2207     have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
  2208     have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
  2209     have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)" .
  2210     have avar: "(v, s2') = avar G i a s2" .
  2211     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2212     have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
  2213     then obtain elemT
  2214        where wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  2215              wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  2216                  T: "T= Inl elemT"
  2217       by (rule wt_elim_cases) auto
  2218     from  conf_s0 wt_e1 hyp_e1 
  2219     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2220             conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  2221             error_free_s1: "error_free s1"
  2222       by force
  2223     from conf_s1 error_free_s1 wt_e2 hyp_e2
  2224     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2225       by blast
  2226     from avar 
  2227     have "store s2'=store s2"
  2228       by (cases s2) (simp add: avar_def2)
  2229     with avar conf_s2 
  2230     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  2231       by (cases s2) (auto simp add: avar_def2)
  2232     from avar error_free_s2
  2233     have error_free_s2': "error_free s2'"
  2234       by (cases s2) (auto simp add: avar_def2 )
  2235     have "normal s2' \<Longrightarrow> 
  2236            G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  2237     proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  2238       assume normal: "normal s2'"
  2239       show ?thesis
  2240       proof -
  2241 	obtain vv vf x1 store1 x2 store2 store2'
  2242 	   where  v: "v=(vv,vf)" and
  2243                  s1: "s1=(x1,store1)" and
  2244                  s2: "s2=(x2,store2)" and
  2245 	    store2': "store2'=store s2'"
  2246 	  by (cases v,cases s1, cases s2, cases s2') blast 
  2247 	have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  2248 	proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  2249                                  OF wf])
  2250 	  from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  2251 	    by simp
  2252 	  from v normal s2 store2' avar 
  2253 	  show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  2254 	    by auto
  2255 	  from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  2256 	  from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  2257 	  from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  2258 	qed
  2259 	with v s1 s2 store2' 
  2260 	show ?thesis
  2261 	  by simp
  2262       qed
  2263     qed
  2264     with conf_s2' error_free_s2' T 
  2265     show "s2'\<Colon>\<preceq>(G, L) \<and>
  2266            (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  2267            (error_free (Norm s0) = error_free s2') "
  2268       by auto
  2269   next
  2270     case (Nil s0 L accC T)
  2271     then show ?case
  2272       by (auto elim!: wt_elim_cases)
  2273   next
  2274     case (Cons e es s0 s1 s2 v vs L accC T)
  2275     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  2276     have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
  2277     have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  2278     have hyp_es: "PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)" .
  2279     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  2280     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T" .
  2281     then obtain eT esT where
  2282        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2283        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  2284        T: "T=Inr (eT#esT)"
  2285       by (rule wt_elim_cases) blast
  2286     from hyp_e [OF conf_s0 wt_e]
  2287     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  2288       conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  2289       by auto
  2290     from eval_es conf_v 
  2291     have conf_v': "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2292       apply clarify
  2293       apply (rule conf_gext)
  2294       apply (auto dest: eval_gext)
  2295       done
  2296     from hyp_es [OF conf_s1 wt_es] error_free_s1 
  2297     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2298            error_free_s2: "error_free s2" and
  2299            conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  2300       by auto
  2301     with conf_v' T
  2302     show 
  2303       "s2\<Colon>\<preceq>(G, L) \<and> 
  2304       (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  2305       (error_free (Norm s0) = error_free s2) "
  2306       by auto
  2307   qed
  2308   then show ?thesis .
  2309 qed
  2310  
  2311 corollary eval_ts: 
  2312  "\<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> 
  2313 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  2314      (error_free s = error_free s')"
  2315 apply (drule (3) eval_type_sound)
  2316 apply clarsimp
  2317 done
  2318 
  2319 corollary evals_ts: 
  2320 "\<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> 
  2321 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  2322      (error_free s = error_free s')" 
  2323 apply (drule (3) eval_type_sound)
  2324 apply clarsimp
  2325 done
  2326 
  2327 corollary evar_ts: 
  2328 "\<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>  
  2329   s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  2330   (error_free s = error_free s')"
  2331 apply (drule (3) eval_type_sound)
  2332 apply clarsimp
  2333 done
  2334 
  2335 theorem exec_ts: 
  2336 "\<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> 
  2337  \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  2338 apply (drule (3) eval_type_sound)
  2339 apply clarsimp
  2340 done
  2341 end