src/HOL/Bali/TypeSafe.thy
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 13690 ac335b2f4a39
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  *)
     1.5  header {* The type soundness proof for Java *}
     1.6  
     1.7 -theory TypeSafe = Eval + WellForm + Conform:
     1.8 +theory TypeSafe = DefiniteAssignmentCorrect + Conform:
     1.9  
    1.10  section "error free"
    1.11   
    1.12 @@ -24,8 +24,7 @@
    1.13    have "error_free (abrupt1,store1)"
    1.14    proof (induct)
    1.15      case Abrupt 
    1.16 -    then show ?case
    1.17 -      .
    1.18 +    then show ?case .
    1.19    next
    1.20      case New
    1.21      then show ?case
    1.22 @@ -101,27 +100,64 @@
    1.23   (\<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>
    1.24   (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
    1.25  
    1.26 +
    1.27 +constdefs
    1.28    rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
    1.29            ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_"                               [71,71,71,71,71,71] 70)
    1.30    "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
    1.31      \<equiv> case T of
    1.32 -        Inl T  \<Rightarrow> if (\<exists>vf. t=In2 vf)
    1.33 -                  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.34 +        Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
    1.35 +                  then (\<forall> n. (the_In2 t) = LVar n 
    1.36 +                         \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
    1.37 +                             (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
    1.38 +                      (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
    1.39 +                      (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
    1.40                    else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
    1.41        | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
    1.42  
    1.43 +text {*
    1.44 + With @{term rconf} we describe the conformance of the result value of a term.
    1.45 + This definition gets rather complicated because of the relations between the
    1.46 + injections of the different terms, types and values. The main case distinction
    1.47 + is between single values and value lists. In case of value lists, every 
    1.48 + value has to conform to its type. For single values we have to do a further
    1.49 + case distinction, between values of variables @{term "\<exists>var. t=In2 var" } and
    1.50 + ordinary values. Values of variables are modelled as pairs consisting of the
    1.51 + current value and an update function which will perform an assignment to the
    1.52 + variable. This stems form the decision, that we only have one evaluation rule
    1.53 + for each kind of variable. The decision if we read or write to the 
    1.54 + variable is made by syntactic enclosing rules. So conformance of 
    1.55 + variable-values must ensure that both the current value and an update will 
    1.56 + conform to the type. With the introduction of definite assignment of local
    1.57 + variables we have to do another case distinction. For the notion of conformance
    1.58 + local variables are allowed to be @{term None}, since the definedness is not 
    1.59 + ensured by conformance but by definite assignment. Field and array variables 
    1.60 + must contain a value. 
    1.61 +*}
    1.62 + 
    1.63 +
    1.64 +
    1.65  lemma rconf_In1 [simp]: 
    1.66   "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
    1.67  apply (unfold rconf_def)
    1.68  apply (simp (no_asm))
    1.69  done
    1.70  
    1.71 -lemma rconf_In2 [simp]: 
    1.72 - "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.73 +lemma rconf_In2_no_LVar [simp]: 
    1.74 + "\<forall> n. va\<noteq>LVar n \<Longrightarrow> 
    1.75 +   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.76  apply (unfold rconf_def)
    1.77 -apply (simp (no_asm))
    1.78 +apply auto
    1.79  done
    1.80  
    1.81 +lemma rconf_In2_LVar [simp]: 
    1.82 + "va=LVar n \<Longrightarrow> 
    1.83 +   G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  
    1.84 +    = ((fst vf = the (locals s n)) \<and>
    1.85 +       (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst vf\<Colon>\<preceq>T) \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
    1.86 +apply (unfold rconf_def)
    1.87 +by simp
    1.88 +
    1.89  lemma rconf_In3 [simp]: 
    1.90   "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.91  apply (unfold rconf_def)
    1.92 @@ -222,13 +258,6 @@
    1.93  apply (auto intro!: oconf_init_obj_lemma unique_fields)
    1.94  done
    1.95  
    1.96 -(*
    1.97 -lemma obj_split: "P obj = (\<forall> oi vs. obj = \<lparr>tag=oi,values=vs\<rparr> \<longrightarrow> ?P \<lparr>tag=oi,values=vs\<rparr>)"
    1.98 -apply auto
    1.99 -apply (case_tac "obj")
   1.100 -apply auto
   1.101 -*)
   1.102 -
   1.103  lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
   1.104    wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   1.105                          | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   1.106 @@ -272,9 +301,14 @@
   1.107  done
   1.108  
   1.109  lemma sxalloc_type_sound: 
   1.110 - "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> case fst s1 of  
   1.111 -  None \<Rightarrow> s2 = s1 | Some x \<Rightarrow>  
   1.112 -  (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))"
   1.113 + "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> 
   1.114 +  case fst s1 of  
   1.115 +    None \<Rightarrow> s2 = s1 
   1.116 +  | Some abr \<Rightarrow> (case abr of
   1.117 +                   Xcpt x \<Rightarrow> (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> 
   1.118 +                                  (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))
   1.119 +                 | Jump j \<Rightarrow> s2 = s1
   1.120 +                 | Error e \<Rightarrow> s2 = s1)"
   1.121  apply (simp (no_asm_simp) only: split_tupled_all)
   1.122  apply (erule sxalloc.induct)
   1.123  apply   auto
   1.124 @@ -555,7 +589,43 @@
   1.125           eq_declC_sm_dm eq_mheads static
   1.126      show ?thesis by auto
   1.127    qed
   1.128 -qed   
   1.129 +qed
   1.130 +
   1.131 +corollary DynT_mheadsE [consumes 7]: 
   1.132 +--{* Same as @{text DynT_mheadsD} but better suited for application in 
   1.133 +typesafety proof   *}
   1.134 + assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
   1.135 +     and wf: "wf_prog G" 
   1.136 +     and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   1.137 +     and mheads: "(statDeclT,sm) \<in> mheads G C statT sig"
   1.138 +     and mode: "mode=invmode sm e" 
   1.139 +     and invC: "invC = invocation_class mode s a' statT"
   1.140 +     and declC: "declC =invocation_declclass G mode s a' statT sig"
   1.141 +     and dm: "\<And> dm. \<lbrakk>methd G declC sig = Some dm; 
   1.142 +                      dynlookup G statT invC sig = Some dm; 
   1.143 +                      G\<turnstile>resTy (mthd dm)\<preceq>resTy sm; 
   1.144 +                      wf_mdecl G declC (sig, mthd dm);
   1.145 +                      declC = declclass dm;
   1.146 +                      is_static dm = is_static sm;  
   1.147 +                      is_class G invC; is_class G declC; G\<turnstile>invC\<preceq>\<^sub>C declC;  
   1.148 +                      (if invmode sm e = IntVir
   1.149 +                      then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   1.150 +                      else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   1.151 +                             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and>
   1.152 +                             statDeclT = ClassT (declclass dm))\<rbrakk> \<Longrightarrow> P"
   1.153 +   shows "P"
   1.154 +proof -
   1.155 +    from invC_compatible mode have "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" by simp 
   1.156 +    moreover note wf wt_e mheads
   1.157 +    moreover from invC mode 
   1.158 +    have "invC = invocation_class (invmode sm e) s a' statT" by simp
   1.159 +    moreover from declC mode 
   1.160 +    have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
   1.161 +    ultimately show ?thesis
   1.162 +      by (rule DynT_mheadsD [THEN exE,rule_format])
   1.163 +         (elim conjE,rule dm)
   1.164 +qed
   1.165 +   
   1.166  
   1.167  lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
   1.168   isrtype G (statT);
   1.169 @@ -605,9 +675,10 @@
   1.170  done
   1.171  
   1.172  lemma Fin_lemma: 
   1.173 -"\<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.174 +"\<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);
   1.175 +  dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
   1.176  \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   1.177 -apply (force elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   1.178 +apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   1.179  done
   1.180  
   1.181  lemma FVar_lemma1: 
   1.182 @@ -634,8 +705,6 @@
   1.183  apply clarsimp
   1.184  apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   1.185  apply (auto dest!: widen_Array split add: obj_tag.split)
   1.186 -apply (rotate_tac -1) (* to front: tag obja = CInst pid_field_type to enable
   1.187 -                         conditional rewrite *)
   1.188  apply (rule fields_table_SomeI)
   1.189  apply (auto elim!: fields_mono subcls_is_class2)
   1.190  done
   1.191 @@ -750,17 +819,17 @@
   1.192           intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
   1.193  done
   1.194  
   1.195 +
   1.196  section "Call"
   1.197  
   1.198  lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   1.199 -  wf_mhead G P sig mh; 
   1.200 -  Ball (set lvars) (split (\<lambda>vn. is_type G)); 
   1.201 +  wf_mhead G P sig mh;
   1.202    list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   1.203 -  G,s\<turnstile>init_vals (table_of lvars)(pars mh[\<mapsto>]pvs)
   1.204 -      [\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   1.205 +  G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
   1.206 +      [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   1.207  apply (unfold wf_mhead_def)
   1.208  apply clarify
   1.209 -apply (erule (2) Ball_set_table [THEN lconf_init_vals, THEN lconf_ext_list])
   1.210 +apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
   1.211  apply (drule wf_ws_prog)
   1.212  apply (erule (2) conf_list_widen)
   1.213  done
   1.214 @@ -771,9 +840,15 @@
   1.215     =
   1.216    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.217  apply (unfold lconf_def)
   1.218 -apply safe
   1.219 -apply (case_tac "n")
   1.220 -apply (force split add: lname.split)+
   1.221 +apply (auto split add: lname.splits)
   1.222 +done
   1.223 +
   1.224 +lemma wlconf_map_lname [simp]: 
   1.225 +  "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
   1.226 +   =
   1.227 +  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.228 +apply (unfold wlconf_def)
   1.229 +apply (auto split add: lname.splits)
   1.230  done
   1.231  
   1.232  lemma lconf_map_ename [simp]:
   1.233 @@ -781,10 +856,18 @@
   1.234     =
   1.235    (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.236  apply (unfold lconf_def)
   1.237 -apply safe
   1.238 -apply (force split add: ename.split)+
   1.239 +apply (auto split add: ename.splits)
   1.240  done
   1.241  
   1.242 +lemma wlconf_map_ename [simp]:
   1.243 +  "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
   1.244 +   =
   1.245 +  (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   1.246 +apply (unfold wlconf_def)
   1.247 +apply (auto split add: ename.splits)
   1.248 +done
   1.249 +
   1.250 +
   1.251  
   1.252  lemma defval_conf1 [rule_format (no_asm), elim]: 
   1.253    "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
   1.254 @@ -793,6 +876,9 @@
   1.255  apply (auto intro: prim_ty.induct)
   1.256  done
   1.257  
   1.258 +lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
   1.259 +by (auto simp add: abrupt_if_def)
   1.260 +
   1.261  declare split_paired_All [simp del] split_paired_Ex [simp del] 
   1.262  declare split_if     [split del] split_if_asm     [split del] 
   1.263          option.split [split del] option.split_asm [split del]
   1.264 @@ -814,8 +900,7 @@
   1.265      \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
   1.266    invC  = invocation_class (invmode (mhd sm) e) s a' statT;
   1.267    declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
   1.268 -  Ball (set (lcls (mbody (mthd dm)))) 
   1.269 -       (split (\<lambda>vn. is_type G)) 
   1.270 +  x\<noteq>Some (Jump Ret) 
   1.271   \<rbrakk> \<Longrightarrow>  
   1.272    init_lvars G declC sig (invmode (mhd sm) e) a'  
   1.273    pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
   1.274 @@ -833,14 +918,20 @@
   1.275  apply (drule  (4) DynT_conf)
   1.276  apply clarsimp
   1.277  (* apply intro *)
   1.278 -apply (drule (4) conforms_init_lvars_lemma)
   1.279 +apply (drule (3) conforms_init_lvars_lemma 
   1.280 +                 [where ?lvars="(lcls (mbody (mthd dm)))"])
   1.281  apply (case_tac "dm",simp)
   1.282  apply (rule conjI)
   1.283 -apply (unfold lconf_def, clarify)
   1.284 -apply (rule defval_conf1)
   1.285 -apply (clarsimp simp add: wf_mhead_def is_acc_type_def)
   1.286 -apply (case_tac "is_static sm")
   1.287 -apply simp_all
   1.288 +apply (unfold wlconf_def, clarify)
   1.289 +apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
   1.290 +apply   (case_tac "is_static sm")
   1.291 +apply     simp
   1.292 +apply     simp
   1.293 +
   1.294 +apply   simp
   1.295 +apply   (case_tac "is_static sm")
   1.296 +apply     simp
   1.297 +apply     (simp add: np_no_jump)
   1.298  done
   1.299  declare split_paired_All [simp] split_paired_Ex [simp] 
   1.300  declare split_if     [split] split_if_asm     [split] 
   1.301 @@ -851,7 +942,6 @@
   1.302  *}
   1.303  
   1.304  
   1.305 -
   1.306  subsection "accessibility"
   1.307  
   1.308  text {* 
   1.309 @@ -859,7 +949,6 @@
   1.310  *} (* dummy text command to break paragraph for latex;
   1.311                large paragraphs exhaust memory of debian pdflatex *)
   1.312  
   1.313 -(* #### stat raus und gleich is_static f schreiben *) 
   1.314  theorem dynamic_field_access_ok:
   1.315    assumes wf: "wf_prog G" and
   1.316      not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   1.317 @@ -871,8 +960,8 @@
   1.318          dynC: "if stat then dynC=declclass f  
   1.319                         else dynC=obj_class (lookup_obj (store s) a)" and
   1.320          stat: "if stat then (is_static f) else (\<not> is_static f)"
   1.321 -  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   1.322 -     G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.323 +  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<and>
   1.324 +         G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.325  proof (cases "stat")
   1.326    case True
   1.327    with stat have static: "(is_static f)" by simp
   1.328 @@ -914,112 +1003,6 @@
   1.329      by blast
   1.330  qed
   1.331  
   1.332 -(*
   1.333 -theorem dynamic_field_access_ok:
   1.334 -  (assumes wf: "wf_prog G" and
   1.335 -     not_Null: "\<not> is_static f \<longrightarrow> a\<noteq>Null" and
   1.336 -    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   1.337 -    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   1.338 -     normal_s: "normal s" and
   1.339 -         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   1.340 -            f: "accfield G accC statC fn = Some f" and
   1.341 -         dynC: "if is_static f 
   1.342 -                   then dynC=declclass f  
   1.343 -                   else dynC=obj_class (lookup_obj (store s) a)" 
   1.344 -  ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
   1.345 -     G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.346 -proof (cases "is_static f")
   1.347 -  case True
   1.348 -  from True dynC 
   1.349 -  have dynC': "dynC=declclass f" by simp
   1.350 -  with f
   1.351 -  have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   1.352 -    by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   1.353 -  moreover
   1.354 -  from wt_e wf have "is_class G statC"
   1.355 -    by (auto dest!: ty_expr_is_type)
   1.356 -  moreover note wf dynC'
   1.357 -  ultimately have
   1.358 -     "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   1.359 -    by (auto dest: fields_declC)
   1.360 -  with dynC' f True wf
   1.361 -  show ?thesis
   1.362 -    by (auto dest: static_to_dynamic_accessible_from_static
   1.363 -            dest!: accfield_accessibleD )
   1.364 -next
   1.365 -  case False
   1.366 -  with wf conform_a not_Null conform_s dynC
   1.367 -  obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   1.368 -    "is_class G dynC"
   1.369 -    by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   1.370 -              dest: obj_ty_obj_class1
   1.371 -          simp add: obj_ty_obj_class )
   1.372 -  with wf f
   1.373 -  have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   1.374 -    by (auto simp add: accfield_def Let_def
   1.375 -                 dest: fields_mono
   1.376 -                dest!: table_of_remap_SomeD)
   1.377 -  moreover
   1.378 -  from f subclseq
   1.379 -  have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   1.380 -    by (auto intro!: static_to_dynamic_accessible_from 
   1.381 -               dest: accfield_accessibleD)
   1.382 -  ultimately show ?thesis
   1.383 -    by blast
   1.384 -qed
   1.385 -*)
   1.386 -
   1.387 -
   1.388 -(* ### Einsetzen in case FVar des TypeSoundness Proofs *)
   1.389 -(*
   1.390 -lemma FVar_check_error_free:
   1.391 -(assumes fvar: "(v, s2') = fvar statDeclC stat fn a s2" and 
   1.392 -        check: "s3 = check_field_access G accC statDeclC fn stat a s2'" and
   1.393 -       conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
   1.394 -      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   1.395 -    initd_statDeclC_s2: "initd statDeclC s2" and
   1.396 -    wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   1.397 -    accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   1.398 -    stat: "stat=is_static f" and
   1.399 -      wf: "wf_prog G"
   1.400 -)  "s3=s2'"
   1.401 -proof -
   1.402 -  from fvar 
   1.403 -  have store_s2': "store s2'=store s2"
   1.404 -    by (cases s2) (simp add: fvar_def2)
   1.405 -  with fvar conf_s2 
   1.406 -  have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
   1.407 -    by (cases s2,cases stat) (auto simp add: fvar_def2)
   1.408 -  from initd_statDeclC_s2 store_s2' 
   1.409 -  have initd_statDeclC_s2': "initd statDeclC s2"
   1.410 -    by simp
   1.411 -  show ?thesis
   1.412 -  proof (cases "normal s2'")
   1.413 -    case False
   1.414 -    with check show ?thesis 
   1.415 -      by (auto simp add: check_field_access_def Let_def)
   1.416 -  next
   1.417 -    case True
   1.418 -    with fvar store_s2' 
   1.419 -    have not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" 
   1.420 -      by (cases s2) (auto simp add: fvar_def2)
   1.421 -    from True fvar store_s2'
   1.422 -    have "normal s2"
   1.423 -      by (cases s2,cases stat) (auto simp add: fvar_def2)
   1.424 -    with conf_a store_s2'
   1.425 -    have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
   1.426 -      by simp 
   1.427 -    from conf_a' conf_s2'  check True initd_statDeclC_s2' 
   1.428 -      dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
   1.429 -                                   True wt_e accfield ] stat
   1.430 -    show ?thesis
   1.431 -      by (cases stat)
   1.432 -         (auto dest!: initedD
   1.433 -           simp add: check_field_access_def Let_def)
   1.434 -  qed
   1.435 -qed
   1.436 -*)
   1.437 -
   1.438  lemma error_free_field_access:
   1.439    assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
   1.440                wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   1.441 @@ -1199,26 +1182,581 @@
   1.442    qed
   1.443  qed
   1.444  
   1.445 +lemma map_upds_eq_length_append_simp:
   1.446 +  "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
   1.447 +proof (induct ps) 
   1.448 +  case Nil thus ?case by simp
   1.449 +next
   1.450 +  case (Cons p ps tab qs)
   1.451 +  have "length (p#ps) = length qs" .
   1.452 +  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
   1.453 +    by (cases qs) auto
   1.454 +  from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
   1.455 +    by (rule Cons.hyps)
   1.456 +  with qs show ?case 
   1.457 +    by simp
   1.458 +qed
   1.459 +
   1.460 +lemma map_upds_upd_eq_length_simp:
   1.461 +  "\<And> tab qs x y. length ps = length qs 
   1.462 +                  \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
   1.463 +proof (induct "ps")
   1.464 +  case Nil thus ?case by simp
   1.465 +next
   1.466 +  case (Cons p ps tab qs x y)
   1.467 +  have "length (p#ps) = length qs" .
   1.468 +  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
   1.469 +    by (cases qs) auto
   1.470 +  from eq_length 
   1.471 +  have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
   1.472 +    by (rule Cons.hyps)
   1.473 +  with qs show ?case
   1.474 +    by simp
   1.475 +qed
   1.476 +
   1.477 +
   1.478 +lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
   1.479 +by simp
   1.480 +
   1.481 +lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) z"
   1.482 +by (simp add: fun_upd_def)
   1.483 +
   1.484 +lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
   1.485 +by (cases xs) simp+
   1.486 +
   1.487 +lemma map_upds_cong_ext: 
   1.488 + "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) z"
   1.489 +proof (induct xs)
   1.490 +  case Nil thus ?case by simp
   1.491 +next
   1.492 +  case (Cons x xs tab tab' ys)
   1.493 +  have "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) z"
   1.494 +    by (rule Cons.hyps) (rule map_upd_cong_ext)
   1.495 +  thus ?case
   1.496 +    by simp
   1.497 +qed
   1.498 +   
   1.499 +lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
   1.500 +  by simp
   1.501 +
   1.502 +
   1.503 +lemma map_upds_override_cong:
   1.504 +"\<And> tab tab' zs. x\<in> set ws \<Longrightarrow> 
   1.505 + (tab(ws[\<mapsto>]zs)) x = (tab'(ws[\<mapsto>]zs)) x"
   1.506 +proof (induct ws)
   1.507 +  case Nil thus ?case by simp
   1.508 +next
   1.509 +  case (Cons w ws tab tab' zs)
   1.510 +  have x: "x \<in> set (w#ws)" .
   1.511 +  show ?case
   1.512 +  proof (cases "x=w")
   1.513 +    case True thus ?thesis
   1.514 +      by simp (rule map_upds_cong_ext, rule map_upd_override)
   1.515 +  next
   1.516 +    case False
   1.517 +    with x have "x \<in> set ws"
   1.518 +      by simp
   1.519 +    with Cons.hyps show ?thesis
   1.520 +      by simp
   1.521 +  qed
   1.522 +qed
   1.523 +
   1.524 +lemma map_upds_in_suffix: assumes x: "x \<in> set xs" 
   1.525 + shows "\<And> tab qs. (tab(ps @ xs[\<mapsto>]qs)) x = (tab(xs[\<mapsto>]drop (length ps) qs)) x"
   1.526 +proof (induct ps)
   1.527 +  case Nil thus ?case by simp
   1.528 +next
   1.529 +  case (Cons p ps tab qs)
   1.530 +  have "(tab(p\<mapsto>hd qs)(ps @ xs[\<mapsto>](tl qs))) x
   1.531 +          =(tab(p\<mapsto>hd qs)(xs[\<mapsto>]drop (length ps) (tl qs))) x"
   1.532 +    by (rule Cons.hyps)
   1.533 +  moreover
   1.534 +  have "drop (Suc (length ps)) qs=drop (length ps) (tl qs)"
   1.535 +    by (cases qs) simp+
   1.536 +  ultimately show ?case
   1.537 +    by simp (rule map_upds_override_cong)
   1.538 +qed
   1.539 + 
   1.540 +
   1.541 +lemma map_upds_eq_length_suffix: "\<And> tab qs. 
   1.542 +        length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
   1.543 +proof (induct ps)
   1.544 +  case Nil thus ?case by simp
   1.545 +next
   1.546 +  case (Cons p ps tab qs)
   1.547 +  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
   1.548 +    by (cases qs) auto
   1.549 +  from eq_length
   1.550 +  have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
   1.551 +    by (rule Cons.hyps)
   1.552 +  with qs show ?case 
   1.553 +    by simp
   1.554 +qed
   1.555 +  
   1.556 +  
   1.557 +lemma map_upds_upds_eq_length_prefix_simp:
   1.558 +  "\<And> tab qs. length ps = length qs
   1.559 +              \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
   1.560 +proof (induct ps)
   1.561 +  case Nil thus ?case by simp
   1.562 +next
   1.563 +  case (Cons p ps tab qs)
   1.564 +  then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
   1.565 +    by (cases qs) auto
   1.566 +  from eq_length 
   1.567 +  have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
   1.568 +    by (rule Cons.hyps)
   1.569 +  with qs 
   1.570 +  show ?case by simp
   1.571 +qed
   1.572 +
   1.573 +lemma map_upd_cut_irrelevant:
   1.574 +"\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<rbrakk>
   1.575 +    \<Longrightarrow> tab vn = Some el"
   1.576 +by (cases "tab' vn = None") (simp add: fun_upd_def)+
   1.577 +
   1.578 +lemma map_upd_Some_expand:
   1.579 +"\<lbrakk>tab vn = Some z\<rbrakk>
   1.580 +    \<Longrightarrow> \<exists> z. (tab(x\<mapsto>y)) vn = Some z"
   1.581 +by (simp add: fun_upd_def)
   1.582 +
   1.583 +lemma map_upds_Some_expand:
   1.584 +"\<And> tab ys z. \<lbrakk>tab vn = Some z\<rbrakk>
   1.585 +    \<Longrightarrow> \<exists> z. (tab(xs[\<mapsto>]ys)) vn = Some z"
   1.586 +proof (induct xs)
   1.587 +  case Nil thus ?case by simp
   1.588 +next
   1.589 +  case (Cons x xs tab ys z)
   1.590 +  have "tab vn = Some z" .
   1.591 +  then obtain z' where "(tab(x\<mapsto>hd ys)) vn = Some z'" 
   1.592 +    by (rule map_upd_Some_expand [of tab,elim_format]) blast
   1.593 +  hence "\<exists> z. (tab (x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
   1.594 +    by (rule Cons.hyps)
   1.595 +  thus ?case
   1.596 +    by simp
   1.597 +qed
   1.598 +
   1.599 +
   1.600 +lemma map_upd_Some_swap:
   1.601 + "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
   1.602 +by (simp add: fun_upd_def)
   1.603 +
   1.604 +lemma map_upd_None_swap:
   1.605 + "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
   1.606 +by (simp add: fun_upd_def)
   1.607 +
   1.608 +
   1.609 +lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
   1.610 +by (simp add: fun_upd_def)
   1.611 +
   1.612 +lemma map_eq_upds_eq: 
   1.613 +  "\<And> tab tab' ys. 
   1.614 +   tab vn = tab' vn \<Longrightarrow> (tab(xs[\<mapsto>]ys)) vn = (tab'(xs[\<mapsto>]ys)) vn"
   1.615 +proof (induct xs)
   1.616 +  case Nil thus ?case by simp 
   1.617 +next
   1.618 +  case (Cons x xs tab tab' ys)
   1.619 +  have "tab vn = tab' vn" .
   1.620 +  hence "(tab(x\<mapsto>hd ys)) vn = (tab'(x\<mapsto>hd ys)) vn"
   1.621 +    by (rule map_eq_upd_eq)
   1.622 +  hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   1.623 +    by (rule Cons.hyps)
   1.624 +  thus ?case 
   1.625 +    by simp
   1.626 +qed
   1.627 +
   1.628 +lemma map_upd_in_expansion_map_swap:
   1.629 + "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
   1.630 +                 \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
   1.631 +by (simp add: fun_upd_def)
   1.632 +
   1.633 +lemma map_upds_in_expansion_map_swap:
   1.634 + "\<And>tab tab' ys z. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
   1.635 +                 \<Longrightarrow>  (tab'(xs[\<mapsto>]ys)) vn = Some z"
   1.636 +proof (induct xs)
   1.637 +  case Nil thus ?case by simp
   1.638 +next
   1.639 +  case (Cons x xs tab tab' ys z)
   1.640 +  from Cons.prems obtain 
   1.641 +    some: "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z" and
   1.642 +    tab_not_z: "tab vn \<noteq> Some z"
   1.643 +    by simp
   1.644 +  show ?case
   1.645 +  proof (cases "(tab(x\<mapsto>hd ys)) vn \<noteq> Some z")
   1.646 +    case True
   1.647 +    with some have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = Some z"
   1.648 +      by (rule Cons.hyps)
   1.649 +    thus ?thesis 
   1.650 +      by simp
   1.651 +  next
   1.652 +    case False
   1.653 +    hence tabx_z: "(tab(x\<mapsto>hd ys)) vn = Some z" by blast
   1.654 +    moreover
   1.655 +    from tabx_z tab_not_z
   1.656 +    have "(tab'(x\<mapsto>hd ys)) vn = Some z" 
   1.657 +      by (rule map_upd_in_expansion_map_swap)
   1.658 +    ultimately
   1.659 +    have "(tab(x\<mapsto>hd ys)) vn =(tab'(x\<mapsto>hd ys)) vn"
   1.660 +      by simp
   1.661 +    hence "(tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = (tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn"
   1.662 +      by (rule map_eq_upds_eq)
   1.663 +    with some 
   1.664 +    show ?thesis 
   1.665 +      by simp
   1.666 +  qed
   1.667 +qed
   1.668 +   
   1.669 +lemma map_upds_Some_swap: 
   1.670 + assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
   1.671 +    shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
   1.672 +proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
   1.673 +  case True
   1.674 +  then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
   1.675 +    by (rule map_upd_Some_swap [elim_format]) blast
   1.676 +  thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
   1.677 +    by (rule map_upds_Some_expand)
   1.678 +next
   1.679 +  case False
   1.680 +  with r_u
   1.681 +  have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
   1.682 +    by (rule map_upds_in_expansion_map_swap)
   1.683 +  thus ?thesis
   1.684 +    by simp
   1.685 +qed
   1.686 + 
   1.687 +lemma map_upds_Some_insert:
   1.688 +  assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
   1.689 +    shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
   1.690 +proof (cases "\<exists> z. tab vn = Some z")
   1.691 +  case True
   1.692 +  then obtain z' where "tab vn = Some z'" by blast
   1.693 +  then obtain z'' where "(tab(u\<mapsto>v)) vn = Some z''"
   1.694 +    by (rule map_upd_Some_expand [elim_format]) blast
   1.695 +  thus ?thesis
   1.696 +    by (rule map_upds_Some_expand)
   1.697 +next
   1.698 +  case False
   1.699 +  hence "tab vn \<noteq> Some z" by simp
   1.700 +  with z
   1.701 +  have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
   1.702 +    by (rule map_upds_in_expansion_map_swap)
   1.703 +  thus ?thesis ..
   1.704 +qed
   1.705 +   
   1.706 +lemma map_upds_None_cut:
   1.707 +assumes expand_None: "(tab(xs[\<mapsto>]ys)) vn = None"
   1.708 +  shows "tab vn = None"
   1.709 +proof (cases "tab vn = None")
   1.710 +  case True thus ?thesis by simp
   1.711 +next
   1.712 +  case False then obtain z where "tab vn = Some z" by blast
   1.713 +  then obtain z' where "(tab(xs[\<mapsto>]ys)) vn = Some z'"
   1.714 +    by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
   1.715 +  with expand_None show ?thesis
   1.716 +    by simp
   1.717 +qed
   1.718 +    
   1.719 +
   1.720 +lemma map_upds_cut_irrelevant:
   1.721 +"\<And> tab tab' ys. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some el; (tab'(xs[\<mapsto>]ys)) vn = None\<rbrakk>
   1.722 +                  \<Longrightarrow> tab vn = Some el"
   1.723 +proof  (induct "xs")
   1.724 +  case Nil thus ?case by simp
   1.725 +next
   1.726 +  case (Cons x xs tab tab' ys)
   1.727 +  from Cons.prems
   1.728 +  have "(tab(x\<mapsto>hd ys)) vn = Some el"
   1.729 +    by - (rule Cons.hyps,auto)
   1.730 +  moreover from Cons.prems 
   1.731 +  have "(tab'(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) vn = None" 
   1.732 +    by simp
   1.733 +  hence "(tab'(x\<mapsto>hd ys)) vn = None"
   1.734 +    by (rule map_upds_None_cut)
   1.735 +  ultimately show "tab vn = Some el" 
   1.736 +    by (rule map_upd_cut_irrelevant)
   1.737 +qed
   1.738 +   
   1.739 +lemma dom_vname_split:
   1.740 + "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
   1.741 +   = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
   1.742 +     dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
   1.743 +  (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
   1.744 +proof 
   1.745 +  show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
   1.746 +  proof 
   1.747 +    fix el 
   1.748 +    assume el_in_list: "el \<in> ?List x xs y ys"
   1.749 +    show "el \<in>  ?Hd x y \<union> ?Tl xs ys"
   1.750 +    proof (cases el)
   1.751 +      case This
   1.752 +      with el_in_list show ?thesis by (simp add: dom_def)
   1.753 +    next
   1.754 +      case (EName en)
   1.755 +      show ?thesis
   1.756 +      proof (cases en)
   1.757 +	case Res
   1.758 +	with EName el_in_list show ?thesis by (simp add: dom_def)
   1.759 +      next
   1.760 +	case (VNam vn)
   1.761 +	with EName el_in_list show ?thesis 
   1.762 +	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
   1.763 +      qed
   1.764 +    qed
   1.765 +  qed
   1.766 +next
   1.767 +  show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
   1.768 +  proof 
   1.769 +    fix el 
   1.770 +    assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
   1.771 +    show "el \<in> ?List x xs y ys"
   1.772 +    proof (cases el)
   1.773 +      case This
   1.774 +      with el_in_hd_tl show ?thesis by (simp add: dom_def)
   1.775 +    next
   1.776 +      case (EName en)
   1.777 +      show ?thesis
   1.778 +      proof (cases en)
   1.779 +	case Res
   1.780 +	with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
   1.781 +      next
   1.782 +	case (VNam vn)
   1.783 +	with EName el_in_hd_tl show ?thesis 
   1.784 +	  by (auto simp add: dom_def intro: map_upds_Some_expand 
   1.785 +                                            map_upds_Some_insert)
   1.786 +      qed
   1.787 +    qed
   1.788 +  qed
   1.789 +qed
   1.790 +
   1.791 +lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
   1.792 +by (auto simp add: dom_def fun_upd_def)
   1.793 +
   1.794 +lemma dom_map_upds: "\<And> tab ys. dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
   1.795 +proof (induct xs)
   1.796 +  case Nil thus ?case by (simp add: dom_def)
   1.797 +next
   1.798 +  case (Cons x xs tab ys)
   1.799 +  have "dom (tab(x\<mapsto>hd ys)(xs[\<mapsto>]tl ys)) = dom (tab(x\<mapsto>hd ys)) \<union> set xs" .
   1.800 +  moreover 
   1.801 +  have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
   1.802 +    by (rule dom_map_upd)
   1.803 +  ultimately
   1.804 +  show ?case
   1.805 +    by simp
   1.806 +qed
   1.807 + 
   1.808 +
   1.809 +
   1.810 +lemma dom_ename_case_None_simp:
   1.811 + "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
   1.812 +  apply (auto simp add: dom_def image_def )
   1.813 +  apply (case_tac "x")
   1.814 +  apply auto
   1.815 +  done
   1.816 +
   1.817 +lemma dom_ename_case_Some_simp:
   1.818 + "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
   1.819 +  apply (auto simp add: dom_def image_def )
   1.820 +  apply (case_tac "x")
   1.821 +  apply auto
   1.822 +  done
   1.823 +
   1.824 +lemma dom_lname_case_None_simp:
   1.825 +  "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
   1.826 +  apply (auto simp add: dom_def image_def )
   1.827 +  apply (case_tac "x")
   1.828 +  apply auto
   1.829 +  done
   1.830 +
   1.831 +lemma dom_lname_case_Some_simp:
   1.832 + "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
   1.833 +  apply (auto simp add: dom_def image_def)
   1.834 +  apply (case_tac "x")
   1.835 +  apply auto
   1.836 +  done
   1.837 +
   1.838 +lemmas dom_lname_ename_case_simps =  
   1.839 +     dom_ename_case_None_simp dom_ename_case_Some_simp 
   1.840 +     dom_lname_case_None_simp dom_lname_case_Some_simp
   1.841 +
   1.842 +lemma image_comp: 
   1.843 + "f ` g ` A = (f \<circ> g) ` A"
   1.844 +by (auto simp add: image_def)
   1.845 +
   1.846 +lemma dom_locals_init_lvars: 
   1.847 +  assumes m: "m=(mthd (the (methd G C sig)))"  
   1.848 +  shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
   1.849 +           = parameters m"
   1.850 +proof -
   1.851 +  from m
   1.852 +  have static_m': "is_static m = static m"
   1.853 +    by simp
   1.854 +  have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
   1.855 +    by (simp add: dom_map_upds)
   1.856 +  show ?thesis
   1.857 +  proof (cases "static m")
   1.858 +    case True
   1.859 +    with static_m' dom_vnames m
   1.860 +    show ?thesis
   1.861 +      by (cases s) (simp add: init_lvars_def Let_def parameters_def
   1.862 +                              dom_lname_ename_case_simps image_comp)
   1.863 +  next
   1.864 +    case False
   1.865 +    with static_m' dom_vnames m
   1.866 +    show ?thesis
   1.867 +      by (cases s) (simp add: init_lvars_def Let_def parameters_def
   1.868 +                              dom_lname_ename_case_simps image_comp)
   1.869 +  qed
   1.870 +qed
   1.871 +
   1.872 +lemma da_e2_BinOp:
   1.873 +  assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.874 +                  \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
   1.875 +    and wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T"
   1.876 +    and wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" 
   1.877 +    and wt_binop: "wt_binop G binop e1T e2T" 
   1.878 +    and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   1.879 +    and normal_s1: "normal s1"
   1.880 +    and	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
   1.881 +    and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
   1.882 +    and wf: "wf_prog G"
   1.883 +  shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
   1.884 +         \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
   1.885 +proof -
   1.886 +  note inj_term_simps [simp]
   1.887 +  from da obtain E1 where
   1.888 +    da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
   1.889 +    by cases simp+
   1.890 +  obtain E2 where
   1.891 +    "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
   1.892 +      \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
   1.893 +  proof (cases "need_second_arg binop v1")
   1.894 +    case False
   1.895 +    obtain S where
   1.896 +      daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.897 +                  \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>Skip\<rangle>\<^sub>s\<guillemotright> S"
   1.898 +      by (auto intro: da_Skip [simplified] assigned.select_convs)
   1.899 +    thus ?thesis
   1.900 +      using that by (simp add: False)
   1.901 +  next
   1.902 +    case True
   1.903 +    from eval_e1 have 
   1.904 +      s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
   1.905 +      by (rule dom_locals_eval_mono_elim)
   1.906 +    {
   1.907 +      assume condAnd: "binop=CondAnd"
   1.908 +      have ?thesis
   1.909 +      proof -
   1.910 +	from da obtain E2' where
   1.911 +	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.912 +             \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
   1.913 +	  by cases (simp add: condAnd)+
   1.914 +	moreover
   1.915 +	have "dom (locals (store s0)) 
   1.916 +          \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
   1.917 +	proof -
   1.918 +	  from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
   1.919 +	    by simp
   1.920 +	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.921 +	    by (auto dest: conf_Boolean)
   1.922 +	  with True condAnd
   1.923 +	  have v1: "v1=Bool True"
   1.924 +	    by simp
   1.925 +	  from eval_e1 normal_s1 
   1.926 +	  have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
   1.927 +	    by (rule assigns_if_good_approx' [elim_format])
   1.928 +	       (insert wt_e1, simp_all add: e1T v1)
   1.929 +	  with s0_s1 show ?thesis by (rule Un_least)
   1.930 +	qed
   1.931 +	ultimately
   1.932 +	show ?thesis
   1.933 +	  using that by (cases rule: da_weakenE) (simp add: True)
   1.934 +      qed
   1.935 +    }
   1.936 +    moreover
   1.937 +    { 
   1.938 +      assume condOr: "binop=CondOr"
   1.939 +      have ?thesis
   1.940 +	(* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
   1.941 +      proof -
   1.942 +	from da obtain E2' where
   1.943 +	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.944 +              \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
   1.945 +	  by cases (simp add: condOr)+
   1.946 +	moreover
   1.947 +	have "dom (locals (store s0)) 
   1.948 +                     \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
   1.949 +	proof -
   1.950 +	  from condOr wt_binop have e1T: "e1T=PrimT Boolean"
   1.951 +	    by simp
   1.952 +	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.953 +	    by (auto dest: conf_Boolean)
   1.954 +	  with True condOr
   1.955 +	  have v1: "v1=Bool False"
   1.956 +	    by simp
   1.957 +	  from eval_e1 normal_s1 
   1.958 +	  have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
   1.959 +	    by (rule assigns_if_good_approx' [elim_format])
   1.960 +	       (insert wt_e1, simp_all add: e1T v1)
   1.961 +	  with s0_s1 show ?thesis by (rule Un_least)
   1.962 +	qed
   1.963 +	ultimately
   1.964 +	show ?thesis
   1.965 +	  using that by (rule da_weakenE) (simp add: True)
   1.966 +      qed
   1.967 +    }
   1.968 +    moreover
   1.969 +    {
   1.970 +      assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
   1.971 +      have ?thesis
   1.972 +      proof -
   1.973 +	from da notAndOr obtain E1' where
   1.974 +          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.975 +                  \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
   1.976 +	  and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
   1.977 +	  by cases simp+
   1.978 +	from eval_e1 wt_e1 da_e1 wf normal_s1 
   1.979 +	have "nrm E1' \<subseteq> dom (locals (store s1))"
   1.980 +	  by (cases rule: da_good_approxE') rules
   1.981 +	with da_e2 show ?thesis
   1.982 +	  using that by (rule da_weakenE) (simp add: True)
   1.983 +      qed
   1.984 +    }
   1.985 +    ultimately show ?thesis
   1.986 +      by (cases binop) auto
   1.987 +  qed
   1.988 +  thus ?thesis ..
   1.989 +qed
   1.990 +
   1.991  section "main proof of type safety"
   1.992 -
   1.993 +    
   1.994  lemma eval_type_sound:
   1.995 -  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
   1.996 -            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
   1.997 -            wf: "wf_prog G" and 
   1.998 -       conf_s0: "s0\<Colon>\<preceq>(G,L)"           
   1.999 +  assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1.1000 +   and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  1.1001 +   and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  1.1002 +   and      wf: "wf_prog G" 
  1.1003 +   and conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1.1004    shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1.1005           (error_free s0 = error_free s1)"
  1.1006  proof -
  1.1007 +  note inj_term_simps [simp]
  1.1008 +  let ?TypeSafeObj = "\<lambda> s0 s1 t v. 
  1.1009 +          \<forall>  L accC T A. s0\<Colon>\<preceq>(G,L) \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T
  1.1010 +                      \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A  
  1.1011 +                      \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1.1012 +                          \<and> (error_free s0 = error_free s1)"
  1.1013    from eval 
  1.1014 -  have "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>  
  1.1015 +  have "\<And> L accC T A. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  1.1016 +                      \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  1.1017          \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1.1018              \<and> (error_free s0 = error_free s1)"
  1.1019     (is "PROP ?TypeSafe s0 s1 t v"
  1.1020 -    is "\<And> L accC T. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1.1021 +    is "\<And> L accC T A. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1.1022 +                 \<Longrightarrow> ?DefAss L accC s0 t A 
  1.1023                   \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1.1024                       ?ErrorFree s0 s1")
  1.1025    proof (induct)
  1.1026 -    case (Abrupt s t xc L accC T) 
  1.1027 +    case (Abrupt s t xc L accC T A) 
  1.1028      have "(Some xc, s)\<Colon>\<preceq>(G,L)" .
  1.1029      then show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1.1030        (normal (Some xc, s) 
  1.1031 @@ -1226,7 +1764,7 @@
  1.1032        (error_free (Some xc, s) = error_free (Some xc, s))"
  1.1033        by (simp)
  1.1034    next
  1.1035 -    case (Skip s L accC T)
  1.1036 +    case (Skip s L accC T A)
  1.1037      have "Norm s\<Colon>\<preceq>(G, L)" and  
  1.1038             "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T" .
  1.1039      then show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1.1040 @@ -1234,33 +1772,42 @@
  1.1041                (error_free (Norm s) = error_free (Norm s))"
  1.1042        by (simp)
  1.1043    next
  1.1044 -    case (Expr e s0 s1 v L accC T)
  1.1045 +    case (Expr e s0 s1 v L accC T A)
  1.1046      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1.1047      have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1.1048      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1049 +    moreover
  1.1050      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T" .
  1.1051      then obtain eT 
  1.1052        where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1.1053        by (rule wt_elim_cases) (blast)
  1.1054 -    with conf_s0 hyp 
  1.1055 +    moreover
  1.1056 +    from Expr.prems obtain E where
  1.1057 +      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
  1.1058 +      by (elim da_elim_cases) simp
  1.1059 +    ultimately 
  1.1060      obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1.1061 -      by (blast)
  1.1062 +      by (rule hyp [elim_format]) simp
  1.1063      with wt
  1.1064      show "s1\<Colon>\<preceq>(G, L) \<and>
  1.1065            (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1.1066            (error_free (Norm s0) = error_free s1)"
  1.1067        by (simp)
  1.1068    next
  1.1069 -    case (Lab c l s0 s1 L accC T)
  1.1070 +    case (Lab c l s0 s1 L accC T A)
  1.1071      have     hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>" .
  1.1072      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1073 +    moreover
  1.1074      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T" .
  1.1075      then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1.1076        by (rule wt_elim_cases) (blast)
  1.1077 -    with conf_s0 hyp
  1.1078 +    moreover from Lab.prems obtain C where
  1.1079 +     "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
  1.1080 +      by (elim da_elim_cases) simp
  1.1081 +    ultimately
  1.1082      obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1.1083             error_free_s1: "error_free s1" 
  1.1084 -      by (blast)
  1.1085 +      by (rule hyp [elim_format]) simp
  1.1086      from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
  1.1087        by (cases s1) (auto intro: conforms_absorb)
  1.1088      with wt error_free_s1
  1.1089 @@ -1270,9 +1817,9 @@
  1.1090            (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
  1.1091        by (simp)
  1.1092    next
  1.1093 -    case (Comp c1 c2 s0 s1 s2 L accC T)
  1.1094 -    have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1095 -    have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1.1096 +    case (Comp c1 c2 s0 s1 s2 L accC T A)
  1.1097 +    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1098 +    have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1.1099      have  hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1.1100      have  hyp_c2: "PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>" .
  1.1101      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1102 @@ -1280,91 +1827,263 @@
  1.1103      then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1104                  wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1.1105        by (rule wt_elim_cases) (blast)
  1.1106 -    with conf_s0 hyp_c1 hyp_c2
  1.1107 -    obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1.1108 -      by (blast)
  1.1109 -    with wt
  1.1110 +    from Comp.prems
  1.1111 +    obtain C1 C2
  1.1112 +      where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  1.1113 +                      dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and 
  1.1114 +            da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>In1r c2\<guillemotright> C2" 
  1.1115 +      by (elim da_elim_cases) simp
  1.1116 +    from conf_s0 wt_c1 da_c1
  1.1117 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1.1118 +           error_free_s1: "error_free s1"
  1.1119 +      by (rule hyp_c1 [elim_format]) simp
  1.1120      show "s2\<Colon>\<preceq>(G, L) \<and>
  1.1121            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1.1122            (error_free (Norm s0) = error_free s2)"
  1.1123 -      by (simp)
  1.1124 +    proof (cases "normal s1")
  1.1125 +      case False
  1.1126 +      with eval_c2 have "s2=s1" by auto
  1.1127 +      with conf_s1 error_free_s1 False wt show ?thesis
  1.1128 +	by simp
  1.1129 +    next
  1.1130 +      case True
  1.1131 +      obtain C2' where 
  1.1132 +	"\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
  1.1133 +      proof -
  1.1134 +	from eval_c1 wt_c1 da_c1 wf True
  1.1135 +	have "nrm C1 \<subseteq> dom (locals (store s1))"
  1.1136 +	  by (cases rule: da_good_approxE') rules
  1.1137 +	with da_c2 show ?thesis
  1.1138 +	  by (rule da_weakenE)
  1.1139 +      qed
  1.1140 +      with conf_s1 wt_c2 
  1.1141 +      obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1.1142 +	by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
  1.1143 +      thus ?thesis
  1.1144 +	using wt by simp
  1.1145 +    qed
  1.1146    next
  1.1147      case (If b c1 c2 e s0 s1 s2 L accC T)
  1.1148 -    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1.1149 -    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1.1150 +    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1.1151 +    have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1.1152      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1.1153      have hyp_then_else: 
  1.1154              "PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
  1.1155      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1156      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
  1.1157 -    then obtain "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
  1.1158 -                "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1.1159 +    then obtain 
  1.1160 +              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1.1161 +      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1.1162 +      (*
  1.1163 +                wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1164 +                wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
  1.1165        by (rule wt_elim_cases) (auto split add: split_if)
  1.1166 -    with conf_s0 hyp_e hyp_then_else
  1.1167 -    obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1.1168 -      by (blast)
  1.1169 -    with wt
  1.1170 +    from If.prems obtain E C where
  1.1171 +      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  1.1172 +                                       \<guillemotright>In1l e\<guillemotright> E" and
  1.1173 +      da_then_else: 
  1.1174 +      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.1175 +         (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  1.1176 +          \<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C"
  1.1177 +     (*
  1.1178 +     da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1.1179 +                                      \<union> assigns_if True e) \<guillemotright>In1r c1\<guillemotright> C1" and
  1.1180 +     da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1.1181 +                                       \<union> assigns_if False e) \<guillemotright>In1r c2\<guillemotright> C2" *)
  1.1182 +      by (elim da_elim_cases) (cases "the_Bool b",auto)
  1.1183 +    from conf_s0 wt_e da_e  
  1.1184 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1185 +      by (rule hyp_e [elim_format]) simp
  1.1186      show "s2\<Colon>\<preceq>(G, L) \<and>
  1.1187             (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1.1188             (error_free (Norm s0) = error_free s2)"
  1.1189 -      by (simp)
  1.1190 +    proof (cases "normal s1")
  1.1191 +      case False
  1.1192 +      with eval_then_else have "s2=s1" by auto
  1.1193 +      with conf_s1 error_free_s1 False wt show ?thesis
  1.1194 +	by simp
  1.1195 +    next
  1.1196 +      case True
  1.1197 +      obtain C' where
  1.1198 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.1199 +          (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
  1.1200 +      proof -
  1.1201 +	from eval_e have 
  1.1202 +	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.1203 +	  by (rule dom_locals_eval_mono_elim)
  1.1204 +        moreover
  1.1205 +	from eval_e True wt_e 
  1.1206 +	have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.1207 +	  by (rule assigns_if_good_approx')
  1.1208 +	ultimately 
  1.1209 +	have "dom (locals (store ((Norm s0)::state))) 
  1.1210 +                \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.1211 +	  by (rule Un_least)
  1.1212 +	with da_then_else show ?thesis
  1.1213 +	  by (rule da_weakenE)
  1.1214 +      qed
  1.1215 +      with conf_s1 wt_then_else  
  1.1216 +      obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1.1217 +	by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
  1.1218 +      with wt show ?thesis
  1.1219 +	by simp
  1.1220 +    qed
  1.1221 +    -- {* Note that we don't have to show that @{term b} really is a boolean 
  1.1222 +          value. With @{term the_Bool} we enforce to get a value of boolean 
  1.1223 +          type. So execution will be type safe, even if b would be
  1.1224 +          a string, for example. We might not expect such a behaviour to be
  1.1225 +          called type safe. To remedy the situation we would have to change
  1.1226 +          the evaulation rule, so that it only has a type safe evaluation if
  1.1227 +          we actually get a boolean value for the condition. That b is actually
  1.1228 +          a boolean value is part of @{term hyp_e}. See also Loop 
  1.1229 +       *}
  1.1230    next
  1.1231 -    case (Loop b c e l s0 s1 s2 s3 L accC T)
  1.1232 -    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1.1233 +    case (Loop b c e l s0 s1 s2 s3 L accC T A)
  1.1234 +    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1.1235      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
  1.1236      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1237      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1.1238      then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1.1239                  wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1.1240        by (rule wt_elim_cases) (blast)
  1.1241 -    from conf_s0 wt_e hyp_e
  1.1242 +    have da:"\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.1243 +            \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A".
  1.1244 +    then
  1.1245 +    obtain E C where
  1.1246 +      da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.1247 +              \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E" and
  1.1248 +      da_c: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.1249 +              \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1.1250 +                   \<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C" 
  1.1251 +      by (rule da_elim_cases) simp
  1.1252 +    from conf_s0 wt_e da_e 
  1.1253      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1254 -      by blast
  1.1255 +      by (rule hyp_e [elim_format]) simp
  1.1256      show "s3\<Colon>\<preceq>(G, L) \<and>
  1.1257            (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1.1258            (error_free (Norm s0) = error_free s3)"
  1.1259 -    proof (cases "normal s1 \<and> the_Bool b")
  1.1260 +    proof (cases "normal s1")
  1.1261        case True
  1.1262 -      from Loop True have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" by auto
  1.1263 -      from Loop True have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1.1264 -	by auto
  1.1265 -      from Loop True have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>"
  1.1266 -	by (auto)
  1.1267 -      from Loop True have hyp_w: "PROP ?TypeSafe (abupd (absorb (Cont l)) s2)
  1.1268 -                                       s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1.1269 -	by (auto)
  1.1270 -      from conf_s1 error_free_s1 wt_c hyp_c
  1.1271 -      obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.1272 -	by blast
  1.1273 -      from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1.1274 -	by (cases s2) (auto intro: conforms_absorb)
  1.1275 -      moreover
  1.1276 -      from error_free_s2 have "error_free (abupd (absorb (Cont l)) s2)"
  1.1277 -	by simp
  1.1278 -      moreover note wt hyp_w
  1.1279 -      ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  1.1280 -	by blast
  1.1281 -      with wt 
  1.1282 +      note normal_s1 = this
  1.1283        show ?thesis
  1.1284 -	by (simp)
  1.1285 +      proof (cases "the_Bool b")
  1.1286 +	case True
  1.1287 +	with Loop.hyps  obtain
  1.1288 +          eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  1.1289 +          eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1.1290 +	  by simp 
  1.1291 +	have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
  1.1292 +	  using Loop.hyps True by simp
  1.1293 +	note hyp_c = this [rule_format]
  1.1294 +	have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
  1.1295 +          s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1.1296 +	  using Loop.hyps True by simp
  1.1297 +	note hyp_w = this [rule_format]
  1.1298 +	from eval_e have 
  1.1299 +	  s0_s1: "dom (locals (store ((Norm s0)::state)))
  1.1300 +                    \<subseteq> dom (locals (store s1))"
  1.1301 +	  by (rule dom_locals_eval_mono_elim)
  1.1302 +	obtain C' where
  1.1303 +	  "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
  1.1304 +	proof -
  1.1305 +	  note s0_s1
  1.1306 +          moreover
  1.1307 +	  from eval_e normal_s1 wt_e 
  1.1308 +	  have "assigns_if True e \<subseteq> dom (locals (store s1))"
  1.1309 +	    by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
  1.1310 +	  ultimately 
  1.1311 +	  have "dom (locals (store ((Norm s0)::state))) 
  1.1312 +                 \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
  1.1313 +	    by (rule Un_least)
  1.1314 +	  with da_c show ?thesis
  1.1315 +	    by (rule da_weakenE)
  1.1316 +	qed
  1.1317 +	with conf_s1 wt_c  
  1.1318 +	obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.1319 +	  by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  1.1320 +	from error_free_s2 
  1.1321 +	have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
  1.1322 +	  by simp
  1.1323 +	from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1.1324 +	  by (cases s2) (auto intro: conforms_absorb)
  1.1325 +	moreover note wt
  1.1326 +	moreover
  1.1327 +	obtain A' where 
  1.1328 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.1329 +              dom (locals(store (abupd (absorb (Cont l)) s2)))
  1.1330 +                \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A'"
  1.1331 +	proof -
  1.1332 +	  note s0_s1
  1.1333 +	  also from eval_c 
  1.1334 +	  have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  1.1335 +	    by (rule dom_locals_eval_mono_elim)
  1.1336 +	  also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  1.1337 +	    by simp
  1.1338 +	  finally
  1.1339 +          have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
  1.1340 +	  with da show ?thesis
  1.1341 +	    by (rule da_weakenE)
  1.1342 +	qed
  1.1343 +	ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  1.1344 +	  by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
  1.1345 +	with wt show ?thesis
  1.1346 +	  by simp
  1.1347 +      next
  1.1348 +	case False
  1.1349 +	with Loop.hyps have "s3=s1" by simp
  1.1350 +	with conf_s1 error_free_s1 wt
  1.1351 +	show ?thesis
  1.1352 +	  by simp
  1.1353 +      qed
  1.1354      next
  1.1355        case False
  1.1356 -      with Loop have "s3=s1" by simp
  1.1357 +      have "s3=s1"
  1.1358 +      proof -
  1.1359 +	from False obtain abr where abr: "abrupt s1 = Some abr"
  1.1360 +	  by (cases s1) auto
  1.1361 +	from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  1.1362 +	  by (rule eval_expression_no_jump 
  1.1363 +               [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified]) 
  1.1364 +             (simp_all add: wf)
  1.1365 +	    
  1.1366 +	show ?thesis
  1.1367 +	proof (cases "the_Bool b")
  1.1368 +	  case True  
  1.1369 +	  with Loop.hyps obtain
  1.1370 +            eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  1.1371 +            eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1.1372 +	    by simp
  1.1373 +	  from eval_c abr have "s2=s1" by auto
  1.1374 +	  moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  1.1375 +	    by (cases s1) (simp add: absorb_def)
  1.1376 +	  ultimately show ?thesis
  1.1377 +	    using eval_while abr
  1.1378 +	    by auto
  1.1379 +	next
  1.1380 +	  case False
  1.1381 +	  with Loop.hyps show ?thesis by simp
  1.1382 +	qed
  1.1383 +      qed
  1.1384        with conf_s1 error_free_s1 wt
  1.1385        show ?thesis
  1.1386 -	by (simp)
  1.1387 +	by simp
  1.1388      qed
  1.1389    next
  1.1390 -    case (Do j s L accC T)
  1.1391 +    case (Jmp j s L accC T A)
  1.1392      have "Norm s\<Colon>\<preceq>(G, L)" .
  1.1393 +    moreover
  1.1394 +    from Jmp.prems 
  1.1395 +    have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
  1.1396 +      by (elim da_elim_cases)
  1.1397 +    ultimately have "(Some (Jump j), s)\<Colon>\<preceq>(G, L)" by auto
  1.1398      then 
  1.1399      show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  1.1400             (normal (Some (Jump j), s) 
  1.1401 -           \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Do j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1.1402 +           \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Jmp j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1.1403             (error_free (Norm s) = error_free (Some (Jump j), s))"
  1.1404        by simp
  1.1405    next
  1.1406 -    case (Throw a e s0 s1 L accC T)
  1.1407 +    case (Throw a e s0 s1 L accC T A)
  1.1408      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  1.1409      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  1.1410      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1411 @@ -1373,11 +2092,15 @@
  1.1412        where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  1.1413              throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  1.1414        by (rule wt_elim_cases) (auto)
  1.1415 -    from conf_s0 wt_e hyp obtain
  1.1416 +    from Throw.prems obtain E where 
  1.1417 +      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1418 +             \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  1.1419 +      by (elim da_elim_cases) simp
  1.1420 +    from conf_s0 wt_e da_e obtain
  1.1421        "s1\<Colon>\<preceq>(G, L)" and
  1.1422        "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  1.1423        error_free_s1: "error_free s1"
  1.1424 -      by force
  1.1425 +      by (rule hyp [elim_format]) simp
  1.1426      with wf throwable
  1.1427      have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  1.1428        by (cases s1) (auto dest: Throw_lemma)
  1.1429 @@ -1388,35 +2111,43 @@
  1.1430              (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  1.1431        by simp
  1.1432    next
  1.1433 -    case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
  1.1434 -    have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1435 +    case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T A)
  1.1436 +    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1437      have sx_alloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1.1438      have hyp_c1: "PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1.1439      have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
  1.1440      have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  1.1441      then obtain 
  1.1442        wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1443 -      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  1.1444 +      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  1.1445        fresh_vn: "L(VName vn)=None"
  1.1446 -      by (rule wt_elim_cases) (auto)
  1.1447 -    with conf_s0 hyp_c1
  1.1448 +      by (rule wt_elim_cases) simp
  1.1449 +    from Try.prems obtain C1 C2 where
  1.1450 +      da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1451 +                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1"  and
  1.1452 +      da_c2:
  1.1453 +       "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  1.1454 +        \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>In1r c2\<guillemotright> C2"
  1.1455 +      by (elim da_elim_cases) simp
  1.1456 +    from conf_s0 wt_c1 da_c1
  1.1457      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1458 -      by blast
  1.1459 +      by (rule hyp_c1 [elim_format]) simp
  1.1460      from conf_s1 sx_alloc wf 
  1.1461      have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  1.1462 -      by (auto dest: sxalloc_type_sound split: option.splits)
  1.1463 +      by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits)
  1.1464      from sx_alloc error_free_s1 
  1.1465      have error_free_s2: "error_free s2"
  1.1466        by (rule error_free_sxalloc)
  1.1467      show "s3\<Colon>\<preceq>(G, L) \<and>
  1.1468            (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  1.1469            (error_free (Norm s0) = error_free s3)"
  1.1470 -    proof (cases "normal s1")  
  1.1471 -      case True
  1.1472 -      with sx_alloc wf 
  1.1473 +    proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
  1.1474 +      case False
  1.1475 +      from sx_alloc wf
  1.1476        have eq_s2_s1: "s2=s1"
  1.1477 -	by (auto dest: sxalloc_type_sound split: option.splits)
  1.1478 -      with True 
  1.1479 +	by (rule sxalloc_type_sound [elim_format])
  1.1480 +	   (insert False, auto split: option.splits abrupt.splits )
  1.1481 +      with False 
  1.1482        have "\<not>  G,s2\<turnstile>catch catchC"
  1.1483  	by (simp add: catch_def)
  1.1484        with Try
  1.1485 @@ -1426,7 +2157,7 @@
  1.1486        show ?thesis
  1.1487  	by simp
  1.1488      next
  1.1489 -      case False
  1.1490 +      case True
  1.1491        note exception_s1 = this
  1.1492        show ?thesis
  1.1493        proof (cases "G,s2\<turnstile>catch catchC") 
  1.1494 @@ -1440,24 +2171,54 @@
  1.1495        next
  1.1496  	case True
  1.1497  	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  1.1498 -	from True Try 
  1.1499 -	have hyp_c2: "PROP ?TypeSafe (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1.1500 -	  by auto
  1.1501 +	from True Try.hyps
  1.1502 +	have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1.1503 +	  by simp
  1.1504 +	note hyp_c2 = this [rule_format]
  1.1505  	from exception_s1 sx_alloc wf
  1.1506  	obtain a 
  1.1507  	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  1.1508 -	  by (auto dest!: sxalloc_type_sound split: option.splits)
  1.1509 +	  by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
  1.1510  	with True
  1.1511  	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  1.1512  	  by (cases s2) simp
  1.1513  	with xcpt_s2 conf_s2 wf
  1.1514 -	have "Norm (lupd(VName vn\<mapsto>Addr a) (store s2))
  1.1515 -              \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1.1516 +	have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1.1517  	  by (auto dest: Try_lemma)
  1.1518 -	with hyp_c2 wt_c2 xcpt_s2 error_free_s2
  1.1519 +	moreover note wt_c2
  1.1520 +	moreover
  1.1521 +	obtain C2' where
  1.1522 +	  "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  1.1523 +          \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>In1r c2\<guillemotright> C2'"
  1.1524 +	proof -
  1.1525 +	  have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  1.1526 +                  \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  1.1527 +          proof -
  1.1528 +            have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1529 +            hence "dom (locals (store ((Norm s0)::state))) 
  1.1530 +                    \<subseteq> dom (locals (store s1))"
  1.1531 +              by (rule dom_locals_eval_mono_elim)
  1.1532 +            also
  1.1533 +            from sx_alloc
  1.1534 +            have "\<dots> \<subseteq> dom (locals (store s2))"
  1.1535 +              by (rule dom_locals_sxalloc_mono)
  1.1536 +            also 
  1.1537 +            have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  1.1538 +              by (cases s2) (simp add: new_xcpt_var_def, blast) 
  1.1539 +            also
  1.1540 +            have "{VName vn} \<subseteq> \<dots>"
  1.1541 +              by (cases s2) simp
  1.1542 +            ultimately show ?thesis
  1.1543 +              by (rule Un_least)
  1.1544 +          qed
  1.1545 +	  with da_c2 show ?thesis
  1.1546 +	    by (rule da_weakenE)
  1.1547 +	qed
  1.1548 +	ultimately
  1.1549  	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  1.1550                 error_free_s3: "error_free s3"
  1.1551 -	  by (cases s2) auto
  1.1552 +	  by (rule hyp_c2 [elim_format])
  1.1553 +             (cases s2, simp add: xcpt_s2 error_free_s2) 
  1.1554  	from conf_s3 fresh_vn 
  1.1555  	have "s3\<Colon>\<preceq>(G,L)"
  1.1556  	  by (blast intro: conforms_deallocL)
  1.1557 @@ -1467,9 +2228,9 @@
  1.1558        qed
  1.1559      qed
  1.1560    next
  1.1561 -    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
  1.1562 -    have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  1.1563 -    have c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  1.1564 +    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
  1.1565 +    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
  1.1566 +    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  1.1567      have s3: "s3= (if \<exists>err. x1 = Some (Error err) 
  1.1568                       then (x1, s1)
  1.1569                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  1.1570 @@ -1478,17 +2239,38 @@
  1.1571      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1572      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
  1.1573      then obtain
  1.1574 -      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1575 -      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1.1576 +      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1577 +      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1.1578        by (rule wt_elim_cases) blast
  1.1579 -    from conf_s0 wt_c1 hyp_c1  
  1.1580 +    from Fin.prems obtain C1 C2 where 
  1.1581 +      da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1582 +               \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
  1.1583 +      da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1584 +               \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c2\<guillemotright> C2"
  1.1585 +      by (elim da_elim_cases) simp 
  1.1586 +    from conf_s0 wt_c1 da_c1   
  1.1587      obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  1.1588 -      by blast
  1.1589 +      by (rule hyp_c1 [elim_format]) simp
  1.1590      from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  1.1591        by (rule conforms_NormI)
  1.1592 -    with wt_c2 hyp_c2
  1.1593 +    moreover note wt_c2
  1.1594 +    moreover obtain C2'
  1.1595 +      where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1596 +               \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>In1r c2\<guillemotright> C2'"
  1.1597 +    proof -
  1.1598 +      from eval_c1
  1.1599 +      have "dom (locals (store ((Norm s0)::state))) 
  1.1600 +             \<subseteq> dom (locals (store (x1,s1)))"
  1.1601 +        by (rule dom_locals_eval_mono_elim)
  1.1602 +      hence "dom (locals (store ((Norm s0)::state))) 
  1.1603 +              \<subseteq> dom (locals (store ((Norm s1)::state)))"
  1.1604 +	by simp
  1.1605 +      with da_c2 show ?thesis
  1.1606 +	by (rule da_weakenE)
  1.1607 +    qed
  1.1608 +    ultimately
  1.1609      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.1610 -      by blast
  1.1611 +      by (rule hyp_c2 [elim_format]) simp
  1.1612      from error_free_s1 s3 
  1.1613      have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  1.1614        by simp
  1.1615 @@ -1499,7 +2281,10 @@
  1.1616        case None with conf_s2 s3' wt show ?thesis by auto
  1.1617      next
  1.1618        case (Some x) 
  1.1619 -      with c2 wf conf_s1 conf_s2
  1.1620 +      from eval_c2 have 
  1.1621 +	"dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
  1.1622 +	by (rule dom_locals_eval_mono_elim)
  1.1623 +      with Some eval_c2 wf conf_s1 conf_s2
  1.1624        have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  1.1625  	by (cases s2) (auto dest: Fin_lemma)
  1.1626        from Some error_free_s1
  1.1627 @@ -1523,50 +2308,91 @@
  1.1628            (error_free (Norm s0) = error_free s3)"
  1.1629      proof (cases "inited C (globs s0)")
  1.1630        case True
  1.1631 -      with Init have "s3 = Norm s0"
  1.1632 +      with Init.hyps have "s3 = Norm s0"
  1.1633  	by simp
  1.1634        with conf_s0 wt show ?thesis 
  1.1635  	by simp
  1.1636      next
  1.1637        case False
  1.1638 -      with Init 
  1.1639 -      have "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1.1640 +      with Init.hyps obtain 
  1.1641 +           eval_init_super: 
  1.1642 +           "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1.1643                \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  1.1644          eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  1.1645  	s3: "s3 = (set_lvars (locals (store s1))) s2" 
  1.1646 -	by auto
  1.1647 -      from False Init 
  1.1648 -      have hyp_init_super: 
  1.1649 -             "PROP ?TypeSafe (Norm ((init_class_obj G C) s0)) s1
  1.1650 +	by simp
  1.1651 +      have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
  1.1652  	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  1.1653 -	by auto
  1.1654 -      with False Init (* without chaining hyp_init_super, the simplifier will
  1.1655 -                          loop! *)
  1.1656 -      have hyp_init_c:
  1.1657 -	"PROP ?TypeSafe ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  1.1658 -	by auto
  1.1659 +	using False Init.hyps by simp
  1.1660 +      note hyp_init_super = this [rule_format] 
  1.1661 +      have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  1.1662 +	using False Init.hyps by simp
  1.1663 +      note hyp_init_c = this [rule_format]
  1.1664        from conf_s0 wf cls_C False
  1.1665 -      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1.1666 +      have "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1.1667  	by (auto dest: conforms_init_class_obj)
  1.1668 -      from wf cls_C have
  1.1669 -	wt_super:"\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1.1670 -                   \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1.1671 +      moreover from wf cls_C have
  1.1672 +	wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1.1673 +                         \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1.1674  	by (cases "C=Object")
  1.1675             (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1.1676 -      with conf_s0' hyp_init_super
  1.1677 +      moreover
  1.1678 +      obtain S where
  1.1679 +	da_init_super:
  1.1680 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1681 +          \<turnstile> dom (locals (store ((Norm ((init_class_obj G C) s0))::state))) 
  1.1682 +               \<guillemotright>In1r (if C = Object then Skip else Init (super c))\<guillemotright> S"
  1.1683 +      proof (cases "C=Object")
  1.1684 +	case True 
  1.1685 +	with da_Skip show ?thesis
  1.1686 +	  using that by (auto intro: assigned.select_convs)
  1.1687 +      next
  1.1688 +	case False 
  1.1689 +	with da_Init show ?thesis
  1.1690 +	  by - (rule that, auto intro: assigned.select_convs)
  1.1691 +      qed
  1.1692 +      ultimately 
  1.1693        obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1694 -	by blast 
  1.1695 -      then
  1.1696 +	by (rule hyp_init_super [elim_format]) simp
  1.1697 +      from eval_init_super wt_init_super wf
  1.1698 +      have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  1.1699 +	by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
  1.1700 +              auto)
  1.1701 +      with conf_s1
  1.1702        have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1.1703 -	by (cases s1) (auto dest: conforms_set_locals )
  1.1704 -      moreover from error_free_s1
  1.1705 -      have "error_free ((set_lvars empty) s1)"
  1.1706 +	by (cases s1) (auto intro: conforms_set_locals)
  1.1707 +      moreover 
  1.1708 +      from error_free_s1
  1.1709 +      have error_free_empty: "error_free ((set_lvars empty) s1)"
  1.1710  	by simp
  1.1711 -      moreover note hyp_init_c wf cls_C 
  1.1712 +      from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
  1.1713 +	by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
  1.1714 +      moreover from cls_C wf obtain I
  1.1715 +	where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
  1.1716 +	by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
  1.1717 +       (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
  1.1718 +      then obtain I' where
  1.1719 +	"\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
  1.1720 +            \<guillemotright>In1r (init c)\<guillemotright> I'"
  1.1721 +	  by (rule da_weakenE) simp
  1.1722        ultimately
  1.1723        obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  1.1724 -	by (auto dest!: wf_prog_cdecl wf_cdecl_wt_init)
  1.1725 -      with s3 conf_s1 eval_init
  1.1726 +	by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
  1.1727 +      have "abrupt s2 \<noteq> Some (Jump Ret)"
  1.1728 +      proof -
  1.1729 +	from s1_no_ret 
  1.1730 +	have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
  1.1731 +	  by simp
  1.1732 +	moreover
  1.1733 +	from cls_C wf have "jumpNestingOkS {} (init c)"
  1.1734 +	  by (rule wf_prog_cdecl [THEN wf_cdeclE])
  1.1735 +	ultimately 
  1.1736 +	show ?thesis
  1.1737 +	  using eval_init wt_init_c wf
  1.1738 +	  by - (rule eval_statement_no_jump 
  1.1739 +                     [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
  1.1740 +      qed
  1.1741 +      with conf_s2 s3 conf_s1 eval_init
  1.1742        have "s3\<Colon>\<preceq>(G, L)"
  1.1743  	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  1.1744        moreover from error_free_s2 s3
  1.1745 @@ -1577,18 +2403,25 @@
  1.1746  	by simp
  1.1747      qed
  1.1748    next
  1.1749 -    case (NewC C a s0 s1 s2 L accC T)
  1.1750 +    case (NewC C a s0 s1 s2 L accC T A)
  1.1751      have         "G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1" .
  1.1752      have halloc: "G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2" .
  1.1753      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>" .
  1.1754      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1755 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  1.1756 +    moreover
  1.1757 +    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T" .
  1.1758      then obtain is_cls_C: "is_class G C" and
  1.1759                         T: "T=Inl (Class C)"
  1.1760        by (rule wt_elim_cases) (auto dest: is_acc_classD)
  1.1761 -    with conf_s0 hyp
  1.1762 +    hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" by auto
  1.1763 +    moreover obtain I where 
  1.1764 +      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1765 +          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init C)\<guillemotright> I"
  1.1766 +      by (auto intro: da_Init [simplified] assigned.select_convs)
  1.1767 +     (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  1.1768 +    ultimately 
  1.1769      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1770 -      by auto
  1.1771 +      by (rule hyp [elim_format]) simp 
  1.1772      from conf_s1 halloc wf is_cls_C
  1.1773      obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  1.1774                               "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  1.1775 @@ -1602,42 +2435,78 @@
  1.1776            (error_free (Norm s0) = error_free s2)"
  1.1777        by auto
  1.1778    next
  1.1779 -    case (NewA T a e i s0 s1 s2 s3 L accC Ta)
  1.1780 -    have "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1" .
  1.1781 -    have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  1.1782 -    have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1.1783 -    have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
  1.1784 +    case (NewA elT a e i s0 s1 s2 s3 L accC T A)
  1.1785 +    have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1" .
  1.1786 +    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2" .
  1.1787 +    have halloc: "G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3".
  1.1788 +    have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>" .
  1.1789      have hyp_size: "PROP ?TypeSafe s1 s2 (In1l e) (In1 i)" .
  1.1790      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1791 -    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
  1.1792 +    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T" .
  1.1793      then obtain
  1.1794 -      wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
  1.1795 +      wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
  1.1796        wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  1.1797 -            T: "is_type G T" and
  1.1798 -           Ta: "Ta=Inl (T.[])"
  1.1799 +            elT: "is_type G elT" and
  1.1800 +           T: "T=Inl (elT.[])"
  1.1801        by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  1.1802 -    from conf_s0 wt_init hyp_init
  1.1803 -    obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  1.1804 -      by blast
  1.1805 -    with wt_size hyp_size
  1.1806 +    from NewA.prems 
  1.1807 +    have da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1808 +                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  1.1809 +      by (elim da_elim_cases) simp
  1.1810 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1811 +    proof -
  1.1812 +      note conf_s0 wt_init
  1.1813 +      moreover obtain I where
  1.1814 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1815 +         \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
  1.1816 +      proof (cases "\<exists>C. elT = Class C")
  1.1817 +	case True
  1.1818 +	thus ?thesis
  1.1819 +	  by - (rule that, (auto intro: da_Init [simplified] 
  1.1820 +                                        assigned.select_convs
  1.1821 +                              simp add: init_comp_ty_def))
  1.1822 +	 (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  1.1823 +      next
  1.1824 +	case False
  1.1825 +	thus ?thesis
  1.1826 +	by - (rule that, (auto intro: da_Skip [simplified] 
  1.1827 +                                      assigned.select_convs
  1.1828 +                           simp add: init_comp_ty_def))
  1.1829 +         (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
  1.1830 +      qed
  1.1831 +      ultimately show ?thesis
  1.1832 +	by (rule hyp_init [elim_format]) auto
  1.1833 +    qed 
  1.1834      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.1835 -      by blast
  1.1836 +    proof -
  1.1837 +      from eval_init 
  1.1838 +      have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.1839 +	by (rule dom_locals_eval_mono_elim)
  1.1840 +      with da_e 
  1.1841 +      obtain A' where
  1.1842 +       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1843 +            \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  1.1844 +	by (rule da_weakenE)
  1.1845 +      with conf_s1 wt_size
  1.1846 +      show ?thesis
  1.1847 +	by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
  1.1848 +    qed
  1.1849      from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  1.1850        by (cases s2) auto
  1.1851 -    with halloc wf T 
  1.1852 +    with halloc wf elT 
  1.1853      have halloc_type_safe:
  1.1854 -          "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>T.[])"
  1.1855 +          "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>elT.[])"
  1.1856        by (cases s3) (auto dest!: halloc_type_sound)
  1.1857      from halloc error_free_s2
  1.1858      have "error_free s3"
  1.1859        by (auto dest: error_free_halloc)
  1.1860 -    with halloc_type_safe Ta
  1.1861 +    with halloc_type_safe T
  1.1862      show "s3\<Colon>\<preceq>(G, L) \<and> 
  1.1863 -          (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New T[e])\<succ>In1 (Addr a)\<Colon>\<preceq>Ta) \<and>
  1.1864 +          (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New elT[e])\<succ>In1 (Addr a)\<Colon>\<preceq>T) \<and>
  1.1865            (error_free (Norm s0) = error_free s3) "
  1.1866        by simp
  1.1867    next
  1.1868 -    case (Cast castT e s0 s1 s2 v L accC T)
  1.1869 +    case (Cast castT e s0 s1 s2 v L accC T A)
  1.1870      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1.1871      have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
  1.1872      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1.1873 @@ -1648,9 +2517,15 @@
  1.1874                eT: "G\<turnstile>eT\<preceq>? castT" and 
  1.1875                 T: "T=Inl castT"
  1.1876        by (rule wt_elim_cases) auto
  1.1877 -    with conf_s0 hyp
  1.1878 -    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.1879 -      by blast
  1.1880 +    from Cast.prems 
  1.1881 +    have "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1882 +                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  1.1883 +      by (elim da_elim_cases) simp
  1.1884 +    with conf_s0 wt_e
  1.1885 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1.1886 +           v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  1.1887 +      error_free_s1: "error_free s1"
  1.1888 +      by (rule hyp [elim_format]) simp
  1.1889      from conf_s1 s2 
  1.1890      have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  1.1891        by (cases s1) simp
  1.1892 @@ -1663,9 +2538,9 @@
  1.1893        proof -
  1.1894  	from s2 norm_s2 have "normal s1"
  1.1895  	  by (cases s1) simp
  1.1896 -	with wt_e conf_s0 hyp 
  1.1897 +	with v_ok 
  1.1898  	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  1.1899 -	  by force
  1.1900 +	  by simp
  1.1901  	with eT wf s2 T norm_s2
  1.1902  	show ?thesis
  1.1903  	  by (cases s1) (auto dest: fits_conf)
  1.1904 @@ -1677,16 +2552,31 @@
  1.1905             (error_free (Norm s0) = error_free s2)"
  1.1906        by blast
  1.1907    next
  1.1908 -    case (Inst T b e s0 s1 v L accC T')
  1.1909 -    then show ?case
  1.1910 -      by (auto elim!: wt_elim_cases)
  1.1911 +    case (Inst instT b e s0 s1 v L accC T A)
  1.1912 +    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1.1913 +    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1914 +    from Inst.prems obtain eT
  1.1915 +    where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
  1.1916 +             T: "T=Inl (PrimT Boolean)" 
  1.1917 +      by (elim wt_elim_cases) simp
  1.1918 +    from Inst.prems 
  1.1919 +    have da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1920 +                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  1.1921 +      by (elim da_elim_cases) simp
  1.1922 +    from conf_s0 wt_e da_e
  1.1923 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1.1924 +              v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>RefT eT" and
  1.1925 +      error_free_s1: "error_free s1"
  1.1926 +      by (rule hyp [elim_format]) simp
  1.1927 +    with T show ?case
  1.1928 +      by simp
  1.1929    next
  1.1930 -    case (Lit s v L accC T)
  1.1931 +    case (Lit s v L accC T A)
  1.1932      then show ?case
  1.1933        by (auto elim!: wt_elim_cases 
  1.1934                 intro: conf_litval simp add: empty_dt_def)
  1.1935    next
  1.1936 -    case (UnOp e s0 s1 unop v L accC T)
  1.1937 +    case (UnOp e s0 s1 unop v L accC T A)
  1.1938      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1.1939      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1940      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T" .
  1.1941 @@ -1695,11 +2585,15 @@
  1.1942              wt_unop: "wt_unop unop eT" and
  1.1943                    T: "T=Inl (PrimT (unop_type unop))" 
  1.1944        by (auto elim!: wt_elim_cases)
  1.1945 -    from conf_s0 wt_e 
  1.1946 +    from UnOp.prems obtain A where
  1.1947 +       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1948 +                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  1.1949 +      by (elim da_elim_cases) simp
  1.1950 +    from conf_s0 wt_e da_e
  1.1951      obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  1.1952                    wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  1.1953           error_free_s1: "error_free s1"
  1.1954 -      by (auto dest!: hyp)
  1.1955 +      by (rule hyp [elim_format]) simp
  1.1956      from wt_v T wt_unop
  1.1957      have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
  1.1958        by (cases unop) auto
  1.1959 @@ -1709,7 +2603,10 @@
  1.1960       error_free (Norm s0) = error_free s1"
  1.1961        by simp
  1.1962    next
  1.1963 -    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
  1.1964 +    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T A)
  1.1965 +    have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" .
  1.1966 +    have eval_e2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  1.1967 +                             else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
  1.1968      have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
  1.1969      have hyp_e2: "PROP ?TypeSafe       s1  s2 
  1.1970                     (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
  1.1971 @@ -1721,30 +2618,83 @@
  1.1972           wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  1.1973        wt_binop: "wt_binop G binop e1T e2T" and
  1.1974               T: "T=Inl (PrimT (binop_type binop))"
  1.1975 -      by (auto elim!: wt_elim_cases)
  1.1976 +      by (elim wt_elim_cases) simp
  1.1977      have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
  1.1978        by simp
  1.1979 -    from conf_s0 wt_e1 
  1.1980 +    obtain S where
  1.1981 +      daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1982 +                  \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
  1.1983 +      by (auto intro: da_Skip [simplified] assigned.select_convs)
  1.1984 +    have da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
  1.1985 +                  \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A".
  1.1986 +    then obtain E1 where
  1.1987 +      da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1988 +                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
  1.1989 +      by (elim da_elim_cases) simp+
  1.1990 +    from conf_s0 wt_e1 da_e1
  1.1991      obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  1.1992                    wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  1.1993            error_free_s1: "error_free s1"
  1.1994 -      by (auto dest!: hyp_e1)
  1.1995 -    from conf_s1 wt_e2 wt_Skip error_free_s1
  1.1996 -    obtain      conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
  1.1997 -          error_free_s2: "error_free s2"
  1.1998 -      by (cases "need_second_arg binop v1")
  1.1999 -         (auto dest!: hyp_e2 )
  1.2000 +      by (rule hyp_e1 [elim_format]) simp
  1.2001      from wt_binop T
  1.2002 -    have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  1.2003 +    have conf_v:
  1.2004 +      "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  1.2005        by (cases binop) auto
  1.2006 -    with conf_s2 conf_s1 error_free_s2 error_free_s1
  1.2007 +    -- {* Note that we don't use the information that v1 really is compatible 
  1.2008 +          with the expected type e1T and v2 is compatible with e2T, 
  1.2009 +          because @{text eval_binop} will anyway produce an output of 
  1.2010 +          the right type.
  1.2011 +          So evaluating the addition of an integer with a string is type
  1.2012 +          safe. This is a little bit annoying since we may regard such a
  1.2013 +          behaviour as not type safe.
  1.2014 +          If we want to avoid this we can redefine @{text eval_binop} so that
  1.2015 +          it only produces a output of proper type if it is assigned to 
  1.2016 +          values of the expected types, and arbitrary if the inputs have 
  1.2017 +          unexpected types. The proof can easily be adapted since we
  1.2018 +          have the hypothesis that the values have a proper type.
  1.2019 +          This also applies to unary operations.
  1.2020 +       *}
  1.2021 +    from eval_e1 have 
  1.2022 +      s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.2023 +      by (rule dom_locals_eval_mono_elim)
  1.2024      show "s2\<Colon>\<preceq>(G, L) \<and>
  1.2025            (normal s2 \<longrightarrow>
  1.2026          G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  1.2027            error_free (Norm s0) = error_free s2"
  1.2028 -      by simp
  1.2029 +    proof (cases "normal s1")
  1.2030 +      case False
  1.2031 +      with eval_e2 have "s2=s1" by auto
  1.2032 +      with conf_s1 error_free_s1 False show ?thesis
  1.2033 +	by auto
  1.2034 +    next
  1.2035 +      case True
  1.2036 +      note normal_s1 = this
  1.2037 +      show ?thesis 
  1.2038 +      proof (cases "need_second_arg binop v1")
  1.2039 +	case False
  1.2040 +	with normal_s1 eval_e2 have "s2=s1"
  1.2041 +	  by (cases s1) (simp, elim eval_elim_cases,simp)
  1.2042 +	with conf_s1 conf_v error_free_s1
  1.2043 +	show ?thesis by simp
  1.2044 +      next
  1.2045 +	case True
  1.2046 +	note need_second_arg = this
  1.2047 +	with hyp_e2 
  1.2048 +	have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
  1.2049 +	from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
  1.2050 +          wt_v1 [rule_format,OF normal_s1] wf
  1.2051 +	obtain E2 where
  1.2052 +	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
  1.2053 +	  by (rule da_e2_BinOp [elim_format]) 
  1.2054 +             (auto simp add: need_second_arg )
  1.2055 +	with conf_s1 wt_e2 
  1.2056 +	obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1.2057 +	  by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
  1.2058 +	with conf_v show ?thesis by simp
  1.2059 +      qed
  1.2060 +    qed
  1.2061    next
  1.2062 -    case (Super s L accC T)
  1.2063 +    case (Super s L accC T A)
  1.2064      have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
  1.2065      have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
  1.2066      then obtain C c where
  1.2067 @@ -1753,8 +2703,11 @@
  1.2068           cls_C: "class G C = Some c" and
  1.2069               T: "T=Inl (Class (super c))"
  1.2070        by (rule wt_elim_cases) auto
  1.2071 -    from C conf_s have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  1.2072 -      by (blast intro: conforms_localD [THEN lconfD])
  1.2073 +    from Super.prems
  1.2074 +    obtain "This \<in> dom (locals s)"
  1.2075 +      by (elim da_elim_cases) simp
  1.2076 +    with conf_s C  have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  1.2077 +      by (auto dest: conforms_localD [THEN wlconfD])
  1.2078      with neq_Obj cls_C wf
  1.2079      have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  1.2080        by (auto intro: conf_widen
  1.2081 @@ -1766,14 +2719,50 @@
  1.2082             (error_free (Norm s) = error_free (Norm s))"
  1.2083        by simp
  1.2084    next
  1.2085 -    case (Acc f s0 s1 v va L accC T)
  1.2086 -    then show ?case
  1.2087 -      by (force elim!: wt_elim_cases)
  1.2088 +    case (Acc upd s0 s1 w v L accC T A) 
  1.2089 +    have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
  1.2090 +    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.2091 +    from Acc.prems obtain vT where
  1.2092 +      wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
  1.2093 +         T: "T=Inl vT"
  1.2094 +      by (elim wt_elim_cases) simp
  1.2095 +    from Acc.prems obtain V where
  1.2096 +      da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2097 +                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
  1.2098 +      by (cases "\<exists> n. v=LVar n") (insert da.LVar,auto elim!: da_elim_cases)
  1.2099 +    {
  1.2100 +      fix n assume lvar: "v=LVar n"
  1.2101 +      have "locals (store s1) n \<noteq> None"
  1.2102 +      proof -
  1.2103 +	from Acc.prems lvar have 
  1.2104 +	  "n \<in> dom (locals s0)"
  1.2105 +	  by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
  1.2106 +	also
  1.2107 +	have "dom (locals s0) \<subseteq> dom (locals (store s1))"
  1.2108 +	proof -
  1.2109 +	  have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
  1.2110 +	  thus ?thesis
  1.2111 +	    by (rule dom_locals_eval_mono_elim) simp
  1.2112 +	qed
  1.2113 +	finally show ?thesis
  1.2114 +	  by blast
  1.2115 +      qed
  1.2116 +    } note lvar_in_locals = this 
  1.2117 +    from conf_s0 wt_v da_v
  1.2118 +    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
  1.2119 +      and  conf_var: "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In2 v\<succ>In2 (w, upd)\<Colon>\<preceq>Inl vT)"
  1.2120 +      and  error_free_s1: "error_free s1"
  1.2121 +      by (rule hyp [elim_format]) simp
  1.2122 +    from lvar_in_locals conf_var T
  1.2123 +    have "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1l (Acc v)\<succ>In1 w\<Colon>\<preceq>T)"
  1.2124 +      by (cases "\<exists> n. v=LVar n") auto
  1.2125 +    with conf_s1 error_free_s1 show ?case
  1.2126 +      by simp
  1.2127    next
  1.2128 -    case (Ass e f s0 s1 s2 v var w L accC T)
  1.2129 -    have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> s1" .
  1.2130 +    case (Ass e upd s0 s1 s2 v var w L accC T A)
  1.2131 +    have eval_var: "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" .
  1.2132      have   eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2" .
  1.2133 -    have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,f))" .
  1.2134 +    have  hyp_var: "PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))" .
  1.2135      have    hyp_e: "PROP ?TypeSafe s1 s2 (In1l e) (In1 v)" .
  1.2136      have  conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.2137      have       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T" .
  1.2138 @@ -1783,58 +2772,157 @@
  1.2139  	  widen: "G\<turnstile>eT\<preceq>varT" and
  1.2140                T: "T=Inl eT"
  1.2141        by (rule wt_elim_cases) auto
  1.2142 -    from conf_s0 wt_var hyp_var
  1.2143 -    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.2144 -      by blast
  1.2145 -    with wt_e hyp_e
  1.2146 -    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.2147 -      by blast
  1.2148 -    show "assign f v s2\<Colon>\<preceq>(G, L) \<and>
  1.2149 -           (normal (assign f v s2) \<longrightarrow>
  1.2150 -            G,L,store (assign f v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1.2151 -            (error_free (Norm s0) = error_free (assign f v s2))"
  1.2152 -    proof (cases "normal s1")
  1.2153 +    show "assign upd v s2\<Colon>\<preceq>(G, L) \<and>
  1.2154 +           (normal (assign upd v s2) \<longrightarrow>
  1.2155 +            G,L,store (assign upd v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1.2156 +      (error_free (Norm s0) = error_free (assign upd v s2))"
  1.2157 +    proof (cases "\<exists> vn. var=LVar vn")
  1.2158        case False
  1.2159 -      with eval_e 
  1.2160 -      have "s2=s1"
  1.2161 -	by auto
  1.2162 -      with False conf_s1 error_free_s1
  1.2163 +      with Ass.prems
  1.2164 +      obtain V E where
  1.2165 +	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2166 +                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V" and
  1.2167 +	da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  1.2168 +	by (elim da_elim_cases) simp+
  1.2169 +      from conf_s0 wt_var da_var 
  1.2170 +      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  1.2171 +	and  conf_var: "normal s1 
  1.2172 +                         \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.2173 +	and  error_free_s1: "error_free s1"
  1.2174 +	by (rule hyp_var [elim_format]) simp
  1.2175        show ?thesis
  1.2176 -	by auto
  1.2177 -    next
  1.2178 -      case True
  1.2179 -      note normal_s1=this
  1.2180 -      show ?thesis 
  1.2181 -      proof (cases "normal s2")
  1.2182 +      proof (cases "normal s1")
  1.2183  	case False
  1.2184 -	with conf_s2 error_free_s2 
  1.2185 -	show ?thesis
  1.2186 +	with eval_e have "s2=s1" by auto
  1.2187 +	with False have "assign upd v s2=s1"
  1.2188 +	  by simp
  1.2189 +	with conf_s1 error_free_s1 False show ?thesis
  1.2190  	  by auto
  1.2191        next
  1.2192  	case True
  1.2193 -	from True normal_s1 conf_s1 wt_e hyp_e
  1.2194 -	have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.2195 -	  by force
  1.2196 -	with widen wf
  1.2197 -	have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.2198 -	  by (auto intro: conf_widen)
  1.2199 -	from conf_s0 normal_s1 wt_var hyp_var
  1.2200 -	have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, f)\<Colon>\<preceq>Inl varT"
  1.2201 -	  by blast
  1.2202 -	then 
  1.2203 -	have conf_assign:  "store s1\<le>|f\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.2204 +	note normal_s1=this
  1.2205 +	obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2206 +                         \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  1.2207 +	proof -
  1.2208 +	  from eval_var wt_var da_var wf normal_s1
  1.2209 +	  have "nrm V \<subseteq>  dom (locals (store s1))"
  1.2210 +	    by (cases rule: da_good_approxE') rules
  1.2211 +	  with da_e show ?thesis
  1.2212 +	    by (rule da_weakenE) 
  1.2213 +	qed
  1.2214 +	with conf_s1 wt_e 
  1.2215 +	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.2216 +          conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  1.2217 +          error_free_s2: "error_free s2"
  1.2218 +	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.2219 +	show ?thesis 
  1.2220 +	proof (cases "normal s2")
  1.2221 +	  case False
  1.2222 +	  with conf_s2 error_free_s2 
  1.2223 +	  show ?thesis
  1.2224 +	    by auto
  1.2225 +	next
  1.2226 +	  case True
  1.2227 +	  from True conf_v
  1.2228 +	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.2229 +	    by simp
  1.2230 +	  with widen wf
  1.2231 +	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.2232 +	    by (auto intro: conf_widen)
  1.2233 +	  from normal_s1 conf_var
  1.2234 +	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.2235 +	    by simp
  1.2236 +	  then 
  1.2237 +	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.2238 +	    by (simp add: rconf_def)
  1.2239 +	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.2240 +	    eval_e T conf_s2 error_free_s2
  1.2241 +	  show ?thesis
  1.2242 +	    by (cases s1, cases s2) 
  1.2243 +	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.2244 +	qed
  1.2245 +      qed
  1.2246 +    next
  1.2247 +      case True
  1.2248 +      then obtain vn where vn: "var=LVar vn"
  1.2249 +	by blast
  1.2250 +      with Ass.prems
  1.2251 +      obtain E where
  1.2252 +	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  1.2253 +	           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  1.2254 +	by (elim da_elim_cases) simp+
  1.2255 +      from da.LVar vn obtain V where
  1.2256 +	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2257 +                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V"
  1.2258 +	by auto
  1.2259 +      obtain E' where
  1.2260 +	da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2261 +                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> E'"
  1.2262 +      proof -
  1.2263 +	have "dom (locals (store ((Norm s0)::state))) 
  1.2264 +                \<subseteq> dom (locals (store (s1)))"
  1.2265 +	  by (rule dom_locals_eval_mono_elim)
  1.2266 +	with da_e show ?thesis
  1.2267 +	  by (rule da_weakenE)
  1.2268 +      qed
  1.2269 +      from conf_s0 wt_var da_var 
  1.2270 +      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  1.2271 +	and  conf_var: "normal s1 
  1.2272 +                         \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.2273 +	and  error_free_s1: "error_free s1"
  1.2274 +	by (rule hyp_var [elim_format]) simp
  1.2275 +      show ?thesis
  1.2276 +      proof (cases "normal s1")
  1.2277 +	case False
  1.2278 +	with eval_e have "s2=s1" by auto
  1.2279 +	with False have "assign upd v s2=s1"
  1.2280 +	  by simp
  1.2281 +	with conf_s1 error_free_s1 False show ?thesis
  1.2282  	  by auto
  1.2283 -	from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.2284 -	  eval_e T conf_s2 error_free_s2
  1.2285 -	show ?thesis
  1.2286 -	  by (cases s1, cases s2) 
  1.2287 -	     (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.2288 +      next
  1.2289 +	case True
  1.2290 +	note normal_s1 = this
  1.2291 +	from conf_s1 wt_e da_e'
  1.2292 +	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.2293 +          conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  1.2294 +          error_free_s2: "error_free s2"
  1.2295 +	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.2296 +	show ?thesis 
  1.2297 +	proof (cases "normal s2")
  1.2298 +	  case False
  1.2299 +	  with conf_s2 error_free_s2 
  1.2300 +	  show ?thesis
  1.2301 +	    by auto
  1.2302 +	next
  1.2303 +	  case True
  1.2304 +	  from True conf_v
  1.2305 +	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.2306 +	    by simp
  1.2307 +	  with widen wf
  1.2308 +	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.2309 +	    by (auto intro: conf_widen)
  1.2310 +	  from normal_s1 conf_var
  1.2311 +	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.2312 +	    by simp
  1.2313 +	  then 
  1.2314 +	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.2315 +	    by (simp add: rconf_def)
  1.2316 +	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.2317 +	    eval_e T conf_s2 error_free_s2
  1.2318 +	  show ?thesis
  1.2319 +	    by (cases s1, cases s2) 
  1.2320 +	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.2321 +	qed
  1.2322        qed
  1.2323      qed
  1.2324    next
  1.2325 -    case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
  1.2326 +-- {* 
  1.2327 +\par
  1.2328 +*} (* dummy text command to break paragraph for latex;
  1.2329 +              large paragraphs exhaust memory of debian pdflatex *)
  1.2330 +    case (Cond b e0 e1 e2 s0 s1 s2 v L accC T A)
  1.2331      have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  1.2332 -    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  1.2333 +    have eval_e1_e2: "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2" .
  1.2334      have hyp_e0: "PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)" .
  1.2335      have hyp_if: "PROP ?TypeSafe s1 s2 
  1.2336                         (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  1.2337 @@ -1847,40 +2935,98 @@
  1.2338        statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  1.2339        T    : "T=Inl statT"
  1.2340        by (rule wt_elim_cases) auto
  1.2341 -    with wt_e0 conf_s0 hyp_e0
  1.2342 +    with Cond.prems obtain E0 E1 E2 where
  1.2343 +         da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2344 +                  \<turnstile> dom (locals (store ((Norm s0)::state))) 
  1.2345 +                      \<guillemotright>In1l e0\<guillemotright> E0" and
  1.2346 +         da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2347 +                  \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1.2348 +                         \<union> assigns_if True e0) \<guillemotright>In1l e1\<guillemotright> E1" and
  1.2349 +         da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2350 +                  \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1.2351 +                        \<union> assigns_if False e0) \<guillemotright>In1l e2\<guillemotright> E2"
  1.2352 +       by (elim da_elim_cases) simp+
  1.2353 +    from conf_s0 wt_e0 da_e0  
  1.2354      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  1.2355 -      by blast
  1.2356 -    with wt_e1 wt_e2 statT hyp_if
  1.2357 -    obtain dynT where
  1.2358 -      conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2" and
  1.2359 -      conf_res: 
  1.2360 -          "(normal s2 \<longrightarrow>
  1.2361 -        G,L,store s2\<turnstile>In1l (if the_Bool b then e1 else e2)\<succ>In1 v\<Colon>\<preceq>Inl dynT)" and
  1.2362 -      dynT: "dynT = (if the_Bool b then T1 else T2)"
  1.2363 -      by (cases "the_Bool b") force+
  1.2364 -    from statT dynT  
  1.2365 -    have "G\<turnstile>dynT\<preceq>statT"
  1.2366 -      by (cases "the_Bool b") auto
  1.2367 -    with conf_s2 conf_res error_free_s2 T wf
  1.2368 +      by (rule hyp_e0 [elim_format]) simp
  1.2369      show "s2\<Colon>\<preceq>(G, L) \<and>
  1.2370             (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1.2371             (error_free (Norm s0) = error_free s2)"
  1.2372 -      by (auto)
  1.2373 +    proof (cases "normal s1")
  1.2374 +      case False
  1.2375 +      with eval_e1_e2 have "s2=s1" by auto
  1.2376 +      with conf_s1 error_free_s1 False show ?thesis
  1.2377 +	by auto
  1.2378 +    next
  1.2379 +      case True
  1.2380 +      have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  1.2381 +                    \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1.2382 +      proof -
  1.2383 +	from eval_e0 have 
  1.2384 +	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.2385 +	  by (rule dom_locals_eval_mono_elim)
  1.2386 +        moreover
  1.2387 +	from eval_e0 True wt_e0 
  1.2388 +	have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1.2389 +	  by (rule assigns_if_good_approx') 
  1.2390 +	ultimately show ?thesis by (rule Un_least)
  1.2391 +      qed 
  1.2392 +      show ?thesis
  1.2393 +      proof (cases "the_Bool b")
  1.2394 +	case True
  1.2395 +	with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  1.2396 +	  by simp
  1.2397 +	from da_e1 s0_s1 True obtain E1' where
  1.2398 +	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  1.2399 +	  by - (rule da_weakenE,auto)
  1.2400 +	with conf_s1 wt_e1
  1.2401 +	obtain 
  1.2402 +	  "s2\<Colon>\<preceq>(G, L)"
  1.2403 +	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  1.2404 +	  "error_free s2"            
  1.2405 +	  by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  1.2406 +	moreover
  1.2407 +	from statT  
  1.2408 +	have "G\<turnstile>T1\<preceq>statT"
  1.2409 +	  by auto
  1.2410 +	ultimately show ?thesis
  1.2411 +	  using T wf by auto
  1.2412 +      next
  1.2413 +	case False
  1.2414 +	with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  1.2415 +	  by simp
  1.2416 +	from da_e2 s0_s1 False obtain E2' where
  1.2417 +	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  1.2418 +	  by - (rule da_weakenE,auto)
  1.2419 +	with conf_s1 wt_e2
  1.2420 +	obtain 
  1.2421 +	  "s2\<Colon>\<preceq>(G, L)"
  1.2422 +	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  1.2423 +	  "error_free s2"            
  1.2424 +	  by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.2425 +	moreover
  1.2426 +	from statT  
  1.2427 +	have "G\<turnstile>T2\<preceq>statT"
  1.2428 +	  by auto
  1.2429 +	ultimately show ?thesis
  1.2430 +	  using T wf by auto
  1.2431 +      qed
  1.2432 +    qed
  1.2433    next
  1.2434 -    case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1.2435 -           v vs L accC T)
  1.2436 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
  1.2437 +    case (Call invDeclC a accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1.2438 +           v vs L accC T A)
  1.2439 +    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" .
  1.2440      have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  1.2441      have invDeclC: "invDeclC 
  1.2442 -                      = invocation_declclass G mode (store s2) a' statT 
  1.2443 +                      = invocation_declclass G mode (store s2) a statT 
  1.2444                             \<lparr>name = mn, parTs = pTs'\<rparr>" .
  1.2445      have init_lvars: 
  1.2446 -           "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2".
  1.2447 +           "s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2".
  1.2448      have check: "s3' =
  1.2449 -       check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
  1.2450 +       check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3" .
  1.2451      have eval_methd: 
  1.2452             "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  1.2453 -    have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a')" .
  1.2454 +    have     hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)" .
  1.2455      have  hyp_args: "PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)" .
  1.2456      have hyp_methd: "PROP ?TypeSafe s3' s4 
  1.2457                 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  1.2458 @@ -1896,128 +3042,155 @@
  1.2459                      T: "T =Inl (resTy statM)" and
  1.2460          eq_accC_accC': "accC=accC'"
  1.2461        by (rule wt_elim_cases) fastsimp+
  1.2462 -    from conf_s0 wt_e hyp_e 
  1.2463 +    from Call.prems obtain E where
  1.2464 +      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2465 +               \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  1.2466 +      da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 args\<guillemotright> A" 
  1.2467 +      by (elim da_elim_cases) simp
  1.2468 +    from conf_s0 wt_e da_e  
  1.2469      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1.2470 -           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" and
  1.2471 +           conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1.2472             error_free_s1: "error_free s1" 
  1.2473 -      by force
  1.2474 -    with wt_args hyp_args
  1.2475 -    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.2476 -            conf_args: "normal s2 
  1.2477 -                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  1.2478 -        error_free_s2: "error_free s2" 
  1.2479 -      by force
  1.2480 -    from error_free_s2 init_lvars
  1.2481 -    have error_free_s3: "error_free s3"
  1.2482 -      by (auto simp add: init_lvars_def2)
  1.2483 -    from statM 
  1.2484 -    obtain
  1.2485 -      statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1.2486 -      pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1.2487 -      by (blast dest: max_spec2mheads)
  1.2488 -    from check
  1.2489 -    have eq_store_s3'_s3: "store s3'=store s3"
  1.2490 -      by (cases s3) (simp add: check_method_access_def Let_def)
  1.2491 -    obtain invC
  1.2492 -      where invC: "invC = invocation_class mode (store s2) a' statT"
  1.2493 -      by simp
  1.2494 -    with init_lvars
  1.2495 -    have invC': "invC = (invocation_class mode (store s3) a' statT)"
  1.2496 -      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1.2497 +      by (rule hyp_e [elim_format]) simp
  1.2498 +    { 
  1.2499 +      assume abnormal_s2: "\<not> normal s2"
  1.2500 +      have "set_lvars (locals (store s2)) s4 = s2"
  1.2501 +      proof -
  1.2502 +	from abnormal_s2 init_lvars 
  1.2503 +	obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1.2504 +             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1.2505 +                                            mode a vs s2)" 
  1.2506 +	  by (auto simp add: init_lvars_def2)
  1.2507 +	moreover
  1.2508 +	from keep_abrupt abnormal_s2 check
  1.2509 +	have eq_s3'_s3: "s3'=s3" 
  1.2510 +	  by (auto simp add: check_method_access_def Let_def)
  1.2511 +	moreover
  1.2512 +	from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  1.2513 +	have "s4=s3'"
  1.2514 +	  by auto
  1.2515 +	ultimately show
  1.2516 +	  "set_lvars (locals (store s2)) s4 = s2"
  1.2517 +	  by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.2518 +      qed
  1.2519 +    } note propagate_abnormal_s2 = this
  1.2520      show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  1.2521 -             (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  1.2522 -               G,L,store ((set_lvars (locals (store s2))) s4)
  1.2523 +           (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  1.2524 +             G,L,store ((set_lvars (locals (store s2))) s4)
  1.2525                 \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1.2526 -             (error_free (Norm s0) =
  1.2527 +           (error_free (Norm s0) =
  1.2528                  error_free ((set_lvars (locals (store s2))) s4))"
  1.2529 -    proof (cases "normal s2")
  1.2530 +    proof (cases "normal s1")
  1.2531        case False
  1.2532 -      with init_lvars 
  1.2533 -      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1.2534 -             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1.2535 -                                            mode a' vs s2)" 
  1.2536 -	by (auto simp add: init_lvars_def2)
  1.2537 -      moreover
  1.2538 -      from keep_abrupt False check
  1.2539 -      have eq_s3'_s3: "s3'=s3" 
  1.2540 -	by (auto simp add: check_method_access_def Let_def)
  1.2541 -      moreover
  1.2542 -      from eq_s3'_s3 False keep_abrupt eval_methd
  1.2543 -      have "s4=s3'"
  1.2544 -	by auto
  1.2545 -      ultimately have
  1.2546 -	"set_lvars (locals (store s2)) s4 = s2"
  1.2547 -	by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
  1.2548 -      with False conf_s2 error_free_s2
  1.2549 +      with eval_args have "s2=s1" by auto
  1.2550 +      with False propagate_abnormal_s2 conf_s1 error_free_s1 
  1.2551        show ?thesis
  1.2552  	by auto
  1.2553      next
  1.2554        case True
  1.2555 -      note normal_s2 = True
  1.2556 -      with eval_args
  1.2557 -      have normal_s1: "normal s1"
  1.2558 -	by (cases "normal s1") auto
  1.2559 -      with conf_a' eval_args 
  1.2560 -      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
  1.2561 -	by (auto dest: eval_gext intro: conf_gext)
  1.2562 +      note normal_s1 = this
  1.2563 +      obtain A' where 
  1.2564 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  1.2565 +      proof -
  1.2566 +	from eval_e wt_e da_e wf normal_s1
  1.2567 +	have "nrm E \<subseteq>  dom (locals (store s1))"
  1.2568 +	  by (cases rule: da_good_approxE') rules
  1.2569 +	with da_args show ?thesis
  1.2570 +	  by (rule da_weakenE) 
  1.2571 +      qed
  1.2572 +      with conf_s1 wt_args 
  1.2573 +      obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.2574 +              conf_args: "normal s2 
  1.2575 +                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  1.2576 +          error_free_s2: "error_free s2" 
  1.2577 +	by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  1.2578 +      from error_free_s2 init_lvars
  1.2579 +      have error_free_s3: "error_free s3"
  1.2580 +	by (auto simp add: init_lvars_def2)
  1.2581 +      from statM 
  1.2582 +      obtain
  1.2583 +	statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1.2584 +	pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1.2585 +	by (blast dest: max_spec2mheads)
  1.2586 +      from check
  1.2587 +      have eq_store_s3'_s3: "store s3'=store s3"
  1.2588 +	by (cases s3) (simp add: check_method_access_def Let_def)
  1.2589 +      obtain invC
  1.2590 +	where invC: "invC = invocation_class mode (store s2) a statT"
  1.2591 +	by simp
  1.2592 +      with init_lvars
  1.2593 +      have invC': "invC = (invocation_class mode (store s3) a statT)"
  1.2594 +	by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1.2595        show ?thesis
  1.2596 -      proof (cases "a'=Null \<longrightarrow> is_static statM")
  1.2597 +      proof (cases "normal s2")
  1.2598  	case False
  1.2599 -	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
  1.2600 -	  by blast
  1.2601 -	with normal_s2 init_lvars mode
  1.2602 -	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1.2603 -                   "store s3 = store (init_lvars G invDeclC 
  1.2604 -                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
  1.2605 -	  by (auto simp add: init_lvars_def2)
  1.2606 -	moreover
  1.2607 -	from np check
  1.2608 -	have eq_s3'_s3: "s3'=s3" 
  1.2609 -	  by (auto simp add: check_method_access_def Let_def)
  1.2610 -	moreover
  1.2611 -	from eq_s3'_s3 np eval_methd
  1.2612 -	have "s4=s3'"
  1.2613 +	with propagate_abnormal_s2 conf_s2 error_free_s2
  1.2614 +	show ?thesis
  1.2615  	  by auto
  1.2616 -	ultimately have
  1.2617 -	  "set_lvars (locals (store s2)) s4 
  1.2618 -           = (Some (Xcpt (Std NullPointer)),store s2)"
  1.2619 -	  by (cases s2) (cases s4, fastsimp simp add: init_lvars_def2)
  1.2620 -	with conf_s2 error_free_s2
  1.2621 -	show ?thesis
  1.2622 -	  by (cases s2) (auto dest: conforms_NormI)
  1.2623        next
  1.2624  	case True
  1.2625 -	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
  1.2626 -	  by (auto dest!: Null_staticD)
  1.2627 -	with conf_s2 conf_a'_s2 wf invC  
  1.2628 -	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1.2629 -	  by (cases s2) (auto intro: DynT_propI)
  1.2630 -	with wt_e statM' invC mode wf 
  1.2631 -	obtain dynM where 
  1.2632 -          dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.2633 -          acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1.2634 -                          in invC dyn_accessible_from accC"
  1.2635 -	  by (force dest!: call_access_ok)
  1.2636 -	with invC' check eq_accC_accC'
  1.2637 -	have eq_s3'_s3: "s3'=s3"
  1.2638 -	  by (auto simp add: check_method_access_def Let_def)
  1.2639 -	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1.2640 -	obtain 
  1.2641 -	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1.2642 -	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.2643 -           iscls_invDeclC: "is_class G invDeclC" and
  1.2644 -	        invDeclC': "invDeclC = declclass dynM" and
  1.2645 -	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1.2646 -	    resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1.2647 -	   is_static_eq: "is_static dynM = is_static statM" and
  1.2648 -	   involved_classes_prop:
  1.2649 +	note normal_s2 = True
  1.2650 +	with normal_s1 conf_a eval_args 
  1.2651 +	have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1.2652 +	  by (auto dest: eval_gext intro: conf_gext)
  1.2653 +	show ?thesis
  1.2654 +	proof (cases "a=Null \<longrightarrow> is_static statM")
  1.2655 +	  case False
  1.2656 +	  then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  1.2657 +	    by blast
  1.2658 +	  with normal_s2 init_lvars mode
  1.2659 +	  obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1.2660 +                     "store s3 = store (init_lvars G invDeclC 
  1.2661 +                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2)"
  1.2662 +	    by (auto simp add: init_lvars_def2)
  1.2663 +	  moreover
  1.2664 +	  from np check
  1.2665 +	  have eq_s3'_s3: "s3'=s3" 
  1.2666 +	    by (auto simp add: check_method_access_def Let_def)
  1.2667 +	  moreover
  1.2668 +	  from eq_s3'_s3 np eval_methd
  1.2669 +	  have "s4=s3'"
  1.2670 +	    by auto
  1.2671 +	  ultimately have
  1.2672 +	    "set_lvars (locals (store s2)) s4 
  1.2673 +            = (Some (Xcpt (Std NullPointer)),store s2)"
  1.2674 +	    by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.2675 +	  with conf_s2 error_free_s2
  1.2676 +	  show ?thesis
  1.2677 +	    by (cases s2) (auto dest: conforms_NormI)
  1.2678 +	next
  1.2679 +	  case True
  1.2680 +	  with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  1.2681 +	    by (auto dest!: Null_staticD)
  1.2682 +	  with conf_s2 conf_a_s2 wf invC  
  1.2683 +	  have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1.2684 +	    by (cases s2) (auto intro: DynT_propI)
  1.2685 +	  with wt_e statM' invC mode wf 
  1.2686 +	  obtain dynM where 
  1.2687 +            dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.2688 +            acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1.2689 +                            in invC dyn_accessible_from accC"
  1.2690 +	    by (force dest!: call_access_ok)
  1.2691 +	  with invC' check eq_accC_accC'
  1.2692 +	  have eq_s3'_s3: "s3'=s3"
  1.2693 +	    by (auto simp add: check_method_access_def Let_def)
  1.2694 +	  from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1.2695 +	  obtain 
  1.2696 +	    wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1.2697 +	      dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.2698 +            iscls_invDeclC: "is_class G invDeclC" and
  1.2699 +	         invDeclC': "invDeclC = declclass dynM" and
  1.2700 +	      invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1.2701 +	     resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1.2702 +	    is_static_eq: "is_static dynM = is_static statM" and
  1.2703 +	    involved_classes_prop:
  1.2704               "(if invmode statM e = IntVir
  1.2705                 then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1.2706                 else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1.2707                       (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1.2708                        statDeclT = ClassT invDeclC)"
  1.2709 -	  by (auto dest: DynT_mheadsD)
  1.2710 -	obtain L' where 
  1.2711 +	    by (cases rule: DynT_mheadsE) simp
  1.2712 +	  obtain L' where 
  1.2713  	   L':"L'=(\<lambda> k. 
  1.2714                   (case k of
  1.2715                      EName e
  1.2716 @@ -2028,73 +3201,148 @@
  1.2717                          | Res \<Rightarrow> Some (resTy dynM))
  1.2718                    | This \<Rightarrow> if is_static statM 
  1.2719                              then None else Some (Class invDeclC)))"
  1.2720 -	  by simp
  1.2721 -	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1.2722 -             wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
  1.2723 -	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1.2724 -	  apply - 
  1.2725 -             (* FIXME confomrs_init_lvars should be 
  1.2726 -                adjusted to be more directy applicable *)
  1.2727 -	  apply (drule conforms_init_lvars [of G invDeclC 
  1.2728 -                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1.2729 -                  L statT invC a' "(statDeclT,statM)" e])
  1.2730 -	  apply (rule wf)
  1.2731 -	  apply (rule conf_args,assumption)
  1.2732 -	  apply (simp add: pTs_widen)
  1.2733 -	  apply (cases s2,simp)
  1.2734 -	  apply (rule dynM')
  1.2735 -	  apply (force dest: ty_expr_is_type)
  1.2736 -	  apply (rule invC_widen)
  1.2737 -	  apply (force intro: conf_gext dest: eval_gext)
  1.2738 -	  apply simp
  1.2739 -	  apply simp
  1.2740 -	  apply (simp add: invC)
  1.2741 -	  apply (simp add: invDeclC)
  1.2742 -	  apply (force dest: wf_mdeclD1 is_acc_typeD)
  1.2743 -	  apply (cases s2, simp add: L' init_lvars
  1.2744 -	                      cong add: lname.case_cong ename.case_cong)
  1.2745 -	  done 
  1.2746 -	from  is_static_eq wf_dynM L'
  1.2747 -	obtain mthdT where
  1.2748 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.2749 -            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  1.2750 -	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1.2751 -	  by - (drule wf_mdecl_bodyD,
  1.2752 -                auto simp: cong add: lname.case_cong ename.case_cong)
  1.2753 -	with dynM' iscls_invDeclC invDeclC'
  1.2754 -	have
  1.2755 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.2756 -            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1.2757 -	  by (auto intro: wt.Methd)
  1.2758 -	with eq_s3'_s3 conf_s3 error_free_s3 
  1.2759 -             hyp_methd [of L' invDeclC "Inl mthdT"]
  1.2760 -	obtain  conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  1.2761 -	       conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  1.2762 -	  error_free_s4: "error_free s4"
  1.2763 -	  by auto
  1.2764 -	from init_lvars eval_methd eq_s3'_s3 
  1.2765 -	have "store s2\<le>|store s4"
  1.2766 -	  by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  1.2767 -	with conf_s2 conf_s4
  1.2768 -	have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  1.2769 -	  by (cases s2,cases s4) (auto intro: conforms_return)
  1.2770 -	moreover 
  1.2771 -	from conf_Res mthdT_widen resTy_widen wf
  1.2772 -	have "normal s4 
  1.2773 -             \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  1.2774 -	  by (auto dest: widen_trans)
  1.2775 -	then
  1.2776 -	have "normal ((set_lvars (locals (store s2))) s4)
  1.2777 +	    by simp
  1.2778 +	  from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1.2779 +            wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  1.2780 +	  have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1.2781 +	    apply - 
  1.2782 +               (* FIXME confomrs_init_lvars should be 
  1.2783 +                  adjusted to be more directy applicable *)
  1.2784 +	    apply (drule conforms_init_lvars [of G invDeclC 
  1.2785 +                    "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1.2786 +                    L statT invC a "(statDeclT,statM)" e])
  1.2787 +	    apply (rule wf)
  1.2788 +	    apply (rule conf_args,assumption)
  1.2789 +	    apply (simp add: pTs_widen)
  1.2790 +	    apply (cases s2,simp)
  1.2791 +	    apply (rule dynM')
  1.2792 +	    apply (force dest: ty_expr_is_type)
  1.2793 +	    apply (rule invC_widen)
  1.2794 +	    apply (force intro: conf_gext dest: eval_gext)
  1.2795 +	    apply simp
  1.2796 +	    apply simp
  1.2797 +	    apply (simp add: invC)
  1.2798 +	    apply (simp add: invDeclC)
  1.2799 +	    apply (simp add: normal_s2)
  1.2800 +	    apply (cases s2, simp add: L' init_lvars
  1.2801 +	                     cong add: lname.case_cong ename.case_cong)
  1.2802 +	    done
  1.2803 +	  with eq_s3'_s3 
  1.2804 +	  have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  1.2805 +	  moreover
  1.2806 +	  from  is_static_eq wf_dynM L'
  1.2807 +	  obtain mthdT where
  1.2808 +	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.2809 +               \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  1.2810 +	    mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1.2811 +	    by - (drule wf_mdecl_bodyD,
  1.2812 +                 auto simp add: callee_lcl_def  
  1.2813 +                      cong add: lname.case_cong ename.case_cong)
  1.2814 +	  with dynM' iscls_invDeclC invDeclC'
  1.2815 +	  have
  1.2816 +	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.2817 +               \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1.2818 +	    by (auto intro: wt.Methd)
  1.2819 +	  moreover
  1.2820 +	  obtain M where 
  1.2821 +	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  1.2822 +	       \<turnstile> dom (locals (store s3')) 
  1.2823 +	          \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  1.2824 +	  proof -
  1.2825 +	    from wf_dynM
  1.2826 +	    obtain M' where
  1.2827 +	      da_body: 
  1.2828 +	      "\<lparr>prg=G, cls=invDeclC
  1.2829 +               ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  1.2830 +               \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  1.2831 +              res: "Result \<in> nrm M'"
  1.2832 +	      by (rule wf_mdeclE) rules
  1.2833 +	    from da_body is_static_eq L' have
  1.2834 +	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.2835 +                 \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  1.2836 +	      by (simp add: callee_lcl_def  
  1.2837 +                  cong add: lname.case_cong ename.case_cong)
  1.2838 +	    moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  1.2839 +	    proof -
  1.2840 +	      from is_static_eq 
  1.2841 +	      have "(invmode (mthd dynM) e) = (invmode statM e)"
  1.2842 +		by (simp add: invmode_def)
  1.2843 +	      with init_lvars dynM' is_static_eq normal_s2 mode 
  1.2844 +	      have "parameters (mthd dynM) = dom (locals (store s3))"
  1.2845 +		using dom_locals_init_lvars 
  1.2846 +                  [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" e a vs s2]
  1.2847 +		by simp
  1.2848 +	      also from check
  1.2849 +	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  1.2850 +		by (simp add:  eq_s3'_s3)
  1.2851 +	      finally show ?thesis .
  1.2852 +	    qed
  1.2853 +	    ultimately obtain M2 where
  1.2854 +	      da:
  1.2855 +	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.2856 +                \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  1.2857 +              M2: "nrm M' \<subseteq> nrm M2"
  1.2858 +	      by (rule da_weakenE)
  1.2859 +	    from res M2 have "Result \<in> nrm M2"
  1.2860 +	      by blast
  1.2861 +	    moreover from wf_dynM
  1.2862 +	    have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  1.2863 +	      by (rule wf_mdeclE)
  1.2864 +	    ultimately
  1.2865 +	    obtain M3 where
  1.2866 +	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  1.2867 +                     \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  1.2868 +	      using da
  1.2869 +	      by (rules intro: da.Body assigned.select_convs)
  1.2870 +	    from _ this [simplified]
  1.2871 +	    show ?thesis
  1.2872 +	      by (rule da.Methd [simplified,elim_format])
  1.2873 +	         (auto intro: dynM')
  1.2874 +	  qed
  1.2875 +	  ultimately obtain  
  1.2876 +	    conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  1.2877 +	    conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  1.2878 +	    error_free_s4: "error_free s4"
  1.2879 +	    by (rule hyp_methd [elim_format]) 
  1.2880 +               (simp add: error_free_s3 eq_s3'_s3)
  1.2881 +	  from init_lvars eval_methd eq_s3'_s3 
  1.2882 +	  have "store s2\<le>|store s4"
  1.2883 +	    by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  1.2884 +	  moreover
  1.2885 +	  have "abrupt s4 \<noteq> Some (Jump Ret)"
  1.2886 +	  proof -
  1.2887 +	    from normal_s2 init_lvars
  1.2888 +	    have "abrupt s3 \<noteq> Some (Jump Ret)"
  1.2889 +	      by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  1.2890 +	    with check
  1.2891 +	    have "abrupt s3' \<noteq> Some (Jump Ret)"
  1.2892 +	      by (cases s3) (auto simp add: check_method_access_def Let_def)
  1.2893 +	    with eval_methd
  1.2894 +	    show ?thesis
  1.2895 +	      by (rule Methd_no_jump)
  1.2896 +	  qed
  1.2897 +	  ultimately 
  1.2898 +	  have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  1.2899 +	    using conf_s2 conf_s4
  1.2900 +	    by (cases s2,cases s4) (auto intro: conforms_return)
  1.2901 +	  moreover 
  1.2902 +	  from conf_Res mthdT_widen resTy_widen wf
  1.2903 +	  have "normal s4 
  1.2904 +                  \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  1.2905 +	    by (auto dest: widen_trans)
  1.2906 +	  then
  1.2907 +	  have "normal ((set_lvars (locals (store s2))) s4)
  1.2908               \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  1.2909 -	  by (cases s4) auto
  1.2910 -	moreover note error_free_s4 T
  1.2911 -	ultimately 
  1.2912 -	show ?thesis
  1.2913 -	  by simp
  1.2914 +	    by (cases s4) auto
  1.2915 +	  moreover note error_free_s4 T
  1.2916 +	  ultimately 
  1.2917 +	  show ?thesis
  1.2918 +	    by simp
  1.2919 +	qed
  1.2920        qed
  1.2921      qed
  1.2922    next
  1.2923 -    case (Methd D s0 s1 sig v L accC T)
  1.2924 +    case (Methd D s0 s1 sig v L accC T A)
  1.2925      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
  1.2926      have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
  1.2927      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.2928 @@ -2106,15 +3354,22 @@
  1.2929                    \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  1.2930        T: "T=Inl bodyT"
  1.2931        by (rule wt_elim_cases) auto
  1.2932 -    with hyp [of _ _ "(Inl bodyT)"] conf_s0 
  1.2933 +    moreover
  1.2934 +    from Methd.prems m have 
  1.2935 +       da_body: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2936 +                   \<turnstile> (dom (locals (store ((Norm s0)::state))))
  1.2937 +                       \<guillemotright>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<guillemotright> A"
  1.2938 +      by - (erule da_elim_cases,simp)
  1.2939 +    ultimately
  1.2940      show "s1\<Colon>\<preceq>(G, L) \<and> 
  1.2941             (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  1.2942             (error_free (Norm s0) = error_free s1)"
  1.2943 +      using hyp [of _ _ "(Inl bodyT)"] conf_s0 
  1.2944        by (auto simp add: Let_def body_def)
  1.2945    next
  1.2946 -    case (Body D c s0 s1 s2 L accC T)
  1.2947 -    have "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  1.2948 -    have "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  1.2949 +    case (Body D c s0 s1 s2 s3 L accC T A)
  1.2950 +    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1" .
  1.2951 +    have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" .
  1.2952      have hyp_init: "PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>" .
  1.2953      have hyp_c: "PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>" .
  1.2954      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.2955 @@ -2126,12 +3381,35 @@
  1.2956        isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  1.2957                 T: "T=Inl bodyT"
  1.2958        by (rule wt_elim_cases) auto
  1.2959 -    from conf_s0 iscls_D hyp_init
  1.2960 -    obtain "s1\<Colon>\<preceq>(G, L)" "error_free s1"
  1.2961 -      by auto
  1.2962 -    with wt_c hyp_c
  1.2963 +    from Body.prems obtain C where
  1.2964 +      da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2965 +                   \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1r c\<guillemotright> C" and
  1.2966 +      jmpOk: "jumpNestingOkS {Ret} c" and
  1.2967 +      res: "Result \<in> nrm C"
  1.2968 +      by (elim da_elim_cases) simp
  1.2969 +    note conf_s0
  1.2970 +    moreover from iscls_D 
  1.2971 +    have "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init D\<Colon>\<surd>" by auto
  1.2972 +    moreover obtain I where 
  1.2973 +      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2974 +          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init D)\<guillemotright> I"
  1.2975 +      by (auto intro: da_Init [simplified] assigned.select_convs)
  1.2976 +    ultimately obtain
  1.2977 +      conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1:  "error_free s1"
  1.2978 +       by (rule hyp_init [elim_format]) simp
  1.2979 +    obtain C' where da_C': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.2980 +                             \<turnstile> (dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'"
  1.2981 +               and nrm_C': "nrm C \<subseteq> nrm C'"
  1.2982 +    proof -
  1.2983 +      from eval_init 
  1.2984 +      have "(dom (locals (store ((Norm s0)::state)))) 
  1.2985 +                     \<subseteq> (dom (locals (store s1)))"
  1.2986 +	by (rule dom_locals_eval_mono_elim)
  1.2987 +      with da_c show ?thesis by (rule da_weakenE)
  1.2988 +    qed
  1.2989 +    from conf_s1 wt_c da_C' 
  1.2990      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.2991 -      by blast
  1.2992 +      by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  1.2993      from conf_s2
  1.2994      have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  1.2995        by (cases s2) (auto intro: conforms_absorb)
  1.2996 @@ -2139,13 +3417,55 @@
  1.2997      from error_free_s2
  1.2998      have "error_free (abupd (absorb Ret) s2)"
  1.2999        by simp
  1.3000 +    moreover have "abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump Ret)"
  1.3001 +      by (cases s3) (simp add: absorb_def)
  1.3002 +    moreover have "s3=s2"
  1.3003 +    proof -
  1.3004 +      from iscls_D
  1.3005 +      have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
  1.3006 +	by auto
  1.3007 +      from eval_init wf
  1.3008 +      have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  1.3009 +	by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  1.3010 +      from eval_c _ wt_c wf
  1.3011 +      have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  1.3012 +	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  1.3013 +      moreover 
  1.3014 +      have "s3 =
  1.3015 +                (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  1.3016 +                        abrupt s2 = Some (Jump (Cont l))
  1.3017 +                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
  1.3018 +      ultimately show ?thesis 
  1.3019 +	by force
  1.3020 +    qed
  1.3021 +    moreover
  1.3022 +    {
  1.3023 +      assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
  1.3024 +      have "Result \<in> dom (locals (store s2))"
  1.3025 +      proof -
  1.3026 +	from normal_upd_s2
  1.3027 +	have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  1.3028 +	  by (cases s2) (simp add: absorb_def)
  1.3029 +	thus ?thesis
  1.3030 +	proof 
  1.3031 +	  assume "normal s2"
  1.3032 +	  with eval_c wt_c da_C' wf res nrm_C'
  1.3033 +	  show ?thesis
  1.3034 +	    by (cases rule: da_good_approxE') blast
  1.3035 +	next
  1.3036 +	  assume "abrupt s2 = Some (Jump Ret)"
  1.3037 +	  with conf_s2 show ?thesis
  1.3038 +	    by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  1.3039 +	qed 
  1.3040 +      qed
  1.3041 +    }
  1.3042      moreover note T resultT
  1.3043      ultimately
  1.3044 -    show "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L) \<and>
  1.3045 -           (normal (abupd (absorb Ret) s2) \<longrightarrow>
  1.3046 -             G,L,store (abupd (absorb Ret) s2)
  1.3047 +    show "abupd (absorb Ret) s3\<Colon>\<preceq>(G, L) \<and>
  1.3048 +           (normal (abupd (absorb Ret) s3) \<longrightarrow>
  1.3049 +             G,L,store (abupd (absorb Ret) s3)
  1.3050               \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  1.3051 -          (error_free (Norm s0) = error_free (abupd (absorb Ret) s2)) "
  1.3052 +          (error_free (Norm s0) = error_free (abupd (absorb Ret) s3)) "
  1.3053        by (cases s2) (auto intro: conforms_locals)
  1.3054    next
  1.3055      case (LVar s vn L accC T)
  1.3056 @@ -2156,9 +3476,9 @@
  1.3057          T: "T=Inl vnT"
  1.3058        by (auto elim!: wt_elim_cases)
  1.3059      from conf_s vnT
  1.3060 -    have conf_fst: "G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  1.3061 -      by (auto elim: conforms_localD [THEN lconfD]  
  1.3062 -               simp add: lvar_def)
  1.3063 +    have conf_fst: "locals s vn \<noteq> None \<longrightarrow> G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  1.3064 +     by (auto elim: conforms_localD [THEN wlconfD]  
  1.3065 +              simp add: lvar_def) 
  1.3066      moreover
  1.3067      from conf_s conf_fst vnT 
  1.3068      have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  1.3069 @@ -2169,9 +3489,9 @@
  1.3070                   (normal (Norm s) \<longrightarrow>
  1.3071                      G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  1.3072                   (error_free (Norm s) = error_free (Norm s))"
  1.3073 -      by simp 
  1.3074 +      by (simp add: lvar_def) 
  1.3075    next
  1.3076 -    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
  1.3077 +    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T A)
  1.3078      have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  1.3079      have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  1.3080      have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  1.3081 @@ -2187,22 +3507,42 @@
  1.3082                  stat: "stat=is_static f" and
  1.3083  	           T: "T=(Inl (type f))"
  1.3084        by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  1.3085 +    from FVar.prems eq_accC_accC'
  1.3086 +    have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.3087 +                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> A"
  1.3088 +      by (elim da_elim_cases) simp
  1.3089 +    note conf_s0
  1.3090 +    moreover
  1.3091      from wf wt_e 
  1.3092      have iscls_statC: "is_class G statC"
  1.3093        by (auto dest: ty_expr_is_type type_is_class)
  1.3094      with wf accfield 
  1.3095      have iscls_statDeclC: "is_class G statDeclC"
  1.3096        by (auto dest!: accfield_fields dest: fields_declC)
  1.3097 -    with conf_s0 hyp_init
  1.3098 +    hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  1.3099 +      by simp
  1.3100 +    moreover obtain I where 
  1.3101 +      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.3102 +        \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init statDeclC)\<guillemotright> I"
  1.3103 +      by (auto intro: da_Init [simplified] assigned.select_convs)
  1.3104 +    ultimately 
  1.3105      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1.3106 -      by auto
  1.3107 -    from conf_s1 wt_e hyp_e
  1.3108 +      by (rule hyp_init [elim_format]) simp
  1.3109 +    obtain A' where 
  1.3110 +      "\<lparr>prg=G, cls=accC, lcl=L\<rparr> \<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e\<guillemotright> A'"
  1.3111 +    proof -
  1.3112 +      from eval_init
  1.3113 +      have "(dom (locals (store ((Norm s0)::state)))) 
  1.3114 +	       \<subseteq> (dom (locals (store s1)))"
  1.3115 +	by (rule dom_locals_eval_mono_elim)
  1.3116 +      with da_e show ?thesis
  1.3117 +	by (rule da_weakenE)
  1.3118 +    qed
  1.3119 +    with conf_s1 wt_e 
  1.3120      obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.3121 -                  conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" 
  1.3122 -      by force
  1.3123 -    from conf_s1 wt_e error_free_s1 hyp_e
  1.3124 -    have error_free_s2: "error_free s2"
  1.3125 -      by auto
  1.3126 +                  conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  1.3127 +           error_free_s2: "error_free s2"
  1.3128 +      by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.3129      from fvar 
  1.3130      have store_s2': "store s2'=store s2"
  1.3131        by (cases s2) (simp add: fvar_def2)
  1.3132 @@ -2267,7 +3607,7 @@
  1.3133            (error_free (Norm s0) = error_free s3)"
  1.3134        by auto
  1.3135    next
  1.3136 -    case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
  1.3137 +    case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T A)
  1.3138      have eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1" .
  1.3139      have eval_e2: "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2" .
  1.3140      have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)" .
  1.3141 @@ -2276,67 +3616,98 @@
  1.3142      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.3143      have wt:  "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T" .
  1.3144      then obtain elemT
  1.3145 -       where wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  1.3146 -             wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  1.3147 +       where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  1.3148 +             wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  1.3149                   T: "T= Inl elemT"
  1.3150        by (rule wt_elim_cases) auto
  1.3151 -    from  conf_s0 wt_e1 hyp_e1 
  1.3152 +    from AVar.prems obtain E1 where
  1.3153 +      da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.3154 +                \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e1\<guillemotright> E1" and
  1.3155 +      da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>In1l e2\<guillemotright> A" 
  1.3156 +      by (elim da_elim_cases) simp
  1.3157 +    from conf_s0 wt_e1 da_e1  
  1.3158      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1.3159              conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  1.3160              error_free_s1: "error_free s1"
  1.3161 -      by force
  1.3162 -    from conf_s1 error_free_s1 wt_e2 hyp_e2
  1.3163 -    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.3164 -      by blast
  1.3165 -    from avar 
  1.3166 -    have "store s2'=store s2"
  1.3167 -      by (cases s2) (simp add: avar_def2)
  1.3168 -    with avar conf_s2 
  1.3169 -    have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1.3170 -      by (cases s2) (auto simp add: avar_def2)
  1.3171 -    from avar error_free_s2
  1.3172 -    have error_free_s2': "error_free s2'"
  1.3173 -      by (cases s2) (auto simp add: avar_def2 )
  1.3174 -    have "normal s2' \<Longrightarrow> 
  1.3175 -           G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.3176 -    proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  1.3177 -      assume normal: "normal s2'"
  1.3178 -      show ?thesis
  1.3179 -      proof -
  1.3180 -	obtain vv vf x1 store1 x2 store2 store2'
  1.3181 -	   where  v: "v=(vv,vf)" and
  1.3182 -                 s1: "s1=(x1,store1)" and
  1.3183 -                 s2: "s2=(x2,store2)" and
  1.3184 -	    store2': "store2'=store s2'"
  1.3185 -	  by (cases v,cases s1, cases s2, cases s2') blast 
  1.3186 -	have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.3187 -	proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  1.3188 -                                 OF wf])
  1.3189 -	  from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  1.3190 -	    by simp
  1.3191 -	  from v normal s2 store2' avar 
  1.3192 -	  show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  1.3193 -	    by auto
  1.3194 -	  from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.3195 -	  from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  1.3196 -	  from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  1.3197 -	qed
  1.3198 -	with v s1 s2 store2' 
  1.3199 -	show ?thesis
  1.3200 -	  by simp
  1.3201 -      qed
  1.3202 -    qed
  1.3203 -    with conf_s2' error_free_s2' T 
  1.3204 +      by (rule hyp_e1 [elim_format]) simp
  1.3205      show "s2'\<Colon>\<preceq>(G, L) \<and>
  1.3206             (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  1.3207             (error_free (Norm s0) = error_free s2') "
  1.3208 -      by auto
  1.3209 +    proof (cases "normal s1")
  1.3210 +      case False
  1.3211 +      moreover
  1.3212 +      from False eval_e2 have eq_s2_s1: "s2=s1" by auto
  1.3213 +      moreover
  1.3214 +      from eq_s2_s1 False have  "\<not> normal s2" by simp
  1.3215 +      then have "snd (avar G i a s2) = s2"
  1.3216 +	by (cases s2) (simp add: avar_def2)
  1.3217 +      with avar have "s2'=s2"
  1.3218 +	by (cases "(avar G i a s2)") simp
  1.3219 +      ultimately show ?thesis
  1.3220 +	using conf_s1 error_free_s1
  1.3221 +	by auto
  1.3222 +    next
  1.3223 +      case True
  1.3224 +      obtain A' where 
  1.3225 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  1.3226 +      proof -
  1.3227 +	from eval_e1 wt_e1 da_e1 wf True
  1.3228 +	have "nrm E1 \<subseteq> dom (locals (store s1))"
  1.3229 +	  by (cases rule: da_good_approxE') rules
  1.3230 +	with da_e2 show ?thesis
  1.3231 +	  by (rule da_weakenE)
  1.3232 +      qed
  1.3233 +      with conf_s1 wt_e2
  1.3234 +      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.3235 +	by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.3236 +      from avar 
  1.3237 +      have "store s2'=store s2"
  1.3238 +	by (cases s2) (simp add: avar_def2)
  1.3239 +      with avar conf_s2 
  1.3240 +      have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1.3241 +	by (cases s2) (auto simp add: avar_def2)
  1.3242 +      from avar error_free_s2
  1.3243 +      have error_free_s2': "error_free s2'"
  1.3244 +	by (cases s2) (auto simp add: avar_def2 )
  1.3245 +      have "normal s2' \<Longrightarrow> 
  1.3246 +        G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.3247 +      proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  1.3248 +	assume normal: "normal s2'"
  1.3249 +	show ?thesis
  1.3250 +	proof -
  1.3251 +	  obtain vv vf x1 store1 x2 store2 store2'
  1.3252 +	    where  v: "v=(vv,vf)" and
  1.3253 +                  s1: "s1=(x1,store1)" and
  1.3254 +                  s2: "s2=(x2,store2)" and
  1.3255 +	     store2': "store2'=store s2'"
  1.3256 +	    by (cases v,cases s1, cases s2, cases s2') blast 
  1.3257 +	  have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.3258 +	  proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  1.3259 +                                  OF wf])
  1.3260 +	    from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  1.3261 +	      by simp
  1.3262 +	    from v normal s2 store2' avar 
  1.3263 +	    show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  1.3264 +	      by auto
  1.3265 +	    from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.3266 +	    from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  1.3267 +	    from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  1.3268 +	  qed
  1.3269 +	  with v s1 s2 store2' 
  1.3270 +	  show ?thesis
  1.3271 +	    by simp
  1.3272 +	qed
  1.3273 +      qed
  1.3274 +      with conf_s2' error_free_s2' T 
  1.3275 +      show ?thesis 
  1.3276 +	by auto
  1.3277 +    qed
  1.3278    next
  1.3279      case (Nil s0 L accC T)
  1.3280      then show ?case
  1.3281        by (auto elim!: wt_elim_cases)
  1.3282    next
  1.3283 -    case (Cons e es s0 s1 s2 v vs L accC T)
  1.3284 +    case (Cons e es s0 s1 s2 v vs L accC T A)
  1.3285      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  1.3286      have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .
  1.3287      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)" .
  1.3288 @@ -2348,27 +3719,50 @@
  1.3289         wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  1.3290         T: "T=Inr (eT#esT)"
  1.3291        by (rule wt_elim_cases) blast
  1.3292 -    from hyp_e [OF conf_s0 wt_e]
  1.3293 +    from Cons.prems obtain E where
  1.3294 +      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.3295 +                \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  1.3296 +      da_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 es\<guillemotright> A" 
  1.3297 +      by (elim da_elim_cases) simp
  1.3298 +    from conf_s0 wt_e da_e 
  1.3299      obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  1.3300        conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  1.3301 -      by auto
  1.3302 -    from eval_es conf_v 
  1.3303 -    have conf_v': "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.3304 -      apply clarify
  1.3305 -      apply (rule conf_gext)
  1.3306 -      apply (auto dest: eval_gext)
  1.3307 -      done
  1.3308 -    from hyp_es [OF conf_s1 wt_es] error_free_s1 
  1.3309 -    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.3310 -           error_free_s2: "error_free s2" and
  1.3311 -           conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  1.3312 -      by auto
  1.3313 -    with conf_v' T
  1.3314 +      by (rule hyp_e [elim_format]) simp
  1.3315      show 
  1.3316        "s2\<Colon>\<preceq>(G, L) \<and> 
  1.3317        (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  1.3318 -      (error_free (Norm s0) = error_free s2) "
  1.3319 -      by auto
  1.3320 +      (error_free (Norm s0) = error_free s2)"
  1.3321 +    proof (cases "normal s1")
  1.3322 +      case False
  1.3323 +      with eval_es have "s2=s1" by auto
  1.3324 +      with False conf_s1 error_free_s1
  1.3325 +      show ?thesis
  1.3326 +	by auto
  1.3327 +    next
  1.3328 +      case True
  1.3329 +      obtain A' where 
  1.3330 +	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  1.3331 +      proof -
  1.3332 +	from eval_e wt_e da_e wf True
  1.3333 +	have "nrm E \<subseteq> dom (locals (store s1))"
  1.3334 +	  by (cases rule: da_good_approxE') rules
  1.3335 +	with da_es show ?thesis
  1.3336 +	  by (rule da_weakenE)
  1.3337 +      qed
  1.3338 +      with conf_s1 wt_es
  1.3339 +      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.3340 +           error_free_s2: "error_free s2" and
  1.3341 +           conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  1.3342 +	by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  1.3343 +      moreover
  1.3344 +      from True eval_es conf_v 
  1.3345 +      have conf_v': "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.3346 +	apply clarify
  1.3347 +	apply (rule conf_gext)
  1.3348 +	apply (auto dest: eval_gext)
  1.3349 +	done
  1.3350 +      ultimately show ?thesis using T by simp
  1.3351 +    qed
  1.3352    qed
  1.3353    then show ?thesis .
  1.3354  qed
  1.3355 @@ -2378,48 +3772,66 @@
  1.3356  
  1.3357  *} (* dummy text command to break paragraph for latex;
  1.3358                large paragraphs exhaust memory of debian pdflatex *)
  1.3359 +
  1.3360 +corollary eval_type_soundE [consumes 5]:
  1.3361 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  1.3362 +  and     conf: "s0\<Colon>\<preceq>(G, L)"
  1.3363 +  and       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>t\<Colon>T"
  1.3364 +  and       da: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile> dom (locals (snd s0)) \<guillemotright>t\<guillemotright> A"
  1.3365 +  and       wf: "wf_prog G"
  1.3366 +  and     elim: "\<lbrakk>s1\<Colon>\<preceq>(G, L); normal s1 \<Longrightarrow> G,L,snd s1\<turnstile>t\<succ>v\<Colon>\<preceq>T; 
  1.3367 +                  error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
  1.3368 +  shows "P"
  1.3369 +using eval wt da wf conf
  1.3370 +by (rule eval_type_sound [elim_format]) (rules intro: elim) 
  1.3371 +
  1.3372   
  1.3373  corollary eval_ts: 
  1.3374 - "\<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> 
  1.3375 + "\<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;
  1.3376 +   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1l e\<guillemotright>A\<rbrakk> 
  1.3377  \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  1.3378       (error_free s = error_free s')"
  1.3379 -apply (drule (3) eval_type_sound)
  1.3380 +apply (drule (4) eval_type_sound)
  1.3381  apply clarsimp
  1.3382  done
  1.3383  
  1.3384  corollary evals_ts: 
  1.3385 -"\<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> 
  1.3386 +"\<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;
  1.3387 +  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In3 es\<guillemotright>A\<rbrakk> 
  1.3388  \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  1.3389       (error_free s = error_free s')" 
  1.3390 -apply (drule (3) eval_type_sound)
  1.3391 +apply (drule (4) eval_type_sound)
  1.3392  apply clarsimp
  1.3393  done
  1.3394  
  1.3395  corollary evar_ts: 
  1.3396 -"\<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>  
  1.3397 +"\<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;
  1.3398 + \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In2 v\<guillemotright>A\<rbrakk> \<Longrightarrow>  
  1.3399    s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  1.3400    (error_free s = error_free s')"
  1.3401 -apply (drule (3) eval_type_sound)
  1.3402 +apply (drule (4) eval_type_sound)
  1.3403  apply clarsimp
  1.3404  done
  1.3405  
  1.3406  theorem exec_ts: 
  1.3407 -"\<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> 
  1.3408 +"\<lbrakk>G\<turnstile>s \<midarrow>c\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  1.3409 + \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1r c\<guillemotright>A\<rbrakk> 
  1.3410   \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  1.3411 -apply (drule (3) eval_type_sound)
  1.3412 +apply (drule (4) eval_type_sound)
  1.3413  apply clarsimp
  1.3414  done
  1.3415  
  1.3416  lemma wf_eval_Fin: 
  1.3417 -  assumes wf:    "wf_prog G" and
  1.3418 -          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
  1.3419 -        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
  1.3420 -        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
  1.3421 -        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
  1.3422 -            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  1.3423 +  assumes wf:    "wf_prog G" 
  1.3424 +    and   wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)"
  1.3425 +    and   da_c1: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store (Norm s0)))\<guillemotright>In1r c1\<guillemotright>A"
  1.3426 +    and conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" 
  1.3427 +    and eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" 
  1.3428 +    and eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" 
  1.3429 +    and      s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  1.3430    shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
  1.3431  proof -
  1.3432 -  from eval_c1 wt_c1 wf conf_s0
  1.3433 +  from eval_c1 wt_c1 da_c1 wf conf_s0
  1.3434    have "error_free (x1,s1)"
  1.3435      by (auto dest: eval_type_sound)
  1.3436    with eval_c1 eval_c2 s3
  1.3437 @@ -2427,4 +3839,209 @@
  1.3438      by - (rule eval.Fin, auto simp add: error_free_def)
  1.3439  qed
  1.3440  
  1.3441 +subsection "Ideas for the future"
  1.3442 +
  1.3443 +text {* In the type soundness proof and the correctness proof of 
  1.3444 +definite assignment we perform induction on the evaluation relation with the 
  1.3445 +further preconditions that the term is welltyped and definitely assigned. During
  1.3446 +the proofs we have to establish the welltypedness and definite assignment of 
  1.3447 +the subterms to be able to apply the induction hypothesis. So large parts of
  1.3448 +both proofs are the same work in propagating welltypedness and definite 
  1.3449 +assignment. So we can derive a new induction rule for induction on the 
  1.3450 +evaluation of a wellformed term, were these propagations is already done, once
  1.3451 +and forever. 
  1.3452 +Then we can do the proofs with this rule and can enjoy the time we have saved.
  1.3453 +Here is a first and incomplete sketch of such a rule.*}
  1.3454 +theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab 
  1.3455 +                                Comp If]:
  1.3456 +  assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1.3457 +   and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  1.3458 +   and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  1.3459 +   and      wf: "wf_prog G" 
  1.3460 +   and  abrupt: "\<And> s t abr L accC T A. 
  1.3461 +                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
  1.3462 +                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
  1.3463 +                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
  1.3464 +   and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
  1.3465 +   and    expr: "\<And> e s0 s1 v L accC eT E.
  1.3466 +                 \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
  1.3467 +                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.3468 +                     \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E;
  1.3469 +                  P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1\<rbrakk> 
  1.3470 +                 \<Longrightarrow>  P L accC (Norm s0) \<langle>Expr e\<rangle>\<^sub>s \<diamondsuit> s1"
  1.3471 +   and     lab: "\<And> c l s0 s1 L accC C.
  1.3472 +                 \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  1.3473 +                  \<lparr>prg=G,cls=accC, lcl=L\<rparr>
  1.3474 +                     \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
  1.3475 +                  P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1\<rbrakk>
  1.3476 +                  \<Longrightarrow> P L accC (Norm s0) \<langle>l\<bullet> c\<rangle>\<^sub>s \<diamondsuit> (abupd (absorb l) s1)"
  1.3477 +   and    comp: "\<And> c1 c2 s0 s1 s2 L accC C1.
  1.3478 +                 \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;G\<turnstile>s1 \<midarrow>c2 \<rightarrow> s2;
  1.3479 +                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>;
  1.3480 +                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>;
  1.3481 +                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.3482 +                     dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1;
  1.3483 +                  P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1;
  1.3484 +                  \<And> Q. \<lbrakk>normal s1; 
  1.3485 +                         \<And> C2.\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.3486 +                                  \<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2;
  1.3487 +                               P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
  1.3488 +                        \<rbrakk> \<Longrightarrow> Q 
  1.3489 +                  \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  1.3490 +    and    if: "\<And> b c1 c2 e s0 s1 s2 L accC E.
  1.3491 +                \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
  1.3492 +                 G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
  1.3493 +                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
  1.3494 +                 \<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>;
  1.3495 +                 \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.3496 +                     dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E;
  1.3497 +                 P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1;
  1.3498 +                 \<And> Q. \<lbrakk>normal s1;
  1.3499 +                        \<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  1.3500 +                                   \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  1.3501 +                              P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  1.3502 +                              \<rbrakk> \<Longrightarrow> Q
  1.3503 +                       \<rbrakk> \<Longrightarrow> Q
  1.3504 +                \<rbrakk> \<Longrightarrow> P L accC (Norm s0) \<langle>If(e) c1 Else c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  1.3505 +   shows "P L accC s0 t v s1"  
  1.3506 +proof -
  1.3507 +  note inj_term_simps [simp]
  1.3508 +  from eval 
  1.3509 +  show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  1.3510 +                       \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  1.3511 +        \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
  1.3512 +  proof (induct)
  1.3513 +    case Abrupt with abrupt show ?case .
  1.3514 +  next
  1.3515 +    case Skip from skip show ?case by simp
  1.3516 +  next
  1.3517 +    case (Expr e s0 s1 v L accC T A) 
  1.3518 +    from Expr.prems obtain eT where 
  1.3519 +      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
  1.3520 +      by (elim wt_elim_cases) 
  1.3521 +    moreover
  1.3522 +    from Expr.prems obtain E where
  1.3523 +      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E"
  1.3524 +      by (elim da_elim_cases) simp
  1.3525 +    moreover from calculation
  1.3526 +    have "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1"
  1.3527 +      by (rule Expr.hyps) 
  1.3528 +    ultimately show ?case
  1.3529 +      by (rule expr)
  1.3530 +  next
  1.3531 +    case (Lab c l s0 s1 L accC T A)
  1.3532 +    from Lab.prems 
  1.3533 +    have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1.3534 +      by (elim wt_elim_cases)
  1.3535 +    moreover
  1.3536 +    from Lab.prems obtain C where
  1.3537 +      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C"
  1.3538 +      by (elim da_elim_cases) simp
  1.3539 +    moreover from calculation
  1.3540 +    have "P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1"
  1.3541 +      by (rule  Lab.hyps)  
  1.3542 +    ultimately show ?case
  1.3543 +      by (rule lab)
  1.3544 +  next
  1.3545 +    case (Comp c1 c2 s0 s1 s2 L accC T A) 
  1.3546 +    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.3547 +    have eval_c2: "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  1.3548 +    from Comp.prems obtain 
  1.3549 +      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.3550 +      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1.3551 +      by (elim wt_elim_cases) 
  1.3552 +    from Comp.prems
  1.3553 +    obtain C1 C2
  1.3554 +      where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  1.3555 +                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and 
  1.3556 +            da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2" 
  1.3557 +      by (elim da_elim_cases) simp
  1.3558 +    from wt_c1 da_c1
  1.3559 +    have P_c1: "P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1"
  1.3560 +      by (rule Comp.hyps)
  1.3561 +    {
  1.3562 +      fix Q
  1.3563 +      assume normal_s1: "normal s1"
  1.3564 +      assume elim: "\<And> C2'. 
  1.3565 +                    \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright>C2';
  1.3566 +                       P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
  1.3567 +      have Q
  1.3568 +      proof -
  1.3569 +	obtain C2' where 
  1.3570 +	  da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  1.3571 +	proof -
  1.3572 +	  from eval_c1 wt_c1 da_c1 wf normal_s1
  1.3573 +	  have "nrm C1 \<subseteq> dom (locals (store s1))"
  1.3574 +	    by (cases rule: da_good_approxE') rules
  1.3575 +	  with da_c2 show ?thesis
  1.3576 +	    by (rule da_weakenE)
  1.3577 +	qed
  1.3578 +	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.3579 +	  by (rule Comp.hyps)
  1.3580 +	with da show ?thesis
  1.3581 +	  using elim by rules
  1.3582 +      qed
  1.3583 +    }
  1.3584 +    with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
  1.3585 +    show ?case
  1.3586 +      by (rule comp) rules+
  1.3587 +  next
  1.3588 +    case (If b c1 c2 e s0 s1 s2 L accC T A)
  1.3589 +    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1.3590 +    have eval_then_else: "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  1.3591 +    from If.prems
  1.3592 +    obtain 
  1.3593 +              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1.3594 +      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1.3595 +      by (elim wt_elim_cases) (auto split add: split_if)
  1.3596 +    from If.prems obtain E C where
  1.3597 +      da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  1.3598 +                                       \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  1.3599 +      da_then_else: 
  1.3600 +      "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.3601 +         (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  1.3602 +          \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C"
  1.3603 +      by (elim da_elim_cases) (cases "the_Bool b",auto)
  1.3604 +    from wt_e da_e
  1.3605 +    have P_e: "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1"
  1.3606 +      by (rule If.hyps)
  1.3607 +    {
  1.3608 +      fix Q
  1.3609 +      assume normal_s1: "normal s1"
  1.3610 +      assume elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  1.3611 +                                   \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  1.3612 +                              P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  1.3613 +                              \<rbrakk> \<Longrightarrow> Q"
  1.3614 +      have Q
  1.3615 +      proof -
  1.3616 +	obtain C' where
  1.3617 +	  da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.3618 +                (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
  1.3619 +	proof -
  1.3620 +	  from eval_e have 
  1.3621 +	    "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.3622 +	    by (rule dom_locals_eval_mono_elim)
  1.3623 +          moreover
  1.3624 +	  from eval_e normal_s1 wt_e 
  1.3625 +	  have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.3626 +	    by (rule assigns_if_good_approx')
  1.3627 +	  ultimately 
  1.3628 +	  have "dom (locals (store ((Norm s0)::state))) 
  1.3629 +            \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.3630 +	    by (rule Un_least)
  1.3631 +	  with da_then_else show ?thesis
  1.3632 +	    by (rule da_weakenE)
  1.3633 +	qed
  1.3634 +	with wt_then_else
  1.3635 +	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.3636 +	  by (rule If.hyps)
  1.3637 +	with da show ?thesis using elim by rules
  1.3638 +      qed
  1.3639 +    }
  1.3640 +    with eval_e eval_then_else wt_e wt_then_else da_e P_e
  1.3641 +    show ?case
  1.3642 +      by (rule if) rules+
  1.3643 +  next
  1.3644 +    oops
  1.3645 +
  1.3646  end