src/HOL/Bali/TypeSafe.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,1211 @@
     1.4 +(*  Title:      isabelle/Bali/TypeSafe.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* The type soundness proof for Java *}
    1.10 +
    1.11 +
    1.12 +theory TypeSafe = Eval + WellForm + Conform:
    1.13 +
    1.14 +section "result conformance"
    1.15 +
    1.16 +constdefs
    1.17 +  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
    1.18 +          ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
    1.19 + "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
    1.20 +  \<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"
    1.21 +
    1.22 +  rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
    1.23 +          ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_"                               [71,71,71,71,71,71] 70)
    1.24 +  "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
    1.25 +    \<equiv> case T of
    1.26 +        Inl T  \<Rightarrow> if (\<exists>vf. t=In2 vf)
    1.27 +                  then G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T \<and> s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L)
    1.28 +                  else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
    1.29 +      | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
    1.30 +
    1.31 +lemma rconf_In1 [simp]: 
    1.32 + "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
    1.33 +apply (unfold rconf_def)
    1.34 +apply (simp (no_asm))
    1.35 +done
    1.36 +
    1.37 +lemma rconf_In2 [simp]: 
    1.38 + "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))"
    1.39 +apply (unfold rconf_def)
    1.40 +apply (simp (no_asm))
    1.41 +done
    1.42 +
    1.43 +lemma rconf_In3 [simp]: 
    1.44 + "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"
    1.45 +apply (unfold rconf_def)
    1.46 +apply (simp (no_asm))
    1.47 +done
    1.48 +
    1.49 +section "fits and conf"
    1.50 +
    1.51 +(* unused *)
    1.52 +lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
    1.53 +apply (unfold fits_def)
    1.54 +apply clarify
    1.55 +apply (erule swap, simp (no_asm_use))
    1.56 +apply (drule conf_RefTD)
    1.57 +apply auto
    1.58 +done
    1.59 +
    1.60 +lemma fits_conf: 
    1.61 +  "\<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'"
    1.62 +apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
    1.63 +apply (force dest: conf_RefTD intro: conf_AddrI)
    1.64 +done
    1.65 +
    1.66 +lemma fits_Array: 
    1.67 + "\<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'"
    1.68 +apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
    1.69 +apply (force dest: conf_RefTD intro: conf_AddrI)
    1.70 +done
    1.71 +
    1.72 +
    1.73 +
    1.74 +section "gext"
    1.75 +
    1.76 +lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
    1.77 +apply (simp (no_asm_simp) only: split_tupled_all)
    1.78 +apply (erule halloc.induct)
    1.79 +apply  (auto dest!: new_AddrD)
    1.80 +done
    1.81 +
    1.82 +lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
    1.83 +apply (simp (no_asm_simp) only: split_tupled_all)
    1.84 +apply (erule sxalloc.induct)
    1.85 +apply   (auto dest!: halloc_gext)
    1.86 +done
    1.87 +
    1.88 +lemma eval_gext_lemma [rule_format (no_asm)]: 
    1.89 + "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
    1.90 +    In1 v \<Rightarrow> True  
    1.91 +  | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
    1.92 +  | In3 vs \<Rightarrow> True)"
    1.93 +apply (erule eval_induct)
    1.94 +prefer 24 
    1.95 +  apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
    1.96 +apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
    1.97 + simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2
    1.98 + split del: split_if_asm split add: sum3.split)
    1.99 +(* 6 subgoals *)
   1.100 +apply force+
   1.101 +done
   1.102 +
   1.103 +lemma evar_gext_f: 
   1.104 +  "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
   1.105 +apply (drule eval_gext_lemma [THEN conjunct2])
   1.106 +apply auto
   1.107 +done
   1.108 +
   1.109 +lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
   1.110 +
   1.111 +lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,x2,s2) \<Longrightarrow> s1\<le>|s2"
   1.112 +apply (drule eval_gext)
   1.113 +apply auto
   1.114 +done
   1.115 +
   1.116 +lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
   1.117 +apply (erule eval_cases , auto split del: split_if_asm)
   1.118 +apply (case_tac "inited C (globs s1)")
   1.119 +apply  (clarsimp split del: split_if_asm)+
   1.120 +apply (drule eval_gext')+
   1.121 +apply (drule init_class_obj_inited)
   1.122 +apply (erule inited_gext)
   1.123 +apply (simp (no_asm_use))
   1.124 +done
   1.125 +
   1.126 +
   1.127 +section "Lemmas"
   1.128 +
   1.129 +lemma obj_ty_obj_class1: 
   1.130 + "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
   1.131 +apply (case_tac "tag obj")
   1.132 +apply (auto simp add: obj_ty_def obj_class_def)
   1.133 +done
   1.134 +
   1.135 +lemma oconf_init_obj: 
   1.136 + "\<lbrakk>wf_prog G;  
   1.137 + (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
   1.138 +\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   1.139 +apply (auto intro!: oconf_init_obj_lemma unique_fields)
   1.140 +done
   1.141 +
   1.142 +(*
   1.143 +lemma obj_split: "P obj = (\<forall> oi vs. obj = \<lparr>tag=oi,values=vs\<rparr> \<longrightarrow> ?P \<lparr>tag=oi,values=vs\<rparr>)"
   1.144 +apply auto
   1.145 +apply (case_tac "obj")
   1.146 +apply auto
   1.147 +*)
   1.148 +
   1.149 +lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
   1.150 +  wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   1.151 +                        | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   1.152 +  (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   1.153 +apply (unfold init_obj_def)
   1.154 +apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   1.155 +            simp add: obj.update_defs)
   1.156 +done
   1.157 +
   1.158 +lemma conforms_init_class_obj: 
   1.159 + "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   1.160 +  (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
   1.161 +apply (rule not_initedD [THEN conforms_newG])
   1.162 +apply    (auto)
   1.163 +done
   1.164 +
   1.165 +
   1.166 +lemma fst_init_lvars[simp]: 
   1.167 + "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
   1.168 +  (if static m then x else (np a') x)"
   1.169 +apply (simp (no_asm) add: init_lvars_def2)
   1.170 +done
   1.171 +
   1.172 +
   1.173 +lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
   1.174 +  is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
   1.175 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.176 +apply (case_tac "aa")
   1.177 +apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
   1.178 +       intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
   1.179 +done
   1.180 +
   1.181 +lemma halloc_type_sound: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
   1.182 +  T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
   1.183 +  (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
   1.184 +apply (auto elim!: halloc_conforms)
   1.185 +apply (case_tac "aa")
   1.186 +apply (subst obj_ty_eq)
   1.187 +apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   1.188 +done
   1.189 +
   1.190 +lemma sxalloc_type_sound: 
   1.191 + "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> case fst s1 of  
   1.192 +  None \<Rightarrow> s2 = s1 | Some x \<Rightarrow>  
   1.193 +  (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))"
   1.194 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.195 +apply (erule sxalloc.induct)
   1.196 +apply   auto
   1.197 +apply (rule halloc_conforms [THEN conforms_xconf])
   1.198 +apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   1.199 +done
   1.200 +
   1.201 +lemma wt_init_comp_ty: 
   1.202 +"is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
   1.203 +apply (unfold init_comp_ty_def)
   1.204 +apply (clarsimp simp add: accessible_in_RefT_simp 
   1.205 +                          is_acc_type_def is_acc_class_def)
   1.206 +done
   1.207 +
   1.208 +
   1.209 +declare fun_upd_same [simp]
   1.210 +
   1.211 +declare fun_upd_apply [simp del]
   1.212 +
   1.213 +
   1.214 +constdefs
   1.215 +  DynT_prop::"[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" 
   1.216 +                                              ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
   1.217 + "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
   1.218 +                     (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
   1.219 +
   1.220 +lemma DynT_propI: 
   1.221 + "\<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> 
   1.222 +  \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   1.223 +proof (unfold DynT_prop_def)
   1.224 +  assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
   1.225 +     and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
   1.226 +     and            wf: "wf_prog G"
   1.227 +     and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   1.228 +  let ?invCls = "(invocation_class mode s a' statT)"
   1.229 +  let ?IntVir = "mode = IntVir"
   1.230 +  let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
   1.231 +                          (if \<exists>T. statT = ArrayT T
   1.232 +                                  then invCls = Object
   1.233 +                                  else G\<turnstile>Class invCls\<preceq>RefT statT)"
   1.234 +  show "?IntVir \<longrightarrow> ?Concl ?invCls"
   1.235 +  proof  
   1.236 +    assume modeIntVir: ?IntVir 
   1.237 +    with mode have not_Null: "a' \<noteq> Null" ..
   1.238 +    from statT_a' not_Null state_conform 
   1.239 +    obtain a obj 
   1.240 +      where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
   1.241 +                        "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
   1.242 +      by (blast dest: conforms_RefTD)
   1.243 +    show "?Concl ?invCls"
   1.244 +    proof (cases "tag obj")
   1.245 +      case CInst
   1.246 +      with modeIntVir obj_props
   1.247 +      show ?thesis 
   1.248 +	by (auto dest!: widen_Array2 split add: split_if)
   1.249 +    next
   1.250 +      case Arr
   1.251 +      from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
   1.252 +      moreover from Arr have "obj_class obj = Object" 
   1.253 +	by (blast dest: obj_class_Arr1)
   1.254 +      moreover note modeIntVir obj_props wf 
   1.255 +      ultimately show ?thesis by (auto dest!: widen_Array )
   1.256 +    qed
   1.257 +  qed
   1.258 +qed
   1.259 +
   1.260 +lemma invocation_methd:
   1.261 +"\<lbrakk>wf_prog G; statT \<noteq> NullT; 
   1.262 + (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
   1.263 + (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
   1.264 + (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
   1.265 + G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
   1.266 + dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
   1.267 +\<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
   1.268 +proof -
   1.269 +  assume         wf: "wf_prog G"
   1.270 +     and  not_NullT: "statT \<noteq> NullT"
   1.271 +     and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   1.272 +     and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
   1.273 +     and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
   1.274 +     and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   1.275 +     and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
   1.276 +                      = Some m"
   1.277 +  show ?thesis
   1.278 +  proof (cases statT)
   1.279 +    case NullT
   1.280 +    with not_NullT show ?thesis by simp
   1.281 +  next
   1.282 +    case IfaceT
   1.283 +    with statI_prop obtain I 
   1.284 +      where    statI: "statT = IfaceT I" and 
   1.285 +            is_iface: "is_iface G I"     and
   1.286 +          not_SuperM: "mode \<noteq> SuperM" by blast            
   1.287 +    
   1.288 +    show ?thesis 
   1.289 +    proof (cases mode)
   1.290 +      case Static
   1.291 +      with wf dynlookup statI is_iface 
   1.292 +      show ?thesis
   1.293 +	by (auto simp add: invocation_declclass_def dynlookup_def 
   1.294 +                           dynimethd_def dynmethd_C_C 
   1.295 +	            intro: dynmethd_declclass
   1.296 +	            dest!: wf_imethdsD
   1.297 +                     dest: table_of_map_SomeI
   1.298 +                    split: split_if_asm)
   1.299 +    next	
   1.300 +      case SuperM
   1.301 +      with not_SuperM show ?thesis ..
   1.302 +    next
   1.303 +      case IntVir
   1.304 +      with wf dynlookup IfaceT invC_prop show ?thesis 
   1.305 +	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   1.306 +                           DynT_prop_def
   1.307 +	            intro: methd_declclass dynmethd_declclass
   1.308 +	            split: split_if_asm)
   1.309 +    qed
   1.310 +  next
   1.311 +    case ClassT
   1.312 +    show ?thesis
   1.313 +    proof (cases mode)
   1.314 +      case Static
   1.315 +      with wf ClassT dynlookup statC_prop 
   1.316 +      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   1.317 +                               intro: dynmethd_declclass)
   1.318 +    next
   1.319 +      case SuperM
   1.320 +      with wf ClassT dynlookup statC_prop 
   1.321 +      show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   1.322 +                               intro: dynmethd_declclass)
   1.323 +    next
   1.324 +      case IntVir
   1.325 +      with wf ClassT dynlookup statC_prop invC_prop 
   1.326 +      show ?thesis
   1.327 +	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   1.328 +                           DynT_prop_def
   1.329 +	            intro: dynmethd_declclass)
   1.330 +    qed
   1.331 +  next
   1.332 +    case ArrayT
   1.333 +    show ?thesis
   1.334 +    proof (cases mode)
   1.335 +      case Static
   1.336 +      with wf ArrayT dynlookup show ?thesis
   1.337 +	by (auto simp add: invocation_declclass_def dynlookup_def 
   1.338 +                           dynimethd_def dynmethd_C_C
   1.339 +                    intro: dynmethd_declclass
   1.340 +                     dest: table_of_map_SomeI)
   1.341 +    next
   1.342 +      case SuperM
   1.343 +      with ArrayT statA_prop show ?thesis by blast
   1.344 +    next
   1.345 +      case IntVir
   1.346 +      with wf ArrayT dynlookup invC_prop show ?thesis
   1.347 +	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   1.348 +                           DynT_prop_def dynmethd_C_C
   1.349 +                    intro: dynmethd_declclass
   1.350 +                     dest: table_of_map_SomeI)
   1.351 +    qed
   1.352 +  qed
   1.353 +qed
   1.354 +   
   1.355 +declare split_paired_All [simp del] split_paired_Ex [simp del] 
   1.356 +ML_setup {*
   1.357 +simpset_ref() := simpset() delloop "split_all_tac";
   1.358 +claset_ref () := claset () delSWrapper "split_all_tac"
   1.359 +*}
   1.360 +lemma DynT_mheadsD: 
   1.361 +"\<lbrakk>G\<turnstile>invmode (mhd sm) e\<rightarrow>invC\<preceq>statT; 
   1.362 +  wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
   1.363 +  sm \<in> mheads G C statT sig; 
   1.364 +  invC = invocation_class (invmode (mhd sm) e) s a' statT;
   1.365 +  declC =invocation_declclass G (invmode (mhd sm) e) s a' statT sig
   1.366 + \<rbrakk> \<Longrightarrow> 
   1.367 +  \<exists> dm. 
   1.368 +  methd G declC sig = Some dm  \<and> G\<turnstile>resTy (mthd dm)\<preceq>resTy (mhd sm) \<and> 
   1.369 +  wf_mdecl G declC (sig, mthd dm) \<and>
   1.370 +  declC = declclass dm \<and>
   1.371 +  is_static dm = is_static sm \<and>  
   1.372 +  is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
   1.373 +  (if invmode (mhd sm) e = IntVir
   1.374 +      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   1.375 +      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   1.376 +            \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
   1.377 +           (declrefT sm) = ClassT (declclass dm))"
   1.378 +proof -
   1.379 +  assume invC_prop: "G\<turnstile>invmode (mhd sm) e\<rightarrow>invC\<preceq>statT" 
   1.380 +     and        wf: "wf_prog G" 
   1.381 +     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   1.382 +     and        sm: "sm \<in> mheads G C statT sig" 
   1.383 +     and      invC: "invC = invocation_class (invmode (mhd sm) e) s a' statT"
   1.384 +     and     declC: "declC = 
   1.385 +                    invocation_declclass G (invmode (mhd sm) e) s a' statT sig"
   1.386 +  from wt_e wf have type_statT: "is_type G (RefT statT)"
   1.387 +    by (auto dest: ty_expr_is_type)
   1.388 +  from sm have not_Null: "statT \<noteq> NullT" by auto
   1.389 +  from type_statT 
   1.390 +  have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   1.391 +    by (auto)
   1.392 +  from type_statT wt_e 
   1.393 +  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   1.394 +                                        invmode (mhd sm) e \<noteq> SuperM)"
   1.395 +    by (auto dest: invocationTypeExpr_noClassD)
   1.396 +  from wt_e
   1.397 +  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode (mhd sm) e \<noteq> SuperM)"
   1.398 +    by (auto dest: invocationTypeExpr_noClassD)
   1.399 +  show ?thesis
   1.400 +  proof (cases "invmode (mhd sm) e = IntVir")
   1.401 +    case True
   1.402 +    with invC_prop not_Null
   1.403 +    have invC_prop': " is_class G invC \<and> 
   1.404 +                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
   1.405 +                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
   1.406 +      by (auto simp add: DynT_prop_def) 
   1.407 +    from True 
   1.408 +    have "\<not> is_static sm"
   1.409 +      by (simp add: invmode_IntVir_eq)
   1.410 +    with invC_prop' not_Null
   1.411 +    have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
   1.412 +      by (cases statT) auto
   1.413 +    with sm wf type_statT obtain dm where
   1.414 +           dm: "dynlookup G statT invC sig = Some dm" and
   1.415 +      resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mhd sm)"      and
   1.416 +       static: "is_static dm = is_static sm"
   1.417 +      by - (drule dynamic_mheadsD,auto)
   1.418 +    with declC invC not_Null 
   1.419 +    have declC': "declC = (declclass dm)" 
   1.420 +      by (auto simp add: invocation_declclass_def)
   1.421 +    with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
   1.422 +    have dm': "methd G declC sig = Some dm"
   1.423 +      by - (drule invocation_methd,auto)
   1.424 +    from wf dm invC_prop' declC' type_statT 
   1.425 +    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   1.426 +      by (auto dest: dynlookup_declC)
   1.427 +    from wf dm' declC_prop declC' 
   1.428 +    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   1.429 +      by (auto dest: methd_wf_mdecl)
   1.430 +    from invC_prop' 
   1.431 +    have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
   1.432 +      by auto
   1.433 +    from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
   1.434 +    show ?thesis by auto
   1.435 +  next
   1.436 +    case False
   1.437 +    with type_statT wf invC not_Null wf_I wf_A
   1.438 +    have invC_prop': "is_class G invC \<and>  
   1.439 +                     ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   1.440 +                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
   1.441 +        by (case_tac "statT") (auto simp add: invocation_class_def 
   1.442 +                                       split: inv_mode.splits)
   1.443 +    with not_Null wf
   1.444 +    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   1.445 +      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
   1.446 +                                            dynimethd_def)
   1.447 +    from sm wf wt_e not_Null False invC_prop' obtain "dm" where
   1.448 +                    dm: "methd G invC sig = Some dm"          and
   1.449 +	eq_declC_sm_dm:"declrefT sm = ClassT (declclass dm)"  and
   1.450 +	     eq_mheads:"mhd sm=mhead (mthd dm) "
   1.451 +      by - (drule static_mheadsD, auto dest: accmethd_SomeD)
   1.452 +    then have static: "is_static dm = is_static sm" by - (case_tac "sm",auto)
   1.453 +    with declC invC dynlookup_static dm
   1.454 +    have declC': "declC = (declclass dm)"  
   1.455 +      by (auto simp add: invocation_declclass_def)
   1.456 +    from invC_prop' wf declC' dm 
   1.457 +    have dm': "methd G declC sig = Some dm"
   1.458 +      by (auto intro: methd_declclass)
   1.459 +    from wf dm invC_prop' declC' type_statT 
   1.460 +    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   1.461 +      by (auto dest: methd_declC )
   1.462 +    then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
   1.463 +    from wf dm' declC_prop declC' 
   1.464 +    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   1.465 +      by (auto dest: methd_wf_mdecl)
   1.466 +    from invC_prop' declC_prop declC_prop1
   1.467 +    have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   1.468 +                       \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
   1.469 +      by auto
   1.470 +    from False dm' wf_dm invC_prop' declC_prop statC_prop declC' 
   1.471 +         eq_declC_sm_dm eq_mheads static
   1.472 +    show ?thesis by auto
   1.473 +  qed
   1.474 +qed
   1.475 +
   1.476 +(*
   1.477 +lemma DynT_mheadsD: 
   1.478 +"\<lbrakk>G\<turnstile>invmode (mhd sm) e\<rightarrow>invC\<preceq>statT; 
   1.479 +  wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
   1.480 +  sm \<in> mheads G C statT sig; 
   1.481 +  invC = invocation_class (invmode (mhd sm) e) s a' statT;
   1.482 +  declC =invocation_declclass G (invmode (mhd sm) e) s a' statT sig
   1.483 + \<rbrakk> \<Longrightarrow> 
   1.484 +  \<exists> dm. 
   1.485 +  methd G declC sig = Some dm  \<and> G\<turnstile>resTy (mthd dm)\<preceq>resTy (mhd sm) \<and> 
   1.486 +  wf_mdecl G declC (sig, mthd dm) \<and>  
   1.487 +  is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
   1.488 +  (if invmode (mhd sm) e = IntVir
   1.489 +      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   1.490 +      else (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>statC \<preceq>\<^sub>C declC) \<and> 
   1.491 +           (declrefT sm) = ClassT (declclass dm))"
   1.492 +proof -
   1.493 +  assume invC_prop: "G\<turnstile>invmode (mhd sm) e\<rightarrow>invC\<preceq>statT" 
   1.494 +     and        wf: "wf_prog G" 
   1.495 +     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   1.496 +     and        sm: "sm \<in> mheads G C statT sig" 
   1.497 +     and      invC: "invC = invocation_class (invmode (mhd sm) e) s a' statT"
   1.498 +     and     declC: "declC = 
   1.499 +                    invocation_declclass G (invmode (mhd sm) e) s a' statT sig"
   1.500 +  from wt_e wf have type_statT: "is_type G (RefT statT)"
   1.501 +    by (auto dest: ty_expr_is_type)
   1.502 +  from sm have not_Null: "statT \<noteq> NullT" by auto
   1.503 +  from type_statT 
   1.504 +  have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   1.505 +    by (auto)
   1.506 +  from type_statT wt_e 
   1.507 +  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   1.508 +                                        invmode (mhd sm) e \<noteq> SuperM)"
   1.509 +    by (auto dest: invocationTypeExpr_noClassD)
   1.510 +  from wt_e
   1.511 +  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode (mhd sm) e \<noteq> SuperM)"
   1.512 +    by (auto dest: invocationTypeExpr_noClassD)
   1.513 +  show ?thesis
   1.514 +  proof (cases "invmode (mhd sm) e = IntVir")
   1.515 +    case True
   1.516 +    with invC_prop not_Null
   1.517 +    have invC_prop': "is_class G invC \<and>  
   1.518 +                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
   1.519 +                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
   1.520 +      by (auto simp add: DynT_prop_def) 
   1.521 +    with sm wf type_statT not_Null obtain dm where
   1.522 +           dm: "dynlookup G statT invC sig = Some dm" and
   1.523 +      resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mhd sm)"
   1.524 +      by - (clarify,drule dynamic_mheadsD,auto)
   1.525 +    with declC invC not_Null 
   1.526 +    have declC': "declC = (declclass dm)" 
   1.527 +      by (auto simp add: invocation_declclass_def)
   1.528 +    with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
   1.529 +    have dm': "methd G declC sig = Some dm"
   1.530 +      by - (drule invocation_methd,auto)
   1.531 +    from wf dm invC_prop' declC' type_statT 
   1.532 +    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   1.533 +      by (auto dest: dynlookup_declC)
   1.534 +    from wf dm' declC_prop declC' 
   1.535 +    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   1.536 +      by (auto dest: methd_wf_mdecl)
   1.537 +    from invC_prop' 
   1.538 +    have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
   1.539 +      by auto
   1.540 +    from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop
   1.541 +    show ?thesis by auto
   1.542 +  next
   1.543 +    case False
   1.544 +    
   1.545 +    with type_statT wf invC not_Null wf_I wf_A
   1.546 +    have invC_prop': "is_class G invC \<and>  
   1.547 +                     ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   1.548 +                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
   1.549 +        
   1.550 +        by (case_tac "statT") (auto simp add: invocation_class_def 
   1.551 +                                       split: inv_mode.splits)
   1.552 +    with not_Null 
   1.553 +    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   1.554 +      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_def 
   1.555 +                                            dynimethd_def)
   1.556 +    from sm wf wt_e not_Null False invC_prop' obtain "dm" where
   1.557 +                    dm: "methd G invC sig = Some dm"          and
   1.558 +	eq_declC_sm_dm:"declrefT sm = ClassT (declclass dm)"  and
   1.559 +	     eq_mheads:"mhd sm=mhead (mthd dm) "
   1.560 +      by - (drule static_mheadsD, auto dest: accmethd_SomeD)
   1.561 +    with declC invC dynlookup_static dm
   1.562 +    have declC': "declC = (declclass dm)"  
   1.563 +      by (auto simp add: invocation_declclass_def)
   1.564 +    from invC_prop' wf declC' dm 
   1.565 +    have dm': "methd G declC sig = Some dm"
   1.566 +      by (auto intro: methd_declclass)
   1.567 +    from wf dm invC_prop' declC' type_statT 
   1.568 +    have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   1.569 +      by (auto dest: methd_declC )   
   1.570 +    from wf dm' declC_prop declC' 
   1.571 +    have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   1.572 +      by (auto dest: methd_wf_mdecl)
   1.573 +    from invC_prop' declC_prop
   1.574 +    have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>statC \<preceq>\<^sub>C declC)" 
   1.575 +      by auto
   1.576 +    from False dm' wf_dm invC_prop' declC_prop statC_prop 
   1.577 +         eq_declC_sm_dm eq_mheads
   1.578 +    show ?thesis by auto
   1.579 +  qed
   1.580 +qed	
   1.581 +*)
   1.582 +
   1.583 +declare split_paired_All [simp del] split_paired_Ex [simp del] 
   1.584 +declare split_if     [split del] split_if_asm     [split del] 
   1.585 +        option.split [split del] option.split_asm [split del]
   1.586 +ML_setup {*
   1.587 +simpset_ref() := simpset() delloop "split_all_tac";
   1.588 +claset_ref () := claset () delSWrapper "split_all_tac"
   1.589 +*}
   1.590 +
   1.591 +lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
   1.592 + isrtype G (statT);
   1.593 + G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
   1.594 +  mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   1.595 +                    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
   1.596 + \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
   1.597 +apply (case_tac "mode = IntVir")
   1.598 +apply (drule conf_RefTD)
   1.599 +apply (force intro!: conf_AddrI 
   1.600 +            simp add: obj_class_def split add: obj_tag.split_asm)
   1.601 +apply  clarsimp
   1.602 +apply  safe
   1.603 +apply    (erule (1) widen.subcls [THEN conf_widen])
   1.604 +apply    (erule wf_ws_prog)
   1.605 +
   1.606 +apply    (frule widen_Object) apply (erule wf_ws_prog)
   1.607 +apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
   1.608 +done
   1.609 +
   1.610 +
   1.611 +lemma Ass_lemma: 
   1.612 + "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2; G,s2\<turnstile>v\<Colon>\<preceq>T'; 
   1.613 +   s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)
   1.614 +  \<rbrakk> \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and> 
   1.615 +        (\<lambda>(x',s'). x' = None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T') (assign f v (Norm s2))"
   1.616 +apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
   1.617 +apply (drule eval_gext', clarsimp)
   1.618 +apply (erule conf_gext)
   1.619 +apply simp
   1.620 +done
   1.621 +
   1.622 +lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
   1.623 +    x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
   1.624 +apply (auto split add: split_abrupt_if simp add: throw_def2)
   1.625 +apply (erule conforms_xconf)
   1.626 +apply (frule conf_RefTD)
   1.627 +apply (auto elim: widen.subcls [THEN conf_widen])
   1.628 +done
   1.629 +
   1.630 +lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
   1.631 + (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
   1.632 + \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
   1.633 +apply (rule conforms_allocL)
   1.634 +apply  (erule conforms_NormI)
   1.635 +apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
   1.636 +apply (auto intro!: conf_AddrI)
   1.637 +done
   1.638 +
   1.639 +lemma Fin_lemma: 
   1.640 +"\<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> 
   1.641 +\<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   1.642 +apply (force elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   1.643 +done
   1.644 +
   1.645 +lemma FVar_lemma1: "\<lbrakk>table_of (DeclConcepts.fields G Ca) (fn, C) = Some f ; 
   1.646 +  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class Ca; wf_prog G; G\<turnstile>Ca\<preceq>\<^sub>C C; C \<noteq> Object; 
   1.647 +  class G C = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1); 
   1.648 +  (if static f then id else np a) x2 = None\<rbrakk> 
   1.649 + \<Longrightarrow>  
   1.650 +  \<exists>obj. globs s2 (if static f then Inr C else Inl (the_Addr a)) = Some obj \<and> 
   1.651 +  var_tys G (tag obj)  (if static f then Inr C else Inl(the_Addr a)) 
   1.652 +          (Inl(fn,C)) = Some (type f)"
   1.653 +apply (drule initedD)
   1.654 +apply (frule subcls_is_class2, simp (no_asm_simp))
   1.655 +apply (case_tac "static f")
   1.656 +apply  clarsimp
   1.657 +apply  (drule (1) rev_gext_objD, clarsimp)
   1.658 +apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
   1.659 +apply  (rule var_tys_Some_eq [THEN iffD2])
   1.660 +apply  clarsimp
   1.661 +apply  (erule fields_table_SomeI, simp (no_asm))
   1.662 +apply clarsimp
   1.663 +apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   1.664 +apply (auto dest!: widen_Array split add: obj_tag.split)
   1.665 +apply (rotate_tac -1) (* to front: tag obja = CInst pid_field_type to enable
   1.666 +                         conditional rewrite *)
   1.667 +apply (rule fields_table_SomeI)
   1.668 +apply (auto elim!: fields_mono subcls_is_class2)
   1.669 +done
   1.670 +
   1.671 +lemma FVar_lemma: 
   1.672 +"\<lbrakk>((v, f), Norm s2') = fvar C (static field) fn a (x2, s2); G\<turnstile>Ca\<preceq>\<^sub>C C;  
   1.673 +  table_of (DeclConcepts.fields G Ca) (fn, C) = Some field; wf_prog G;   
   1.674 +  x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C \<noteq> Object; class G C = Some y;   
   1.675 +  (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1)\<rbrakk> \<Longrightarrow>  
   1.676 +  G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
   1.677 +apply (unfold assign_conforms_def)
   1.678 +apply (drule sym)
   1.679 +apply (clarsimp simp add: fvar_def2)
   1.680 +apply (drule (9) FVar_lemma1)
   1.681 +apply (clarsimp)
   1.682 +apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   1.683 +apply clarsimp
   1.684 +apply (drule (1) rev_gext_objD)
   1.685 +apply (auto elim!: conforms_upd_gobj)
   1.686 +done
   1.687 +
   1.688 +
   1.689 +lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
   1.690 + the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
   1.691 +\<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
   1.692 +apply (erule widen_Array_Array [THEN conf_widen])
   1.693 +apply  (erule_tac [2] wf_ws_prog)
   1.694 +apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   1.695 +defer apply assumption
   1.696 +apply (force intro: var_tys_Some_eq [THEN iffD2])
   1.697 +done
   1.698 +
   1.699 +lemma obj_split: "\<And> obj. \<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
   1.700 +proof record_split
   1.701 +  fix tag values more
   1.702 +  show "\<exists>t vs. \<lparr>tag = tag, values = values, \<dots> = more\<rparr> = \<lparr>tag = t, values = vs\<rparr>"
   1.703 +    by auto
   1.704 +qed
   1.705 + 
   1.706 +lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
   1.707 +  ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
   1.708 +  (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)"
   1.709 +apply (unfold assign_conforms_def)
   1.710 +apply (drule sym)
   1.711 +apply (clarsimp simp add: avar_def2)
   1.712 +apply (drule (1) conf_gext)
   1.713 +apply (drule conf_RefTD, clarsimp)
   1.714 +apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
   1.715 +defer
   1.716 +apply   (rule obj_split)
   1.717 +apply clarify
   1.718 +apply (frule obj_ty_widenD)
   1.719 +apply (auto dest!: widen_Class)
   1.720 +apply  (force dest: AVar_lemma1)
   1.721 +apply (auto split add: split_if)
   1.722 +apply (force elim!: fits_Array dest: gext_objD 
   1.723 +       intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
   1.724 +done
   1.725 +
   1.726 +
   1.727 +section "Call"
   1.728 +lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   1.729 +  wf_mhead G P sig mh; 
   1.730 +  Ball (set lvars) (split (\<lambda>vn. is_type G)); 
   1.731 +  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   1.732 +  G,s\<turnstile>init_vals (table_of lvars)(pars mh[\<mapsto>]pvs)
   1.733 +      [\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   1.734 +apply (unfold wf_mhead_def)
   1.735 +apply clarify
   1.736 +apply (erule (2) Ball_set_table [THEN lconf_init_vals, THEN lconf_ext_list])
   1.737 +apply (drule wf_ws_prog)
   1.738 +apply (erule (2) conf_list_widen)
   1.739 +done
   1.740 +
   1.741 +
   1.742 +lemma lconf_map_lname [simp]: 
   1.743 +  "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
   1.744 +   =
   1.745 +  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.746 +apply (unfold lconf_def)
   1.747 +apply safe
   1.748 +apply (case_tac "n")
   1.749 +apply (force split add: lname.split)+
   1.750 +done
   1.751 +
   1.752 +lemma lconf_map_ename [simp]:
   1.753 +  "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
   1.754 +   =
   1.755 +  (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.756 +apply (unfold lconf_def)
   1.757 +apply safe
   1.758 +apply (force split add: ename.split)+
   1.759 +done
   1.760 +
   1.761 +
   1.762 +lemma defval_conf1 [rule_format (no_asm), elim]: 
   1.763 +  "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
   1.764 +apply (unfold conf_def)
   1.765 +apply (induct "T")
   1.766 +apply (auto intro: prim_ty.induct)
   1.767 +done
   1.768 +
   1.769 +
   1.770 +lemma conforms_init_lvars: 
   1.771 +"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   1.772 +  list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
   1.773 +  (x, s)\<Colon>\<preceq>(G, L); 
   1.774 +  methd G declC sig = Some dm;  
   1.775 +  isrtype G statT;
   1.776 +  G\<turnstile>invC\<preceq>\<^sub>C declC; 
   1.777 +  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
   1.778 +  invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
   1.779 +  invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
   1.780 +       (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   1.781 +    \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
   1.782 +  invC  = invocation_class (invmode (mhd sm) e) s a' statT;
   1.783 +  declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
   1.784 +  Ball (set (lcls (mbody (mthd dm)))) 
   1.785 +       (split (\<lambda>vn. is_type G)) 
   1.786 + \<rbrakk> \<Longrightarrow>  
   1.787 +  init_lvars G declC sig (invmode (mhd sm) e) a'  
   1.788 +  pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
   1.789 +                (case k of
   1.790 +                   EName e \<Rightarrow> (case e of 
   1.791 +                                 VNam v 
   1.792 +                                  \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
   1.793 +                                        (pars (mthd dm)[\<mapsto>]parTs sig)) v
   1.794 +                               | Res \<Rightarrow> Some (resTy (mthd dm)))
   1.795 +                 | This \<Rightarrow> if (static (mthd sm)) 
   1.796 +                              then None else Some (Class declC)))"
   1.797 +apply (simp add: init_lvars_def2)
   1.798 +apply (rule conforms_set_locals)
   1.799 +apply  (simp (no_asm_simp) split add: split_if)
   1.800 +apply (drule  (4) DynT_conf)
   1.801 +apply clarsimp
   1.802 +(* apply intro *)
   1.803 +apply (drule (4) conforms_init_lvars_lemma)
   1.804 +apply (case_tac "dm",simp)
   1.805 +apply (rule conjI)
   1.806 +apply (unfold lconf_def, clarify)
   1.807 +apply (rule defval_conf1)
   1.808 +apply (clarsimp simp add: wf_mhead_def is_acc_type_def)
   1.809 +apply (case_tac "is_static sm")
   1.810 +apply simp_all
   1.811 +done
   1.812 +
   1.813 +
   1.814 +lemma Call_type_sound: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> (x2, s2);  
   1.815 + declC 
   1.816 + = invocation_declclass G (invmode (mhd esm) e) s2 a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.817 +s2'=init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> (invmode (mhd esm) e) a' pvs (x2,s2);
   1.818 + G\<turnstile>s2' \<midarrow>Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> (x3, s3);    
   1.819 + \<forall>L. s2'\<Colon>\<preceq>(G, L) 
   1.820 +     \<longrightarrow> (\<forall>T. \<lparr>prg=G,cls=declC,lcl=L\<rparr>\<turnstile> Methd declC \<lparr>name=mn,parTs=pTs\<rparr>\<Colon>-T 
   1.821 +     \<longrightarrow> (x3, s3)\<Colon>\<preceq>(G, L) \<and> (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>T));  
   1.822 + Norm s0\<Colon>\<preceq>(G, L); 
   1.823 + \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>ps\<Colon>\<doteq>pTsa;  
   1.824 + max_spec G C statT \<lparr>name=mn,parTs=pTsa\<rparr> = {(esm, pTs)}; 
   1.825 + (x1, s1)\<Colon>\<preceq>(G, L); 
   1.826 + x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq>RefT statT; (x2, s2)\<Colon>\<preceq>(G, L);  
   1.827 + x2 = None \<longrightarrow> list_all2 (conf G s2) pvs pTsa;
   1.828 + sm=(mhd esm)\<rbrakk> \<Longrightarrow>     
   1.829 + (x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) \<and> 
   1.830 + (x3 = None \<longrightarrow> G,s3\<turnstile>v\<Colon>\<preceq>resTy sm)"
   1.831 +apply clarify
   1.832 +apply (case_tac "x2")
   1.833 +defer
   1.834 +apply  (clarsimp split add: split_if_asm simp add: init_lvars_def2)
   1.835 +apply (case_tac "a' = Null \<and> \<not> (static (mhd esm)) \<and> e \<noteq> Super")
   1.836 +apply  (clarsimp simp add: init_lvars_def2)
   1.837 +apply clarsimp
   1.838 +apply (drule eval_gext')
   1.839 +apply (frule (1) conf_gext)
   1.840 +apply (drule max_spec2mheads, clarsimp)
   1.841 +apply (subgoal_tac "invmode (mhd esm) e = IntVir \<longrightarrow> a' \<noteq> Null")
   1.842 +defer  
   1.843 +apply  (clarsimp simp add: invmode_IntVir_eq)
   1.844 +apply (frule (6) DynT_mheadsD [OF DynT_propI,of _ "s2"],(rule HOL.refl)+)
   1.845 +apply clarify
   1.846 +apply (drule wf_mdeclD1, clarsimp) 
   1.847 +apply (frule  ty_expr_is_type) apply simp
   1.848 +apply (frule (2) conforms_init_lvars)
   1.849 +apply   simp
   1.850 +apply   assumption+
   1.851 +apply   simp
   1.852 +apply   assumption+
   1.853 +apply   clarsimp
   1.854 +apply   (rule HOL.refl)
   1.855 +apply   simp
   1.856 +apply   (rule Ball_weaken)
   1.857 +apply     assumption
   1.858 +apply     (force simp add: is_acc_type_def)
   1.859 +apply (tactic "smp_tac 1 1")
   1.860 +apply (frule (2) wt_MethdI, clarsimp)
   1.861 +apply (subgoal_tac "is_static dm = (static (mthd esm))") 
   1.862 +apply   (simp only:)
   1.863 +apply   (tactic "smp_tac 1 1")
   1.864 +apply   (rule conjI)
   1.865 +apply     (erule  conforms_return)
   1.866 +apply     blast
   1.867 +
   1.868 +apply     (force dest!: eval_gext del: impCE simp add: init_lvars_def2)
   1.869 +apply     clarsimp
   1.870 +apply     (drule (2) widen_trans, erule (1) conf_widen)
   1.871 +apply     (erule wf_ws_prog)
   1.872 +
   1.873 +apply   auto
   1.874 +done
   1.875 +
   1.876 +
   1.877 +subsection "accessibility"
   1.878 +
   1.879 +theorem dynamic_field_access_ok:
   1.880 +  (assumes wf: "wf_prog G" and
   1.881 +       eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
   1.882 +     not_Null: "a\<noteq>Null" and
   1.883 +    conform_a: "G,(store s2)\<turnstile>a\<Colon>\<preceq> Class statC" and
   1.884 +   conform_s2: "s2\<Colon>\<preceq>(G, L)" and 
   1.885 +    normal_s2: "normal s2" and
   1.886 +         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>,dt\<Turnstile>e\<Colon>-Class statC" and
   1.887 +            f: "accfield G accC statC fn = Some f" and
   1.888 +         dynC: "if stat then dynC=statC  
   1.889 +                        else dynC=obj_class (lookup_obj (store s2) a)"
   1.890 +  ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   1.891 +     G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.892 +proof (cases "stat")
   1.893 +  case True
   1.894 +  with dynC 
   1.895 +  have dynC': "dynC=statC" by simp
   1.896 +  with f
   1.897 +  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   1.898 +    by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   1.899 +  with dynC' f
   1.900 +  show ?thesis
   1.901 +    by (auto intro!: static_to_dynamic_accessible_from
   1.902 +         dest: accfield_accessibleD accessible_from_commonD)
   1.903 +next
   1.904 +  case False
   1.905 +  with wf conform_a not_Null conform_s2 dynC
   1.906 +  obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.907 +    "is_class G dynC"
   1.908 +    by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s2)" L]
   1.909 +              dest: obj_ty_obj_class1
   1.910 +          simp add: obj_ty_obj_class )
   1.911 +  with wf f
   1.912 +  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   1.913 +    by (auto simp add: accfield_def Let_def
   1.914 +                 dest: fields_mono
   1.915 +                dest!: table_of_remap_SomeD)
   1.916 +  moreover
   1.917 +  from f subclseq
   1.918 +  have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.919 +    by (auto intro!: static_to_dynamic_accessible_from 
   1.920 +               dest: accfield_accessibleD)
   1.921 +  ultimately show ?thesis
   1.922 +    by blast
   1.923 +qed
   1.924 +
   1.925 +lemma call_access_ok: 
   1.926 +(assumes invC_prop: "G\<turnstile>invmode (mhd statM) e\<rightarrow>invC\<preceq>statT" 
   1.927 +     and        wf: "wf_prog G" 
   1.928 +     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   1.929 +     and     statM: "statM \<in> mheads G accC statT sig" 
   1.930 +     and      invC: "invC = invocation_class (invmode (mhd statM) e) s a statT"
   1.931 +)"\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
   1.932 +  G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
   1.933 +proof -
   1.934 +  from wt_e wf have type_statT: "is_type G (RefT statT)"
   1.935 +    by (auto dest: ty_expr_is_type)
   1.936 +  from statM have not_Null: "statT \<noteq> NullT" by auto
   1.937 +  from type_statT wt_e 
   1.938 +  have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   1.939 +                                        invmode (mhd statM) e \<noteq> SuperM)"
   1.940 +    by (auto dest: invocationTypeExpr_noClassD)
   1.941 +  from wt_e
   1.942 +  have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode (mhd statM) e \<noteq> SuperM)"
   1.943 +    by (auto dest: invocationTypeExpr_noClassD)
   1.944 +  show ?thesis
   1.945 +  proof (cases "invmode (mhd statM) e = IntVir")
   1.946 +    case True
   1.947 +    with invC_prop not_Null
   1.948 +    have invC_prop': "is_class G invC \<and>  
   1.949 +                      (if (\<exists>T. statT=ArrayT T) then invC=Object 
   1.950 +                                              else G\<turnstile>Class invC\<preceq>RefT statT)"
   1.951 +      by (auto simp add: DynT_prop_def)
   1.952 +    with True not_Null
   1.953 +    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
   1.954 +     by (cases statT) (auto simp add: invmode_def 
   1.955 +                         split: split_if split_if_asm) (*  was deleted above *)
   1.956 +    with statM type_statT wf 
   1.957 +    show ?thesis
   1.958 +      by - (rule dynlookup_access,auto)
   1.959 +  next
   1.960 +    case False
   1.961 +    with type_statT wf invC not_Null wf_I wf_A
   1.962 +    have invC_prop': " is_class G invC \<and>
   1.963 +                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   1.964 +                      (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
   1.965 +        by (case_tac "statT") (auto simp add: invocation_class_def 
   1.966 +                                       split: inv_mode.splits)
   1.967 +    with not_Null wf
   1.968 +    have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   1.969 +      by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
   1.970 +                                            dynimethd_def)
   1.971 +   from statM wf wt_e not_Null False invC_prop' obtain dynM where
   1.972 +                "accmethd G accC invC sig = Some dynM" 
   1.973 +     by (auto dest!: static_mheadsD)
   1.974 +   from invC_prop' False not_Null wf_I
   1.975 +   have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
   1.976 +     by (cases statT) (auto simp add: invmode_def
   1.977 +                        split: split_if split_if_asm) (*  was deleted above *)
   1.978 +   with statM type_statT wf 
   1.979 +    show ?thesis
   1.980 +      by - (rule dynlookup_access,auto)
   1.981 +  qed
   1.982 +qed
   1.983 +
   1.984 +section "main proof of type safety"
   1.985 +
   1.986 +ML {*
   1.987 +val forward_hyp_tac = EVERY' [smp_tac 1,
   1.988 +	FIRST'[mp_tac,etac exI,smp_tac 2,smp_tac 1,EVERY'[etac impE,etac exI]],
   1.989 +	REPEAT o (etac conjE)];
   1.990 +val typD_tac = eresolve_tac (thms "wt_elim_cases") THEN_ALL_NEW 
   1.991 +	EVERY' [full_simp_tac (simpset() setloop (K no_tac)), 
   1.992 +         clarify_tac(claset() addSEs[])]
   1.993 +*}
   1.994 +
   1.995 +lemma conforms_locals [rule_format]: 
   1.996 +  "(a,b)\<Colon>\<preceq>(G, L) \<longrightarrow> L x = Some T \<longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
   1.997 +apply (force simp: conforms_def Let_def lconf_def)
   1.998 +done
   1.999 +
  1.1000 +lemma eval_type_sound [rule_format (no_asm)]: 
  1.1001 + "wf_prog G \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1) \<Longrightarrow> (\<forall>L. s0\<Colon>\<preceq>(G,L) \<longrightarrow>    
  1.1002 +  (\<forall>C T. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and>  
  1.1003 +  (let (x,s) = s1 in x = None \<longrightarrow> G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T)))"
  1.1004 +apply (erule eval_induct)
  1.1005 +
  1.1006 +(* 29 subgoals *)
  1.1007 +(* Xcpt, Inst, Methd, Nil, Skip, Expr, Comp *)
  1.1008 +apply         (simp_all (no_asm_use) add: Let_def body_def)
  1.1009 +apply       (tactic "ALLGOALS (EVERY'[Clarify_tac, TRY o typD_tac, 
  1.1010 +                     TRY o forward_hyp_tac])")
  1.1011 +apply      (tactic"ALLGOALS(EVERY'[asm_simp_tac(simpset()),TRY o Clarify_tac])")
  1.1012 +
  1.1013 +(* 20 subgoals *)
  1.1014 +
  1.1015 +(* Break *)
  1.1016 +apply (erule conforms_absorb)
  1.1017 +
  1.1018 +(* Cons *)
  1.1019 +apply (erule_tac V = "G\<turnstile>Norm s0 \<midarrow>?ea\<succ>\<rightarrow> ?vs1" in thin_rl)
  1.1020 +apply (frule eval_gext')
  1.1021 +apply force
  1.1022 +
  1.1023 +(* LVar *)
  1.1024 +apply (force elim: conforms_localD [THEN lconfD] conforms_lupd 
  1.1025 +       simp add: assign_conforms_def lvar_def)
  1.1026 +
  1.1027 +(* Cast *)
  1.1028 +apply (force dest: fits_conf)
  1.1029 +
  1.1030 +(* Lit *)
  1.1031 +apply (rule conf_litval)
  1.1032 +apply (simp add: empty_dt_def)
  1.1033 +
  1.1034 +(* Super *)
  1.1035 +apply (rule conf_widen)
  1.1036 +apply   (erule (1) subcls_direct [THEN widen.subcls])
  1.1037 +apply  (erule (1) conforms_localD [THEN lconfD])
  1.1038 +apply (erule wf_ws_prog)
  1.1039 +
  1.1040 +(* Acc *)
  1.1041 +apply fast
  1.1042 +
  1.1043 +(* Body *)
  1.1044 +apply (rule conjI)
  1.1045 +apply (rule conforms_absorb)
  1.1046 +apply (fast)
  1.1047 +apply (fast intro: conforms_locals)
  1.1048 +
  1.1049 +(* Cond *)
  1.1050 +apply (simp split: split_if_asm)
  1.1051 +apply  (tactic "forward_hyp_tac 1", force)
  1.1052 +apply (tactic "forward_hyp_tac 1", force)
  1.1053 +
  1.1054 +(* If *)
  1.1055 +apply (force split add: split_if_asm)
  1.1056 +
  1.1057 +(* Loop *)
  1.1058 +apply (drule (1) wt.Loop)
  1.1059 +apply (clarsimp split: split_if_asm)
  1.1060 +apply (fast intro: conforms_absorb)
  1.1061 +
  1.1062 +(* Fin *)
  1.1063 +apply (case_tac "x1", force)
  1.1064 +apply (drule spec, erule impE, erule conforms_NormI)
  1.1065 +apply (erule impE)
  1.1066 +apply   blast
  1.1067 +apply (clarsimp)
  1.1068 +apply (erule (3) Fin_lemma)
  1.1069 +
  1.1070 +(* Throw *)
  1.1071 +apply (erule (3) Throw_lemma)
  1.1072 +
  1.1073 +(* NewC *)
  1.1074 +apply (clarsimp simp add: is_acc_class_def)
  1.1075 +apply (drule (1) halloc_type_sound,blast, rule HOL.refl, simp, simp)
  1.1076 +
  1.1077 +(* NewA *)
  1.1078 +apply (tactic "smp_tac 1 1",frule wt_init_comp_ty,erule impE,blast)
  1.1079 +apply (tactic "forward_hyp_tac 1")
  1.1080 +apply (case_tac "check_neg i' ab")
  1.1081 +apply  (clarsimp simp add: is_acc_type_def)
  1.1082 +apply  (drule (2) halloc_type_sound, rule HOL.refl, simp, simp)
  1.1083 +apply force
  1.1084 +
  1.1085 +(* Level 34, 6 subgoals *)
  1.1086 +
  1.1087 +(* Init *)
  1.1088 +apply (case_tac "inited C (globs s0)")
  1.1089 +apply  (clarsimp)
  1.1090 +apply (clarsimp)
  1.1091 +apply (frule (1) wf_prog_cdecl)
  1.1092 +apply (drule spec, erule impE, erule (3) conforms_init_class_obj)
  1.1093 +apply (drule_tac "psi" = "class G C = ?x" in asm_rl,erule impE,
  1.1094 +      force dest!: wf_cdecl_supD split add: split_if simp add: is_acc_class_def)
  1.1095 +apply (drule spec, erule impE, erule conforms_set_locals, rule lconf_empty)
  1.1096 +apply (erule impE) apply (rule exI) apply (erule wf_cdecl_wt_init)
  1.1097 +apply (drule (1) conforms_return, force dest: eval_gext', assumption)
  1.1098 +
  1.1099 +
  1.1100 +(* Ass *)
  1.1101 +apply (tactic "forward_hyp_tac 1")
  1.1102 +apply (rename_tac x1 s1 x2 s2 v va w L C Ta T', case_tac x1)
  1.1103 +prefer 2 apply force
  1.1104 +apply (case_tac x2)
  1.1105 +prefer 2 apply force
  1.1106 +apply (simp, drule conjunct2)
  1.1107 +apply (drule (1) conf_widen)
  1.1108 +apply  (erule wf_ws_prog)
  1.1109 +apply (erule (2) Ass_lemma)
  1.1110 +apply (clarsimp simp add: assign_conforms_def)
  1.1111 +
  1.1112 +(* Try *)
  1.1113 +apply (drule (1) sxalloc_type_sound, simp (no_asm_use))
  1.1114 +apply (case_tac a)
  1.1115 +apply  clarsimp
  1.1116 +apply clarsimp
  1.1117 +apply (tactic "smp_tac 1 1")
  1.1118 +apply (simp split add: split_if_asm)
  1.1119 +apply (fast dest: conforms_deallocL Try_lemma)
  1.1120 +
  1.1121 +(* FVar *)
  1.1122 +
  1.1123 +apply (frule accfield_fields)
  1.1124 +apply (frule ty_expr_is_type [THEN type_is_class],simp)
  1.1125 +apply simp
  1.1126 +apply (frule wf_ws_prog)
  1.1127 +apply (frule (1) fields_declC,simp)
  1.1128 +apply clarsimp 
  1.1129 +(*b y EVERY'[datac cfield_defpl_is_class 2, Clarsimp_tac] 1; not useful here*)
  1.1130 +apply (tactic "smp_tac 1 1")
  1.1131 +apply (tactic "forward_hyp_tac 1")
  1.1132 +apply (rule conjI, force split add: split_if simp add: fvar_def2)
  1.1133 +apply (drule init_yields_initd, frule eval_gext')
  1.1134 +apply clarsimp
  1.1135 +apply (case_tac "C=Object")
  1.1136 +apply  clarsimp
  1.1137 +apply (erule (9) FVar_lemma)
  1.1138 +
  1.1139 +(* AVar *)
  1.1140 +apply (tactic "forward_hyp_tac 1")
  1.1141 +apply (erule_tac V = "G\<turnstile>Norm s0 \<midarrow>?e1-\<succ>?a'\<rightarrow> (?x1 1, ?s1)" in thin_rl, 
  1.1142 +         frule eval_gext')
  1.1143 +apply (rule conjI)
  1.1144 +apply  (clarsimp simp add: avar_def2)
  1.1145 +apply clarsimp
  1.1146 +apply (erule (5) AVar_lemma)
  1.1147 +
  1.1148 +(* Call *)
  1.1149 +apply (tactic "forward_hyp_tac 1")
  1.1150 +apply (rule Call_type_sound)
  1.1151 +apply auto
  1.1152 +done
  1.1153 +
  1.1154 +
  1.1155 +declare fun_upd_apply [simp]
  1.1156 +declare split_paired_All [simp] split_paired_Ex [simp]
  1.1157 +declare split_if     [split] split_if_asm     [split] 
  1.1158 +        option.split [split] option.split_asm [split]
  1.1159 +ML_setup {* 
  1.1160 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac);
  1.1161 +claset_ref()  := claset () addSbefore ("split_all_tac", split_all_tac)
  1.1162 +*}
  1.1163 +
  1.1164 +theorem eval_ts: 
  1.1165 + "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T\<rbrakk> 
  1.1166 +\<Longrightarrow>  (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T)"
  1.1167 +apply (drule (3) eval_type_sound)
  1.1168 +apply (unfold Let_def)
  1.1169 +apply clarsimp
  1.1170 +done
  1.1171 +
  1.1172 +theorem evals_ts: 
  1.1173 +"\<lbrakk>G\<turnstile>s \<midarrow>es\<doteq>\<succ>vs\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>es\<Colon>\<doteq>Ts\<rbrakk> 
  1.1174 +\<Longrightarrow>  (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> list_all2 (conf G s') vs Ts)"
  1.1175 +apply (drule (3) eval_type_sound)
  1.1176 +apply (unfold Let_def)
  1.1177 +apply clarsimp
  1.1178 +done
  1.1179 +
  1.1180 +theorem evar_ts: 
  1.1181 +"\<lbrakk>G\<turnstile>s \<midarrow>v=\<succ>vf\<rightarrow> (x',s'); wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>v\<Colon>=T\<rbrakk> \<Longrightarrow>  
  1.1182 +  (x',s')\<Colon>\<preceq>(G,L) \<and> (x'=None \<longrightarrow> G,L,s'\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T)"
  1.1183 +apply (drule (3) eval_type_sound)
  1.1184 +apply (unfold Let_def)
  1.1185 +apply clarsimp
  1.1186 +done
  1.1187 +
  1.1188 +theorem exec_ts: 
  1.1189 +"\<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> \<Longrightarrow> s'\<Colon>\<preceq>(G,L)"
  1.1190 +apply (drule (3) eval_type_sound)
  1.1191 +apply (unfold Let_def)
  1.1192 +apply clarsimp
  1.1193 +done
  1.1194 +
  1.1195 +(*
  1.1196 +theorem dyn_methods_understood: 
  1.1197 + "\<And>s. \<lbrakk>wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>{t,md,IntVir}e..mn({pTs'}ps)\<Colon>-rT;  
  1.1198 +  s\<Colon>\<preceq>(G,L); G\<turnstile>s \<midarrow>e-\<succ>a'\<rightarrow> Norm s'; a' \<noteq> Null\<rbrakk> \<Longrightarrow>  
  1.1199 +  \<exists>a obj. a'=Addr a \<and> heap s' a = Some obj \<and> 
  1.1200 +  cmethd G (obj_class obj) (mn, pTs') \<noteq> None"
  1.1201 +apply (erule wt_elim_cases)
  1.1202 +apply (drule max_spec2mheads)
  1.1203 +apply (drule (3) eval_ts)
  1.1204 +apply (clarsimp split del: split_if split_if_asm)
  1.1205 +apply (drule (2) DynT_propI)
  1.1206 +apply  (simp (no_asm_simp))
  1.1207 +apply (tactic *) (* {* exhaust_cmethd_tac "the (cmethd G (target (invmode m e) s' a' md) (mn, pTs'))" 1 *} *)(*)
  1.1208 +apply (drule (4) DynT_mheadsD [THEN conjunct1], rule HOL.refl)
  1.1209 +apply (drule conf_RefTD)
  1.1210 +apply clarsimp
  1.1211 +done 
  1.1212 +*)
  1.1213 +
  1.1214 +end