src/HOL/Bali/TypeSafe.thy
changeset 32960 69916a850301
parent 32693 6c6b1ba5e71e
child 35069 09154b995ed8
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -366,12 +366,12 @@
     1.4        case CInst
     1.5        with modeIntVir obj_props
     1.6        show ?thesis 
     1.7 -	by (auto dest!: widen_Array2 split add: split_if)
     1.8 +        by (auto dest!: widen_Array2 split add: split_if)
     1.9      next
    1.10        case Arr
    1.11        from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
    1.12        moreover from Arr have "obj_class obj = Object" 
    1.13 -	by (blast dest: obj_class_Arr1)
    1.14 +        by (blast dest: obj_class_Arr1)
    1.15        moreover note modeIntVir obj_props wf 
    1.16        ultimately show ?thesis by (auto dest!: widen_Array )
    1.17      qed
    1.18 @@ -411,22 +411,22 @@
    1.19        case Static
    1.20        with wf dynlookup statI is_iface 
    1.21        show ?thesis
    1.22 -	by (auto simp add: invocation_declclass_def dynlookup_def 
    1.23 +        by (auto simp add: invocation_declclass_def dynlookup_def 
    1.24                             dynimethd_def dynmethd_C_C 
    1.25 -	            intro: dynmethd_declclass
    1.26 -	            dest!: wf_imethdsD
    1.27 +                    intro: dynmethd_declclass
    1.28 +                    dest!: wf_imethdsD
    1.29                       dest: table_of_map_SomeI
    1.30                      split: split_if_asm)
    1.31 -    next	
    1.32 +    next        
    1.33        case SuperM
    1.34        with not_SuperM show ?thesis ..
    1.35      next
    1.36        case IntVir
    1.37        with wf dynlookup IfaceT invC_prop show ?thesis 
    1.38 -	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.39 +        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.40                             DynT_prop_def
    1.41 -	            intro: methd_declclass dynmethd_declclass
    1.42 -	            split: split_if_asm)
    1.43 +                    intro: methd_declclass dynmethd_declclass
    1.44 +                    split: split_if_asm)
    1.45      qed
    1.46    next
    1.47      case ClassT
    1.48 @@ -445,9 +445,9 @@
    1.49        case IntVir
    1.50        with wf ClassT dynlookup statC_prop invC_prop 
    1.51        show ?thesis
    1.52 -	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.53 +        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.54                             DynT_prop_def
    1.55 -	            intro: dynmethd_declclass)
    1.56 +                    intro: dynmethd_declclass)
    1.57      qed
    1.58    next
    1.59      case ArrayT
    1.60 @@ -455,7 +455,7 @@
    1.61      proof (cases mode)
    1.62        case Static
    1.63        with wf ArrayT dynlookup show ?thesis
    1.64 -	by (auto simp add: invocation_declclass_def dynlookup_def 
    1.65 +        by (auto simp add: invocation_declclass_def dynlookup_def 
    1.66                             dynimethd_def dynmethd_C_C
    1.67                      intro: dynmethd_declclass
    1.68                       dest: table_of_map_SomeI)
    1.69 @@ -465,7 +465,7 @@
    1.70      next
    1.71        case IntVir
    1.72        with wf ArrayT dynlookup invC_prop show ?thesis
    1.73 -	by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.74 +        by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
    1.75                             DynT_prop_def dynmethd_C_C
    1.76                      intro: dynmethd_declclass
    1.77                       dest: table_of_map_SomeI)
    1.78 @@ -564,8 +564,8 @@
    1.79                                              dynimethd_def)
    1.80      from sm wf wt_e not_Null False invC_prop' obtain "dm" where
    1.81                      dm: "methd G invC sig = Some dm"          and
    1.82 -	eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
    1.83 -	     eq_mheads:"sm=mhead (mthd dm) "
    1.84 +        eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
    1.85 +             eq_mheads:"sm=mhead (mthd dm) "
    1.86        by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
    1.87      then have static: "is_static dm = is_static sm" by - (auto)
    1.88      with declC invC dynlookup_static dm
    1.89 @@ -1339,24 +1339,24 @@
    1.90      proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
    1.91        case True
    1.92        with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
    1.93 -	by (fastsimp intro: Cons.hyps)
    1.94 +        by (fastsimp intro: Cons.hyps)
    1.95        with ys show ?thesis 
    1.96 -	by simp
    1.97 +        by simp
    1.98      next
    1.99        case False
   1.100        hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
   1.101        moreover
   1.102        from tabx_z tab_not_z
   1.103        have "(tab'(x\<mapsto>y)) vn = Some z" 
   1.104 -	by (rule map_upd_in_expansion_map_swap)
   1.105 +        by (rule map_upd_in_expansion_map_swap)
   1.106        ultimately
   1.107        have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
   1.108 -	by simp
   1.109 +        by simp
   1.110        hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
   1.111 -	by (rule map_upds_cong_ext)
   1.112 +        by (rule map_upds_cong_ext)
   1.113        with some ys
   1.114        show ?thesis 
   1.115 -	by simp
   1.116 +        by simp
   1.117      qed
   1.118    qed
   1.119  qed
   1.120 @@ -1460,12 +1460,12 @@
   1.121        case (EName en)
   1.122        show ?thesis
   1.123        proof (cases en)
   1.124 -	case Res
   1.125 -	with EName el_in_list show ?thesis by (simp add: dom_def)
   1.126 +        case Res
   1.127 +        with EName el_in_list show ?thesis by (simp add: dom_def)
   1.128        next
   1.129 -	case (VNam vn)
   1.130 -	with EName el_in_list show ?thesis 
   1.131 -	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
   1.132 +        case (VNam vn)
   1.133 +        with EName el_in_list show ?thesis 
   1.134 +          by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
   1.135        qed
   1.136      qed
   1.137    qed
   1.138 @@ -1482,12 +1482,12 @@
   1.139        case (EName en)
   1.140        show ?thesis
   1.141        proof (cases en)
   1.142 -	case Res
   1.143 -	with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
   1.144 +        case Res
   1.145 +        with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
   1.146        next
   1.147 -	case (VNam vn)
   1.148 -	with EName el_in_hd_tl show ?thesis 
   1.149 -	  by (auto simp add: dom_def intro: map_upds_Some_expand 
   1.150 +        case (VNam vn)
   1.151 +        with EName el_in_hd_tl show ?thesis 
   1.152 +          by (auto simp add: dom_def intro: map_upds_Some_expand 
   1.153                                              map_upds_Some_insert)
   1.154        qed
   1.155      qed
   1.156 @@ -1595,7 +1595,7 @@
   1.157      and wt_binop: "wt_binop G binop e1T e2T" 
   1.158      and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
   1.159      and normal_s1: "normal s1"
   1.160 -    and	eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
   1.161 +    and eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
   1.162      and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
   1.163      and wf: "wf_prog G"
   1.164    shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
   1.165 @@ -1625,62 +1625,62 @@
   1.166        assume condAnd: "binop=CondAnd"
   1.167        have ?thesis
   1.168        proof -
   1.169 -	from da obtain E2' where
   1.170 -	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.171 +        from da obtain E2' where
   1.172 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.173               \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
   1.174 -	  by cases (simp add: condAnd)+
   1.175 -	moreover
   1.176 -	have "dom (locals (store s0)) 
   1.177 +          by cases (simp add: condAnd)+
   1.178 +        moreover
   1.179 +        have "dom (locals (store s0)) 
   1.180            \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
   1.181 -	proof -
   1.182 -	  from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
   1.183 -	    by simp
   1.184 -	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.185 -	    by (auto dest: conf_Boolean)
   1.186 -	  with True condAnd
   1.187 -	  have v1: "v1=Bool True"
   1.188 -	    by simp
   1.189 -	  from eval_e1 normal_s1 
   1.190 -	  have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
   1.191 -	    by (rule assigns_if_good_approx' [elim_format])
   1.192 -	       (insert wt_e1, simp_all add: e1T v1)
   1.193 -	  with s0_s1 show ?thesis by (rule Un_least)
   1.194 -	qed
   1.195 -	ultimately
   1.196 -	show ?thesis
   1.197 -	  using that by (cases rule: da_weakenE) (simp add: True)
   1.198 +        proof -
   1.199 +          from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
   1.200 +            by simp
   1.201 +          with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.202 +            by (auto dest: conf_Boolean)
   1.203 +          with True condAnd
   1.204 +          have v1: "v1=Bool True"
   1.205 +            by simp
   1.206 +          from eval_e1 normal_s1 
   1.207 +          have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
   1.208 +            by (rule assigns_if_good_approx' [elim_format])
   1.209 +               (insert wt_e1, simp_all add: e1T v1)
   1.210 +          with s0_s1 show ?thesis by (rule Un_least)
   1.211 +        qed
   1.212 +        ultimately
   1.213 +        show ?thesis
   1.214 +          using that by (cases rule: da_weakenE) (simp add: True)
   1.215        qed
   1.216      }
   1.217      moreover
   1.218      { 
   1.219        assume condOr: "binop=CondOr"
   1.220        have ?thesis
   1.221 -	(* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
   1.222 +        (* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
   1.223        proof -
   1.224 -	from da obtain E2' where
   1.225 -	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.226 +        from da obtain E2' where
   1.227 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.228                \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
   1.229 -	  by cases (simp add: condOr)+
   1.230 -	moreover
   1.231 -	have "dom (locals (store s0)) 
   1.232 +          by cases (simp add: condOr)+
   1.233 +        moreover
   1.234 +        have "dom (locals (store s0)) 
   1.235                       \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
   1.236 -	proof -
   1.237 -	  from condOr wt_binop have e1T: "e1T=PrimT Boolean"
   1.238 -	    by simp
   1.239 -	  with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.240 -	    by (auto dest: conf_Boolean)
   1.241 -	  with True condOr
   1.242 -	  have v1: "v1=Bool False"
   1.243 -	    by simp
   1.244 -	  from eval_e1 normal_s1 
   1.245 -	  have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
   1.246 -	    by (rule assigns_if_good_approx' [elim_format])
   1.247 -	       (insert wt_e1, simp_all add: e1T v1)
   1.248 -	  with s0_s1 show ?thesis by (rule Un_least)
   1.249 -	qed
   1.250 -	ultimately
   1.251 -	show ?thesis
   1.252 -	  using that by (rule da_weakenE) (simp add: True)
   1.253 +        proof -
   1.254 +          from condOr wt_binop have e1T: "e1T=PrimT Boolean"
   1.255 +            by simp
   1.256 +          with normal_s1 conf_v1 obtain b where "v1=Bool b"
   1.257 +            by (auto dest: conf_Boolean)
   1.258 +          with True condOr
   1.259 +          have v1: "v1=Bool False"
   1.260 +            by simp
   1.261 +          from eval_e1 normal_s1 
   1.262 +          have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
   1.263 +            by (rule assigns_if_good_approx' [elim_format])
   1.264 +               (insert wt_e1, simp_all add: e1T v1)
   1.265 +          with s0_s1 show ?thesis by (rule Un_least)
   1.266 +        qed
   1.267 +        ultimately
   1.268 +        show ?thesis
   1.269 +          using that by (rule da_weakenE) (simp add: True)
   1.270        qed
   1.271      }
   1.272      moreover
   1.273 @@ -1688,16 +1688,16 @@
   1.274        assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
   1.275        have ?thesis
   1.276        proof -
   1.277 -	from da notAndOr obtain E1' where
   1.278 +        from da notAndOr obtain E1' where
   1.279            da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.280                    \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
   1.281 -	  and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
   1.282 -	  by cases simp+
   1.283 -	from eval_e1 wt_e1 da_e1 wf normal_s1 
   1.284 -	have "nrm E1' \<subseteq> dom (locals (store s1))"
   1.285 -	  by (cases rule: da_good_approxE') iprover
   1.286 -	with da_e2 show ?thesis
   1.287 -	  using that by (rule da_weakenE) (simp add: True)
   1.288 +          and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
   1.289 +          by cases simp+
   1.290 +        from eval_e1 wt_e1 da_e1 wf normal_s1 
   1.291 +        have "nrm E1' \<subseteq> dom (locals (store s1))"
   1.292 +          by (cases rule: da_good_approxE') iprover
   1.293 +        with da_e2 show ?thesis
   1.294 +          using that by (rule da_weakenE) (simp add: True)
   1.295        qed
   1.296      }
   1.297      ultimately show ?thesis
   1.298 @@ -1822,23 +1822,23 @@
   1.299        case False
   1.300        with eval_c2 have "s2=s1" by auto
   1.301        with conf_s1 error_free_s1 False wt show ?thesis
   1.302 -	by simp
   1.303 +        by simp
   1.304      next
   1.305        case True
   1.306        obtain C2' where 
   1.307 -	"\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
   1.308 +        "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
   1.309        proof -
   1.310 -	from eval_c1 wt_c1 da_c1 wf True
   1.311 -	have "nrm C1 \<subseteq> dom (locals (store s1))"
   1.312 -	  by (cases rule: da_good_approxE') iprover
   1.313 -	with da_c2 show thesis
   1.314 -	  by (rule da_weakenE) (rule that)
   1.315 +        from eval_c1 wt_c1 da_c1 wf True
   1.316 +        have "nrm C1 \<subseteq> dom (locals (store s1))"
   1.317 +          by (cases rule: da_good_approxE') iprover
   1.318 +        with da_c2 show thesis
   1.319 +          by (rule da_weakenE) (rule that)
   1.320        qed
   1.321        with conf_s1 wt_c2 
   1.322        obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
   1.323 -	by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
   1.324 +        by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
   1.325        thus ?thesis
   1.326 -	using wt by simp
   1.327 +        using wt by simp
   1.328      qed
   1.329    next
   1.330      case (If s0 e b s1 c1 c2 s2 L accC T A)
   1.331 @@ -1879,32 +1879,32 @@
   1.332        case False
   1.333        with eval_then_else have "s2=s1" by auto
   1.334        with conf_s1 error_free_s1 False wt show ?thesis
   1.335 -	by simp
   1.336 +        by simp
   1.337      next
   1.338        case True
   1.339        obtain C' where
   1.340 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
   1.341 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
   1.342            (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
   1.343        proof -
   1.344 -	from eval_e have 
   1.345 -	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
   1.346 -	  by (rule dom_locals_eval_mono_elim)
   1.347 +        from eval_e have 
   1.348 +          "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
   1.349 +          by (rule dom_locals_eval_mono_elim)
   1.350          moreover
   1.351 -	from eval_e True wt_e 
   1.352 -	have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
   1.353 -	  by (rule assigns_if_good_approx')
   1.354 -	ultimately 
   1.355 -	have "dom (locals (store ((Norm s0)::state))) 
   1.356 +        from eval_e True wt_e 
   1.357 +        have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
   1.358 +          by (rule assigns_if_good_approx')
   1.359 +        ultimately 
   1.360 +        have "dom (locals (store ((Norm s0)::state))) 
   1.361                  \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
   1.362 -	  by (rule Un_least)
   1.363 -	with da_then_else show thesis
   1.364 -	  by (rule da_weakenE) (rule that)
   1.365 +          by (rule Un_least)
   1.366 +        with da_then_else show thesis
   1.367 +          by (rule da_weakenE) (rule that)
   1.368        qed
   1.369        with conf_s1 wt_then_else  
   1.370        obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
   1.371 -	by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
   1.372 +        by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
   1.373        with wt show ?thesis
   1.374 -	by simp
   1.375 +        by simp
   1.376      qed
   1.377      -- {* Note that we don't have to show that @{term b} really is a boolean 
   1.378            value. With @{term the_Bool} we enforce to get a value of boolean 
   1.379 @@ -1945,106 +1945,106 @@
   1.380        note normal_s1 = this
   1.381        show ?thesis
   1.382        proof (cases "the_Bool b")
   1.383 -	case True
   1.384 -	with Loop.hyps  obtain
   1.385 +        case True
   1.386 +        with Loop.hyps  obtain
   1.387            eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
   1.388            eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   1.389 -	  by simp 
   1.390 -	have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
   1.391 -	  using Loop.hyps True by simp
   1.392 -	note hyp_c = this [rule_format]
   1.393 -	have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
   1.394 +          by simp 
   1.395 +        have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
   1.396 +          using Loop.hyps True by simp
   1.397 +        note hyp_c = this [rule_format]
   1.398 +        have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
   1.399            s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
   1.400 -	  using Loop.hyps True by simp
   1.401 -	note hyp_w = this [rule_format]
   1.402 -	from eval_e have 
   1.403 -	  s0_s1: "dom (locals (store ((Norm s0)::state)))
   1.404 +          using Loop.hyps True by simp
   1.405 +        note hyp_w = this [rule_format]
   1.406 +        from eval_e have 
   1.407 +          s0_s1: "dom (locals (store ((Norm s0)::state)))
   1.408                      \<subseteq> dom (locals (store s1))"
   1.409 -	  by (rule dom_locals_eval_mono_elim)
   1.410 -	obtain C' where
   1.411 -	  "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
   1.412 -	proof -
   1.413 -	  note s0_s1
   1.414 +          by (rule dom_locals_eval_mono_elim)
   1.415 +        obtain C' where
   1.416 +          "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
   1.417 +        proof -
   1.418 +          note s0_s1
   1.419            moreover
   1.420 -	  from eval_e normal_s1 wt_e 
   1.421 -	  have "assigns_if True e \<subseteq> dom (locals (store s1))"
   1.422 -	    by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
   1.423 -	  ultimately 
   1.424 -	  have "dom (locals (store ((Norm s0)::state))) 
   1.425 +          from eval_e normal_s1 wt_e 
   1.426 +          have "assigns_if True e \<subseteq> dom (locals (store s1))"
   1.427 +            by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
   1.428 +          ultimately 
   1.429 +          have "dom (locals (store ((Norm s0)::state))) 
   1.430                   \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
   1.431 -	    by (rule Un_least)
   1.432 -	  with da_c show thesis
   1.433 -	    by (rule da_weakenE) (rule that)
   1.434 -	qed
   1.435 -	with conf_s1 wt_c  
   1.436 -	obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
   1.437 -	  by (rule hyp_c [elim_format]) (simp add: error_free_s1)
   1.438 -	from error_free_s2 
   1.439 -	have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
   1.440 -	  by simp
   1.441 -	from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
   1.442 -	  by (cases s2) (auto intro: conforms_absorb)
   1.443 -	moreover note wt
   1.444 -	moreover
   1.445 -	obtain A' where 
   1.446 +            by (rule Un_least)
   1.447 +          with da_c show thesis
   1.448 +            by (rule da_weakenE) (rule that)
   1.449 +        qed
   1.450 +        with conf_s1 wt_c  
   1.451 +        obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
   1.452 +          by (rule hyp_c [elim_format]) (simp add: error_free_s1)
   1.453 +        from error_free_s2 
   1.454 +        have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
   1.455 +          by simp
   1.456 +        from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
   1.457 +          by (cases s2) (auto intro: conforms_absorb)
   1.458 +        moreover note wt
   1.459 +        moreover
   1.460 +        obtain A' where 
   1.461            "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
   1.462                dom (locals(store (abupd (absorb (Cont l)) s2)))
   1.463                  \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A'"
   1.464 -	proof -
   1.465 -	  note s0_s1
   1.466 -	  also from eval_c 
   1.467 -	  have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
   1.468 -	    by (rule dom_locals_eval_mono_elim)
   1.469 -	  also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
   1.470 -	    by simp
   1.471 -	  finally
   1.472 +        proof -
   1.473 +          note s0_s1
   1.474 +          also from eval_c 
   1.475 +          have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
   1.476 +            by (rule dom_locals_eval_mono_elim)
   1.477 +          also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
   1.478 +            by simp
   1.479 +          finally
   1.480            have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
   1.481 -	  with da show thesis
   1.482 -	    by (rule da_weakenE) (rule that)
   1.483 -	qed
   1.484 -	ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
   1.485 -	  by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
   1.486 -	with wt show ?thesis
   1.487 -	  by simp
   1.488 +          with da show thesis
   1.489 +            by (rule da_weakenE) (rule that)
   1.490 +        qed
   1.491 +        ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
   1.492 +          by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
   1.493 +        with wt show ?thesis
   1.494 +          by simp
   1.495        next
   1.496 -	case False
   1.497 -	with Loop.hyps have "s3=s1" by simp
   1.498 -	with conf_s1 error_free_s1 wt
   1.499 -	show ?thesis
   1.500 -	  by simp
   1.501 +        case False
   1.502 +        with Loop.hyps have "s3=s1" by simp
   1.503 +        with conf_s1 error_free_s1 wt
   1.504 +        show ?thesis
   1.505 +          by simp
   1.506        qed
   1.507      next
   1.508        case False
   1.509        have "s3=s1"
   1.510        proof -
   1.511 -	from False obtain abr where abr: "abrupt s1 = Some abr"
   1.512 -	  by (cases s1) auto
   1.513 -	from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
   1.514 -	  by (rule eval_expression_no_jump 
   1.515 +        from False obtain abr where abr: "abrupt s1 = Some abr"
   1.516 +          by (cases s1) auto
   1.517 +        from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
   1.518 +          by (rule eval_expression_no_jump 
   1.519                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified]) 
   1.520               (simp_all add: wf)
   1.521 -	    
   1.522 -	show ?thesis
   1.523 -	proof (cases "the_Bool b")
   1.524 -	  case True  
   1.525 -	  with Loop.hyps obtain
   1.526 +            
   1.527 +        show ?thesis
   1.528 +        proof (cases "the_Bool b")
   1.529 +          case True  
   1.530 +          with Loop.hyps obtain
   1.531              eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
   1.532              eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   1.533 -	    by simp
   1.534 -	  from eval_c abr have "s2=s1" by auto
   1.535 -	  moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
   1.536 -	    by (cases s1) (simp add: absorb_def)
   1.537 -	  ultimately show ?thesis
   1.538 -	    using eval_while abr
   1.539 -	    by auto
   1.540 -	next
   1.541 -	  case False
   1.542 -	  with Loop.hyps show ?thesis by simp
   1.543 -	qed
   1.544 +            by simp
   1.545 +          from eval_c abr have "s2=s1" by auto
   1.546 +          moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
   1.547 +            by (cases s1) (simp add: absorb_def)
   1.548 +          ultimately show ?thesis
   1.549 +            using eval_while abr
   1.550 +            by auto
   1.551 +        next
   1.552 +          case False
   1.553 +          with Loop.hyps show ?thesis by simp
   1.554 +        qed
   1.555        qed
   1.556        with conf_s1 error_free_s1 wt
   1.557        show ?thesis
   1.558 -	by simp
   1.559 +        by simp
   1.560      qed
   1.561    next
   1.562      case (Jmp s j L accC T A)
   1.563 @@ -2123,53 +2123,53 @@
   1.564        case False
   1.565        from sx_alloc wf
   1.566        have eq_s2_s1: "s2=s1"
   1.567 -	by (rule sxalloc_type_sound [elim_format])
   1.568 -	   (insert False, auto split: option.splits abrupt.splits )
   1.569 +        by (rule sxalloc_type_sound [elim_format])
   1.570 +           (insert False, auto split: option.splits abrupt.splits )
   1.571        with False 
   1.572        have "\<not>  G,s2\<turnstile>catch catchC"
   1.573 -	by (simp add: catch_def)
   1.574 +        by (simp add: catch_def)
   1.575        with Try
   1.576        have "s3=s2"
   1.577 -	by simp
   1.578 +        by simp
   1.579        with wt conf_s1 error_free_s1 eq_s2_s1
   1.580        show ?thesis
   1.581 -	by simp
   1.582 +        by simp
   1.583      next
   1.584        case True
   1.585        note exception_s1 = this
   1.586        show ?thesis
   1.587        proof (cases "G,s2\<turnstile>catch catchC") 
   1.588 -	case False
   1.589 -	with Try
   1.590 -	have "s3=s2"
   1.591 -	  by simp
   1.592 -	with wt conf_s2 error_free_s2 
   1.593 -	show ?thesis
   1.594 -	  by simp
   1.595 +        case False
   1.596 +        with Try
   1.597 +        have "s3=s2"
   1.598 +          by simp
   1.599 +        with wt conf_s2 error_free_s2 
   1.600 +        show ?thesis
   1.601 +          by simp
   1.602        next
   1.603 -	case True
   1.604 -	with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
   1.605 -	from True Try.hyps
   1.606 -	have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
   1.607 -	  by simp
   1.608 -	note hyp_c2 = this [rule_format]
   1.609 -	from exception_s1 sx_alloc wf
   1.610 -	obtain a 
   1.611 -	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
   1.612 -	  by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
   1.613 -	with True
   1.614 -	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
   1.615 -	  by (cases s2) simp
   1.616 -	with xcpt_s2 conf_s2 wf
   1.617 -	have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
   1.618 -	  by (auto dest: Try_lemma)
   1.619 -	moreover note wt_c2
   1.620 -	moreover
   1.621 -	obtain C2' where
   1.622 -	  "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
   1.623 +        case True
   1.624 +        with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
   1.625 +        from True Try.hyps
   1.626 +        have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
   1.627 +          by simp
   1.628 +        note hyp_c2 = this [rule_format]
   1.629 +        from exception_s1 sx_alloc wf
   1.630 +        obtain a 
   1.631 +          where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
   1.632 +          by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
   1.633 +        with True
   1.634 +        have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
   1.635 +          by (cases s2) simp
   1.636 +        with xcpt_s2 conf_s2 wf
   1.637 +        have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
   1.638 +          by (auto dest: Try_lemma)
   1.639 +        moreover note wt_c2
   1.640 +        moreover
   1.641 +        obtain C2' where
   1.642 +          "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
   1.643            \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>In1r c2\<guillemotright> C2'"
   1.644 -	proof -
   1.645 -	  have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
   1.646 +        proof -
   1.647 +          have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
   1.648                    \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
   1.649            proof -
   1.650              from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   1.651 @@ -2189,20 +2189,20 @@
   1.652              ultimately show ?thesis
   1.653                by (rule Un_least)
   1.654            qed
   1.655 -	  with da_c2 show thesis
   1.656 -	    by (rule da_weakenE) (rule that)
   1.657 -	qed
   1.658 -	ultimately
   1.659 -	obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
   1.660 +          with da_c2 show thesis
   1.661 +            by (rule da_weakenE) (rule that)
   1.662 +        qed
   1.663 +        ultimately
   1.664 +        obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
   1.665                 error_free_s3: "error_free s3"
   1.666 -	  by (rule hyp_c2 [elim_format])
   1.667 +          by (rule hyp_c2 [elim_format])
   1.668               (cases s2, simp add: xcpt_s2 error_free_s2) 
   1.669 -	from conf_s3 fresh_vn 
   1.670 -	have "s3\<Colon>\<preceq>(G,L)"
   1.671 -	  by (blast intro: conforms_deallocL)
   1.672 -	with wt error_free_s3
   1.673 -	show ?thesis
   1.674 -	  by simp
   1.675 +        from conf_s3 fresh_vn 
   1.676 +        have "s3\<Colon>\<preceq>(G,L)"
   1.677 +          by (blast intro: conforms_deallocL)
   1.678 +        with wt error_free_s3
   1.679 +        show ?thesis
   1.680 +          by simp
   1.681        qed
   1.682      qed
   1.683    next
   1.684 @@ -2242,9 +2242,9 @@
   1.685          by (rule dom_locals_eval_mono_elim)
   1.686        hence "dom (locals (store ((Norm s0)::state))) 
   1.687                \<subseteq> dom (locals (store ((Norm s1)::state)))"
   1.688 -	by simp
   1.689 +        by simp
   1.690        with da_c2 show thesis
   1.691 -	by (rule da_weakenE) (rule that)
   1.692 +        by (rule da_weakenE) (rule that)
   1.693      qed
   1.694      ultimately
   1.695      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
   1.696 @@ -2261,19 +2261,19 @@
   1.697      next
   1.698        case (Some x) 
   1.699        from eval_c2 have 
   1.700 -	"dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
   1.701 -	by (rule dom_locals_eval_mono_elim)
   1.702 +        "dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
   1.703 +        by (rule dom_locals_eval_mono_elim)
   1.704        with Some eval_c2 wf conf_s1 conf_s2
   1.705        have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
   1.706 -	by (cases s2) (auto dest: Fin_lemma)
   1.707 +        by (cases s2) (auto dest: Fin_lemma)
   1.708        from Some error_free_s1
   1.709        have "\<not> (\<exists> err. x=Error err)"
   1.710 -	by (simp add: error_free_def)
   1.711 +        by (simp add: error_free_def)
   1.712        with error_free_s2
   1.713        have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
   1.714 -	by (cases s2) simp
   1.715 +        by (cases s2) simp
   1.716        with Some wt conf s3' show ?thesis
   1.717 -	by (cases s2) auto
   1.718 +        by (cases s2) auto
   1.719      qed
   1.720    next
   1.721      case (Init C c s0 s3 s1 s2 L accC T A)
   1.722 @@ -2288,9 +2288,9 @@
   1.723      proof (cases "inited C (globs s0)")
   1.724        case True
   1.725        with Init.hyps have "s3 = Norm s0"
   1.726 -	by simp
   1.727 +        by simp
   1.728        with conf_s0 wt show ?thesis 
   1.729 -	by simp
   1.730 +        by simp
   1.731      next
   1.732        case False
   1.733        with Init.hyps obtain 
   1.734 @@ -2298,88 +2298,88 @@
   1.735             "G\<turnstile>Norm ((init_class_obj G C) s0) 
   1.736                \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
   1.737          eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
   1.738 -	s3: "s3 = (set_lvars (locals (store s1))) s2" 
   1.739 -	by simp
   1.740 +        s3: "s3 = (set_lvars (locals (store s1))) s2" 
   1.741 +        by simp
   1.742        have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
   1.743 -	              (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
   1.744 -	using False Init.hyps by simp
   1.745 +                      (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
   1.746 +        using False Init.hyps by simp
   1.747        note hyp_init_super = this [rule_format] 
   1.748        have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
   1.749 -	using False Init.hyps by simp
   1.750 +        using False Init.hyps by simp
   1.751        note hyp_init_c = this [rule_format]
   1.752        from conf_s0 wf cls_C False
   1.753        have "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
   1.754 -	by (auto dest: conforms_init_class_obj)
   1.755 +        by (auto dest: conforms_init_class_obj)
   1.756        moreover from wf cls_C have
   1.757 -	wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
   1.758 +        wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
   1.759                           \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
   1.760 -	by (cases "C=Object")
   1.761 +        by (cases "C=Object")
   1.762             (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
   1.763        moreover
   1.764        obtain S where
   1.765 -	da_init_super:
   1.766 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.767 +        da_init_super:
   1.768 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.769            \<turnstile> dom (locals (store ((Norm ((init_class_obj G C) s0))::state))) 
   1.770                 \<guillemotright>In1r (if C = Object then Skip else Init (super c))\<guillemotright> S"
   1.771        proof (cases "C=Object")
   1.772 -	case True 
   1.773 -	with da_Skip show ?thesis
   1.774 -	  using that by (auto intro: assigned.select_convs)
   1.775 +        case True 
   1.776 +        with da_Skip show ?thesis
   1.777 +          using that by (auto intro: assigned.select_convs)
   1.778        next
   1.779 -	case False 
   1.780 -	with da_Init show ?thesis
   1.781 -	  by - (rule that, auto intro: assigned.select_convs)
   1.782 +        case False 
   1.783 +        with da_Init show ?thesis
   1.784 +          by - (rule that, auto intro: assigned.select_convs)
   1.785        qed
   1.786        ultimately 
   1.787        obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
   1.788 -	by (rule hyp_init_super [elim_format]) simp
   1.789 +        by (rule hyp_init_super [elim_format]) simp
   1.790        from eval_init_super wt_init_super wf
   1.791        have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
   1.792 -	by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
   1.793 +        by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
   1.794                auto)
   1.795        with conf_s1
   1.796        have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
   1.797 -	by (cases s1) (auto intro: conforms_set_locals)
   1.798 +        by (cases s1) (auto intro: conforms_set_locals)
   1.799        moreover 
   1.800        from error_free_s1
   1.801        have error_free_empty: "error_free ((set_lvars empty) s1)"
   1.802 -	by simp
   1.803 +        by simp
   1.804        from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
   1.805 -	by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
   1.806 +        by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
   1.807        moreover from cls_C wf obtain I
   1.808 -	where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
   1.809 -	by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
   1.810 +        where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
   1.811 +        by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
   1.812         (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
   1.813        then obtain I' where
   1.814 -	"\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
   1.815 +        "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
   1.816              \<guillemotright>In1r (init c)\<guillemotright> I'"
   1.817 -	  by (rule da_weakenE) simp
   1.818 +          by (rule da_weakenE) simp
   1.819        ultimately
   1.820        obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
   1.821 -	by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
   1.822 +        by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
   1.823        have "abrupt s2 \<noteq> Some (Jump Ret)"
   1.824        proof -
   1.825 -	from s1_no_ret 
   1.826 -	have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
   1.827 -	  by simp
   1.828 -	moreover
   1.829 -	from cls_C wf have "jumpNestingOkS {} (init c)"
   1.830 -	  by (rule wf_prog_cdecl [THEN wf_cdeclE])
   1.831 -	ultimately 
   1.832 -	show ?thesis
   1.833 -	  using eval_init wt_init_c wf
   1.834 -	  by - (rule eval_statement_no_jump 
   1.835 +        from s1_no_ret 
   1.836 +        have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
   1.837 +          by simp
   1.838 +        moreover
   1.839 +        from cls_C wf have "jumpNestingOkS {} (init c)"
   1.840 +          by (rule wf_prog_cdecl [THEN wf_cdeclE])
   1.841 +        ultimately 
   1.842 +        show ?thesis
   1.843 +          using eval_init wt_init_c wf
   1.844 +          by - (rule eval_statement_no_jump 
   1.845                       [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
   1.846        qed
   1.847        with conf_s2 s3 conf_s1 eval_init
   1.848        have "s3\<Colon>\<preceq>(G, L)"
   1.849 -	by (cases s2,cases s1) (force dest: conforms_return eval_gext')
   1.850 +        by (cases s2,cases s1) (force dest: conforms_return eval_gext')
   1.851        moreover from error_free_s2 s3
   1.852        have "error_free s3"
   1.853 -	by simp
   1.854 +        by simp
   1.855        moreover note wt
   1.856        ultimately show ?thesis
   1.857 -	by simp
   1.858 +        by simp
   1.859      qed
   1.860    next
   1.861      case (NewC s0 C s1 a s2 L accC T A)
   1.862 @@ -2436,39 +2436,39 @@
   1.863      proof -
   1.864        note conf_s0 wt_init
   1.865        moreover obtain I where
   1.866 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.867 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.868           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
   1.869        proof (cases "\<exists>C. elT = Class C")
   1.870 -	case True
   1.871 -	thus ?thesis
   1.872 -	  by - (rule that, (auto intro: da_Init [simplified] 
   1.873 +        case True
   1.874 +        thus ?thesis
   1.875 +          by - (rule that, (auto intro: da_Init [simplified] 
   1.876                                          assigned.select_convs
   1.877                                simp add: init_comp_ty_def))
   1.878 -	 (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
   1.879 +         (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
   1.880        next
   1.881 -	case False
   1.882 -	thus ?thesis
   1.883 -	by - (rule that, (auto intro: da_Skip [simplified] 
   1.884 +        case False
   1.885 +        thus ?thesis
   1.886 +        by - (rule that, (auto intro: da_Skip [simplified] 
   1.887                                        assigned.select_convs
   1.888                             simp add: init_comp_ty_def))
   1.889           (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
   1.890        qed
   1.891        ultimately show thesis
   1.892 -	by (rule hyp_init [elim_format]) (auto intro: that)
   1.893 +        by (rule hyp_init [elim_format]) (auto intro: that)
   1.894      qed 
   1.895      obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
   1.896      proof -
   1.897        from eval_init 
   1.898        have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
   1.899 -	by (rule dom_locals_eval_mono_elim)
   1.900 +        by (rule dom_locals_eval_mono_elim)
   1.901        with da_e 
   1.902        obtain A' where
   1.903         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
   1.904              \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
   1.905 -	by (rule da_weakenE)
   1.906 +        by (rule da_weakenE)
   1.907        with conf_s1 wt_size
   1.908        show ?thesis
   1.909 -	by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
   1.910 +        by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
   1.911      qed
   1.912      from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
   1.913        by (cases s2) auto
   1.914 @@ -2515,14 +2515,14 @@
   1.915        assume norm_s2: "normal s2"
   1.916        have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
   1.917        proof -
   1.918 -	from s2 norm_s2 have "normal s1"
   1.919 -	  by (cases s1) simp
   1.920 -	with v_ok 
   1.921 -	have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
   1.922 -	  by simp
   1.923 -	with eT wf s2 T norm_s2
   1.924 -	show ?thesis
   1.925 -	  by (cases s1) (auto dest: fits_conf)
   1.926 +        from s2 norm_s2 have "normal s1"
   1.927 +          by (cases s1) simp
   1.928 +        with v_ok 
   1.929 +        have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
   1.930 +          by simp
   1.931 +        with eT wf s2 T norm_s2
   1.932 +        show ?thesis
   1.933 +          by (cases s1) (auto dest: fits_conf)
   1.934        qed
   1.935      }
   1.936      with conf_s2 error_free_s2
   1.937 @@ -2644,32 +2644,32 @@
   1.938        case False
   1.939        with eval_e2 have "s2=s1" by auto
   1.940        with conf_s1 error_free_s1 False show ?thesis
   1.941 -	by auto
   1.942 +        by auto
   1.943      next
   1.944        case True
   1.945        note normal_s1 = this
   1.946        show ?thesis 
   1.947        proof (cases "need_second_arg binop v1")
   1.948 -	case False
   1.949 -	with normal_s1 eval_e2 have "s2=s1"
   1.950 -	  by (cases s1) (simp, elim eval_elim_cases,simp)
   1.951 -	with conf_s1 conf_v error_free_s1
   1.952 -	show ?thesis by simp
   1.953 +        case False
   1.954 +        with normal_s1 eval_e2 have "s2=s1"
   1.955 +          by (cases s1) (simp, elim eval_elim_cases,simp)
   1.956 +        with conf_s1 conf_v error_free_s1
   1.957 +        show ?thesis by simp
   1.958        next
   1.959 -	case True
   1.960 -	note need_second_arg = this
   1.961 -	with hyp_e2 
   1.962 -	have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
   1.963 -	from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
   1.964 +        case True
   1.965 +        note need_second_arg = this
   1.966 +        with hyp_e2 
   1.967 +        have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
   1.968 +        from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
   1.969            wt_v1 [rule_format,OF normal_s1] wf
   1.970 -	obtain E2 where
   1.971 -	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
   1.972 -	  by (rule da_e2_BinOp [elim_format]) 
   1.973 +        obtain E2 where
   1.974 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
   1.975 +          by (rule da_e2_BinOp [elim_format]) 
   1.976               (auto simp add: need_second_arg )
   1.977 -	with conf_s1 wt_e2 
   1.978 -	obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
   1.979 -	  by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
   1.980 -	with conf_v show ?thesis by simp
   1.981 +        with conf_s1 wt_e2 
   1.982 +        obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
   1.983 +          by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
   1.984 +        with conf_v show ?thesis by simp
   1.985        qed
   1.986      qed
   1.987    next
   1.988 @@ -2713,18 +2713,18 @@
   1.989        fix n assume lvar: "v=LVar n"
   1.990        have "locals (store s1) n \<noteq> None"
   1.991        proof -
   1.992 -	from Acc.prems lvar have 
   1.993 -	  "n \<in> dom (locals s0)"
   1.994 -	  by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
   1.995 -	also
   1.996 -	have "dom (locals s0) \<subseteq> dom (locals (store s1))"
   1.997 -	proof -
   1.998 -	  from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
   1.999 -	  show ?thesis
  1.1000 -	    by (rule dom_locals_eval_mono_elim) simp
  1.1001 -	qed
  1.1002 -	finally show ?thesis
  1.1003 -	  by blast
  1.1004 +        from Acc.prems lvar have 
  1.1005 +          "n \<in> dom (locals s0)"
  1.1006 +          by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
  1.1007 +        also
  1.1008 +        have "dom (locals s0) \<subseteq> dom (locals (store s1))"
  1.1009 +        proof -
  1.1010 +          from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
  1.1011 +          show ?thesis
  1.1012 +            by (rule dom_locals_eval_mono_elim) simp
  1.1013 +        qed
  1.1014 +        finally show ?thesis
  1.1015 +          by blast
  1.1016        qed
  1.1017      } note lvar_in_locals = this 
  1.1018      from conf_s0 wt_v da_v
  1.1019 @@ -2746,9 +2746,9 @@
  1.1020      note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1.1021      note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T`
  1.1022      then obtain varT eT where
  1.1023 -	 wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  1.1024 -	   wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1.1025 -	  widen: "G\<turnstile>eT\<preceq>varT" and
  1.1026 +         wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  1.1027 +           wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  1.1028 +          widen: "G\<turnstile>eT\<preceq>varT" and
  1.1029                T: "T=Inl eT"
  1.1030        by (rule wt_elim_cases) auto
  1.1031      show "assign upd v s2\<Colon>\<preceq>(G, L) \<and>
  1.1032 @@ -2759,139 +2759,139 @@
  1.1033        case False
  1.1034        with Ass.prems
  1.1035        obtain V E where
  1.1036 -	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1037 +        da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1038                     \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V" and
  1.1039 -	da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  1.1040 -	by (elim da_elim_cases) simp+
  1.1041 +        da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  1.1042 +        by (elim da_elim_cases) simp+
  1.1043        from conf_s0 wt_var da_var 
  1.1044        obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  1.1045 -	and  conf_var: "normal s1 
  1.1046 +        and  conf_var: "normal s1 
  1.1047                           \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1048 -	and  error_free_s1: "error_free s1"
  1.1049 -	by (rule hyp_var [elim_format]) simp
  1.1050 +        and  error_free_s1: "error_free s1"
  1.1051 +        by (rule hyp_var [elim_format]) simp
  1.1052        show ?thesis
  1.1053        proof (cases "normal s1")
  1.1054 -	case False
  1.1055 -	with eval_e have "s2=s1" by auto
  1.1056 -	with False have "assign upd v s2=s1"
  1.1057 -	  by simp
  1.1058 -	with conf_s1 error_free_s1 False show ?thesis
  1.1059 -	  by auto
  1.1060 +        case False
  1.1061 +        with eval_e have "s2=s1" by auto
  1.1062 +        with False have "assign upd v s2=s1"
  1.1063 +          by simp
  1.1064 +        with conf_s1 error_free_s1 False show ?thesis
  1.1065 +          by auto
  1.1066        next
  1.1067 -	case True
  1.1068 -	note normal_s1=this
  1.1069 -	obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1070 +        case True
  1.1071 +        note normal_s1=this
  1.1072 +        obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1073                           \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  1.1074 -	proof -
  1.1075 -	  from eval_var wt_var da_var wf normal_s1
  1.1076 -	  have "nrm V \<subseteq>  dom (locals (store s1))"
  1.1077 -	    by (cases rule: da_good_approxE') iprover
  1.1078 -	  with da_e show thesis
  1.1079 -	    by (rule da_weakenE) (rule that)
  1.1080 -	qed
  1.1081 -	with conf_s1 wt_e 
  1.1082 -	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.1083 +        proof -
  1.1084 +          from eval_var wt_var da_var wf normal_s1
  1.1085 +          have "nrm V \<subseteq>  dom (locals (store s1))"
  1.1086 +            by (cases rule: da_good_approxE') iprover
  1.1087 +          with da_e show thesis
  1.1088 +            by (rule da_weakenE) (rule that)
  1.1089 +        qed
  1.1090 +        with conf_s1 wt_e 
  1.1091 +        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.1092            conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  1.1093            error_free_s2: "error_free s2"
  1.1094 -	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.1095 -	show ?thesis 
  1.1096 -	proof (cases "normal s2")
  1.1097 -	  case False
  1.1098 -	  with conf_s2 error_free_s2 
  1.1099 -	  show ?thesis
  1.1100 -	    by auto
  1.1101 -	next
  1.1102 -	  case True
  1.1103 -	  from True conf_v
  1.1104 -	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.1105 -	    by simp
  1.1106 -	  with widen wf
  1.1107 -	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.1108 -	    by (auto intro: conf_widen)
  1.1109 -	  from normal_s1 conf_var
  1.1110 -	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1111 -	    by simp
  1.1112 -	  then 
  1.1113 -	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.1114 -	    by (simp add: rconf_def)
  1.1115 -	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.1116 -	    eval_e T conf_s2 error_free_s2
  1.1117 -	  show ?thesis
  1.1118 -	    by (cases s1, cases s2) 
  1.1119 -	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.1120 -	qed
  1.1121 +          by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.1122 +        show ?thesis 
  1.1123 +        proof (cases "normal s2")
  1.1124 +          case False
  1.1125 +          with conf_s2 error_free_s2 
  1.1126 +          show ?thesis
  1.1127 +            by auto
  1.1128 +        next
  1.1129 +          case True
  1.1130 +          from True conf_v
  1.1131 +          have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.1132 +            by simp
  1.1133 +          with widen wf
  1.1134 +          have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.1135 +            by (auto intro: conf_widen)
  1.1136 +          from normal_s1 conf_var
  1.1137 +          have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1138 +            by simp
  1.1139 +          then 
  1.1140 +          have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.1141 +            by (simp add: rconf_def)
  1.1142 +          from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.1143 +            eval_e T conf_s2 error_free_s2
  1.1144 +          show ?thesis
  1.1145 +            by (cases s1, cases s2) 
  1.1146 +               (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.1147 +        qed
  1.1148        qed
  1.1149      next
  1.1150        case True
  1.1151        then obtain vn where vn: "var=LVar vn"
  1.1152 -	by blast
  1.1153 +        by blast
  1.1154        with Ass.prems
  1.1155        obtain E where
  1.1156 -	da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  1.1157 -	           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  1.1158 -	by (elim da_elim_cases) simp+
  1.1159 +        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  1.1160 +                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  1.1161 +        by (elim da_elim_cases) simp+
  1.1162        from da.LVar vn obtain V where
  1.1163 -	da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1164 +        da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1165                     \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V"
  1.1166 -	by auto
  1.1167 +        by auto
  1.1168        obtain E' where
  1.1169 -	da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1170 +        da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1.1171                     \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> E'"
  1.1172        proof -
  1.1173 -	have "dom (locals (store ((Norm s0)::state))) 
  1.1174 +        have "dom (locals (store ((Norm s0)::state))) 
  1.1175                  \<subseteq> dom (locals (store (s1)))"
  1.1176 -	  by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
  1.1177 -	with da_e show thesis
  1.1178 -	  by (rule da_weakenE) (rule that)
  1.1179 +          by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
  1.1180 +        with da_e show thesis
  1.1181 +          by (rule da_weakenE) (rule that)
  1.1182        qed
  1.1183        from conf_s0 wt_var da_var 
  1.1184        obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  1.1185 -	and  conf_var: "normal s1 
  1.1186 +        and  conf_var: "normal s1 
  1.1187                           \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1188 -	and  error_free_s1: "error_free s1"
  1.1189 -	by (rule hyp_var [elim_format]) simp
  1.1190 +        and  error_free_s1: "error_free s1"
  1.1191 +        by (rule hyp_var [elim_format]) simp
  1.1192        show ?thesis
  1.1193        proof (cases "normal s1")
  1.1194 -	case False
  1.1195 -	with eval_e have "s2=s1" by auto
  1.1196 -	with False have "assign upd v s2=s1"
  1.1197 -	  by simp
  1.1198 -	with conf_s1 error_free_s1 False show ?thesis
  1.1199 -	  by auto
  1.1200 +        case False
  1.1201 +        with eval_e have "s2=s1" by auto
  1.1202 +        with False have "assign upd v s2=s1"
  1.1203 +          by simp
  1.1204 +        with conf_s1 error_free_s1 False show ?thesis
  1.1205 +          by auto
  1.1206        next
  1.1207 -	case True
  1.1208 -	note normal_s1 = this
  1.1209 -	from conf_s1 wt_e da_e'
  1.1210 -	obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.1211 +        case True
  1.1212 +        note normal_s1 = this
  1.1213 +        from conf_s1 wt_e da_e'
  1.1214 +        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.1215            conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  1.1216            error_free_s2: "error_free s2"
  1.1217 -	  by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.1218 -	show ?thesis 
  1.1219 -	proof (cases "normal s2")
  1.1220 -	  case False
  1.1221 -	  with conf_s2 error_free_s2 
  1.1222 -	  show ?thesis
  1.1223 -	    by auto
  1.1224 -	next
  1.1225 -	  case True
  1.1226 -	  from True conf_v
  1.1227 -	  have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.1228 -	    by simp
  1.1229 -	  with widen wf
  1.1230 -	  have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.1231 -	    by (auto intro: conf_widen)
  1.1232 -	  from normal_s1 conf_var
  1.1233 -	  have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1234 -	    by simp
  1.1235 -	  then 
  1.1236 -	  have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.1237 -	    by (simp add: rconf_def)
  1.1238 -	  from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.1239 -	    eval_e T conf_s2 error_free_s2
  1.1240 -	  show ?thesis
  1.1241 -	    by (cases s1, cases s2) 
  1.1242 -	       (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.1243 -	qed
  1.1244 +          by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  1.1245 +        show ?thesis 
  1.1246 +        proof (cases "normal s2")
  1.1247 +          case False
  1.1248 +          with conf_s2 error_free_s2 
  1.1249 +          show ?thesis
  1.1250 +            by auto
  1.1251 +        next
  1.1252 +          case True
  1.1253 +          from True conf_v
  1.1254 +          have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.1255 +            by simp
  1.1256 +          with widen wf
  1.1257 +          have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  1.1258 +            by (auto intro: conf_widen)
  1.1259 +          from normal_s1 conf_var
  1.1260 +          have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  1.1261 +            by simp
  1.1262 +          then 
  1.1263 +          have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  1.1264 +            by (simp add: rconf_def)
  1.1265 +          from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  1.1266 +            eval_e T conf_s2 error_free_s2
  1.1267 +          show ?thesis
  1.1268 +            by (cases s1, cases s2) 
  1.1269 +               (auto dest!: Ass_lemma simp add: assign_conforms_def)
  1.1270 +        qed
  1.1271        qed
  1.1272      qed
  1.1273    next
  1.1274 @@ -2931,60 +2931,60 @@
  1.1275        case False
  1.1276        with eval_e1_e2 have "s2=s1" by auto
  1.1277        with conf_s1 error_free_s1 False show ?thesis
  1.1278 -	by auto
  1.1279 +        by auto
  1.1280      next
  1.1281        case True
  1.1282        have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  1.1283                      \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1.1284        proof -
  1.1285 -	from eval_e0 have 
  1.1286 -	  "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.1287 -	  by (rule dom_locals_eval_mono_elim)
  1.1288 +        from eval_e0 have 
  1.1289 +          "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.1290 +          by (rule dom_locals_eval_mono_elim)
  1.1291          moreover
  1.1292 -	from eval_e0 True wt_e0 
  1.1293 -	have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1.1294 -	  by (rule assigns_if_good_approx') 
  1.1295 -	ultimately show ?thesis by (rule Un_least)
  1.1296 +        from eval_e0 True wt_e0 
  1.1297 +        have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  1.1298 +          by (rule assigns_if_good_approx') 
  1.1299 +        ultimately show ?thesis by (rule Un_least)
  1.1300        qed 
  1.1301        show ?thesis
  1.1302        proof (cases "the_Bool b")
  1.1303 -	case True
  1.1304 -	with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  1.1305 -	  by simp
  1.1306 -	from da_e1 s0_s1 True obtain E1' where
  1.1307 -	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  1.1308 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  1.1309 -	with conf_s1 wt_e1
  1.1310 -	obtain 
  1.1311 -	  "s2\<Colon>\<preceq>(G, L)"
  1.1312 -	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  1.1313 -	  "error_free s2"            
  1.1314 -	  by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  1.1315 -	moreover
  1.1316 -	from statT  
  1.1317 -	have "G\<turnstile>T1\<preceq>statT"
  1.1318 -	  by auto
  1.1319 -	ultimately show ?thesis
  1.1320 -	  using T wf by auto
  1.1321 +        case True
  1.1322 +        with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  1.1323 +          by simp
  1.1324 +        from da_e1 s0_s1 True obtain E1' where
  1.1325 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  1.1326 +          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  1.1327 +        with conf_s1 wt_e1
  1.1328 +        obtain 
  1.1329 +          "s2\<Colon>\<preceq>(G, L)"
  1.1330 +          "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  1.1331 +          "error_free s2"            
  1.1332 +          by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  1.1333 +        moreover
  1.1334 +        from statT  
  1.1335 +        have "G\<turnstile>T1\<preceq>statT"
  1.1336 +          by auto
  1.1337 +        ultimately show ?thesis
  1.1338 +          using T wf by auto
  1.1339        next
  1.1340 -	case False
  1.1341 -	with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  1.1342 -	  by simp
  1.1343 -	from da_e2 s0_s1 False obtain E2' where
  1.1344 -	  "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  1.1345 -	  by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  1.1346 -	with conf_s1 wt_e2
  1.1347 -	obtain 
  1.1348 -	  "s2\<Colon>\<preceq>(G, L)"
  1.1349 -	  "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  1.1350 -	  "error_free s2"            
  1.1351 -	  by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.1352 -	moreover
  1.1353 -	from statT  
  1.1354 -	have "G\<turnstile>T2\<preceq>statT"
  1.1355 -	  by auto
  1.1356 -	ultimately show ?thesis
  1.1357 -	  using T wf by auto
  1.1358 +        case False
  1.1359 +        with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  1.1360 +          by simp
  1.1361 +        from da_e2 s0_s1 False obtain E2' where
  1.1362 +          "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  1.1363 +          by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  1.1364 +        with conf_s1 wt_e2
  1.1365 +        obtain 
  1.1366 +          "s2\<Colon>\<preceq>(G, L)"
  1.1367 +          "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  1.1368 +          "error_free s2"            
  1.1369 +          by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.1370 +        moreover
  1.1371 +        from statT  
  1.1372 +        have "G\<turnstile>T2\<preceq>statT"
  1.1373 +          by auto
  1.1374 +        ultimately show ?thesis
  1.1375 +          using T wf by auto
  1.1376        qed
  1.1377      qed
  1.1378    next
  1.1379 @@ -3031,22 +3031,22 @@
  1.1380        assume abnormal_s2: "\<not> normal s2"
  1.1381        have "set_lvars (locals (store s2)) s4 = s2"
  1.1382        proof -
  1.1383 -	from abnormal_s2 init_lvars 
  1.1384 -	obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1.1385 +        from abnormal_s2 init_lvars 
  1.1386 +        obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1.1387               "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1.1388                                              mode a vs s2)" 
  1.1389 -	  by (auto simp add: init_lvars_def2)
  1.1390 -	moreover
  1.1391 -	from keep_abrupt abnormal_s2 check
  1.1392 -	have eq_s3'_s3: "s3'=s3" 
  1.1393 -	  by (auto simp add: check_method_access_def Let_def)
  1.1394 -	moreover
  1.1395 -	from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  1.1396 -	have "s4=s3'"
  1.1397 -	  by auto
  1.1398 -	ultimately show
  1.1399 -	  "set_lvars (locals (store s2)) s4 = s2"
  1.1400 -	  by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.1401 +          by (auto simp add: init_lvars_def2)
  1.1402 +        moreover
  1.1403 +        from keep_abrupt abnormal_s2 check
  1.1404 +        have eq_s3'_s3: "s3'=s3" 
  1.1405 +          by (auto simp add: check_method_access_def Let_def)
  1.1406 +        moreover
  1.1407 +        from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  1.1408 +        have "s4=s3'"
  1.1409 +          by auto
  1.1410 +        ultimately show
  1.1411 +          "set_lvars (locals (store s2)) s4 = s2"
  1.1412 +          by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.1413        qed
  1.1414      } note propagate_abnormal_s2 = this
  1.1415      show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  1.1416 @@ -3060,113 +3060,113 @@
  1.1417        with eval_args have "s2=s1" by auto
  1.1418        with False propagate_abnormal_s2 conf_s1 error_free_s1 
  1.1419        show ?thesis
  1.1420 -	by auto
  1.1421 +        by auto
  1.1422      next
  1.1423        case True
  1.1424        note normal_s1 = this
  1.1425        obtain A' where 
  1.1426 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  1.1427 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  1.1428        proof -
  1.1429 -	from eval_e wt_e da_e wf normal_s1
  1.1430 -	have "nrm E \<subseteq>  dom (locals (store s1))"
  1.1431 -	  by (cases rule: da_good_approxE') iprover
  1.1432 -	with da_args show thesis
  1.1433 -	  by (rule da_weakenE) (rule that)
  1.1434 +        from eval_e wt_e da_e wf normal_s1
  1.1435 +        have "nrm E \<subseteq>  dom (locals (store s1))"
  1.1436 +          by (cases rule: da_good_approxE') iprover
  1.1437 +        with da_args show thesis
  1.1438 +          by (rule da_weakenE) (rule that)
  1.1439        qed
  1.1440        with conf_s1 wt_args 
  1.1441        obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.1442                conf_args: "normal s2 
  1.1443                           \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  1.1444            error_free_s2: "error_free s2" 
  1.1445 -	by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  1.1446 +        by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  1.1447        from error_free_s2 init_lvars
  1.1448        have error_free_s3: "error_free s3"
  1.1449 -	by (auto simp add: init_lvars_def2)
  1.1450 +        by (auto simp add: init_lvars_def2)
  1.1451        from statM 
  1.1452        obtain
  1.1453 -	statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1.1454 -	pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1.1455 -	by (blast dest: max_spec2mheads)
  1.1456 +        statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1.1457 +        pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1.1458 +        by (blast dest: max_spec2mheads)
  1.1459        from check
  1.1460        have eq_store_s3'_s3: "store s3'=store s3"
  1.1461 -	by (cases s3) (simp add: check_method_access_def Let_def)
  1.1462 +        by (cases s3) (simp add: check_method_access_def Let_def)
  1.1463        obtain invC
  1.1464 -	where invC: "invC = invocation_class mode (store s2) a statT"
  1.1465 -	by simp
  1.1466 +        where invC: "invC = invocation_class mode (store s2) a statT"
  1.1467 +        by simp
  1.1468        with init_lvars
  1.1469        have invC': "invC = (invocation_class mode (store s3) a statT)"
  1.1470 -	by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1.1471 +        by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1.1472        show ?thesis
  1.1473        proof (cases "normal s2")
  1.1474 -	case False
  1.1475 -	with propagate_abnormal_s2 conf_s2 error_free_s2
  1.1476 -	show ?thesis
  1.1477 -	  by auto
  1.1478 +        case False
  1.1479 +        with propagate_abnormal_s2 conf_s2 error_free_s2
  1.1480 +        show ?thesis
  1.1481 +          by auto
  1.1482        next
  1.1483 -	case True
  1.1484 -	note normal_s2 = True
  1.1485 -	with normal_s1 conf_a eval_args 
  1.1486 -	have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1.1487 -	  by (auto dest: eval_gext intro: conf_gext)
  1.1488 -	show ?thesis
  1.1489 -	proof (cases "a=Null \<longrightarrow> is_static statM")
  1.1490 -	  case False
  1.1491 -	  then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  1.1492 -	    by blast
  1.1493 -	  with normal_s2 init_lvars mode
  1.1494 -	  obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1.1495 +        case True
  1.1496 +        note normal_s2 = True
  1.1497 +        with normal_s1 conf_a eval_args 
  1.1498 +        have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1.1499 +          by (auto dest: eval_gext intro: conf_gext)
  1.1500 +        show ?thesis
  1.1501 +        proof (cases "a=Null \<longrightarrow> is_static statM")
  1.1502 +          case False
  1.1503 +          then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  1.1504 +            by blast
  1.1505 +          with normal_s2 init_lvars mode
  1.1506 +          obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1.1507                       "store s3 = store (init_lvars G invDeclC 
  1.1508                                         \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2)"
  1.1509 -	    by (auto simp add: init_lvars_def2)
  1.1510 -	  moreover
  1.1511 -	  from np check
  1.1512 -	  have eq_s3'_s3: "s3'=s3" 
  1.1513 -	    by (auto simp add: check_method_access_def Let_def)
  1.1514 -	  moreover
  1.1515 -	  from eq_s3'_s3 np eval_methd
  1.1516 -	  have "s4=s3'"
  1.1517 -	    by auto
  1.1518 -	  ultimately have
  1.1519 -	    "set_lvars (locals (store s2)) s4 
  1.1520 +            by (auto simp add: init_lvars_def2)
  1.1521 +          moreover
  1.1522 +          from np check
  1.1523 +          have eq_s3'_s3: "s3'=s3" 
  1.1524 +            by (auto simp add: check_method_access_def Let_def)
  1.1525 +          moreover
  1.1526 +          from eq_s3'_s3 np eval_methd
  1.1527 +          have "s4=s3'"
  1.1528 +            by auto
  1.1529 +          ultimately have
  1.1530 +            "set_lvars (locals (store s2)) s4 
  1.1531              = (Some (Xcpt (Std NullPointer)),store s2)"
  1.1532 -	    by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.1533 -	  with conf_s2 error_free_s2
  1.1534 -	  show ?thesis
  1.1535 -	    by (cases s2) (auto dest: conforms_NormI)
  1.1536 -	next
  1.1537 -	  case True
  1.1538 -	  with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  1.1539 -	    by (auto dest!: Null_staticD)
  1.1540 -	  with conf_s2 conf_a_s2 wf invC  
  1.1541 -	  have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1.1542 -	    by (cases s2) (auto intro: DynT_propI)
  1.1543 -	  with wt_e statM' invC mode wf 
  1.1544 -	  obtain dynM where 
  1.1545 +            by (cases s2,cases s3) (simp add: init_lvars_def2)
  1.1546 +          with conf_s2 error_free_s2
  1.1547 +          show ?thesis
  1.1548 +            by (cases s2) (auto dest: conforms_NormI)
  1.1549 +        next
  1.1550 +          case True
  1.1551 +          with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  1.1552 +            by (auto dest!: Null_staticD)
  1.1553 +          with conf_s2 conf_a_s2 wf invC  
  1.1554 +          have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1.1555 +            by (cases s2) (auto intro: DynT_propI)
  1.1556 +          with wt_e statM' invC mode wf 
  1.1557 +          obtain dynM where 
  1.1558              dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.1559              acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1.1560                              in invC dyn_accessible_from accC"
  1.1561 -	    by (force dest!: call_access_ok)
  1.1562 -	  with invC' check eq_accC_accC'
  1.1563 -	  have eq_s3'_s3: "s3'=s3"
  1.1564 -	    by (auto simp add: check_method_access_def Let_def)
  1.1565 -	  from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1.1566 -	  obtain 
  1.1567 -	    wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1.1568 -	      dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.1569 +            by (force dest!: call_access_ok)
  1.1570 +          with invC' check eq_accC_accC'
  1.1571 +          have eq_s3'_s3: "s3'=s3"
  1.1572 +            by (auto simp add: check_method_access_def Let_def)
  1.1573 +          from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1.1574 +          obtain 
  1.1575 +            wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1.1576 +              dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.1577              iscls_invDeclC: "is_class G invDeclC" and
  1.1578 -	         invDeclC': "invDeclC = declclass dynM" and
  1.1579 -	      invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1.1580 -	     resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1.1581 -	    is_static_eq: "is_static dynM = is_static statM" and
  1.1582 -	    involved_classes_prop:
  1.1583 +                 invDeclC': "invDeclC = declclass dynM" and
  1.1584 +              invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1.1585 +             resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  1.1586 +            is_static_eq: "is_static dynM = is_static statM" and
  1.1587 +            involved_classes_prop:
  1.1588               "(if invmode statM e = IntVir
  1.1589                 then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1.1590                 else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1.1591                       (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1.1592                        statDeclT = ClassT invDeclC)"
  1.1593 -	    by (cases rule: DynT_mheadsE) simp
  1.1594 -	  obtain L' where 
  1.1595 -	   L':"L'=(\<lambda> k. 
  1.1596 +            by (cases rule: DynT_mheadsE) simp
  1.1597 +          obtain L' where 
  1.1598 +           L':"L'=(\<lambda> k. 
  1.1599                   (case k of
  1.1600                      EName e
  1.1601                      \<Rightarrow> (case e of 
  1.1602 @@ -3176,158 +3176,158 @@
  1.1603                          | Res \<Rightarrow> Some (resTy dynM))
  1.1604                    | This \<Rightarrow> if is_static statM 
  1.1605                              then None else Some (Class invDeclC)))"
  1.1606 -	    by simp
  1.1607 -	  from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1.1608 +            by simp
  1.1609 +          from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1.1610              wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  1.1611 -	  have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1.1612 -	    apply - 
  1.1613 +          have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1.1614 +            apply - 
  1.1615                 (* FIXME confomrs_init_lvars should be 
  1.1616                    adjusted to be more directy applicable *)
  1.1617 -	    apply (drule conforms_init_lvars [of G invDeclC 
  1.1618 +            apply (drule conforms_init_lvars [of G invDeclC 
  1.1619                      "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1.1620                      L statT invC a "(statDeclT,statM)" e])
  1.1621 -	    apply (rule wf)
  1.1622 -	    apply (rule conf_args,assumption)
  1.1623 -	    apply (simp add: pTs_widen)
  1.1624 -	    apply (cases s2,simp)
  1.1625 -	    apply (rule dynM')
  1.1626 -	    apply (force dest: ty_expr_is_type)
  1.1627 -	    apply (rule invC_widen)
  1.1628 -	    apply (force intro: conf_gext dest: eval_gext)
  1.1629 -	    apply simp
  1.1630 -	    apply simp
  1.1631 -	    apply (simp add: invC)
  1.1632 -	    apply (simp add: invDeclC)
  1.1633 -	    apply (simp add: normal_s2)
  1.1634 -	    apply (cases s2, simp add: L' init_lvars
  1.1635 -	                     cong add: lname.case_cong ename.case_cong)
  1.1636 -	    done
  1.1637 -	  with eq_s3'_s3 
  1.1638 -	  have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  1.1639 -	  moreover
  1.1640 -	  from  is_static_eq wf_dynM L'
  1.1641 -	  obtain mthdT where
  1.1642 -	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1643 +            apply (rule wf)
  1.1644 +            apply (rule conf_args,assumption)
  1.1645 +            apply (simp add: pTs_widen)
  1.1646 +            apply (cases s2,simp)
  1.1647 +            apply (rule dynM')
  1.1648 +            apply (force dest: ty_expr_is_type)
  1.1649 +            apply (rule invC_widen)
  1.1650 +            apply (force intro: conf_gext dest: eval_gext)
  1.1651 +            apply simp
  1.1652 +            apply simp
  1.1653 +            apply (simp add: invC)
  1.1654 +            apply (simp add: invDeclC)
  1.1655 +            apply (simp add: normal_s2)
  1.1656 +            apply (cases s2, simp add: L' init_lvars
  1.1657 +                             cong add: lname.case_cong ename.case_cong)
  1.1658 +            done
  1.1659 +          with eq_s3'_s3 
  1.1660 +          have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  1.1661 +          moreover
  1.1662 +          from  is_static_eq wf_dynM L'
  1.1663 +          obtain mthdT where
  1.1664 +            "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1665                 \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  1.1666 -	    mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1.1667 -	    by - (drule wf_mdecl_bodyD,
  1.1668 +            mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  1.1669 +            by - (drule wf_mdecl_bodyD,
  1.1670                   auto simp add: callee_lcl_def  
  1.1671                        cong add: lname.case_cong ename.case_cong)
  1.1672 -	  with dynM' iscls_invDeclC invDeclC'
  1.1673 -	  have
  1.1674 -	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1675 +          with dynM' iscls_invDeclC invDeclC'
  1.1676 +          have
  1.1677 +            "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1678                 \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1.1679 -	    by (auto intro: wt.Methd)
  1.1680 -	  moreover
  1.1681 -	  obtain M where 
  1.1682 -	    "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  1.1683 -	       \<turnstile> dom (locals (store s3')) 
  1.1684 -	          \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  1.1685 -	  proof -
  1.1686 -	    from wf_dynM
  1.1687 -	    obtain M' where
  1.1688 -	      da_body: 
  1.1689 -	      "\<lparr>prg=G, cls=invDeclC
  1.1690 +            by (auto intro: wt.Methd)
  1.1691 +          moreover
  1.1692 +          obtain M where 
  1.1693 +            "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  1.1694 +               \<turnstile> dom (locals (store s3')) 
  1.1695 +                  \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  1.1696 +          proof -
  1.1697 +            from wf_dynM
  1.1698 +            obtain M' where
  1.1699 +              da_body: 
  1.1700 +              "\<lparr>prg=G, cls=invDeclC
  1.1701                 ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  1.1702                 \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  1.1703                res: "Result \<in> nrm M'"
  1.1704 -	      by (rule wf_mdeclE) iprover
  1.1705 -	    from da_body is_static_eq L' have
  1.1706 -	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.1707 +              by (rule wf_mdeclE) iprover
  1.1708 +            from da_body is_static_eq L' have
  1.1709 +              "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.1710                   \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  1.1711 -	      by (simp add: callee_lcl_def  
  1.1712 +              by (simp add: callee_lcl_def  
  1.1713                    cong add: lname.case_cong ename.case_cong)
  1.1714 -	    moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  1.1715 -	    proof -
  1.1716 -	      from is_static_eq 
  1.1717 -	      have "(invmode (mthd dynM) e) = (invmode statM e)"
  1.1718 -		by (simp add: invmode_def)
  1.1719 -	      moreover
  1.1720 -	      have "length (pars (mthd dynM)) = length vs" 
  1.1721 -	      proof -
  1.1722 -		from normal_s2 conf_args
  1.1723 -		have "length vs = length pTs"
  1.1724 -		  by (simp add: list_all2_def)
  1.1725 -		also from pTs_widen
  1.1726 -		have "\<dots> = length pTs'"
  1.1727 -		  by (simp add: widens_def list_all2_def)
  1.1728 -		also from wf_dynM
  1.1729 -		have "\<dots> = length (pars (mthd dynM))"
  1.1730 -		  by (simp add: wf_mdecl_def wf_mhead_def)
  1.1731 -		finally show ?thesis ..
  1.1732 -	      qed
  1.1733 -	      moreover note init_lvars dynM' is_static_eq normal_s2 mode 
  1.1734 -	      ultimately
  1.1735 -	      have "parameters (mthd dynM) = dom (locals (store s3))"
  1.1736 -		using dom_locals_init_lvars 
  1.1737 +            moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  1.1738 +            proof -
  1.1739 +              from is_static_eq 
  1.1740 +              have "(invmode (mthd dynM) e) = (invmode statM e)"
  1.1741 +                by (simp add: invmode_def)
  1.1742 +              moreover
  1.1743 +              have "length (pars (mthd dynM)) = length vs" 
  1.1744 +              proof -
  1.1745 +                from normal_s2 conf_args
  1.1746 +                have "length vs = length pTs"
  1.1747 +                  by (simp add: list_all2_def)
  1.1748 +                also from pTs_widen
  1.1749 +                have "\<dots> = length pTs'"
  1.1750 +                  by (simp add: widens_def list_all2_def)
  1.1751 +                also from wf_dynM
  1.1752 +                have "\<dots> = length (pars (mthd dynM))"
  1.1753 +                  by (simp add: wf_mdecl_def wf_mhead_def)
  1.1754 +                finally show ?thesis ..
  1.1755 +              qed
  1.1756 +              moreover note init_lvars dynM' is_static_eq normal_s2 mode 
  1.1757 +              ultimately
  1.1758 +              have "parameters (mthd dynM) = dom (locals (store s3))"
  1.1759 +                using dom_locals_init_lvars 
  1.1760                    [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
  1.1761 -		by simp
  1.1762 -	      also from check
  1.1763 -	      have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  1.1764 -		by (simp add:  eq_s3'_s3)
  1.1765 -	      finally show ?thesis .
  1.1766 -	    qed
  1.1767 -	    ultimately obtain M2 where
  1.1768 -	      da:
  1.1769 -	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.1770 +                by simp
  1.1771 +              also from check
  1.1772 +              have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  1.1773 +                by (simp add:  eq_s3'_s3)
  1.1774 +              finally show ?thesis .
  1.1775 +            qed
  1.1776 +            ultimately obtain M2 where
  1.1777 +              da:
  1.1778 +              "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  1.1779                  \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  1.1780                M2: "nrm M' \<subseteq> nrm M2"
  1.1781 -	      by (rule da_weakenE)
  1.1782 -	    from res M2 have "Result \<in> nrm M2"
  1.1783 -	      by blast
  1.1784 -	    moreover from wf_dynM
  1.1785 -	    have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  1.1786 -	      by (rule wf_mdeclE)
  1.1787 -	    ultimately
  1.1788 -	    obtain M3 where
  1.1789 -	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  1.1790 +              by (rule da_weakenE)
  1.1791 +            from res M2 have "Result \<in> nrm M2"
  1.1792 +              by blast
  1.1793 +            moreover from wf_dynM
  1.1794 +            have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  1.1795 +              by (rule wf_mdeclE)
  1.1796 +            ultimately
  1.1797 +            obtain M3 where
  1.1798 +              "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  1.1799                       \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  1.1800 -	      using da
  1.1801 -	      by (iprover intro: da.Body assigned.select_convs)
  1.1802 -	    from _ this [simplified]
  1.1803 -	    show ?thesis
  1.1804 -	      by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
  1.1805 -	  qed
  1.1806 -	  ultimately obtain  
  1.1807 -	    conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  1.1808 -	    conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  1.1809 -	    error_free_s4: "error_free s4"
  1.1810 -	    by (rule hyp_methd [elim_format]) 
  1.1811 +              using da
  1.1812 +              by (iprover intro: da.Body assigned.select_convs)
  1.1813 +            from _ this [simplified]
  1.1814 +            show ?thesis
  1.1815 +              by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
  1.1816 +          qed
  1.1817 +          ultimately obtain  
  1.1818 +            conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  1.1819 +            conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  1.1820 +            error_free_s4: "error_free s4"
  1.1821 +            by (rule hyp_methd [elim_format]) 
  1.1822                 (simp add: error_free_s3 eq_s3'_s3)
  1.1823 -	  from init_lvars eval_methd eq_s3'_s3 
  1.1824 -	  have "store s2\<le>|store s4"
  1.1825 -	    by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  1.1826 -	  moreover
  1.1827 -	  have "abrupt s4 \<noteq> Some (Jump Ret)"
  1.1828 -	  proof -
  1.1829 -	    from normal_s2 init_lvars
  1.1830 -	    have "abrupt s3 \<noteq> Some (Jump Ret)"
  1.1831 -	      by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  1.1832 -	    with check
  1.1833 -	    have "abrupt s3' \<noteq> Some (Jump Ret)"
  1.1834 -	      by (cases s3) (auto simp add: check_method_access_def Let_def)
  1.1835 -	    with eval_methd
  1.1836 -	    show ?thesis
  1.1837 -	      by (rule Methd_no_jump)
  1.1838 -	  qed
  1.1839 -	  ultimately 
  1.1840 -	  have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  1.1841 -	    using conf_s2 conf_s4
  1.1842 -	    by (cases s2,cases s4) (auto intro: conforms_return)
  1.1843 -	  moreover 
  1.1844 -	  from conf_Res mthdT_widen resTy_widen wf
  1.1845 -	  have "normal s4 
  1.1846 +          from init_lvars eval_methd eq_s3'_s3 
  1.1847 +          have "store s2\<le>|store s4"
  1.1848 +            by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  1.1849 +          moreover
  1.1850 +          have "abrupt s4 \<noteq> Some (Jump Ret)"
  1.1851 +          proof -
  1.1852 +            from normal_s2 init_lvars
  1.1853 +            have "abrupt s3 \<noteq> Some (Jump Ret)"
  1.1854 +              by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  1.1855 +            with check
  1.1856 +            have "abrupt s3' \<noteq> Some (Jump Ret)"
  1.1857 +              by (cases s3) (auto simp add: check_method_access_def Let_def)
  1.1858 +            with eval_methd
  1.1859 +            show ?thesis
  1.1860 +              by (rule Methd_no_jump)
  1.1861 +          qed
  1.1862 +          ultimately 
  1.1863 +          have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  1.1864 +            using conf_s2 conf_s4
  1.1865 +            by (cases s2,cases s4) (auto intro: conforms_return)
  1.1866 +          moreover 
  1.1867 +          from conf_Res mthdT_widen resTy_widen wf
  1.1868 +          have "normal s4 
  1.1869                    \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  1.1870 -	    by (auto dest: widen_trans)
  1.1871 -	  then
  1.1872 -	  have "normal ((set_lvars (locals (store s2))) s4)
  1.1873 +            by (auto dest: widen_trans)
  1.1874 +          then
  1.1875 +          have "normal ((set_lvars (locals (store s2))) s4)
  1.1876               \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  1.1877 -	    by (cases s4) auto
  1.1878 -	  moreover note error_free_s4 T
  1.1879 -	  ultimately 
  1.1880 -	  show ?thesis
  1.1881 -	    by simp
  1.1882 -	qed
  1.1883 +            by (cases s4) auto
  1.1884 +          moreover note error_free_s4 T
  1.1885 +          ultimately 
  1.1886 +          show ?thesis
  1.1887 +            by simp
  1.1888 +        qed
  1.1889        qed
  1.1890      qed
  1.1891    next
  1.1892 @@ -3393,7 +3393,7 @@
  1.1893        from eval_init 
  1.1894        have "(dom (locals (store ((Norm s0)::state)))) 
  1.1895                       \<subseteq> (dom (locals (store s1)))"
  1.1896 -	by (rule dom_locals_eval_mono_elim)
  1.1897 +        by (rule dom_locals_eval_mono_elim)
  1.1898        with da_c show thesis by (rule da_weakenE) (rule that)
  1.1899      qed
  1.1900      from conf_s1 wt_c da_C' 
  1.1901 @@ -3412,40 +3412,40 @@
  1.1902      proof -
  1.1903        from iscls_D
  1.1904        have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
  1.1905 -	by auto
  1.1906 +        by auto
  1.1907        from eval_init wf
  1.1908        have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  1.1909 -	by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  1.1910 +        by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  1.1911        from eval_c _ wt_c wf
  1.1912        have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  1.1913 -	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  1.1914 +        by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  1.1915        moreover 
  1.1916        note `s3 =
  1.1917                  (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  1.1918                          abrupt s2 = Some (Jump (Cont l))
  1.1919                   then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
  1.1920        ultimately show ?thesis
  1.1921 -	by force
  1.1922 +        by force
  1.1923      qed
  1.1924      moreover
  1.1925      {
  1.1926        assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
  1.1927        have "Result \<in> dom (locals (store s2))"
  1.1928        proof -
  1.1929 -	from normal_upd_s2
  1.1930 -	have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  1.1931 -	  by (cases s2) (simp add: absorb_def)
  1.1932 -	thus ?thesis
  1.1933 -	proof 
  1.1934 -	  assume "normal s2"
  1.1935 -	  with eval_c wt_c da_C' wf res nrm_C'
  1.1936 -	  show ?thesis
  1.1937 -	    by (cases rule: da_good_approxE') blast
  1.1938 -	next
  1.1939 -	  assume "abrupt s2 = Some (Jump Ret)"
  1.1940 -	  with conf_s2 show ?thesis
  1.1941 -	    by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  1.1942 -	qed 
  1.1943 +        from normal_upd_s2
  1.1944 +        have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  1.1945 +          by (cases s2) (simp add: absorb_def)
  1.1946 +        thus ?thesis
  1.1947 +        proof 
  1.1948 +          assume "normal s2"
  1.1949 +          with eval_c wt_c da_C' wf res nrm_C'
  1.1950 +          show ?thesis
  1.1951 +            by (cases rule: da_good_approxE') blast
  1.1952 +        next
  1.1953 +          assume "abrupt s2 = Some (Jump Ret)"
  1.1954 +          with conf_s2 show ?thesis
  1.1955 +            by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  1.1956 +        qed 
  1.1957        qed
  1.1958      }
  1.1959      moreover note T resultT
  1.1960 @@ -3494,7 +3494,7 @@
  1.1961              accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  1.1962         eq_accC_accC': "accC=accC'" and
  1.1963                  stat: "stat=is_static f" and
  1.1964 -	           T: "T=(Inl (type f))"
  1.1965 +                   T: "T=(Inl (type f))"
  1.1966        by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  1.1967      from FVar.prems eq_accC_accC'
  1.1968      have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.1969 @@ -3522,10 +3522,10 @@
  1.1970      proof -
  1.1971        from eval_init
  1.1972        have "(dom (locals (store ((Norm s0)::state)))) 
  1.1973 -	       \<subseteq> (dom (locals (store s1)))"
  1.1974 -	by (rule dom_locals_eval_mono_elim)
  1.1975 +               \<subseteq> (dom (locals (store s1)))"
  1.1976 +        by (rule dom_locals_eval_mono_elim)
  1.1977        with da_e show thesis
  1.1978 -	by (rule da_weakenE) (rule that)
  1.1979 +        by (rule da_weakenE) (rule that)
  1.1980      qed
  1.1981      with conf_s1 wt_e 
  1.1982      obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.1983 @@ -3549,41 +3549,41 @@
  1.1984      proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  1.1985        assume normal: "normal s2'"
  1.1986        obtain vv vf x2 store2 store2'
  1.1987 -	where  v: "v=(vv,vf)" and
  1.1988 +        where  v: "v=(vv,vf)" and
  1.1989                s2: "s2=(x2,store2)" and
  1.1990           store2': "store s2' = store2'"
  1.1991 -	by (cases v,cases s2,cases s2') blast
  1.1992 +        by (cases v,cases s2,cases s2') blast
  1.1993        from iscls_statDeclC obtain c
  1.1994 -	where c: "class G statDeclC = Some c"
  1.1995 -	by auto
  1.1996 +        where c: "class G statDeclC = Some c"
  1.1997 +        by auto
  1.1998        have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  1.1999        proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  1.2000                                 statC G c L "store s1"])
  1.2001 -	from v normal s2 fvar stat store2' 
  1.2002 -	show "((vv, vf), Norm store2') = 
  1.2003 +        from v normal s2 fvar stat store2' 
  1.2004 +        show "((vv, vf), Norm store2') = 
  1.2005                 fvar statDeclC (static f) fn a (x2, store2)"
  1.2006 -	  by (auto simp add: member_is_static_simp)
  1.2007 -	from accfield iscls_statC wf
  1.2008 -	show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  1.2009 -	  by (auto dest!: accfield_fields dest: fields_declC)
  1.2010 -	from accfield
  1.2011 -	show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
  1.2012 -	  by (auto dest!: accfield_fields)
  1.2013 -	from wf show "wf_prog G" .
  1.2014 -	from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  1.2015 -	  by auto
  1.2016 -	from fld wf iscls_statC
  1.2017 -	show "statDeclC \<noteq> Object "
  1.2018 -	  by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  1.2019 -	from c show "class G statDeclC = Some c" .
  1.2020 -	from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.2021 -	from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  1.2022 -	from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  1.2023 -	  by simp
  1.2024 +          by (auto simp add: member_is_static_simp)
  1.2025 +        from accfield iscls_statC wf
  1.2026 +        show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  1.2027 +          by (auto dest!: accfield_fields dest: fields_declC)
  1.2028 +        from accfield
  1.2029 +        show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
  1.2030 +          by (auto dest!: accfield_fields)
  1.2031 +        from wf show "wf_prog G" .
  1.2032 +        from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  1.2033 +          by auto
  1.2034 +        from fld wf iscls_statC
  1.2035 +        show "statDeclC \<noteq> Object "
  1.2036 +          by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  1.2037 +        from c show "class G statDeclC = Some c" .
  1.2038 +        from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.2039 +        from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  1.2040 +        from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  1.2041 +          by simp
  1.2042        qed
  1.2043        with v s2 store2'  
  1.2044        show ?thesis
  1.2045 -	by simp
  1.2046 +        by simp
  1.2047      qed
  1.2048      from fvar error_free_s2
  1.2049      have "error_free s2'"
  1.2050 @@ -3629,67 +3629,67 @@
  1.2051        moreover
  1.2052        from eq_s2_s1 False have  "\<not> normal s2" by simp
  1.2053        then have "snd (avar G i a s2) = s2"
  1.2054 -	by (cases s2) (simp add: avar_def2)
  1.2055 +        by (cases s2) (simp add: avar_def2)
  1.2056        with avar have "s2'=s2"
  1.2057 -	by (cases "(avar G i a s2)") simp
  1.2058 +        by (cases "(avar G i a s2)") simp
  1.2059        ultimately show ?thesis
  1.2060 -	using conf_s1 error_free_s1
  1.2061 -	by auto
  1.2062 +        using conf_s1 error_free_s1
  1.2063 +        by auto
  1.2064      next
  1.2065        case True
  1.2066        obtain A' where 
  1.2067 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  1.2068 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  1.2069        proof -
  1.2070 -	from eval_e1 wt_e1 da_e1 wf True
  1.2071 -	have "nrm E1 \<subseteq> dom (locals (store s1))"
  1.2072 -	  by (cases rule: da_good_approxE') iprover
  1.2073 -	with da_e2 show thesis
  1.2074 -	  by (rule da_weakenE) (rule that)
  1.2075 +        from eval_e1 wt_e1 da_e1 wf True
  1.2076 +        have "nrm E1 \<subseteq> dom (locals (store s1))"
  1.2077 +          by (cases rule: da_good_approxE') iprover
  1.2078 +        with da_e2 show thesis
  1.2079 +          by (rule da_weakenE) (rule that)
  1.2080        qed
  1.2081        with conf_s1 wt_e2
  1.2082        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1.2083 -	by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.2084 +        by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  1.2085        from avar 
  1.2086        have "store s2'=store s2"
  1.2087 -	by (cases s2) (simp add: avar_def2)
  1.2088 +        by (cases s2) (simp add: avar_def2)
  1.2089        with avar conf_s2 
  1.2090        have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1.2091 -	by (cases s2) (auto simp add: avar_def2)
  1.2092 +        by (cases s2) (auto simp add: avar_def2)
  1.2093        from avar error_free_s2
  1.2094        have error_free_s2': "error_free s2'"
  1.2095 -	by (cases s2) (auto simp add: avar_def2 )
  1.2096 +        by (cases s2) (auto simp add: avar_def2 )
  1.2097        have "normal s2' \<Longrightarrow> 
  1.2098          G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.2099        proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  1.2100 -	assume normal: "normal s2'"
  1.2101 -	show ?thesis
  1.2102 -	proof -
  1.2103 -	  obtain vv vf x1 store1 x2 store2 store2'
  1.2104 -	    where  v: "v=(vv,vf)" and
  1.2105 +        assume normal: "normal s2'"
  1.2106 +        show ?thesis
  1.2107 +        proof -
  1.2108 +          obtain vv vf x1 store1 x2 store2 store2'
  1.2109 +            where  v: "v=(vv,vf)" and
  1.2110                    s1: "s1=(x1,store1)" and
  1.2111                    s2: "s2=(x2,store2)" and
  1.2112 -	     store2': "store2'=store s2'"
  1.2113 -	    by (cases v,cases s1, cases s2, cases s2') blast 
  1.2114 -	  have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.2115 -	  proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  1.2116 +             store2': "store2'=store s2'"
  1.2117 +            by (cases v,cases s1, cases s2, cases s2') blast 
  1.2118 +          have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  1.2119 +          proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  1.2120                                    OF wf])
  1.2121 -	    from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  1.2122 -	      by simp
  1.2123 -	    from v normal s2 store2' avar 
  1.2124 -	    show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  1.2125 -	      by auto
  1.2126 -	    from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.2127 -	    from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  1.2128 -	    from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  1.2129 -	  qed
  1.2130 -	  with v s1 s2 store2' 
  1.2131 -	  show ?thesis
  1.2132 -	    by simp
  1.2133 -	qed
  1.2134 +            from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  1.2135 +              by simp
  1.2136 +            from v normal s2 store2' avar 
  1.2137 +            show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  1.2138 +              by auto
  1.2139 +            from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  1.2140 +            from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  1.2141 +            from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  1.2142 +          qed
  1.2143 +          with v s1 s2 store2' 
  1.2144 +          show ?thesis
  1.2145 +            by simp
  1.2146 +        qed
  1.2147        qed
  1.2148        with conf_s2' error_free_s2' T 
  1.2149        show ?thesis 
  1.2150 -	by auto
  1.2151 +        by auto
  1.2152      qed
  1.2153    next
  1.2154      case (Nil s0 L accC T)
  1.2155 @@ -3726,30 +3726,30 @@
  1.2156        with eval_es have "s2=s1" by auto
  1.2157        with False conf_s1 error_free_s1
  1.2158        show ?thesis
  1.2159 -	by auto
  1.2160 +        by auto
  1.2161      next
  1.2162        case True
  1.2163        obtain A' where 
  1.2164 -	"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  1.2165 +        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  1.2166        proof -
  1.2167 -	from eval_e wt_e da_e wf True
  1.2168 -	have "nrm E \<subseteq> dom (locals (store s1))"
  1.2169 -	  by (cases rule: da_good_approxE') iprover
  1.2170 -	with da_es show thesis
  1.2171 -	  by (rule da_weakenE) (rule that)
  1.2172 +        from eval_e wt_e da_e wf True
  1.2173 +        have "nrm E \<subseteq> dom (locals (store s1))"
  1.2174 +          by (cases rule: da_good_approxE') iprover
  1.2175 +        with da_es show thesis
  1.2176 +          by (rule da_weakenE) (rule that)
  1.2177        qed
  1.2178        with conf_s1 wt_es
  1.2179        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  1.2180             error_free_s2: "error_free s2" and
  1.2181             conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  1.2182 -	by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  1.2183 +        by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  1.2184        moreover
  1.2185        from True eval_es conf_v 
  1.2186        have conf_v': "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  1.2187 -	apply clarify
  1.2188 -	apply (rule conf_gext)
  1.2189 -	apply (auto dest: eval_gext)
  1.2190 -	done
  1.2191 +        apply clarify
  1.2192 +        apply (rule conf_gext)
  1.2193 +        apply (auto dest: eval_gext)
  1.2194 +        done
  1.2195        ultimately show ?thesis using T by simp
  1.2196      qed
  1.2197    qed
  1.2198 @@ -3956,19 +3956,19 @@
  1.2199                         P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
  1.2200        have Q
  1.2201        proof -
  1.2202 -	obtain C2' where 
  1.2203 -	  da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  1.2204 -	proof -
  1.2205 -	  from eval_c1 wt_c1 da_c1 wf normal_s1
  1.2206 -	  have "nrm C1 \<subseteq> dom (locals (store s1))"
  1.2207 -	    by (cases rule: da_good_approxE') iprover
  1.2208 -	  with da_c2 show thesis
  1.2209 -	    by (rule da_weakenE) (rule that)
  1.2210 -	qed
  1.2211 -	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.2212 -	  by (rule Comp.hyps)
  1.2213 -	with da show ?thesis
  1.2214 -	  using elim by iprover
  1.2215 +        obtain C2' where 
  1.2216 +          da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  1.2217 +        proof -
  1.2218 +          from eval_c1 wt_c1 da_c1 wf normal_s1
  1.2219 +          have "nrm C1 \<subseteq> dom (locals (store s1))"
  1.2220 +            by (cases rule: da_good_approxE') iprover
  1.2221 +          with da_c2 show thesis
  1.2222 +            by (rule da_weakenE) (rule that)
  1.2223 +        qed
  1.2224 +        with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.2225 +          by (rule Comp.hyps)
  1.2226 +        with da show ?thesis
  1.2227 +          using elim by iprover
  1.2228        qed
  1.2229      }
  1.2230      with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
  1.2231 @@ -4003,28 +4003,28 @@
  1.2232                                \<rbrakk> \<Longrightarrow> Q"
  1.2233        have Q
  1.2234        proof -
  1.2235 -	obtain C' where
  1.2236 -	  da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.2237 +        obtain C' where
  1.2238 +          da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1.2239                  (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
  1.2240 -	proof -
  1.2241 -	  from eval_e have 
  1.2242 -	    "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.2243 -	    by (rule dom_locals_eval_mono_elim)
  1.2244 +        proof -
  1.2245 +          from eval_e have 
  1.2246 +            "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1.2247 +            by (rule dom_locals_eval_mono_elim)
  1.2248            moreover
  1.2249 -	  from eval_e normal_s1 wt_e 
  1.2250 -	  have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.2251 -	    by (rule assigns_if_good_approx')
  1.2252 -	  ultimately 
  1.2253 -	  have "dom (locals (store ((Norm s0)::state))) 
  1.2254 +          from eval_e normal_s1 wt_e 
  1.2255 +          have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.2256 +            by (rule assigns_if_good_approx')
  1.2257 +          ultimately 
  1.2258 +          have "dom (locals (store ((Norm s0)::state))) 
  1.2259              \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1.2260 -	    by (rule Un_least)
  1.2261 -	  with da_then_else show thesis
  1.2262 -	    by (rule da_weakenE) (rule that)
  1.2263 -	qed
  1.2264 -	with wt_then_else
  1.2265 -	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.2266 -	  by (rule If.hyps)
  1.2267 -	with da show ?thesis using elim by iprover
  1.2268 +            by (rule Un_least)
  1.2269 +          with da_then_else show thesis
  1.2270 +            by (rule da_weakenE) (rule that)
  1.2271 +        qed
  1.2272 +        with wt_then_else
  1.2273 +        have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  1.2274 +          by (rule If.hyps)
  1.2275 +        with da show ?thesis using elim by iprover
  1.2276        qed
  1.2277      }
  1.2278      with eval_e eval_then_else wt_e wt_then_else da_e P_e