src/HOL/Bali/DefiniteAssignmentCorrect.thy
author wenzelm
Wed Nov 01 20:46:23 2017 +0100 (22 months ago)
changeset 66983 df83b66f1d94
parent 62042 6c6ccf573479
child 68451 c34aa23a1fb6
permissions -rw-r--r--
proper merge (amending fb46c031c841);
     1 subsection \<open>Correctness of Definite Assignment\<close>
     2 
     3 theory DefiniteAssignmentCorrect imports WellForm Eval begin
     4 
     5 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
     6 
     7 lemma sxalloc_no_jump:
     8   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
     9            no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
    10    shows "abrupt s1 \<noteq> Some (Jump j)"
    11 using sxalloc no_jmp
    12 by cases simp_all
    13 
    14 lemma sxalloc_no_jump':
    15   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
    16           jump:  "abrupt s1 = Some (Jump j)"
    17  shows "abrupt s0 = Some (Jump j)"
    18 using sxalloc jump
    19 by cases simp_all
    20 
    21 lemma halloc_no_jump:
    22   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    23            no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
    24    shows "abrupt s1 \<noteq> Some (Jump j)"
    25 using halloc no_jmp
    26 by cases simp_all
    27 
    28 lemma halloc_no_jump':
    29   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    30           jump:  "abrupt s1 = Some (Jump j)"
    31   shows "abrupt s0 = Some (Jump j)"
    32 using halloc jump
    33 by cases simp_all
    34 
    35 lemma Body_no_jump: 
    36    assumes eval: "G\<turnstile>s0 \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
    37            jump: "abrupt s0 \<noteq> Some (Jump j)"
    38    shows "abrupt s1 \<noteq> Some (Jump j)"
    39 proof (cases "normal s0")
    40   case True
    41   with eval obtain s0' where eval': "G\<turnstile>Norm s0' \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
    42                              s0: "s0 = Norm s0'"
    43     by (cases s0) simp
    44   from eval' obtain s2 where
    45      s1: "s1 = abupd (absorb Ret)
    46              (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
    47                      abrupt s2 = Some (Jump (Cont l))
    48               then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"
    49     by cases simp
    50   show ?thesis
    51   proof (cases "\<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
    52                    abrupt s2 = Some (Jump (Cont l))")
    53     case True
    54     with s1 have "abrupt s1 = Some (Error CrossMethodJump)"
    55       by (cases s2) simp
    56     thus ?thesis by simp
    57   next
    58     case False
    59     with s1 have "s1=abupd (absorb Ret) s2"
    60       by simp
    61     with False show ?thesis
    62       by (cases s2,cases j) (auto simp add: absorb_def)
    63   qed
    64 next
    65   case False
    66   with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"
    67                                  "s0 = (Some abr, s0')"
    68     by (cases s0) fastforce
    69   with this jump
    70   show ?thesis
    71     by (cases) (simp)
    72 qed
    73 
    74 lemma Methd_no_jump: 
    75    assumes eval: "G\<turnstile>s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1" and
    76            jump: "abrupt s0 \<noteq> Some (Jump j)"
    77    shows "abrupt s1 \<noteq> Some (Jump j)"
    78 proof (cases "normal s0")
    79   case True
    80    with eval obtain s0' where "G\<turnstile>Norm s0' \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1" 
    81                               "s0 = Norm s0'"
    82     by (cases s0) simp
    83   then obtain D' body where "G\<turnstile>s0 \<midarrow>Body D' body-\<succ>v\<rightarrow>s1"
    84     by (cases) (simp add: body_def2)
    85   from this jump
    86   show ?thesis
    87     by (rule Body_no_jump)
    88 next
    89   case False
    90   with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"
    91                                  "s0 = (Some abr, s0')"
    92     by (cases s0) fastforce
    93   with this jump
    94   show ?thesis
    95     by (cases) (simp)
    96 qed
    97 
    98 lemma jumpNestingOkS_mono: 
    99   assumes jumpNestingOk_l': "jumpNestingOkS jmps' c" 
   100       and      subset: "jmps' \<subseteq> jmps"
   101  shows "jumpNestingOkS jmps c"
   102 proof -
   103     have True and True and 
   104        "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c" 
   105   proof (induct rule: var.induct expr.induct stmt.induct)
   106     case (Lab j c jmps' jmps)
   107     note jmpOk = \<open>jumpNestingOkS jmps' (j\<bullet> c)\<close>
   108     note jmps = \<open>jmps' \<subseteq> jmps\<close>
   109     with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
   110     moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
   111     ultimately
   112     have "jumpNestingOkS ({j} \<union> jmps) c"
   113       by (rule Lab.hyps)
   114     thus ?case 
   115       by simp
   116   next
   117     case (Jmp j jmps' jmps) 
   118     thus ?case 
   119       by (cases j) auto
   120   next
   121     case (Comp c1 c2 jmps' jmps)
   122     from Comp.prems 
   123     have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto)
   124     moreover from Comp.prems
   125     have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto)
   126     ultimately show ?case
   127       by simp
   128   next
   129     case (If' e c1 c2 jmps' jmps)
   130     from If'.prems 
   131     have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
   132     moreover from If'.prems 
   133     have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
   134     ultimately show ?case
   135       by simp
   136   next
   137     case (Loop l e c jmps' jmps)
   138     from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close>
   139     have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
   140     moreover
   141     from \<open>jmps' \<subseteq> jmps\<close>
   142     have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
   143     ultimately
   144     have "jumpNestingOkS ({Cont l} \<union> jmps) c"
   145       by (rule Loop.hyps)
   146     thus ?case by simp
   147   next
   148     case (TryC c1 C vn c2 jmps' jmps)
   149     from TryC.prems 
   150     have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto)
   151     moreover from TryC.prems 
   152     have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto)
   153     ultimately show ?case
   154       by simp
   155   next
   156     case (Fin c1 c2 jmps' jmps)
   157     from Fin.prems 
   158     have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto)
   159     moreover from Fin.prems 
   160     have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto)
   161     ultimately show ?case
   162       by simp
   163   qed (simp_all)
   164   with jumpNestingOk_l' subset
   165   show ?thesis
   166     by iprover
   167 qed
   168    
   169 corollary jumpNestingOk_mono: 
   170   assumes jmpOk: "jumpNestingOk jmps' t" 
   171      and subset: "jmps' \<subseteq> jmps"
   172   shows  "jumpNestingOk jmps t"
   173 proof (cases t)
   174   case (In1 expr_stmt)
   175   show ?thesis
   176   proof (cases expr_stmt)
   177     case (Inl e)
   178     with In1 show ?thesis by simp
   179   next
   180     case (Inr s)
   181     with In1 jmpOk subset show ?thesis by (auto intro: jumpNestingOkS_mono)
   182   qed
   183 qed (simp_all)
   184 
   185 lemma assign_abrupt_propagation: 
   186  assumes f_ok: "abrupt (f n s) \<noteq> x"
   187    and    ass: "abrupt (assign f n s) = x"
   188   shows "abrupt s = x"
   189 proof (cases x)
   190   case None
   191   with ass show ?thesis
   192     by (cases s) (simp add: assign_def Let_def)
   193 next
   194   case (Some xcpt)
   195   from f_ok
   196   obtain xf sf where "f n s = (xf,sf)"
   197     by (cases "f n s")
   198   with Some ass f_ok show ?thesis
   199     by (cases s) (simp add: assign_def Let_def)
   200 qed
   201  
   202 lemma wt_init_comp_ty': 
   203 "is_acc_type (prg Env) (pid (cls Env)) T \<Longrightarrow> Env\<turnstile>init_comp_ty T\<Colon>\<surd>"
   204 apply (unfold init_comp_ty_def)
   205 apply (clarsimp simp add: accessible_in_RefT_simp 
   206                           is_acc_type_def is_acc_class_def)
   207 done
   208 
   209 lemma fvar_upd_no_jump: 
   210       assumes upd: "upd = snd (fst (fvar statDeclC stat fn a s'))"
   211         and noJmp: "abrupt s \<noteq> Some (Jump j)"
   212         shows "abrupt (upd val s) \<noteq> Some (Jump j)"
   213 proof (cases "stat")
   214   case True
   215   with noJmp upd
   216   show ?thesis
   217     by (cases s) (simp add: fvar_def2)
   218 next
   219   case False
   220   with noJmp upd
   221   show ?thesis
   222     by (cases s) (simp add: fvar_def2)
   223 qed
   224 
   225 
   226 lemma avar_state_no_jump: 
   227   assumes jmp: "abrupt (snd (avar G i a s)) = Some (Jump j)"
   228   shows "abrupt s = Some (Jump j)"
   229 proof (cases "normal s")
   230   case True with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
   231 next
   232   case False with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
   233 qed
   234 
   235 lemma avar_upd_no_jump: 
   236       assumes upd: "upd = snd (fst (avar G i a s'))"
   237         and noJmp: "abrupt s \<noteq> Some (Jump j)"
   238         shows "abrupt (upd val s) \<noteq> Some (Jump j)"
   239 using upd noJmp
   240 by (cases s) (simp add: avar_def2 abrupt_if_def)
   241 
   242 
   243 text \<open>
   244 The next theorem expresses: If jumps (breaks, continues, returns) are nested
   245 correctly, we won't find an unexpected jump in the result state of the 
   246 evaluation. For exeample, a break can't leave its enclosing loop, an return
   247 cant leave its enclosing method.
   248 To proove this, the method call is critical. Allthough the
   249 wellformedness of the whole program guarantees that the jumps (breaks,continues
   250 and returns) are nested
   251 correctly in all method bodies, the call rule alone does not guarantee that I
   252 will call a method or even a class that is part of the program due to dynamic
   253 binding! To be able to enshure this we need a kind of conformance of the
   254 state, like in the typesafety proof. But then we will redo the typesafty
   255 proof here. It would be nice if we could find an easy precondition that will
   256 guarantee that all calls will actually call classes and methods of the current
   257 program, which can be instantiated in the typesafty proof later on.
   258 To fix this problem, I have instrumented the semantic definition of a call
   259 to filter out any breaks in the state and to throw an error instead. 
   260 
   261 To get an induction hypothesis which is strong enough to perform the
   262 proof, we can't just 
   263 assume @{term jumpNestingOk} for the empty set and conlcude, that no jump at 
   264 all will be in the resulting state,  because the set is altered by 
   265 the statements @{term Lab} and @{term While}. 
   266 
   267 The wellformedness of the program is used to enshure that for all
   268 classinitialisations and methods the nesting of jumps is wellformed, too.
   269 \<close>  
   270 theorem jumpNestingOk_eval:
   271   assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   272      and jmpOk: "jumpNestingOk jmps t" 
   273      and wt: "Env\<turnstile>t\<Colon>T" 
   274      and wf: "wf_prog G"
   275      and  G: "prg Env = G"
   276      and no_jmp: "\<forall>j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"
   277                     (is "?Jmp jmps s0")
   278   shows  "(\<forall>j. fst s1 = Some (Jump j) \<longrightarrow> j \<in> jmps) \<and>
   279                  (normal s1 \<longrightarrow>
   280                   (\<forall> w upd. v=In2 (w,upd)
   281                    \<longrightarrow>   (\<forall> s j val.
   282                           abrupt s \<noteq> Some (Jump j) \<longrightarrow>
   283                           abrupt (upd val s) \<noteq> Some (Jump j))))"
   284         (is "?Jmp jmps s1 \<and> ?Upd v s1")  
   285 proof -
   286   let ?HypObj = "\<lambda> t s0 s1 v.
   287        (\<forall> jmps T Env. 
   288           ?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \<longrightarrow> prg Env=G\<longrightarrow>
   289           ?Jmp jmps s1 \<and> ?Upd v s1)"
   290   \<comment> \<open>Variable \<open>?HypObj\<close> is the following goal spelled in terms of
   291         the object logic, instead of the meta logic. It is needed in some
   292         cases of the induction were, the atomize-rulify process of induct 
   293         does not work fine, because the eval rules mix up object and meta
   294         logic. See for example the case for the loop.\<close> 
   295   from eval 
   296   have "\<And> jmps T Env. \<lbrakk>?Jmp jmps s0; jumpNestingOk jmps t; Env\<turnstile>t\<Colon>T;prg Env=G\<rbrakk>
   297             \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1" 
   298         (is "PROP ?Hyp t s0 s1 v")
   299   \<comment> \<open>We need to abstract over @{term jmps} since @{term jmps} are extended
   300         during analysis of @{term Lab}. Also we need to abstract over 
   301         @{term T} and @{term Env} since they are altered in various
   302         typing judgements.\<close>    
   303   proof (induct)   
   304     case Abrupt thus ?case by simp 
   305   next
   306     case Skip thus ?case by simp
   307   next
   308     case Expr thus ?case by (elim wt_elim_cases) simp
   309   next
   310     case (Lab s0 c s1 jmp jmps T Env) 
   311     note jmpOK = \<open>jumpNestingOk jmps (In1r (jmp\<bullet> c))\<close>
   312     note G = \<open>prg Env = G\<close>
   313     have wt_c: "Env\<turnstile>c\<Colon>\<surd>" 
   314       using Lab.prems by (elim wt_elim_cases)
   315     { 
   316       fix j
   317       assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)"
   318       have "j\<in>jmps"          
   319       proof -
   320         from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
   321           by (cases s1) (simp add: absorb_def)
   322         note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>
   323         from ab_s1 have "j \<noteq> jmp" 
   324           by (cases s1) (simp add: absorb_def)
   325         moreover have "j \<in> {jmp} \<union> jmps"
   326         proof -
   327           from jmpOK 
   328           have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp
   329           with wt_c jmp_s1 G hyp_c
   330           show ?thesis
   331             by - (rule hyp_c [THEN conjunct1,rule_format],simp)
   332         qed
   333         ultimately show ?thesis
   334           by simp
   335       qed
   336     }
   337     thus ?case by simp
   338   next
   339     case (Comp s0 c1 s1 c2 s2 jmps T Env)
   340     note jmpOk = \<open>jumpNestingOk jmps (In1r (c1;; c2))\<close>
   341     note G = \<open>prg Env = G\<close>
   342     from Comp.prems obtain
   343       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
   344       by (elim wt_elim_cases)
   345     {
   346       fix j
   347       assume abr_s2: "abrupt s2 = Some (Jump j)"
   348       have "j\<in>jmps"
   349       proof -
   350         have jmp: "?Jmp jmps s1"
   351         proof -
   352           note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>
   353           with wt_c1 jmpOk G 
   354           show ?thesis by simp
   355         qed
   356         moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>
   357         have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
   358         moreover note wt_c2 G abr_s2
   359         ultimately show "j \<in> jmps"
   360           by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
   361       qed
   362     } thus ?case by simp
   363   next
   364     case (If s0 e b s1 c1 c2 s2 jmps T Env)
   365     note jmpOk = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close>
   366     note G = \<open>prg Env = G\<close>
   367     from If.prems obtain 
   368               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
   369       wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
   370       by (elim wt_elim_cases) simp
   371     { 
   372       fix j
   373       assume jmp: "abrupt s2 = Some (Jump j)"
   374       have "j\<in>jmps"
   375       proof -
   376         note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
   377         with wt_e G have "?Jmp jmps s1" 
   378           by simp
   379         moreover note hyp_then_else =
   380           \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>
   381         have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
   382           using jmpOk by (cases "the_Bool b") simp_all
   383         moreover note wt_then_else G jmp
   384         ultimately show "j\<in> jmps" 
   385           by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])
   386       qed
   387     }
   388     thus ?case by simp
   389   next
   390     case (Loop s0 e b s1 c s2 l s3 jmps T Env)
   391     note jmpOk = \<open>jumpNestingOk jmps (In1r (l\<bullet> While(e) c))\<close>
   392     note G = \<open>prg Env = G\<close>
   393     note wt = \<open>Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close>
   394     then obtain 
   395               wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
   396               wt_c: "Env\<turnstile>c\<Colon>\<surd>"
   397       by (elim wt_elim_cases)
   398     {
   399       fix j
   400       assume jmp: "abrupt s3 = Some (Jump j)" 
   401       have "j\<in>jmps"
   402       proof -
   403         note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
   404         with wt_e G have jmp_s1: "?Jmp jmps s1" 
   405           by simp
   406         show ?thesis
   407         proof (cases "the_Bool b")
   408           case False
   409           from Loop.hyps
   410           have "s3=s1"
   411             by (simp (no_asm_use) only: if_False False) 
   412           with jmp_s1 jmp have "j \<in> jmps" by simp
   413           thus ?thesis by simp
   414         next
   415           case True
   416           from Loop.hyps 
   417             (* Because of the mixture of object and pure logic in the rule 
   418                eval.If the atomization-rulification of the induct method 
   419                leaves the hypothesis in object logic *)
   420           have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"
   421             apply (simp (no_asm_use) only: True if_True )
   422             apply (erule conjE)+
   423             apply assumption
   424             done
   425           note hyp_c = this [rule_format (no_asm)]
   426           moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"
   427             by simp
   428           moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
   429           ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
   430             using wt_c G by iprover
   431           have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
   432           proof -
   433             {
   434               fix j'
   435               assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')"
   436               have "j' \<in> jmps"
   437               proof (cases "j' = Cont l")
   438                 case True
   439                 with abs show ?thesis
   440                   by (cases s2) (simp add: absorb_def)
   441               next
   442                 case False 
   443                 with abs have "abrupt s2 = Some (Jump j')"
   444                   by (cases s2) (simp add: absorb_def) 
   445                 with jmp_s2 False show ?thesis
   446                   by simp
   447               qed
   448             }
   449             thus ?thesis by simp
   450           qed
   451           moreover
   452           from Loop.hyps
   453           have "?HypObj (In1r (l\<bullet> While(e) c)) 
   454                         (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::vals)"
   455             apply (simp (no_asm_use) only: True if_True)
   456             apply (erule conjE)+
   457             apply assumption
   458             done
   459           note hyp_w = this [rule_format (no_asm)]
   460           note jmpOk wt G jmp 
   461           ultimately show "j\<in> jmps" 
   462             by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])
   463         qed
   464       qed
   465     }
   466     thus ?case by simp
   467   next
   468     case (Jmp s j jmps T Env) thus ?case by simp
   469   next
   470     case (Throw s0 e a s1 jmps T Env)
   471     note jmpOk = \<open>jumpNestingOk jmps (In1r (Throw e))\<close>
   472     note G = \<open>prg Env = G\<close>
   473     from Throw.prems obtain Te where 
   474       wt_e: "Env\<turnstile>e\<Colon>-Te" 
   475       by (elim wt_elim_cases)
   476     {
   477       fix j
   478       assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
   479       have "j\<in>jmps"
   480       proof -
   481         from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
   482         have "?Jmp jmps s1" using wt_e G by simp
   483         moreover
   484         from jmp 
   485         have "abrupt s1 = Some (Jump j)"
   486           by (cases s1) (simp add: throw_def abrupt_if_def)
   487         ultimately show "j \<in> jmps" by simp
   488       qed
   489     }
   490     thus ?case by simp
   491   next
   492     case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
   493     note jmpOk = \<open>jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))\<close>
   494     note G = \<open>prg Env = G\<close>
   495     from Try.prems obtain 
   496       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
   497       wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
   498       by (elim wt_elim_cases)
   499     {
   500       fix j
   501       assume jmp: "abrupt s3 = Some (Jump j)"
   502       have "j\<in>jmps"
   503       proof -
   504         note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>
   505         with jmpOk wt_c1 G
   506         have jmp_s1: "?Jmp jmps s1" by simp
   507         note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
   508         show "j \<in> jmps"
   509         proof (cases "G,s2\<turnstile>catch C")
   510           case False
   511           from Try.hyps have "s3=s2" 
   512             by (simp (no_asm_use) only: False if_False)
   513           with jmp have "abrupt s1 = Some (Jump j)"
   514             using sxalloc_no_jump' [OF s2] by simp
   515           with jmp_s1 
   516           show ?thesis by simp
   517         next
   518           case True
   519           with Try.hyps 
   520           have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"
   521             apply (simp (no_asm_use) only: True if_True simp_thms)
   522             apply (erule conjE)+
   523             apply assumption
   524             done
   525           note hyp_c2 = this [rule_format (no_asm)]
   526           from jmp_s1 sxalloc_no_jump' [OF s2] 
   527           have "?Jmp jmps s2"
   528             by simp
   529           hence "?Jmp jmps (new_xcpt_var vn s2)"
   530             by (cases s2) simp
   531           moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
   532           moreover note wt_c2
   533           moreover from G 
   534           have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"
   535             by simp
   536           moreover note jmp
   537           ultimately show ?thesis 
   538             by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
   539         qed
   540       qed
   541     }
   542     thus ?case by simp
   543   next
   544     case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
   545     note jmpOk = \<open>jumpNestingOk jmps (In1r (c1 Finally c2))\<close>
   546     note G = \<open>prg Env = G\<close>
   547     from Fin.prems obtain 
   548       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
   549       by (elim wt_elim_cases)
   550     {
   551       fix j
   552       assume jmp: "abrupt s3 = Some (Jump j)" 
   553       have "j \<in> jmps"
   554       proof (cases "x1=Some (Jump j)")
   555         case True
   556         note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>
   557         with True jmpOk wt_c1 G show ?thesis 
   558           by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
   559       next
   560         case False
   561         note hyp_c2 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>
   562         note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
   563                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
   564         with False jmp have "abrupt s2 = Some (Jump j)"
   565           by (cases s2) (simp add: abrupt_if_def)
   566         with jmpOk wt_c2 G show ?thesis 
   567           by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
   568       qed
   569     }
   570     thus ?case by simp
   571   next
   572     case (Init C c s0 s3 s1 s2 jmps T Env)
   573     note \<open>jumpNestingOk jmps (In1r (Init C))\<close>
   574     note G = \<open>prg Env = G\<close>
   575     note \<open>the (class G C) = c\<close>
   576     with Init.prems have c: "class G C = Some c"
   577       by (elim wt_elim_cases) auto
   578     {
   579       fix j
   580       assume jmp: "abrupt s3 = (Some (Jump j))" 
   581       have "j\<in>jmps"
   582       proof (cases "inited C (globs s0)") 
   583         case True
   584         with Init.hyps have "s3=Norm s0"
   585           by simp
   586         with jmp
   587         have "False" by simp thus ?thesis ..
   588       next
   589         case False
   590         from wf c G
   591         have wf_cdecl: "wf_cdecl G (C,c)"
   592           by (simp add: wf_prog_cdecl)
   593         from Init.hyps
   594         have "?HypObj (In1r (if C = Object then Skip else Init (super c))) 
   595                             (Norm ((init_class_obj G C) s0)) s1 (\<diamondsuit>::vals)"
   596           apply (simp (no_asm_use) only: False if_False simp_thms)
   597           apply (erule conjE)+
   598           apply assumption
   599           done
   600         note hyp_s1 = this [rule_format (no_asm)]
   601         from wf_cdecl G have
   602           wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
   603           by (cases "C=Object")
   604              (auto dest: wf_cdecl_supD is_acc_classD) 
   605         from hyp_s1 [OF _ _ wt_super G]
   606         have "?Jmp jmps s1" 
   607           by simp
   608         hence jmp_s1: "?Jmp jmps ((set_lvars empty) s1)" by (cases s1) simp
   609         from False Init.hyps
   610         have "?HypObj (In1r (init c)) ((set_lvars empty) s1) s2 (\<diamondsuit>::vals)" 
   611           apply (simp (no_asm_use) only: False if_False simp_thms)
   612           apply (erule conjE)+
   613           apply assumption
   614           done
   615         note hyp_init_c = this [rule_format (no_asm)] 
   616         from wf_cdecl 
   617         have wt_init_c: "\<lparr>prg = G, cls = C, lcl = empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
   618           by (rule wf_cdecl_wt_init)
   619         from wf_cdecl have "jumpNestingOkS {} (init c)" 
   620           by (cases rule: wf_cdeclE)
   621         hence "jumpNestingOkS jmps (init c)"
   622           by (rule jumpNestingOkS_mono) simp
   623         moreover 
   624         have "abrupt s2 = Some (Jump j)"
   625         proof -
   626           from False Init.hyps 
   627           have "s3 = (set_lvars (locals (store s1))) s2"  by simp
   628           with jmp show ?thesis by (cases s2) simp
   629         qed
   630         ultimately show ?thesis
   631           using hyp_init_c [OF jmp_s1 _ wt_init_c]
   632           by simp
   633       qed
   634     }
   635     thus ?case by simp
   636   next
   637     case (NewC s0 C s1 a s2 jmps T Env)
   638     {
   639       fix j
   640       assume jmp: "abrupt s2 = Some (Jump j)"
   641       have "j\<in>jmps"
   642       proof - 
   643         note \<open>prg Env = G\<close>
   644         moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>
   645         moreover from wf NewC.prems 
   646         have "Env\<turnstile>(Init C)\<Colon>\<surd>"
   647           by (elim wt_elim_cases) (drule is_acc_classD,simp)
   648         moreover 
   649         have "abrupt s1 = Some (Jump j)"
   650         proof -
   651           from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis
   652             by (rule halloc_no_jump')
   653         qed
   654         ultimately show "j \<in> jmps" 
   655           by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)
   656       qed
   657     }
   658     thus ?case by simp
   659   next
   660     case (NewA s0 elT s1 e i s2 a s3 jmps T Env)
   661     {
   662       fix j
   663       assume jmp: "abrupt s3 = Some (Jump j)"
   664       have "j\<in>jmps"
   665       proof -
   666         note G = \<open>prg Env = G\<close>
   667         from NewA.prems 
   668         obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
   669                wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
   670           by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
   671         note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>
   672         with wt_init G 
   673         have "?Jmp jmps s1" 
   674           by (simp add: init_comp_ty_def)
   675         moreover
   676         note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>
   677         have "abrupt s2 = Some (Jump j)"
   678         proof -
   679           note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
   680           moreover note jmp
   681           ultimately 
   682           have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
   683             by (rule halloc_no_jump')
   684           thus ?thesis by (cases s2) auto
   685         qed
   686         ultimately show "j\<in>jmps" using wt_size G 
   687           by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
   688       qed
   689     }
   690     thus ?case by simp
   691   next
   692     case (Cast s0 e v s1 s2 cT jmps T Env)
   693     {
   694       fix j
   695       assume jmp: "abrupt s2 = Some (Jump j)"
   696       have "j\<in>jmps"
   697       proof -
   698         note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
   699         note \<open>prg Env = G\<close>
   700         moreover from Cast.prems
   701         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
   702         moreover 
   703         have "abrupt s1 = Some (Jump j)"
   704         proof -
   705           note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
   706           moreover note jmp
   707           ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
   708         qed
   709         ultimately show ?thesis 
   710           by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
   711       qed
   712     }
   713     thus ?case by simp
   714   next
   715     case (Inst s0 e v s1 b eT jmps T Env)
   716     {
   717       fix j
   718       assume jmp: "abrupt s1 = Some (Jump j)"
   719       have "j\<in>jmps"
   720       proof -
   721         note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
   722         note \<open>prg Env = G\<close>
   723         moreover from Inst.prems
   724         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
   725         moreover note jmp
   726         ultimately show "j\<in>jmps" 
   727           by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
   728       qed
   729     }
   730     thus ?case by simp
   731   next
   732     case Lit thus ?case by simp
   733   next
   734     case (UnOp s0 e v s1 unop jmps T Env)
   735     {
   736       fix j
   737       assume jmp: "abrupt s1 = Some (Jump j)"
   738       have "j\<in>jmps"
   739       proof -
   740         note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
   741         note \<open>prg Env = G\<close>
   742         moreover from UnOp.prems
   743         obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
   744         moreover note jmp
   745         ultimately show  "j\<in>jmps" 
   746           by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) 
   747       qed
   748     }
   749     thus ?case by simp
   750   next
   751     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env)
   752     {
   753       fix j
   754       assume jmp: "abrupt s2 = Some (Jump j)"
   755       have "j\<in>jmps"
   756       proof -
   757         note G = \<open>prg Env = G\<close>
   758         from BinOp.prems
   759         obtain e1T e2T where 
   760           wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
   761           wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
   762           by (elim wt_elim_cases)
   763         note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>
   764         with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
   765         note hyp_e2 =
   766           \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
   767                      s1 s2 (In1 v2)\<close>
   768         show "j\<in>jmps"
   769         proof (cases "need_second_arg binop v1")
   770           case True with jmp_s1 wt_e2 jmp G
   771           show ?thesis 
   772             by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
   773         next
   774           case False with jmp_s1 jmp G
   775           show ?thesis 
   776             by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)
   777         qed
   778       qed
   779     }
   780     thus ?case by simp
   781   next
   782     case Super thus ?case by simp
   783   next
   784     case (Acc s0 va v f s1 jmps T Env)
   785     {
   786       fix j
   787       assume jmp: "abrupt s1 = Some (Jump j)"
   788       have "j\<in>jmps"
   789       proof -
   790         note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>
   791         note \<open>prg Env = G\<close>
   792         moreover from Acc.prems
   793         obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
   794         moreover note jmp
   795         ultimately show "j\<in>jmps" 
   796           by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)
   797       qed
   798     }
   799     thus ?case by simp
   800   next
   801     case (Ass s0 va w f s1 e v s2 jmps T Env)
   802     note G = \<open>prg Env = G\<close>
   803     from Ass.prems
   804     obtain vT eT where
   805       wt_va: "Env\<turnstile>va\<Colon>=vT" and
   806        wt_e: "Env\<turnstile>e\<Colon>-eT"
   807       by (elim wt_elim_cases)
   808     note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close>
   809     note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close>
   810     {
   811       fix j
   812       assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
   813       have "j\<in>jmps"
   814       proof -
   815         have "abrupt s2 = Some (Jump j)"
   816         proof (cases "normal s2")
   817           case True
   818           from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> and True have nrm_s1: "normal s1" 
   819             by (rule eval_no_abrupt_lemma [rule_format]) 
   820           with nrm_s1 wt_va G True
   821           have "abrupt (f v s2) \<noteq> Some (Jump j)"
   822             using hyp_v [THEN conjunct2,rule_format (no_asm)]
   823             by simp
   824           from this jmp
   825           show ?thesis
   826             by (rule assign_abrupt_propagation)
   827         next
   828           case False with jmp 
   829           show ?thesis by (cases s2) (simp add: assign_def Let_def)
   830         qed
   831         moreover from wt_va G
   832         have "?Jmp jmps s1"
   833           by - (rule hyp_v [THEN conjunct1],simp_all)
   834         ultimately show ?thesis using G 
   835           by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
   836       qed
   837     }
   838     thus ?case by simp
   839   next
   840     case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
   841     note G = \<open>prg Env = G\<close>
   842     note hyp_e0 = \<open>PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)\<close>
   843     note hyp_e1_e2 = \<open>PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)\<close>
   844     from Cond.prems
   845     obtain e1T e2T
   846       where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
   847        and  wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
   848        and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
   849       by (elim wt_elim_cases)
   850     {
   851       fix j
   852       assume jmp: "abrupt s2 = Some (Jump j)"
   853       have "j\<in>jmps" 
   854       proof -
   855         from wt_e0 G 
   856         have jmp_s1: "?Jmp jmps s1"
   857           by - (rule hyp_e0 [THEN conjunct1],simp_all)
   858         show ?thesis
   859         proof (cases "the_Bool b")
   860           case True
   861           with jmp_s1 wt_e1 G jmp
   862           show ?thesis
   863             by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
   864         next
   865           case False
   866           with jmp_s1 wt_e2 G jmp
   867           show ?thesis
   868             by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
   869         qed
   870       qed
   871     }
   872     thus ?case by simp
   873   next
   874     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
   875                jmps T Env)
   876     note G = \<open>prg Env = G\<close>
   877     from Call.prems
   878     obtain eT argsT 
   879       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
   880       by (elim wt_elim_cases)
   881     {
   882       fix j
   883       assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) 
   884                      = Some (Jump j)"
   885       have "j\<in>jmps"
   886       proof -
   887         note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
   888         from wt_e G 
   889         have jmp_s1: "?Jmp jmps s1"
   890           by - (rule hyp_e [THEN conjunct1],simp_all)
   891         note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>
   892         have "abrupt s2 = Some (Jump j)"
   893         proof -
   894           note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>
   895           moreover
   896           from jmp have "abrupt s4 = Some (Jump j)"
   897             by (cases s4) simp
   898           ultimately have "abrupt s3' = Some (Jump j)"
   899             by - (rule ccontr,drule (1) Methd_no_jump,simp)
   900           moreover note \<open>s3' = check_method_access G accC statT mode 
   901                               \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close>
   902           ultimately have "abrupt s3 = Some (Jump j)"
   903             by (cases s3) 
   904                (simp add: check_method_access_def abrupt_if_def Let_def)
   905           moreover 
   906           note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>
   907           ultimately show ?thesis
   908             by (cases s2) (auto simp add: init_lvars_def2)
   909         qed
   910         with jmp_s1 wt_args G
   911         show ?thesis
   912           by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)
   913       qed
   914     }
   915     thus ?case by simp
   916   next
   917     case (Methd s0 D sig v s1 jmps T Env)
   918     from \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close>
   919     have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   920       by (rule eval.Methd)
   921     hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
   922       by (rule Methd_no_jump) simp
   923     thus ?case by simp
   924   next
   925     case (Body s0 D s1 c s2 s3 jmps T Env)
   926     have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
   927            \<rightarrow> abupd (absorb Ret) s3"
   928       by (rule eval.Body) (rule Body)+
   929     hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
   930       by (rule Body_no_jump) simp
   931     thus ?case by simp
   932   next
   933     case LVar
   934     thus ?case by (simp add: lvar_def Let_def)
   935   next
   936     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
   937     note G = \<open>prg Env = G\<close>
   938     from wf FVar.prems 
   939     obtain  statC f where
   940       wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
   941       accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)"
   942       by  (elim wt_elim_cases) simp
   943     have wt_init: "Env\<turnstile>Init statDeclC\<Colon>\<surd>"
   944     proof -
   945       from wf wt_e G 
   946       have "is_class (prg Env) statC"
   947         by (auto dest: ty_expr_is_type type_is_class)
   948       with wf accfield G
   949       have "is_class (prg Env) statDeclC"
   950         by (auto dest!: accfield_fields dest: fields_declC)
   951       thus ?thesis
   952         by simp
   953     qed
   954     note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
   955     {
   956       fix j
   957       assume jmp: "abrupt s3 = Some (Jump j)"
   958       have "j\<in>jmps"
   959       proof -
   960         note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>
   961         from G wt_init 
   962         have "?Jmp jmps s1"
   963           by - (rule hyp_init [THEN conjunct1],auto)
   964         moreover
   965         note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>
   966         have "abrupt s2 = Some (Jump j)"
   967         proof -
   968           note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
   969           with jmp have "abrupt s2' = Some (Jump j)"
   970             by (cases s2') 
   971                (simp add: check_field_access_def abrupt_if_def Let_def)
   972          with fvar show "abrupt s2 =  Some (Jump j)"
   973             by (cases s2) (simp add: fvar_def2 abrupt_if_def)
   974         qed
   975         ultimately show ?thesis
   976           using G wt_e
   977           by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)
   978       qed
   979     }
   980     moreover
   981     from fvar obtain upd w
   982       where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
   983               v: "v=(w,upd)"
   984       by (cases "fvar statDeclC stat fn a s2") simp
   985     {
   986       fix j val fix s::state
   987       assume "normal s3"
   988       assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
   989       with upd
   990       have "abrupt (upd val s) \<noteq> Some (Jump j)"
   991         by (rule fvar_upd_no_jump)
   992     }
   993     ultimately show ?case using v by simp
   994   next
   995     case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
   996     note G = \<open>prg Env = G\<close>
   997     from AVar.prems 
   998     obtain  e1T e2T where
   999       wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
  1000       by  (elim wt_elim_cases) simp
  1001     note avar = \<open>(v, s2') = avar G i a s2\<close>
  1002     {
  1003       fix j
  1004       assume jmp: "abrupt s2' = Some (Jump j)"
  1005       have "j\<in>jmps"
  1006       proof -
  1007         note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>
  1008         from G wt_e1
  1009         have "?Jmp jmps s1"
  1010           by - (rule hyp_e1 [THEN conjunct1], auto)
  1011         moreover
  1012         note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>
  1013         have "abrupt s2 = Some (Jump j)"
  1014         proof -
  1015           from avar have "s2' = snd (avar G i a s2)"
  1016             by (cases "avar G i a s2") simp
  1017           with jmp show ?thesis by - (rule avar_state_no_jump,simp) 
  1018         qed  
  1019         ultimately show ?thesis
  1020           using wt_e2 G
  1021           by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)
  1022       qed
  1023     }
  1024     moreover
  1025     from avar obtain upd w
  1026       where upd: "upd = snd (fst (avar G i a s2))" and
  1027               v: "v=(w,upd)"
  1028       by (cases "avar G i a s2") simp
  1029     {
  1030       fix j val fix s::state
  1031       assume "normal s2'"
  1032       assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
  1033       with upd
  1034       have "abrupt (upd val s) \<noteq> Some (Jump j)"
  1035         by (rule avar_upd_no_jump)
  1036     }
  1037     ultimately show ?case using v by simp
  1038   next
  1039     case Nil thus ?case by simp
  1040   next
  1041     case (Cons s0 e v s1 es vs s2 jmps T Env)
  1042     note G = \<open>prg Env = G\<close>
  1043     from Cons.prems obtain eT esT
  1044       where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_e2: "Env\<turnstile>es\<Colon>\<doteq>esT"
  1045       by  (elim wt_elim_cases) simp
  1046     {
  1047       fix j
  1048       assume jmp: "abrupt s2 = Some (Jump j)"
  1049       have "j\<in>jmps"
  1050       proof -
  1051         note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
  1052         from G wt_e
  1053         have "?Jmp jmps s1"
  1054           by - (rule hyp_e [THEN conjunct1],simp_all)
  1055         moreover
  1056         note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>
  1057         ultimately show ?thesis
  1058           using wt_e2 G jmp
  1059           by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
  1060                 (assumption|simp (no_asm_simp))+)
  1061       qed
  1062     }
  1063     thus ?case by simp
  1064   qed
  1065   note generalized = this
  1066   from no_jmp jmpOk wt G
  1067   show ?thesis
  1068     by (rule generalized)
  1069 qed
  1070 
  1071 lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]
  1072 
  1073 
  1074 lemma jumpNestingOk_eval_no_jump:
  1075  assumes    eval: "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1076            jmpOk: "jumpNestingOk {} t" and
  1077           no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
  1078               wt: "Env\<turnstile>t\<Colon>T" and 
  1079               wf: "wf_prog (prg Env)" 
  1080  shows "abrupt s1 \<noteq> Some (Jump j) \<and>
  1081         (normal s1 \<longrightarrow> v=In2 (w,upd)  
  1082          \<longrightarrow> abrupt s \<noteq> Some (Jump j')
  1083          \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))"
  1084 proof (cases "\<exists> j'. abrupt s0 = Some (Jump j')") 
  1085   case True
  1086   then obtain j' where jmp: "abrupt s0 = Some (Jump j')" ..
  1087   with no_jmp have "j'\<noteq>j" by simp
  1088   with eval jmp have "s1=s0" by auto
  1089   with no_jmp jmp show ?thesis by simp
  1090 next
  1091   case False
  1092   obtain G where G: "prg Env = G"
  1093     by (cases Env) simp
  1094   from G eval have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp
  1095   moreover note jmpOk wt
  1096   moreover from G wf have "wf_prog G" by simp
  1097   moreover note G 
  1098   moreover from False have "\<And> j. abrupt s0 = Some (Jump j) \<Longrightarrow> j \<in> {}"
  1099     by simp
  1100   ultimately show ?thesis
  1101     apply (rule jumpNestingOk_evalE)
  1102     apply assumption
  1103     apply simp
  1104     apply fastforce
  1105     done
  1106 qed
  1107 
  1108 lemmas jumpNestingOk_eval_no_jumpE 
  1109        = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]
  1110 
  1111 corollary eval_expression_no_jump:
  1112   assumes eval: "prg Env\<turnstile>s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and
  1113         no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
  1114         wt: "Env\<turnstile>e\<Colon>-T" and 
  1115         wf: "wf_prog (prg Env)" 
  1116   shows "abrupt s1 \<noteq> Some (Jump j)"
  1117 using eval _ no_jmp wt wf
  1118 by (rule jumpNestingOk_eval_no_jumpE, simp_all)
  1119 
  1120 corollary eval_var_no_jump:
  1121   assumes eval: "prg Env\<turnstile>s0 \<midarrow>var=\<succ>(w,upd)\<rightarrow> s1" and
  1122         no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
  1123         wt: "Env\<turnstile>var\<Colon>=T" and 
  1124         wf: "wf_prog (prg Env)" 
  1125   shows "abrupt s1 \<noteq> Some (Jump j) \<and> 
  1126          (normal s1 \<longrightarrow> 
  1127           (abrupt s \<noteq> Some (Jump j') 
  1128            \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j')))"
  1129 apply (rule_tac upd="upd" and val="val" and s="s" and w="w" and j'=j' 
  1130          in jumpNestingOk_eval_no_jumpE [OF eval _ no_jmp wt wf])
  1131 by simp_all
  1132 
  1133 lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]
  1134 
  1135 corollary eval_statement_no_jump:
  1136   assumes eval: "prg Env\<turnstile>s0 \<midarrow>c\<rightarrow> s1" and
  1137          jmpOk: "jumpNestingOkS {} c" and
  1138         no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
  1139         wt: "Env\<turnstile>c\<Colon>\<surd>" and 
  1140         wf: "wf_prog (prg Env)" 
  1141   shows "abrupt s1 \<noteq> Some (Jump j)"
  1142 using eval _ no_jmp wt wf
  1143 by (rule jumpNestingOk_eval_no_jumpE) (simp_all add: jmpOk)
  1144 
  1145 corollary eval_expression_list_no_jump:
  1146   assumes eval: "prg Env\<turnstile>s0 \<midarrow>es\<doteq>\<succ>v\<rightarrow> s1" and
  1147         no_jmp: "abrupt s0 \<noteq> Some (Jump j)" and
  1148         wt: "Env\<turnstile>es\<Colon>\<doteq>T" and 
  1149         wf: "wf_prog (prg Env)" 
  1150   shows "abrupt s1 \<noteq> Some (Jump j)"
  1151 using eval _ no_jmp wt wf
  1152 by (rule jumpNestingOk_eval_no_jumpE, simp_all)
  1153 
  1154 (* ### FIXME: Do i need this *)
  1155 lemma union_subseteq_elim [elim]: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
  1156   by blast
  1157 
  1158 lemma dom_locals_halloc_mono:
  1159   assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1"
  1160   shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1161 proof -
  1162   from halloc show ?thesis
  1163     by cases simp_all
  1164 qed
  1165  
  1166 lemma dom_locals_sxalloc_mono:
  1167   assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1"
  1168   shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1169 proof -
  1170   from sxalloc show ?thesis
  1171   proof (cases)
  1172     case Norm thus ?thesis by simp
  1173   next
  1174     case Jmp thus ?thesis by simp
  1175   next
  1176     case Error thus ?thesis by simp
  1177   next
  1178     case XcptL thus ?thesis by simp
  1179   next
  1180     case SXcpt thus ?thesis 
  1181       by - (drule dom_locals_halloc_mono,simp)
  1182   qed
  1183 qed
  1184     
  1185 
  1186 lemma dom_locals_assign_mono: 
  1187  assumes f_ok: "dom (locals (store s)) \<subseteq> dom (locals (store (f n s)))"
  1188    shows  "dom (locals (store s)) \<subseteq> dom (locals (store (assign f n s)))"
  1189 proof (cases "normal s")
  1190   case False thus ?thesis
  1191     by (cases s) (auto simp add: assign_def Let_def)
  1192 next
  1193   case True
  1194   then obtain s' where s': "s = (None,s')"
  1195     by auto
  1196   moreover
  1197   obtain x1 s1 where "f n s = (x1,s1)"
  1198     by (cases "f n s")
  1199   ultimately
  1200   show ?thesis
  1201     using f_ok
  1202     by (simp add: assign_def Let_def)
  1203 qed
  1204 
  1205 (*
  1206 lemma dom_locals_init_lvars_mono: 
  1207  "dom (locals (store s)) 
  1208    \<subseteq> dom (locals (store (init_lvars G D sig mode a vs s)))"
  1209 proof (cases "mode = Static")
  1210   case True
  1211   thus ?thesis
  1212     apply (cases s)
  1213     apply (simp add: init_lvars_def Let_def)
  1214 *)
  1215 
  1216 lemma dom_locals_lvar_mono:
  1217  "dom (locals (store s)) \<subseteq> dom (locals (store (snd (lvar vn s') val s)))"
  1218 by (simp add: lvar_def) blast
  1219 
  1220 
  1221 lemma dom_locals_fvar_vvar_mono:
  1222 "dom (locals (store s)) 
  1223   \<subseteq> dom (locals (store (snd (fst (fvar statDeclC stat fn a s')) val s)))"
  1224 proof (cases stat) 
  1225   case True
  1226   thus ?thesis
  1227     by (cases s) (simp add: fvar_def2)
  1228 next
  1229   case False
  1230   thus ?thesis
  1231     by (cases s) (simp add: fvar_def2)
  1232 qed
  1233 
  1234 lemma dom_locals_fvar_mono:
  1235 "dom (locals (store s)) 
  1236   \<subseteq> dom (locals (store (snd (fvar statDeclC stat fn a s))))"
  1237 proof (cases stat) 
  1238   case True
  1239   thus ?thesis
  1240     by (cases s) (simp add: fvar_def2)
  1241 next
  1242   case False
  1243   thus ?thesis
  1244     by (cases s) (simp add: fvar_def2)
  1245 qed
  1246 
  1247 
  1248 lemma dom_locals_avar_vvar_mono:
  1249 "dom (locals (store s)) 
  1250   \<subseteq> dom (locals (store (snd (fst (avar G i a s')) val s)))"
  1251 by (cases s, simp add: avar_def2)
  1252 
  1253 lemma dom_locals_avar_mono:
  1254 "dom (locals (store s)) 
  1255   \<subseteq> dom (locals (store (snd (avar G i a s))))"
  1256 by (cases s, simp add: avar_def2)
  1257 
  1258   text \<open>
  1259 Since assignments are modelled as functions from states to states, we
  1260   must take into account these functions. They  appear only in the assignment 
  1261   rule and as result from evaluating a variable. Thats why we need the 
  1262   complicated second part of the conjunction in the goal.
  1263  The reason for the very generic way to treat assignments was the aim
  1264 to omit redundancy. There is only one evaluation rule for each kind of
  1265 variable (locals, fields, arrays). These rules are used for both accessing 
  1266 variables and updating variables. Thats why the evaluation rules for variables
  1267 result in a pair consisting of a value and an update function. Of course we
  1268 could also think of a pair of a value and a reference in the store, instead of
  1269 the generic update function. But as only array updates can cause a special
  1270 exception (if the types mismatch) and not array reads we then have to introduce
  1271 two different rules to handle array reads and updates\<close> 
  1272 lemma dom_locals_eval_mono: 
  1273   assumes   eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1274   shows "dom (locals (store s0)) \<subseteq> dom (locals (store s1)) \<and>
  1275          (\<forall> vv. v=In2 vv \<and> normal s1 
  1276             \<longrightarrow> (\<forall> s val. dom (locals (store s)) 
  1277                            \<subseteq> dom (locals (store ((snd vv) val s)))))"
  1278 proof -
  1279   from eval show ?thesis
  1280   proof (induct)
  1281     case Abrupt thus ?case by simp 
  1282   next
  1283     case Skip thus ?case by simp
  1284   next
  1285     case Expr thus ?case by simp
  1286   next
  1287     case Lab thus ?case by simp
  1288   next
  1289     case (Comp s0 c1 s1 c2 s2) 
  1290     from Comp.hyps 
  1291     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1292       by simp
  1293     also
  1294     from Comp.hyps
  1295     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1296       by simp
  1297     finally show ?case by simp
  1298   next
  1299     case (If s0 e b s1 c1 c2 s2)
  1300     from If.hyps 
  1301     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1302       by simp
  1303     also
  1304     from If.hyps
  1305     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1306       by simp
  1307     finally show ?case by simp
  1308   next
  1309     case (Loop s0 e b s1 c s2 l s3) 
  1310     show ?case
  1311     proof (cases "the_Bool b")
  1312       case True
  1313       with Loop.hyps
  1314       obtain
  1315         s0_s1: 
  1316         "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" and
  1317         s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" and
  1318         s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  1319         by simp
  1320       note s0_s1 also note s1_s2 also note s2_s3
  1321       finally show ?thesis
  1322         by simp
  1323     next
  1324       case False
  1325       with Loop.hyps show ?thesis
  1326         by simp
  1327     qed
  1328   next
  1329     case Jmp thus ?case by simp
  1330   next
  1331     case Throw thus ?case by simp
  1332   next
  1333     case (Try s0 c1 s1 s2 C vn c2 s3)
  1334     then
  1335     have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  1336                   \<subseteq> dom (locals (store s1))" by simp
  1337     from \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
  1338     have s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
  1339       by (rule dom_locals_sxalloc_mono)
  1340     thus ?case 
  1341     proof (cases "G,s2\<turnstile>catch C")
  1342       case True
  1343       note s0_s1 also note s1_s2
  1344       also
  1345       from True Try.hyps 
  1346       have "dom (locals (store (new_xcpt_var vn s2))) 
  1347               \<subseteq> dom (locals (store s3))"
  1348         by simp
  1349       hence "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  1350         by (cases s2, simp )
  1351       finally show ?thesis by simp
  1352     next
  1353       case False
  1354       note s0_s1 also note s1_s2
  1355       finally 
  1356       show ?thesis 
  1357         using False Try.hyps by simp
  1358     qed
  1359   next
  1360     case (Fin s0 c1 x1 s1 c2 s2 s3) 
  1361     show ?case
  1362     proof (cases "\<exists>err. x1 = Some (Error err)")
  1363       case True
  1364       with Fin.hyps show ?thesis
  1365         by simp
  1366     next
  1367       case False
  1368       from Fin.hyps
  1369       have "dom (locals (store ((Norm s0)::state))) 
  1370              \<subseteq> dom (locals (store (x1, s1)))" 
  1371         by simp
  1372       hence "dom (locals (store ((Norm s0)::state))) 
  1373               \<subseteq> dom (locals (store ((Norm s1)::state)))"
  1374         by simp
  1375       also
  1376       from Fin.hyps
  1377       have "\<dots> \<subseteq> dom (locals (store s2))"
  1378         by simp
  1379       finally show ?thesis 
  1380         using Fin.hyps by simp
  1381     qed
  1382   next
  1383     case (Init C c s0 s3 s1 s2)
  1384     show ?case
  1385     proof (cases "inited C (globs s0)")
  1386       case True
  1387       with Init.hyps show ?thesis by simp 
  1388     next
  1389       case False
  1390       with Init.hyps 
  1391       obtain s0_s1: "dom (locals (store (Norm ((init_class_obj G C) s0))))
  1392                      \<subseteq> dom (locals (store s1))" and
  1393              s3: "s3 = (set_lvars (locals (snd s1))) s2"
  1394         by simp
  1395       from s0_s1
  1396       have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s1))"
  1397         by (cases s0) simp
  1398       with s3
  1399       have "dom (locals (store (Norm s0))) \<subseteq> dom (locals (store s3))"
  1400         by (cases s2) simp
  1401       thus ?thesis by simp
  1402     qed
  1403   next
  1404     case (NewC s0 C s1 a s2)
  1405     note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close>
  1406     from NewC.hyps
  1407     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
  1408       by simp
  1409     also
  1410     from halloc
  1411     have "\<dots>  \<subseteq> dom (locals (store s2))" by (rule dom_locals_halloc_mono)
  1412     finally show ?case by simp
  1413   next
  1414     case (NewA s0 T s1 e i s2 a s3)
  1415     note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
  1416     from NewA.hyps
  1417     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
  1418       by simp
  1419     also
  1420     from NewA.hyps
  1421     have "\<dots> \<subseteq> dom (locals (store s2))" by simp
  1422     also
  1423     from halloc 
  1424     have "\<dots> \<subseteq>  dom (locals (store s3))"
  1425       by (rule dom_locals_halloc_mono [elim_format]) simp
  1426     finally show ?case by simp
  1427   next
  1428     case Cast thus ?case by simp
  1429   next
  1430     case Inst thus ?case by simp
  1431   next
  1432     case Lit thus ?case by simp
  1433   next
  1434     case UnOp thus ?case by simp
  1435   next
  1436     case (BinOp s0 e1 v1 s1 binop e2 v2 s2) 
  1437     from BinOp.hyps
  1438     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
  1439       by simp
  1440     also
  1441     from BinOp.hyps
  1442     have "\<dots> \<subseteq> dom (locals (store s2))" by simp
  1443     finally show ?case by simp
  1444   next
  1445     case Super thus ?case by simp
  1446   next
  1447     case Acc thus ?case by simp
  1448   next
  1449     case (Ass s0 va w f s1 e v s2)
  1450     from Ass.hyps
  1451     have s0_s1: 
  1452       "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))" 
  1453       by simp
  1454     show ?case
  1455     proof (cases "normal s1")
  1456       case True
  1457       with Ass.hyps 
  1458       have ass_ok:
  1459         "\<And> s val. dom (locals (store s)) \<subseteq> dom (locals (store (f val s)))"
  1460         by simp
  1461       note s0_s1
  1462       also
  1463       from Ass.hyps
  1464       have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))" 
  1465         by simp
  1466       also
  1467       from ass_ok
  1468       have "\<dots> \<subseteq> dom (locals (store (assign f v s2)))"
  1469         by (rule dom_locals_assign_mono [where f = f])
  1470       finally show ?thesis by simp
  1471     next
  1472       case False
  1473       with \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close>
  1474       have "s2=s1"
  1475         by auto
  1476       with s0_s1 False
  1477       have "dom (locals (store ((Norm s0)::state))) 
  1478             \<subseteq> dom (locals (store (assign f v s2)))"
  1479         by simp
  1480       thus ?thesis
  1481         by simp
  1482     qed
  1483   next
  1484     case (Cond s0 e0 b s1 e1 e2 v s2)
  1485     from Cond.hyps 
  1486     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1487       by simp
  1488     also
  1489     from Cond.hyps
  1490     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1491       by simp
  1492     finally show ?case by simp
  1493   next
  1494     case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
  1495     note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
  1496     from Call.hyps 
  1497     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1498       by simp
  1499     also
  1500     from Call.hyps
  1501     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1502       by simp
  1503     also
  1504     have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
  1505       by (cases s4) simp
  1506     finally show ?case by simp
  1507   next
  1508     case Methd thus ?case by simp
  1509   next
  1510     case (Body s0 D s1 c s2 s3)
  1511     from Body.hyps 
  1512     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1513       by simp
  1514     also
  1515     from Body.hyps
  1516     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1517       by simp
  1518     also
  1519     have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s2)))"
  1520       by simp
  1521     also
  1522     have "\<dots> \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
  1523     proof -
  1524       from \<open>s3 =
  1525          (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  1526                  abrupt s2 = Some (Jump (Cont l))
  1527              then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)\<close>
  1528       show ?thesis
  1529         by simp
  1530     qed
  1531     finally show ?case by simp
  1532   next
  1533     case LVar
  1534     thus ?case
  1535       using dom_locals_lvar_mono
  1536       by simp
  1537   next
  1538     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
  1539     from FVar.hyps
  1540     obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and
  1541              v: "v = fst (fvar statDeclC stat fn a s2)"
  1542       by (cases "fvar statDeclC stat fn a s2" ) simp
  1543     from v 
  1544     have "\<forall>s val. dom (locals (store s)) 
  1545                           \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")
  1546       by (simp add: dom_locals_fvar_vvar_mono) 
  1547     hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s3 \<longrightarrow> ?V_ok)"
  1548       by - (intro strip, simp)
  1549     note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
  1550     from FVar.hyps 
  1551     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1552       by simp
  1553     also
  1554     from FVar.hyps
  1555     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1556       by simp
  1557     also
  1558     from s2'
  1559     have "\<dots> \<subseteq> dom (locals (store s2'))"
  1560       by (simp add: dom_locals_fvar_mono)
  1561     also
  1562     from s3
  1563     have "\<dots> \<subseteq> dom (locals (store s3))"
  1564       by (simp add: check_field_access_def Let_def)
  1565     finally
  1566     show ?case
  1567       using v_ok
  1568       by simp
  1569   next
  1570     case (AVar s0 e1 a s1 e2 i s2 v s2')
  1571     from AVar.hyps
  1572     obtain s2': "s2' = snd (avar G i a s2)" and
  1573              v: "v   = fst (avar G i a s2)"
  1574       by (cases "avar G i a s2") simp
  1575     from v
  1576     have "\<forall>s val. dom (locals (store s)) 
  1577                           \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")
  1578       by (simp add: dom_locals_avar_vvar_mono)
  1579     hence v_ok: "(\<forall>vv. In2 v = In2 vv \<and> normal s2' \<longrightarrow> ?V_ok)"
  1580       by - (intro strip, simp)
  1581     from AVar.hyps 
  1582     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1583       by simp
  1584     also
  1585     from AVar.hyps
  1586     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1587       by simp
  1588     also
  1589     from s2'
  1590     have "\<dots> \<subseteq> dom (locals (store s2'))"
  1591       by (simp add: dom_locals_avar_mono)
  1592     finally
  1593     show ?case using v_ok by simp
  1594   next
  1595     case Nil thus ?case by simp
  1596   next
  1597     case (Cons s0 e v s1 es vs s2)
  1598     from Cons.hyps
  1599     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1600       by simp
  1601     also
  1602     from Cons.hyps
  1603     have "\<dots> \<subseteq> dom (locals (store s2))" 
  1604       by simp
  1605     finally show ?case by simp
  1606   qed
  1607 qed
  1608      
  1609 lemma dom_locals_eval_mono_elim:
  1610   assumes   eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
  1611   obtains "dom (locals (store s0)) \<subseteq> dom (locals (store s1))" and
  1612     "\<And> vv s val. \<lbrakk>v=In2 vv; normal s1\<rbrakk> 
  1613                         \<Longrightarrow> dom (locals (store s))
  1614                              \<subseteq> dom (locals (store ((snd vv) val s)))"
  1615   using eval by (rule dom_locals_eval_mono [THEN conjE]) (rule that, auto)
  1616 
  1617 lemma halloc_no_abrupt:
  1618   assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1" and
  1619           normal: "normal s1"
  1620   shows "normal s0"
  1621 proof -
  1622   from halloc normal show ?thesis
  1623     by cases simp_all
  1624 qed
  1625  
  1626 lemma sxalloc_mono_no_abrupt:
  1627   assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1" and
  1628            normal: "normal s1"
  1629   shows "normal s0"
  1630 proof -
  1631   from sxalloc normal show ?thesis
  1632     by cases simp_all
  1633 qed
  1634    
  1635 lemma union_subseteqI: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A; B' \<subseteq> B\<rbrakk>  \<Longrightarrow>   A' \<union> B' \<subseteq> C"
  1636   by blast
  1637 
  1638 lemma union_subseteqIl: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A\<rbrakk>  \<Longrightarrow>   A' \<union> B \<subseteq> C"
  1639   by blast
  1640 
  1641 lemma union_subseteqIr: "\<lbrakk>A \<union> B \<subseteq> C; B' \<subseteq> B\<rbrakk>  \<Longrightarrow>   A \<union> B' \<subseteq> C"
  1642   by blast
  1643 
  1644 lemma subseteq_union_transl [trans]: "\<lbrakk>A \<subseteq> B; B \<union> C \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"
  1645   by blast
  1646 
  1647 lemma subseteq_union_transr [trans]: "\<lbrakk>A \<subseteq> B; C \<union> B \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"
  1648   by blast
  1649 
  1650 lemma union_subseteq_weaken: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"  
  1651   by blast
  1652 
  1653 lemma assigns_good_approx: 
  1654   assumes
  1655       eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1656     normal: "normal s1" 
  1657   shows "assigns t \<subseteq> dom (locals (store s1))"
  1658 proof -
  1659   from eval normal show ?thesis
  1660   proof (induct)
  1661     case Abrupt thus ?case by simp 
  1662   next \<comment> \<open>For statements its trivial, since then @{term "assigns t = {}"}\<close>
  1663     case Skip show ?case by simp
  1664   next
  1665     case Expr show ?case by simp 
  1666   next
  1667     case Lab show ?case by simp
  1668   next
  1669     case Comp show ?case by simp
  1670   next
  1671     case If show ?case by simp
  1672   next
  1673     case Loop show ?case by simp
  1674   next
  1675     case Jmp show ?case by simp
  1676   next
  1677     case Throw show ?case by simp
  1678   next
  1679     case Try show ?case by simp 
  1680   next
  1681     case Fin show ?case by simp
  1682   next
  1683     case Init show ?case by simp 
  1684   next
  1685     case NewC show ?case by simp
  1686   next
  1687     case (NewA s0 T s1 e i s2 a s3)
  1688     note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
  1689     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1690     proof -
  1691       from NewA
  1692       have "normal (abupd (check_neg i) s2)"
  1693         by - (erule halloc_no_abrupt [rule_format])
  1694       hence "normal s2" by (cases s2) simp
  1695       with NewA.hyps
  1696       show ?thesis by iprover
  1697     qed
  1698     also
  1699     from halloc 
  1700     have "\<dots> \<subseteq>  dom (locals (store s3))"
  1701       by (rule dom_locals_halloc_mono [elim_format]) simp
  1702     finally show ?case by simp 
  1703   next
  1704     case (Cast s0 e v s1 s2 T)
  1705     hence "normal s1" by (cases s1,simp)
  1706     with Cast.hyps
  1707     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1708       by simp
  1709     also
  1710     from Cast.hyps
  1711     have "\<dots> \<subseteq> dom (locals (store s2))"
  1712       by simp
  1713     finally 
  1714     show ?case
  1715       by simp
  1716   next
  1717     case Inst thus ?case by simp
  1718   next
  1719     case Lit thus ?case by simp
  1720   next
  1721     case UnOp thus ?case by simp
  1722   next
  1723     case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
  1724     hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) 
  1725     with BinOp.hyps
  1726     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
  1727       by iprover
  1728     also
  1729     have "\<dots>  \<subseteq> dom (locals (store s2))"
  1730     proof -
  1731       note \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  1732                       else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close>
  1733       thus ?thesis
  1734         by (rule dom_locals_eval_mono_elim)
  1735     qed
  1736     finally have s2: "assigns (In1l e1) \<subseteq> dom (locals (store s2))" .
  1737     show ?case
  1738     proof (cases "binop=CondAnd \<or> binop=CondOr")
  1739       case True
  1740       with s2 show ?thesis by simp 
  1741     next
  1742       case False
  1743       with BinOp 
  1744       have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1745         by (simp add: need_second_arg_def)
  1746       with s2
  1747       show ?thesis using False by simp
  1748     qed
  1749   next
  1750     case Super thus ?case by simp
  1751   next
  1752     case Acc thus ?case by simp
  1753   next 
  1754     case (Ass s0 va w f s1 e v s2)
  1755     note nrm_ass_s2 = \<open>normal (assign f v s2)\<close>
  1756     hence nrm_s2: "normal s2"
  1757       by (cases s2, simp add: assign_def Let_def)
  1758     with Ass.hyps 
  1759     have nrm_s1: "normal s1"
  1760       by - (erule eval_no_abrupt_lemma [rule_format]) 
  1761     with Ass.hyps
  1762     have "assigns (In2 va) \<subseteq> dom (locals (store s1))" 
  1763       by iprover
  1764     also
  1765     from Ass.hyps
  1766     have "\<dots> \<subseteq> dom (locals (store s2))"
  1767       by - (erule dom_locals_eval_mono_elim)
  1768     also
  1769     from nrm_s2 Ass.hyps
  1770     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1771       by iprover
  1772     ultimately
  1773     have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq>  dom (locals (store s2))"
  1774       by (rule Un_least)
  1775     also
  1776     from Ass.hyps nrm_s1
  1777     have "\<dots>  \<subseteq> dom (locals (store (f v s2)))"
  1778       by - (erule dom_locals_eval_mono_elim, cases s2,simp)
  1779     then
  1780     have "dom (locals (store s2))  \<subseteq> dom (locals (store (assign f v s2)))"
  1781       by (rule dom_locals_assign_mono)
  1782     finally
  1783     have va_e: " assigns (In2 va) \<union> assigns (In1l e)
  1784                   \<subseteq> dom (locals (snd (assign f v s2)))" .
  1785     show ?case
  1786     proof (cases "\<exists> n. va = LVar n")
  1787       case False
  1788       with va_e show ?thesis 
  1789         by (simp add: Un_assoc)
  1790     next
  1791       case True
  1792       then obtain n where va: "va = LVar n"
  1793         by blast
  1794       with Ass.hyps 
  1795       have "G\<turnstile>Norm s0 \<midarrow>LVar n=\<succ>(w,f)\<rightarrow> s1" 
  1796         by simp
  1797       hence "(w,f) = lvar n s0"
  1798         by (rule eval_elim_cases) simp
  1799       with nrm_ass_s2
  1800       have "n \<in> dom (locals (store (assign f v s2)))"
  1801         by (cases s2) (simp add: assign_def Let_def lvar_def)
  1802       with va_e True va 
  1803       show ?thesis by (simp add: Un_assoc)
  1804     qed
  1805   next
  1806     case (Cond s0 e0 b s1 e1 e2 v s2) 
  1807     hence "normal s1"
  1808       by - (erule eval_no_abrupt_lemma [rule_format])
  1809     with Cond.hyps
  1810     have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"
  1811       by iprover
  1812     also from Cond.hyps
  1813     have "\<dots> \<subseteq> dom (locals (store s2))"
  1814       by - (erule dom_locals_eval_mono_elim)
  1815     finally have e0: "assigns (In1l e0) \<subseteq> dom (locals (store s2))" .
  1816     show ?case
  1817     proof (cases "the_Bool b")
  1818       case True
  1819       with Cond 
  1820       have "assigns (In1l e1) \<subseteq> dom (locals (store s2))"
  1821         by simp
  1822       hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>" 
  1823         by blast
  1824       with e0
  1825       have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2) 
  1826              \<subseteq> dom (locals (store s2))"
  1827         by (rule Un_least)
  1828       thus ?thesis using True by simp 
  1829     next
  1830       case False
  1831       with Cond 
  1832       have " assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1833         by simp
  1834       hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>"
  1835         by blast
  1836       with e0
  1837       have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2) 
  1838              \<subseteq> dom (locals (store s2))"
  1839         by (rule Un_least)
  1840       thus ?thesis using False by simp 
  1841     qed
  1842   next
  1843     case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
  1844     have nrm_s2: "normal s2"
  1845     proof -
  1846       from \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
  1847       have normal_s4: "normal s4" by simp
  1848       hence "normal s3'" using Call.hyps
  1849         by - (erule eval_no_abrupt_lemma [rule_format]) 
  1850       moreover note
  1851        \<open>s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3\<close>
  1852       ultimately have "normal s3"
  1853         by (cases s3) (simp add: check_method_access_def Let_def) 
  1854       moreover
  1855       note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
  1856       ultimately show "normal s2"
  1857         by (cases s2) (simp add: init_lvars_def2)
  1858     qed
  1859     hence "normal s1" using Call.hyps
  1860       by - (erule eval_no_abrupt_lemma [rule_format])
  1861     with Call.hyps
  1862     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1863       by iprover
  1864     also from Call.hyps
  1865     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1866       by - (erule dom_locals_eval_mono_elim)
  1867     also
  1868     from nrm_s2 Call.hyps
  1869     have "assigns (In3 args) \<subseteq> dom (locals (store s2))"
  1870       by iprover
  1871     ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"
  1872       by (rule Un_least)
  1873     also 
  1874     have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
  1875       by (cases s4) simp
  1876     finally show ?case
  1877       by simp
  1878   next
  1879     case Methd thus ?case by simp
  1880   next
  1881     case Body thus ?case by simp
  1882   next
  1883     case LVar thus ?case by simp
  1884   next
  1885     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
  1886     note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
  1887     note avar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
  1888     have nrm_s2: "normal s2"
  1889     proof -
  1890       note \<open>normal s3\<close>
  1891       with s3 have "normal s2'"
  1892         by (cases s2') (simp add: check_field_access_def Let_def)
  1893       with avar show "normal s2"
  1894         by (cases s2) (simp add: fvar_def2)
  1895     qed
  1896     with FVar.hyps 
  1897     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1898       by iprover
  1899     also
  1900     have "\<dots> \<subseteq>  dom (locals (store s2'))"
  1901     proof -
  1902       from avar
  1903       have "s2' = snd (fvar statDeclC stat fn a s2)"
  1904         by (cases "fvar statDeclC stat fn a s2") simp
  1905       thus ?thesis
  1906         by simp (rule dom_locals_fvar_mono)
  1907     qed
  1908     also from s3
  1909     have "\<dots> \<subseteq>  dom (locals (store s3))"
  1910       by (cases s2') (simp add: check_field_access_def Let_def)
  1911     finally show ?case
  1912       by simp
  1913   next
  1914     case (AVar s0 e1 a s1 e2 i s2 v s2')
  1915     note avar = \<open>(v, s2') = avar G i a s2\<close>
  1916     have nrm_s2: "normal s2"
  1917     proof -
  1918       from avar and \<open>normal s2'\<close>
  1919       show ?thesis by (cases s2) (simp add: avar_def2)
  1920     qed
  1921     with AVar.hyps 
  1922     have "normal s1"
  1923       by - (erule eval_no_abrupt_lemma [rule_format])
  1924     with AVar.hyps
  1925     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
  1926       by iprover
  1927     also from AVar.hyps
  1928     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1929       by - (erule dom_locals_eval_mono_elim)
  1930     also
  1931     from AVar.hyps nrm_s2
  1932     have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1933       by iprover
  1934     ultimately
  1935     have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"
  1936       by (rule Un_least)
  1937     also
  1938     have "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  1939     proof -
  1940       from avar have "s2' = snd (avar G i a s2)"
  1941         by (cases "avar G i a s2") simp
  1942       thus ?thesis
  1943         by simp (rule dom_locals_avar_mono)
  1944     qed
  1945     finally  
  1946     show ?case
  1947       by simp
  1948   next
  1949     case Nil show ?case by simp
  1950   next
  1951     case (Cons s0 e v s1 es vs s2)
  1952     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1953     proof -
  1954       from Cons
  1955       have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
  1956       with Cons.hyps show ?thesis by iprover
  1957     qed
  1958     also from Cons.hyps
  1959     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1960       by - (erule dom_locals_eval_mono_elim)
  1961     also from Cons
  1962     have "assigns (In3 es) \<subseteq> dom (locals (store s2))"
  1963       by iprover
  1964     ultimately
  1965     have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"
  1966       by (rule Un_least)
  1967     thus ?case
  1968       by simp
  1969   qed
  1970 qed
  1971 
  1972 corollary assignsE_good_approx:
  1973   assumes
  1974       eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and
  1975     normal: "normal s1"
  1976   shows "assignsE e \<subseteq> dom (locals (store s1))"
  1977 proof -
  1978 from eval normal show ?thesis
  1979   by (rule assigns_good_approx [elim_format]) simp
  1980 qed
  1981 
  1982 corollary assignsV_good_approx:
  1983   assumes
  1984      eval: "prg Env\<turnstile> s0 \<midarrow>v=\<succ>vf\<rightarrow> s1" and
  1985    normal: "normal s1"
  1986   shows "assignsV v \<subseteq> dom (locals (store s1))"
  1987 proof -
  1988 from eval normal show ?thesis
  1989   by (rule assigns_good_approx [elim_format]) simp
  1990 qed
  1991    
  1992 corollary assignsEs_good_approx:
  1993   assumes
  1994       eval: "prg Env\<turnstile> s0 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s1" and
  1995     normal: "normal s1" 
  1996   shows "assignsEs es \<subseteq> dom (locals (store s1))"
  1997 proof -
  1998 from eval normal show ?thesis
  1999   by (rule assigns_good_approx [elim_format]) simp
  2000 qed
  2001 
  2002 lemma constVal_eval: 
  2003  assumes const: "constVal e = Some c" and
  2004           eval: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s"
  2005   shows "v = c \<and> normal s"
  2006 proof -
  2007   have  True and 
  2008         "\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk> 
  2009                       \<Longrightarrow> v = c \<and> normal s"
  2010         and True
  2011   proof (induct rule: var.induct expr.induct stmt.induct)
  2012     case NewC hence False by simp thus ?case ..
  2013   next
  2014     case NewA hence False by simp thus ?case ..
  2015   next
  2016     case Cast hence False by simp thus ?case ..
  2017   next
  2018     case Inst hence False by simp thus ?case ..
  2019   next
  2020     case (Lit val c v s0 s)
  2021     note \<open>constVal (Lit val) = Some c\<close>
  2022     moreover
  2023     from \<open>G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s\<close>
  2024     obtain "v=val" and "normal s"
  2025       by cases simp
  2026     ultimately show "v=c \<and> normal s" by simp
  2027   next
  2028     case (UnOp unop e c v s0 s)
  2029     note const = \<open>constVal (UnOp unop e) = Some c\<close>
  2030     then obtain ce where ce: "constVal e = Some ce" by simp
  2031     from \<open>G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s\<close>
  2032     obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
  2033                      v: "v = eval_unop unop ve"
  2034       by cases simp
  2035     from ce ve
  2036     obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
  2037       by (rule UnOp.hyps [elim_format]) iprover
  2038     from eq_ve_ce const ce v 
  2039     have "v=c" 
  2040       by simp
  2041     from this nrm_s
  2042     show ?case ..
  2043   next
  2044     case (BinOp binop e1 e2 c v s0 s)
  2045     note const = \<open>constVal (BinOp binop e1 e2) = Some c\<close>
  2046     then obtain c1 c2 where c1: "constVal e1 = Some c1" and
  2047                             c2: "constVal e2 = Some c2" and
  2048                              c: "c = eval_binop binop c1 c2"
  2049       by simp
  2050     from \<open>G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s\<close>
  2051     obtain v1 s1 v2
  2052       where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
  2053             v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  2054                                else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and
  2055              v: "v = eval_binop binop v1 v2"
  2056       by cases simp
  2057     from c1 v1
  2058     obtain eq_v1_c1: "v1 = c1" and 
  2059              nrm_s1: "normal s1"
  2060       by (rule BinOp.hyps [elim_format]) iprover
  2061     show ?case
  2062     proof (cases "need_second_arg binop v1")
  2063       case True
  2064       with v2 nrm_s1  obtain s1' 
  2065         where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s" 
  2066         by (cases s1) simp
  2067       with c2 obtain "v2 = c2" "normal s"
  2068         by (rule BinOp.hyps [elim_format]) iprover
  2069       with c c1 c2 eq_v1_c1 v 
  2070       show ?thesis by simp
  2071     next
  2072       case False
  2073       with nrm_s1 v2
  2074       have "s=s1"
  2075         by (cases s1) (auto elim!: eval_elim_cases)
  2076       moreover
  2077       from False c v eq_v1_c1  
  2078       have "v = c"
  2079         by (simp add: eval_binop_arg2_indep)
  2080       ultimately 
  2081       show ?thesis
  2082         using nrm_s1 by simp
  2083     qed  (* hallo ehco *)
  2084   next
  2085     case Super hence False by simp thus ?case ..
  2086   next
  2087     case Acc hence False by simp thus ?case ..
  2088   next
  2089     case Ass hence False by simp thus ?case ..
  2090   next
  2091     case (Cond b e1 e2 c v s0 s)
  2092     note c = \<open>constVal (b ? e1 : e2) = Some c\<close>
  2093     then obtain cb c1 c2 where
  2094       cb: "constVal b  = Some cb" and
  2095       c1: "constVal e1 = Some c1" and
  2096       c2: "constVal e2 = Some c2"
  2097       by (auto split: bool.splits)
  2098     from \<open>G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s\<close>
  2099     obtain vb s1
  2100       where     vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
  2101             eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
  2102       by cases simp 
  2103     from cb vb
  2104     obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"
  2105       by (rule Cond.hyps [elim_format]) iprover 
  2106     show ?case
  2107     proof (cases "the_Bool vb")
  2108       case True
  2109       with c cb c1 eq_vb_cb 
  2110       have "c = c1"
  2111         by simp
  2112       moreover
  2113       from True eval_v nrm_s1 obtain s1' 
  2114         where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"
  2115         by (cases s1) simp
  2116       with c1 obtain "c1 = v" "normal s"
  2117         by (rule Cond.hyps [elim_format]) iprover 
  2118       ultimately show ?thesis by simp
  2119     next
  2120       case False
  2121       with c cb c2 eq_vb_cb 
  2122       have "c = c2"
  2123         by simp
  2124       moreover
  2125       from False eval_v nrm_s1 obtain s1' 
  2126         where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"
  2127         by (cases s1) simp
  2128       with c2 obtain "c2 = v" "normal s"
  2129         by (rule Cond.hyps [elim_format]) iprover 
  2130       ultimately show ?thesis by simp
  2131     qed
  2132   next
  2133     case Call hence False by simp thus ?case ..
  2134   qed simp_all
  2135   with const eval
  2136   show ?thesis
  2137     by iprover
  2138 qed
  2139   
  2140 lemmas constVal_eval_elim = constVal_eval [THEN conjE]
  2141 
  2142 lemma eval_unop_type: 
  2143   "typeof dt (eval_unop unop v) = Some (PrimT (unop_type unop))"
  2144   by (cases unop) simp_all
  2145 
  2146 lemma eval_binop_type:
  2147   "typeof dt (eval_binop binop v1 v2) = Some (PrimT (binop_type binop))"
  2148   by (cases binop) simp_all
  2149 
  2150 lemma constVal_Boolean: 
  2151  assumes const: "constVal e = Some c" and
  2152             wt: "Env\<turnstile>e\<Colon>-PrimT Boolean"
  2153   shows "typeof empty_dt c = Some (PrimT Boolean)"
  2154 proof - 
  2155   have True and 
  2156        "\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk> 
  2157                 \<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"
  2158        and True 
  2159   proof (induct rule: var.induct expr.induct stmt.induct)
  2160     case NewC hence False by simp thus ?case ..
  2161   next
  2162     case NewA hence False by simp thus ?case ..
  2163   next
  2164     case Cast hence False by simp thus ?case ..
  2165   next
  2166     case Inst hence False by simp thus ?case ..
  2167   next
  2168     case (Lit v c)
  2169     from \<open>constVal (Lit v) = Some c\<close>
  2170     have "c=v" by simp
  2171     moreover
  2172     from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
  2173     have "typeof empty_dt v = Some (PrimT Boolean)"
  2174       by cases simp
  2175     ultimately show ?case by simp
  2176   next
  2177     case (UnOp unop e c)
  2178     from \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
  2179     have "Boolean = unop_type unop" by cases simp
  2180     moreover
  2181     from \<open>constVal (UnOp unop e) = Some c\<close>
  2182     obtain ce where "c = eval_unop unop ce" by auto
  2183     ultimately show ?case by (simp add: eval_unop_type)
  2184   next
  2185     case (BinOp binop e1 e2 c)
  2186     from \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
  2187     have "Boolean = binop_type binop" by cases simp
  2188     moreover
  2189     from \<open>constVal (BinOp binop e1 e2) = Some c\<close>
  2190     obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
  2191     ultimately show ?case by (simp add: eval_binop_type)
  2192   next
  2193     case Super hence False by simp thus ?case ..
  2194   next
  2195     case Acc hence False by simp thus ?case ..
  2196   next
  2197     case Ass hence False by simp thus ?case ..
  2198   next
  2199     case (Cond b e1 e2 c)
  2200     note c = \<open>constVal (b ? e1 : e2) = Some c\<close>
  2201     then obtain cb c1 c2 where
  2202       cb: "constVal b  = Some cb" and
  2203       c1: "constVal e1 = Some c1" and
  2204       c2: "constVal e2 = Some c2"
  2205       by (auto split: bool.splits)
  2206     note wt = \<open>Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean\<close>
  2207     then
  2208     obtain T1 T2
  2209       where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
  2210             wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2211             wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2212       by cases (auto dest: widen_Boolean2)
  2213     show ?case
  2214     proof (cases "the_Bool cb")
  2215       case True
  2216       from c1 wt_e1 
  2217       have  "typeof empty_dt c1 = Some (PrimT Boolean)" 
  2218         by (rule Cond.hyps)
  2219       with True c cb c1 show ?thesis by simp
  2220     next
  2221       case False
  2222       from c2 wt_e2 
  2223       have "typeof empty_dt c2 = Some (PrimT Boolean)" 
  2224         by (rule Cond.hyps)
  2225       with False c cb c2 show ?thesis by simp
  2226     qed
  2227   next
  2228     case Call hence False by simp thus ?case ..
  2229   qed simp_all
  2230   with const wt
  2231   show ?thesis
  2232     by iprover
  2233 qed     
  2234       
  2235 lemma assigns_if_good_approx:
  2236   assumes
  2237      eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>b\<rightarrow> s1"   and
  2238    normal: "normal s1" and
  2239      bool: "Env\<turnstile> e\<Colon>-PrimT Boolean"
  2240   shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  2241 proof -
  2242   \<comment> \<open>To properly perform induction on the evaluation relation we have to
  2243         generalize the lemma to terms not only expressions.\<close>
  2244   { fix t val
  2245    assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
  2246    assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
  2247    assume expr:  "\<exists> expr. t=In1l expr"
  2248    have "assigns_if (the_Bool (the_In1 val)) (the_In1l t) 
  2249                 \<subseteq> dom (locals (store s1))"
  2250    using eval' normal bool' expr
  2251    proof (induct)
  2252      case Abrupt thus ?case by simp
  2253    next
  2254      case (NewC s0 C s1 a s2)
  2255      from \<open>Env\<turnstile>NewC C\<Colon>-PrimT Boolean\<close>
  2256      have False 
  2257        by cases simp
  2258      thus ?case ..
  2259    next
  2260      case (NewA s0 T s1 e i s2 a s3)
  2261      from \<open>Env\<turnstile>New T[e]\<Colon>-PrimT Boolean\<close>
  2262      have False 
  2263        by cases simp
  2264      thus ?case ..
  2265    next
  2266      case (Cast s0 e b s1 s2 T)
  2267      note s2 = \<open>s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1\<close>
  2268      have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))" 
  2269      proof -
  2270        from s2 and \<open>normal s2\<close>
  2271        have "normal s1"
  2272          by (cases s1) simp
  2273        moreover
  2274        from \<open>Env\<turnstile>Cast T e\<Colon>-PrimT Boolean\<close>
  2275        have "Env\<turnstile>e\<Colon>- PrimT Boolean" 
  2276          by cases (auto dest: cast_Boolean2)
  2277        ultimately show ?thesis 
  2278          by (rule Cast.hyps [elim_format]) auto
  2279      qed
  2280      also from s2 
  2281      have "\<dots> \<subseteq> dom (locals (store s2))"
  2282        by simp
  2283      finally show ?case by simp
  2284    next
  2285      case (Inst s0 e v s1 b T)
  2286      from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close> and \<open>normal s1\<close>
  2287      have "assignsE e \<subseteq> dom (locals (store s1))"
  2288        by (rule assignsE_good_approx)
  2289      thus ?case
  2290        by simp
  2291    next
  2292      case (Lit s v)
  2293      from \<open>Env\<turnstile>Lit v\<Colon>-PrimT Boolean\<close>
  2294      have "typeof empty_dt v = Some (PrimT Boolean)"
  2295        by cases simp
  2296      then obtain b where "v=Bool b"
  2297        by (cases v) (simp_all add: empty_dt_def)
  2298      thus ?case
  2299        by simp
  2300    next
  2301      case (UnOp s0 e v s1 unop)
  2302      note bool = \<open>Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean\<close>
  2303      hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" 
  2304        by cases (cases unop,simp_all)
  2305      show ?case
  2306      proof (cases "constVal (UnOp unop e)")
  2307        case None
  2308        note \<open>normal s1\<close>
  2309        moreover note bool_e
  2310        ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
  2311          by (rule UnOp.hyps [elim_format]) auto
  2312        moreover
  2313        from bool have "unop = UNot"
  2314          by cases (cases unop, simp_all)
  2315        moreover note None
  2316        ultimately 
  2317        have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) 
  2318               \<subseteq> dom (locals (store s1))"
  2319          by simp
  2320        thus ?thesis by simp
  2321      next
  2322        case (Some c)
  2323        moreover
  2324        from \<open>prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<close>
  2325        have "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
  2326          by (rule eval.UnOp)
  2327        with Some
  2328        have "eval_unop unop v=c"
  2329          by (rule constVal_eval_elim) simp
  2330        moreover
  2331        from Some bool
  2332        obtain b where "c=Bool b"
  2333          by (rule constVal_Boolean [elim_format])
  2334             (cases c, simp_all add: empty_dt_def)
  2335        ultimately
  2336        have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"
  2337          by simp
  2338        thus ?thesis by simp
  2339      qed
  2340    next
  2341      case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
  2342      note bool = \<open>Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean\<close>
  2343      show ?case
  2344      proof (cases "constVal (BinOp binop e1 e2)") 
  2345        case (Some c)
  2346        moreover
  2347        from BinOp.hyps
  2348        have
  2349          "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
  2350          by - (rule eval.BinOp) 
  2351        with Some
  2352        have "eval_binop binop v1 v2=c"
  2353          by (rule constVal_eval_elim) simp
  2354        moreover
  2355        from Some bool
  2356        obtain b where "c = Bool b"
  2357          by (rule constVal_Boolean [elim_format])
  2358             (cases c, simp_all add: empty_dt_def)
  2359        ultimately
  2360        have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) 
  2361              = {}"
  2362          by simp 
  2363        thus ?thesis by simp
  2364      next
  2365        case None
  2366        show ?thesis
  2367        proof (cases "binop=CondAnd \<or> binop=CondOr")
  2368          case True
  2369          from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2370                           bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2371            using True by cases auto
  2372          have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"
  2373          proof -
  2374            from BinOp have "normal s1"
  2375              by - (erule eval_no_abrupt_lemma [rule_format])
  2376            from this bool_e1
  2377            show ?thesis
  2378              by (rule BinOp.hyps [elim_format]) auto
  2379          qed
  2380          also
  2381          from BinOp.hyps
  2382          have "\<dots> \<subseteq> dom (locals (store s2))"
  2383            by - (erule dom_locals_eval_mono_elim,simp)
  2384          finally
  2385          have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".
  2386          from True show ?thesis
  2387          proof
  2388            assume condAnd: "binop = CondAnd"
  2389            show ?thesis
  2390            proof (cases "the_Bool (eval_binop binop v1 v2)")
  2391              case True
  2392              with condAnd 
  2393              have need_second: "need_second_arg binop v1"
  2394                by (simp add: need_second_arg_def)
  2395              from \<open>normal s2\<close>
  2396              have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2397                by (rule BinOp.hyps [elim_format]) 
  2398                   (simp add: need_second bool_e2)+
  2399              with e1_s2
  2400              have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2401                     \<subseteq> dom (locals (store s2))"
  2402                by (rule Un_least)
  2403              with True condAnd None show ?thesis
  2404                by simp
  2405            next
  2406              case False
  2407              note binop_False = this
  2408              show ?thesis
  2409              proof (cases "need_second_arg binop v1")
  2410                case True
  2411                with binop_False condAnd
  2412                obtain "the_Bool v1=True" and "the_Bool v2 = False"
  2413                  by (simp add: need_second_arg_def)
  2414                moreover
  2415                from \<open>normal s2\<close>
  2416                have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2417                  by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
  2418                with e1_s2
  2419                have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2420                       \<subseteq> dom (locals (store s2))"
  2421                  by (rule Un_least)
  2422                moreover note binop_False condAnd None
  2423                ultimately show ?thesis
  2424                  by auto
  2425              next
  2426                case False
  2427                with binop_False condAnd
  2428                have "the_Bool v1=False"
  2429                  by (simp add: need_second_arg_def)
  2430                with e1_s2 
  2431                show ?thesis
  2432                  using binop_False condAnd None by auto
  2433              qed
  2434            qed
  2435          next
  2436            assume condOr: "binop = CondOr"
  2437            show ?thesis
  2438            proof (cases "the_Bool (eval_binop binop v1 v2)")
  2439              case False
  2440              with condOr 
  2441              have need_second: "need_second_arg binop v1"
  2442                by (simp add: need_second_arg_def)
  2443              from \<open>normal s2\<close>
  2444              have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2445                by (rule BinOp.hyps [elim_format]) 
  2446                   (simp add: need_second bool_e2)+
  2447              with e1_s2
  2448              have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2449                     \<subseteq> dom (locals (store s2))"
  2450                by (rule Un_least)
  2451              with False condOr None show ?thesis
  2452                by simp
  2453            next
  2454              case True
  2455              note binop_True = this
  2456              show ?thesis
  2457              proof (cases "need_second_arg binop v1")
  2458                case True
  2459                with binop_True condOr
  2460                obtain "the_Bool v1=False" and "the_Bool v2 = True"
  2461                  by (simp add: need_second_arg_def)
  2462                moreover
  2463                from \<open>normal s2\<close>
  2464                have "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2465                  by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
  2466                with e1_s2
  2467                have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2468                       \<subseteq> dom (locals (store s2))"
  2469                  by (rule Un_least)
  2470                moreover note binop_True condOr None
  2471                ultimately show ?thesis
  2472                  by auto
  2473              next
  2474                case False
  2475                with binop_True condOr
  2476                have "the_Bool v1=True"
  2477                  by (simp add: need_second_arg_def)
  2478                with e1_s2 
  2479                show ?thesis
  2480                  using binop_True condOr None by auto
  2481              qed
  2482            qed
  2483          qed  
  2484        next
  2485          case False
  2486          note \<open>\<not> (binop = CondAnd \<or> binop = CondOr)\<close>
  2487          from BinOp.hyps
  2488          have
  2489            "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
  2490            by - (rule eval.BinOp)  
  2491          moreover note \<open>normal s2\<close>
  2492          ultimately
  2493          have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
  2494            by (rule assignsE_good_approx)
  2495          with False None
  2496          show ?thesis 
  2497            by simp
  2498        qed
  2499      qed
  2500    next     
  2501      case Super 
  2502      note \<open>Env\<turnstile>Super\<Colon>-PrimT Boolean\<close>
  2503      hence False 
  2504        by cases simp
  2505      thus ?case ..
  2506    next
  2507      case (Acc s0 va v f s1)
  2508      from \<open>prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1\<close> and \<open>normal s1\<close>
  2509      have "assignsV va \<subseteq> dom (locals (store s1))"
  2510        by (rule assignsV_good_approx)
  2511      thus ?case by simp
  2512    next
  2513      case (Ass s0 va w f s1 e v s2)
  2514      hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
  2515        by - (rule eval.Ass)
  2516      moreover note \<open>normal (assign f v s2)\<close>
  2517      ultimately 
  2518      have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
  2519        by (rule assignsE_good_approx)
  2520      thus ?case by simp
  2521    next
  2522      case (Cond s0 e0 b s1 e1 e2 v s2)
  2523      from \<open>Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean\<close>
  2524      obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2525             wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2526        by cases (auto dest: widen_Boolean2)
  2527      note eval_e0 = \<open>prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1\<close>
  2528      have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
  2529      proof -
  2530        note eval_e0 
  2531        moreover
  2532        from Cond.hyps and \<open>normal s2\<close> have "normal s1"
  2533          by - (erule eval_no_abrupt_lemma [rule_format],simp)
  2534        ultimately
  2535        have "assignsE e0 \<subseteq> dom (locals (store s1))"
  2536          by (rule assignsE_good_approx)
  2537        also
  2538        from Cond
  2539        have "\<dots> \<subseteq> dom (locals (store s2))"
  2540          by - (erule dom_locals_eval_mono [elim_format],simp)
  2541        finally show ?thesis .
  2542      qed
  2543      show ?case
  2544      proof (cases "constVal e0")
  2545        case None
  2546        have "assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2 
  2547               \<subseteq> dom (locals (store s2))"
  2548        proof (cases "the_Bool b")
  2549          case True
  2550          from \<open>normal s2\<close>
  2551          have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
  2552            by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
  2553          thus ?thesis
  2554            by blast
  2555        next
  2556          case False
  2557          from \<open>normal s2\<close>
  2558          have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
  2559            by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
  2560          thus ?thesis
  2561            by blast
  2562        qed
  2563        with e0_s2
  2564        have "assignsE e0 \<union> 
  2565              (assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2)
  2566                \<subseteq> dom (locals (store s2))"
  2567          by (rule Un_least)
  2568        with None show ?thesis
  2569          by simp
  2570      next
  2571        case (Some c)
  2572        from this eval_e0 have eq_b_c: "b=c" 
  2573          by (rule constVal_eval_elim) 
  2574        show ?thesis
  2575        proof (cases "the_Bool c")
  2576          case True
  2577          from \<open>normal s2\<close>
  2578          have "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"
  2579            by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True wt_e1)
  2580          with e0_s2
  2581          have "assignsE e0 \<union> assigns_if (the_Bool v) e1  \<subseteq> \<dots>"
  2582            by (rule Un_least)
  2583          with Some True show ?thesis
  2584            by simp
  2585        next
  2586          case False
  2587          from \<open>normal s2\<close>
  2588          have "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
  2589            by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False wt_e2)
  2590          with e0_s2
  2591          have "assignsE e0 \<union> assigns_if (the_Bool v) e2  \<subseteq> \<dots>"
  2592            by (rule Un_least)
  2593          with Some False show ?thesis
  2594            by simp
  2595        qed
  2596      qed
  2597    next
  2598      case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
  2599      hence
  2600      "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow> 
  2601                        (set_lvars (locals (store s2)) s4)"
  2602        by - (rule eval.Call)
  2603      hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args)) 
  2604               \<subseteq>  dom (locals (store ((set_lvars (locals (store s2))) s4)))"
  2605        using \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
  2606        by (rule assignsE_good_approx)
  2607      thus ?case by simp
  2608    next
  2609      case Methd show ?case by simp
  2610    next
  2611      case Body show ?case by simp
  2612    qed simp+ \<comment> \<open>all the statements and variables\<close>
  2613  }
  2614  note generalized = this
  2615  from eval bool show ?thesis
  2616    by (rule generalized [elim_format]) simp+
  2617 qed
  2618 
  2619 lemma assigns_if_good_approx': 
  2620   assumes   eval: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"  
  2621      and  normal: "normal s1" 
  2622      and    bool: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>- (PrimT Boolean)"
  2623   shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  2624 proof -
  2625   from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
  2626   from this normal bool show ?thesis
  2627     by (rule assigns_if_good_approx)
  2628 qed
  2629 
  2630  
  2631 lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C" 
  2632   by blast
  2633 
  2634 lemma subset_Intr: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C" 
  2635   by blast
  2636 
  2637 lemma da_good_approx: 
  2638   assumes  eval: "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  2639            wt: "Env\<turnstile>t\<Colon>T"     (is "?Wt Env t T") and
  2640            da: "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"  (is "?Da Env s0 t A") and 
  2641            wf: "wf_prog (prg Env)" 
  2642      shows "(normal s1 \<longrightarrow> (nrm A \<subseteq>  dom (locals (store s1)))) \<and>
  2643             (\<forall> l. abrupt s1 = Some (Jump (Break l)) \<and> normal s0 
  2644                        \<longrightarrow> (brk A l \<subseteq> dom (locals (store s1)))) \<and>
  2645             (abrupt s1 = Some (Jump Ret) \<and> normal s0 
  2646                        \<longrightarrow> Result \<in> dom (locals (store s1)))"
  2647      (is "?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1")
  2648 proof -
  2649   note inj_term_simps [simp]
  2650   obtain G where G: "prg Env = G" by (cases Env) simp
  2651   with eval have eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp
  2652   from G wf have wf: "wf_prog G" by simp
  2653   let ?HypObj = "\<lambda> t s0 s1.
  2654       \<forall> Env T A. ?Wt Env t T \<longrightarrow>  ?Da Env s0 t A \<longrightarrow> prg Env = G 
  2655        \<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned  s0 s1"
  2656   \<comment> \<open>Goal in object logic variant\<close> 
  2657   let ?Hyp = "\<lambda>t s0 s1. (\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk> 
  2658         \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1)"
  2659   from eval and wt da G
  2660   show ?thesis
  2661   proof (induct arbitrary: Env T A)
  2662     case (Abrupt xc s t Env T A)
  2663     have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp 
  2664     have "?NormalAssigned (Some xc,s) A" 
  2665       by simp
  2666     moreover
  2667     have "?BreakAssigned (Some xc,s) (Some xc,s) A"
  2668       by simp
  2669     moreover have "?ResAssigned (Some xc,s) (Some xc,s)"
  2670       by simp
  2671     ultimately show ?case by (intro conjI)
  2672   next
  2673     case (Skip s Env T A)
  2674     have da: "Env\<turnstile> dom (locals (store (Norm s))) \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
  2675       using Skip.prems by simp
  2676     hence "nrm A = dom (locals (store (Norm s)))"
  2677       by (rule da_elim_cases) simp
  2678     hence "?NormalAssigned (Norm s) A"
  2679       by auto
  2680     moreover
  2681     have "?BreakAssigned (Norm s) (Norm s) A" 
  2682       by simp
  2683     moreover have "?ResAssigned (Norm s) (Norm s)"
  2684       by simp
  2685     ultimately show ?case by (intro conjI)
  2686   next
  2687     case (Expr s0 e v s1 Env T A)
  2688     from Expr.prems
  2689     show "?NormalAssigned s1 A \<and> ?BreakAssigned (Norm s0) s1 A 
  2690            \<and> ?ResAssigned (Norm s0) s1"
  2691       by (elim wt_elim_cases da_elim_cases) 
  2692          (rule Expr.hyps, auto)
  2693   next 
  2694     case (Lab s0 c s1 j Env T A)
  2695     note G = \<open>prg Env = G\<close>
  2696     from Lab.prems
  2697     obtain C l where
  2698       da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
  2699          A: "nrm A = nrm C \<inter> (brk C) l" "brk A = rmlab l (brk C)" and
  2700          j: "j = Break l"
  2701       by - (erule da_elim_cases, simp)
  2702     from Lab.prems
  2703     have wt_c: "Env\<turnstile>c\<Colon>\<surd>"
  2704       by - (erule wt_elim_cases, simp)
  2705     from wt_c da_c G and Lab.hyps
  2706     have norm_c: "?NormalAssigned s1 C" and 
  2707           brk_c: "?BreakAssigned (Norm s0) s1 C" and
  2708           res_c: "?ResAssigned (Norm s0) s1"
  2709       by simp_all
  2710     have "?NormalAssigned (abupd (absorb j) s1) A"
  2711     proof
  2712       assume normal: "normal (abupd (absorb j) s1)"
  2713       show "nrm A \<subseteq> dom (locals (store (abupd (absorb j) s1)))"
  2714       proof (cases "abrupt s1")
  2715         case None
  2716         with norm_c A 
  2717         show ?thesis
  2718           by auto
  2719       next
  2720         case Some
  2721         with normal j 
  2722         have "abrupt s1 = Some (Jump (Break l))"
  2723           by (auto dest: absorb_Some_NoneD)
  2724         with brk_c A
  2725         show ?thesis
  2726           by auto
  2727       qed
  2728     qed
  2729     moreover 
  2730     have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"
  2731     proof -
  2732       {
  2733         fix l'
  2734         assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"
  2735         with j 
  2736         have "l\<noteq>l'"
  2737           by (cases s1) (auto dest!: absorb_Some_JumpD)
  2738         hence "(rmlab l (brk C)) l'= (brk C) l'"
  2739           by (simp)
  2740         with break brk_c A
  2741         have 
  2742           "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"
  2743           by (cases s1) auto
  2744       }
  2745       then show ?thesis
  2746         by simp
  2747     qed
  2748     moreover
  2749     from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)"
  2750       by (cases s1) (simp add: absorb_def)
  2751     ultimately show ?case by (intro conjI)
  2752   next
  2753     case (Comp s0 c1 s1 c2 s2 Env T A)
  2754     note G = \<open>prg Env = G\<close>
  2755     from Comp.prems
  2756     obtain C1 C2
  2757       where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and 
  2758             da_c2: "Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  2759                 A: "nrm A = nrm C2" "brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)"
  2760       by (elim da_elim_cases) simp
  2761     from Comp.prems
  2762     obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  2763            wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
  2764       by (elim wt_elim_cases) simp
  2765     note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1\<close>
  2766     with wt_c1 da_c1 G 
  2767     obtain nrm_c1: "?NormalAssigned s1 C1" and 
  2768            brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
  2769            res_c1: "?ResAssigned (Norm s0) s1"
  2770       by simp
  2771     show ?case
  2772     proof (cases "normal s1")
  2773       case True
  2774       with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover
  2775       with da_c2 obtain C2' 
  2776         where  da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  2777                nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
  2778                brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  2779         by (rule da_weakenE) iprover
  2780       note \<open>PROP ?Hyp (In1r c2) s1 s2\<close>
  2781       with wt_c2 da_c2' G
  2782       obtain nrm_c2': "?NormalAssigned s2 C2'" and 
  2783              brk_c2': "?BreakAssigned s1 s2 C2'" and
  2784              res_c2 : "?ResAssigned s1 s2" 
  2785         by simp
  2786       from nrm_c2' nrm_c2 A
  2787       have "?NormalAssigned s2 A" 
  2788         by blast
  2789       moreover from brk_c2' brk_c2 A
  2790       have "?BreakAssigned s1 s2 A" 
  2791         by fastforce
  2792       with True 
  2793       have "?BreakAssigned (Norm s0) s2 A" by simp
  2794       moreover from res_c2 True
  2795       have "?ResAssigned (Norm s0) s2"
  2796         by simp
  2797       ultimately show ?thesis by (intro conjI)
  2798     next
  2799       case False
  2800       with \<open>G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<close>
  2801       have eq_s1_s2: "s2=s1" by auto
  2802       with False have "?NormalAssigned s2 A" by blast
  2803       moreover
  2804       have "?BreakAssigned (Norm s0) s2 A"
  2805       proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")
  2806         case True
  2807         then obtain l where l: "abrupt s1 = Some (Jump (Break l))" .. 
  2808         with brk_c1
  2809         have "brk C1 l \<subseteq> dom (locals (store s1))"
  2810           by simp
  2811         with A eq_s1_s2 
  2812         have "brk A l \<subseteq> dom (locals (store s2))" 
  2813           by auto
  2814         with l eq_s1_s2
  2815         show ?thesis by simp
  2816       next
  2817         case False
  2818         with eq_s1_s2 show ?thesis by simp
  2819       qed
  2820       moreover from False res_c1 eq_s1_s2
  2821       have "?ResAssigned (Norm s0) s2"
  2822         by simp
  2823       ultimately show ?thesis by (intro conjI)
  2824     qed
  2825   next
  2826     case (If s0 e b s1 c1 c2 s2 Env T A)
  2827     note G = \<open>prg Env = G\<close>
  2828     with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
  2829     from If.prems
  2830     obtain E C1 C2 where
  2831       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  2832       da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2833                    \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
  2834       da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2835                    \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  2836       A: "nrm A = nrm C1 \<inter> nrm C2"  "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
  2837       by (elim da_elim_cases) 
  2838     from If.prems
  2839     obtain 
  2840        wt_e:  "Env\<turnstile>e\<Colon>- PrimT Boolean" and 
  2841        wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  2842        wt_c2: "Env\<turnstile>c2\<Colon>\<surd>" 
  2843       by (elim wt_elim_cases)
  2844     from If.hyps have
  2845      s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2846       by (elim dom_locals_eval_mono_elim)
  2847     show ?case
  2848     proof (cases "normal s1")
  2849       case True
  2850       note normal_s1 = this 
  2851       show ?thesis
  2852       proof (cases "the_Bool b")
  2853         case True
  2854         from eval_e normal_s1 wt_e
  2855         have "assigns_if True e \<subseteq> dom (locals (store s1))"
  2856           by (rule assigns_if_good_approx [elim_format]) (simp add: True)
  2857         with s0_s1
  2858         have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"
  2859           by (rule Un_least)
  2860         with da_c1 obtain C1'
  2861           where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  2862                 nrm_c1: "nrm C1 \<subseteq> nrm C1'"                  and
  2863                 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"
  2864           by (rule da_weakenE) iprover
  2865         from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp
  2866         with wt_c1 da_c1'
  2867         obtain nrm_c1': "?NormalAssigned s2 C1'" and 
  2868                brk_c1': "?BreakAssigned s1 s2 C1'" and
  2869                res_c1: "?ResAssigned s1 s2"
  2870           using G by simp
  2871         from nrm_c1' nrm_c1 A
  2872         have "?NormalAssigned s2 A" 
  2873           by blast
  2874         moreover from brk_c1' brk_c1 A
  2875         have "?BreakAssigned s1 s2 A" 
  2876           by fastforce
  2877         with normal_s1
  2878         have "?BreakAssigned (Norm s0) s2 A" by simp
  2879         moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"
  2880           by simp
  2881         ultimately show ?thesis by (intro conjI)
  2882       next
  2883         case False
  2884         from eval_e normal_s1 wt_e
  2885         have "assigns_if False e \<subseteq> dom (locals (store s1))"
  2886           by (rule assigns_if_good_approx [elim_format]) (simp add: False)
  2887         with s0_s1
  2888         have "dom (locals (store ((Norm s0)::state)))\<union> assigns_if False e \<subseteq> \<dots>"
  2889           by (rule Un_least)
  2890         with da_c2 obtain C2'
  2891           where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  2892                 nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
  2893                 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  2894           by (rule da_weakenE) iprover
  2895         from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp
  2896         with wt_c2 da_c2'
  2897         obtain nrm_c2': "?NormalAssigned s2 C2'" and 
  2898                brk_c2': "?BreakAssigned s1 s2 C2'" and
  2899                res_c2: "?ResAssigned s1 s2"
  2900           using G by simp
  2901         from nrm_c2' nrm_c2 A
  2902         have "?NormalAssigned s2 A" 
  2903           by blast
  2904         moreover from brk_c2' brk_c2 A
  2905         have "?BreakAssigned s1 s2 A" 
  2906           by fastforce
  2907         with normal_s1
  2908         have "?BreakAssigned (Norm s0) s2 A" by simp
  2909         moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"
  2910           by simp
  2911         ultimately show ?thesis by (intro conjI)
  2912       qed
  2913     next
  2914       case False 
  2915       then obtain abr where abr: "abrupt s1 = Some abr"
  2916         by (cases s1) auto
  2917       moreover
  2918       from eval_e _ wt_e have "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2919         by (rule eval_expression_no_jump) (simp_all add: G wf)
  2920       moreover
  2921       have "s2 = s1"
  2922       proof -
  2923         from abr and \<open>G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<close>
  2924         show ?thesis  
  2925           by (cases s1) simp
  2926       qed
  2927       ultimately show ?thesis by simp
  2928     qed
  2929   next
  2930     case (Loop s0 e b s1 c s2 l s3 Env T A)
  2931     note G = \<open>prg Env = G\<close>
  2932     with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" 
  2933       by (simp (no_asm_simp))
  2934     from Loop.prems
  2935     obtain E C where
  2936       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  2937       da_c: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2938                    \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
  2939      A: "nrm A = nrm C \<inter> 
  2940               (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)"
  2941         "brk A = brk C"
  2942       by (elim da_elim_cases) 
  2943     from Loop.prems
  2944     obtain 
  2945        wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
  2946        wt_c: "Env\<turnstile>c\<Colon>\<surd>"
  2947       by (elim wt_elim_cases)
  2948     from wt_e da_e G
  2949     obtain res_s1: "?ResAssigned (Norm s0) s1"  
  2950       by (elim Loop.hyps [elim_format]) simp+
  2951     from Loop.hyps have
  2952       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2953       by (elim dom_locals_eval_mono_elim)
  2954     show ?case
  2955     proof (cases "normal s1")
  2956       case True
  2957       note normal_s1 = this
  2958       show ?thesis
  2959       proof (cases "the_Bool b")
  2960         case True  
  2961         with Loop.hyps obtain
  2962           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  2963           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  2964           by simp
  2965         from Loop.hyps True 
  2966         have "?HypObj (In1r c) s1 s2" by simp
  2967         note hyp_c = this [rule_format]
  2968         from Loop.hyps True
  2969         have "?HypObj (In1r (l\<bullet> While(e) c)) (abupd (absorb (Cont l)) s2) s3"
  2970           by simp
  2971         note hyp_while = this [rule_format]
  2972         from eval_e normal_s1 wt_e
  2973         have "assigns_if True e \<subseteq> dom (locals (store s1))"
  2974           by (rule assigns_if_good_approx [elim_format]) (simp add: True)
  2975         with s0_s1
  2976         have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"
  2977           by (rule Un_least)
  2978         with da_c obtain C'
  2979           where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
  2980              nrm_C_C': "nrm C \<subseteq> nrm C'"                  and
  2981              brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"
  2982           by (rule da_weakenE) iprover
  2983         from hyp_c wt_c da_c'
  2984         obtain nrm_C': "?NormalAssigned s2 C'" and 
  2985           brk_C': "?BreakAssigned s1 s2 C'" and
  2986           res_s2: "?ResAssigned s1 s2"
  2987           using G by simp
  2988         show ?thesis
  2989         proof (cases "normal s2 \<or> abrupt s2 = Some (Jump (Cont l))")
  2990           case True
  2991           from Loop.prems obtain
  2992             wt_while: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" and
  2993             da_while: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) 
  2994                            \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
  2995             by simp
  2996           have "dom (locals (store ((Norm s0)::state)))
  2997                   \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  2998           proof -
  2999             note s0_s1
  3000             also from eval_c 
  3001             have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  3002               by (rule dom_locals_eval_mono_elim)
  3003             also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  3004               by simp
  3005             finally show ?thesis .
  3006           qed
  3007           with da_while obtain A'
  3008             where 
  3009             da_while': "Env\<turnstile> dom (locals (store (abupd (absorb (Cont l)) s2))) 
  3010                        \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" 
  3011             and  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3012             and  brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
  3013             by (rule da_weakenE) simp
  3014           with wt_while hyp_while
  3015           obtain nrm_A': "?NormalAssigned s3 A'" and
  3016                  brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and
  3017                  res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3"
  3018             using G by simp 
  3019           from nrm_A_A' nrm_A'
  3020           have "?NormalAssigned s3 A" 
  3021             by blast
  3022           moreover 
  3023           have "?BreakAssigned (Norm s0) s3 A" 
  3024           proof -
  3025             from brk_A_A' brk_A' 
  3026             have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A" 
  3027               by fastforce
  3028             moreover
  3029             from True have "normal (abupd (absorb (Cont l)) s2)"
  3030               by (cases s2) auto
  3031             ultimately show ?thesis
  3032               by simp
  3033           qed
  3034           moreover from res_s3 True have "?ResAssigned (Norm s0) s3"
  3035             by auto
  3036           ultimately show ?thesis by (intro conjI)
  3037         next
  3038           case False
  3039           then obtain abr where 
  3040             "abrupt s2 = Some abr" and
  3041             "abrupt (abupd (absorb (Cont l)) s2) = Some abr"
  3042             by auto
  3043           with eval_while 
  3044           have eq_s3_s2: "s3=s2"
  3045             by auto
  3046           with nrm_C_C' nrm_C' A
  3047           have "?NormalAssigned s3 A"
  3048             by auto
  3049           moreover
  3050           from eq_s3_s2 brk_C_C' brk_C' normal_s1 A
  3051           have "?BreakAssigned (Norm s0) s3 A"
  3052             by fastforce
  3053           moreover 
  3054           from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"
  3055             by simp
  3056           ultimately show ?thesis by (intro conjI)
  3057         qed
  3058       next
  3059         case False
  3060         with Loop.hyps have eq_s3_s1: "s3=s1"
  3061           by simp
  3062         from eq_s3_s1 res_s1 
  3063         have res_s3: "?ResAssigned (Norm s0) s3"
  3064           by simp
  3065         from eval_e True wt_e
  3066         have "assigns_if False e \<subseteq> dom (locals (store s1))"
  3067           by (rule assigns_if_good_approx [elim_format]) (simp add: False)
  3068         with s0_s1
  3069         have "dom (locals (store ((Norm s0)::state)))\<union>assigns_if False e \<subseteq> \<dots>"
  3070           by (rule Un_least)
  3071         hence "nrm C \<inter> 
  3072                (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)
  3073                \<subseteq> dom (locals (store s1))"
  3074           by (rule subset_Intr)
  3075         with normal_s1 A eq_s3_s1
  3076         have "?NormalAssigned s3 A"
  3077           by simp
  3078         moreover
  3079         from normal_s1 eq_s3_s1
  3080         have "?BreakAssigned (Norm s0) s3 A"
  3081           by simp
  3082         moreover note res_s3
  3083         ultimately show ?thesis by (intro conjI)
  3084       qed
  3085     next
  3086       case False
  3087       then obtain abr where abr: "abrupt s1 = Some abr"
  3088         by (cases s1) auto
  3089       moreover
  3090       from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  3091         by (rule eval_expression_no_jump) (simp_all add: wf G)
  3092       moreover
  3093       have eq_s3_s1: "s3=s1"
  3094       proof (cases "the_Bool b")
  3095         case True  
  3096         with Loop.hyps obtain
  3097           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  3098           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  3099           by simp
  3100         from eval_c abr have "s2=s1" by auto
  3101         moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  3102           by (cases s1) (simp add: absorb_def)
  3103         ultimately show ?thesis
  3104           using eval_while abr
  3105           by auto
  3106       next
  3107         case False
  3108         with Loop.hyps show ?thesis by simp
  3109       qed
  3110       moreover
  3111       from eq_s3_s1 res_s1 
  3112       have res_s3: "?ResAssigned (Norm s0) s3"
  3113         by simp
  3114       ultimately show ?thesis
  3115         by simp 
  3116     qed
  3117   next 
  3118     case (Jmp s j Env T A)
  3119     have "?NormalAssigned (Some (Jump j),s) A" by simp
  3120     moreover
  3121     from Jmp.prems
  3122     obtain ret: "j = Ret \<longrightarrow> Result \<in> dom (locals (store (Norm s)))" and
  3123            brk: "brk A = (case j of
  3124                            Break l \<Rightarrow> \<lambda> k. if k=l 
  3125                                      then dom (locals (store ((Norm s)::state)))
  3126                                      else UNIV     
  3127                          | Cont l  \<Rightarrow> \<lambda> k. UNIV
  3128                          | Ret     \<Rightarrow> \<lambda> k. UNIV)"
  3129       by (elim da_elim_cases) simp
  3130     from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A"
  3131       by simp
  3132     moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)"
  3133       by simp
  3134     ultimately show ?case by (intro conjI)
  3135   next
  3136     case (Throw s0 e a s1 Env T A)
  3137     note G = \<open>prg Env = G\<close>
  3138     from Throw.prems obtain E where 
  3139       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
  3140       by (elim da_elim_cases)
  3141     from Throw.prems
  3142       obtain eT where wt_e: "Env\<turnstile>e\<Colon>-eT"
  3143         by (elim wt_elim_cases)
  3144     have "?NormalAssigned (abupd (throw a) s1) A"
  3145       by (cases s1) (simp add: throw_def)
  3146     moreover
  3147     have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A"
  3148     proof -
  3149       from G Throw.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" 
  3150         by (simp (no_asm_simp))
  3151       from eval_e _ wt_e 
  3152       have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"
  3153         by (rule eval_expression_no_jump) (simp_all add: wf G) 
  3154       hence "\<And> l. abrupt (abupd (throw a) s1) \<noteq> Some (Jump (Break l))"
  3155         by (cases s1) (simp add: throw_def abrupt_if_def)
  3156       thus ?thesis
  3157         by simp
  3158     qed
  3159     moreover
  3160     from wt_e da_e G have "?ResAssigned (Norm s0) s1"
  3161       by (elim Throw.hyps [elim_format]) simp+
  3162     hence "?ResAssigned (Norm s0) (abupd (throw a) s1)"
  3163       by (cases s1) (simp add: throw_def abrupt_if_def)
  3164     ultimately show ?case by (intro conjI)
  3165   next
  3166     case (Try s0 c1 s1 s2 C vn c2 s3 Env T A)
  3167     note G = \<open>prg Env = G\<close>
  3168     from Try.prems obtain C1 C2 where
  3169       da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1"  and
  3170       da_c2:
  3171        "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
  3172         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  3173       A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
  3174       by (elim da_elim_cases) simp
  3175     from Try.prems obtain 
  3176       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  3177       wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
  3178       by (elim wt_elim_cases)
  3179     have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G 
  3180       by (simp (no_asm_simp))
  3181     note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1\<close>
  3182     with wt_c1 da_c1 G
  3183     obtain nrm_C1: "?NormalAssigned s1 C1" and
  3184            brk_C1: "?BreakAssigned (Norm s0) s1 C1" and
  3185            res_s1: "?ResAssigned (Norm s0) s1"
  3186       by simp
  3187     show ?case
  3188     proof (cases "normal s1")
  3189       case True
  3190       with nrm_C1 have "nrm C1 \<inter> nrm C2 \<subseteq> dom (locals (store s1))"
  3191         by auto
  3192       moreover
  3193       have "s3=s1"
  3194       proof -
  3195         from sxalloc True have eq_s2_s1: "s2=s1"
  3196           by (cases s1) (auto elim: sxalloc_elim_cases)
  3197         with True have "\<not>  G,s2\<turnstile>catch C"
  3198           by (simp add: catch_def)
  3199         with Try.hyps have "s3=s2"
  3200           by simp
  3201         with eq_s2_s1 show ?thesis by simp
  3202       qed
  3203       ultimately show ?thesis
  3204         using True A res_s1 by simp
  3205     next
  3206       case False
  3207       note not_normal_s1 = this
  3208       show ?thesis
  3209       proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")
  3210         case True
  3211         then obtain l where l: "abrupt s1 = Some (Jump (Break l))"
  3212           by auto
  3213         with brk_C1 have "(brk C1 \<Rightarrow>\<inter> brk C2) l \<subseteq> dom (locals (store s1))"
  3214           by auto
  3215         moreover have "s3=s1"
  3216         proof -
  3217           from sxalloc l have eq_s2_s1: "s2=s1"
  3218             by (cases s1) (auto elim: sxalloc_elim_cases)
  3219           with l have "\<not>  G,s2\<turnstile>catch C"
  3220             by (simp add: catch_def)
  3221           with Try.hyps have "s3=s2"
  3222             by simp
  3223           with eq_s2_s1 show ?thesis by simp
  3224         qed
  3225         ultimately show ?thesis
  3226           using l A res_s1 by simp
  3227       next
  3228         case False
  3229         note abrupt_no_break = this
  3230         show ?thesis
  3231         proof (cases "G,s2\<turnstile>catch C")
  3232           case True
  3233           with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3"
  3234             by simp
  3235           note hyp_c2 = this [rule_format]
  3236           have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  3237                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  3238           proof -
  3239             from \<open>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1\<close>
  3240             have "dom (locals (store ((Norm s0)::state))) 
  3241                     \<subseteq> dom (locals (store s1))"
  3242               by (rule dom_locals_eval_mono_elim)
  3243             also
  3244             from sxalloc
  3245             have "\<dots> \<subseteq> dom (locals (store s2))"
  3246               by (rule dom_locals_sxalloc_mono)
  3247             also 
  3248             have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  3249               by (cases s2) (simp add: new_xcpt_var_def, blast) 
  3250             also
  3251             have "{VName vn} \<subseteq> \<dots>"
  3252               by (cases s2) simp
  3253             ultimately show ?thesis
  3254               by (rule Un_least)
  3255           qed
  3256           with da_c2 
  3257           obtain C2' where
  3258             da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
  3259                      \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  3260            and nrm_C2': "nrm C2 \<subseteq> nrm C2'" 
  3261            and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  3262             by (rule da_weakenE) simp
  3263           from wt_c2 da_C2' G and hyp_c2
  3264           obtain nrmAss_C2: "?NormalAssigned s3 C2'" and
  3265                  brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and
  3266                  resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3"
  3267             by simp
  3268           from nrmAss_C2 nrm_C2' A 
  3269           have "?NormalAssigned s3 A"
  3270             by auto
  3271           moreover
  3272           have "?BreakAssigned (Norm s0) s3 A"
  3273           proof -
  3274             from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"
  3275               by (cases s2) (auto simp add: new_xcpt_var_def)
  3276             with brk_C2' A show ?thesis 
  3277               by fastforce
  3278           qed
  3279           moreover
  3280           from resAss_s3 have "?ResAssigned (Norm s0) s3"
  3281             by (cases s2) ( simp add: new_xcpt_var_def)
  3282           ultimately show ?thesis by (intro conjI)
  3283         next
  3284           case False
  3285           with Try.hyps 
  3286           have eq_s3_s2: "s3=s2" by simp
  3287           moreover from sxalloc not_normal_s1 abrupt_no_break
  3288           obtain "\<not> normal s2" 
  3289                  "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l))"
  3290             by - (rule sxalloc_cases,auto)
  3291           ultimately obtain 
  3292             "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A"
  3293             by (cases s2) auto
  3294           moreover have "?ResAssigned (Norm s0) s3"
  3295           proof (cases "abrupt s1 = Some (Jump Ret)")
  3296             case True
  3297             with sxalloc have "s2=s1"
  3298               by (elim sxalloc_cases) auto
  3299             with res_s1 eq_s3_s2 show ?thesis by simp
  3300           next
  3301             case False
  3302             with sxalloc
  3303             have "abrupt s2 \<noteq> Some (Jump Ret)"
  3304               by (rule sxalloc_no_jump) 
  3305             with eq_s3_s2 show ?thesis
  3306               by simp
  3307           qed
  3308           ultimately show ?thesis by (intro conjI)
  3309         qed
  3310       qed
  3311     qed
  3312   next
  3313     case (Fin s0 c1 x1 s1 c2 s2 s3 Env T A)
  3314     note G = \<open>prg Env = G\<close>
  3315     from Fin.prems obtain C1 C2 where 
  3316       da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
  3317       da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  3318       nrm_A: "nrm A = nrm C1 \<union> nrm C2" and
  3319       brk_A: "brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)"
  3320       by (elim da_elim_cases) simp
  3321     from Fin.prems obtain 
  3322       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  3323       wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
  3324       by (elim wt_elim_cases)
  3325     note \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)\<close>
  3326     with wt_c1 da_C1 G
  3327     obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and
  3328            brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and
  3329            resAss_s1: "?ResAssigned (Norm s0) (x1,s1)"
  3330       by simp
  3331     obtain nrmAss_C2: "?NormalAssigned s2 C2" and
  3332            brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and
  3333            resAss_s2: "?ResAssigned (Norm s1) s2"
  3334     proof -
  3335       from Fin.hyps
  3336       have "dom (locals (store ((Norm s0)::state))) 
  3337              \<subseteq> dom (locals (store (x1,s1)))"
  3338         by - (rule dom_locals_eval_mono_elim) 
  3339       with da_C2 obtain C2'
  3340         where
  3341         da_C2': "Env\<turnstile> dom (locals (store (x1,s1))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  3342         nrm_C2': "nrm C2 \<subseteq> nrm C2'" and
  3343         brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  3344         by (rule da_weakenE) simp
  3345       note \<open>PROP ?Hyp (In1r c2) (Norm s1) s2\<close>
  3346       with wt_c2 da_C2' G
  3347       obtain nrmAss_C2': "?NormalAssigned s2 C2'" and
  3348              brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and
  3349              resAss_s2': "?ResAssigned (Norm s1) s2"
  3350         by simp
  3351       from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"
  3352         by blast
  3353       moreover
  3354       from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"
  3355         by fastforce
  3356       ultimately
  3357       show ?thesis
  3358         using that resAss_s2' by simp
  3359     qed
  3360     note s3 = \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
  3361                        else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
  3362     have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"
  3363     proof -  
  3364       from \<open>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<close>
  3365       show ?thesis
  3366         by (rule dom_locals_eval_mono_elim) simp
  3367     qed
  3368 
  3369     have "?NormalAssigned s3 A"
  3370     proof 
  3371       assume normal_s3: "normal s3"
  3372       show "nrm A \<subseteq> dom (locals (snd s3))"
  3373       proof -
  3374         have "nrm C1 \<subseteq> dom (locals (snd s3))"
  3375         proof -
  3376           from normal_s3 s3
  3377           have "normal (x1,s1)"
  3378             by (cases s2) (simp add: abrupt_if_def)
  3379           with normal_s3 nrmAss_C1 s3 s1_s2
  3380           show ?thesis
  3381             by fastforce
  3382         qed
  3383         moreover 
  3384         have "nrm C2 \<subseteq> dom (locals (snd s3))"
  3385         proof -
  3386           from normal_s3 s3
  3387           have "normal s2"
  3388             by (cases s2) (simp add: abrupt_if_def)
  3389           with normal_s3 nrmAss_C2 s3 s1_s2
  3390           show ?thesis
  3391             by fastforce
  3392         qed
  3393         ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"
  3394           by (rule Un_least)
  3395         with nrm_A show ?thesis
  3396           by simp
  3397       qed
  3398     qed
  3399     moreover
  3400     {
  3401       fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"
  3402       have "brk A l \<subseteq> dom (locals (store s3))"
  3403       proof (cases "normal s2")
  3404         case True
  3405         with brk_s3 s3 
  3406         have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  3407           by simp
  3408         have "brk C1 l \<subseteq> dom (locals (store s3))"
  3409         proof -
  3410           from True brk_s3 s3 have "x1=Some (Jump (Break l))"
  3411             by (cases s2) (simp add: abrupt_if_def)
  3412           with brkAss_C1 s1_s2 s2_s3
  3413           show ?thesis
  3414             by simp
  3415         qed
  3416         moreover from True nrmAss_C2 s2_s3
  3417         have "nrm C2 \<subseteq> dom (locals (store s3))"
  3418           by - (rule subset_trans, simp_all)
  3419         ultimately 
  3420         have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"
  3421           by blast
  3422         with brk_A show ?thesis
  3423           by simp blast
  3424       next
  3425         case False
  3426         note not_normal_s2 = this
  3427         have "s3=s2"
  3428         proof (cases "normal (x1,s1)")
  3429           case True with not_normal_s2 s3 show ?thesis
  3430             by (cases s2) (simp add: abrupt_if_def)
  3431         next
  3432           case False with not_normal_s2 s3 brk_s3 show ?thesis
  3433             by (cases s2) (simp add: abrupt_if_def)
  3434         qed
  3435         with brkAss_C2 brk_s3
  3436         have "brk C2 l \<subseteq> dom (locals (store s3))"
  3437           by simp
  3438         with brk_A show ?thesis
  3439           by simp blast
  3440       qed
  3441     }
  3442     hence "?BreakAssigned (Norm s0) s3 A"
  3443       by simp
  3444     moreover
  3445     {
  3446       assume abr_s3: "abrupt s3 = Some (Jump Ret)"
  3447       have "Result \<in> dom (locals (store s3))"
  3448       proof (cases "x1 = Some (Jump Ret)")
  3449         case True
  3450         note ret_x1 = this
  3451         with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"
  3452           by simp
  3453         moreover have "dom (locals (store ((Norm s1)::state))) 
  3454                          \<subseteq> dom (locals (store s2))"
  3455           by (rule dom_locals_eval_mono_elim) (rule Fin.hyps)
  3456         ultimately have "Result \<in> dom (locals (store s2))"
  3457           by - (rule subsetD,auto)
  3458         with res_s1 s3 show ?thesis
  3459           by simp
  3460       next
  3461         case False
  3462         with s3 abr_s3 obtain  "abrupt s2 = Some (Jump Ret)" and "s3=s2"
  3463           by (cases s2) (simp add: abrupt_if_def)
  3464         with resAss_s2 show ?thesis
  3465           by simp
  3466       qed
  3467     }
  3468     hence "?ResAssigned (Norm s0) s3"
  3469       by simp
  3470     ultimately show ?case by (intro conjI)
  3471   next 
  3472     case (Init C c s0 s3 s1 s2 Env T A)
  3473     note G = \<open>prg Env = G\<close>
  3474     from Init.hyps
  3475     have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"
  3476       apply (simp only: G) 
  3477       apply (rule eval.Init, assumption)
  3478       apply (cases "inited C (globs s0) ")
  3479       apply   simp
  3480       apply (simp only: if_False )
  3481       apply (elim conjE,intro conjI,assumption+,simp)
  3482       done (* auto or simp alone always do too much *)
  3483     from Init.prems and \<open>the (class G C) = c\<close>
  3484     have c: "class G C = Some c"
  3485       by (elim wt_elim_cases) auto
  3486     from Init.prems obtain
  3487        nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  3488       by (elim da_elim_cases) simp
  3489     show ?case
  3490     proof (cases "inited C (globs s0)")
  3491       case True
  3492       with Init.hyps have "s3=Norm s0" by simp
  3493       thus ?thesis
  3494         using nrm_A by simp
  3495     next
  3496       case False
  3497       from Init.hyps False G
  3498       obtain eval_initC: 
  3499               "prg Env\<turnstile>Norm ((init_class_obj G C) s0) 
  3500                        \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  3501              eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  3502              s3: "s3=(set_lvars (locals (store s1))) s2"
  3503         by simp
  3504       have "?NormalAssigned s3 A"
  3505       proof
  3506         show "nrm A \<subseteq> dom (locals (store s3))"
  3507         proof -
  3508           from nrm_A have "nrm A \<subseteq> dom (locals (init_class_obj G C s0))"
  3509             by simp
  3510           also from eval_initC have "\<dots> \<subseteq> dom (locals (store s1))"
  3511             by (rule dom_locals_eval_mono_elim) simp
  3512           also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"
  3513             by (cases s1) (cases s2, simp add: init_lvars_def2)
  3514           finally show ?thesis .
  3515         qed
  3516       qed
  3517       moreover
  3518       from eval 
  3519       have "\<And> j. abrupt s3 \<noteq> Some (Jump j)"
  3520         by (rule eval_statement_no_jump) (auto simp add: wf c G)
  3521       then obtain "?BreakAssigned (Norm s0) s3 A" 
  3522               and "?ResAssigned (Norm s0) s3"
  3523         by simp
  3524       ultimately show ?thesis by (intro conjI)
  3525     qed
  3526   next 
  3527     case (NewC s0 C s1 a s2 Env T A)
  3528     note G = \<open>prg Env = G\<close>
  3529     from NewC.prems
  3530     obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  3531               "brk A = (\<lambda> l. UNIV)"
  3532       by (elim da_elim_cases) simp
  3533     from wf NewC.prems 
  3534     have wt_init: "Env\<turnstile>(Init C)\<Colon>\<surd>"
  3535       by  (elim wt_elim_cases) (drule is_acc_classD,simp)
  3536     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"
  3537     proof -
  3538       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  3539         by (rule dom_locals_eval_mono_elim) (rule NewC.hyps)
  3540       also
  3541       have "\<dots> \<subseteq> dom (locals (store s2))"
  3542         by (rule dom_locals_halloc_mono) (rule NewC.hyps)
  3543       finally show ?thesis .
  3544     qed
  3545     with A have "?NormalAssigned s2 A"
  3546       by simp
  3547     moreover
  3548     {
  3549       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3550       proof -
  3551         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
  3552           unfolding G by (rule eval.NewC NewC.hyps)+
  3553         from NewC.prems 
  3554         obtain T' where  "T=Inl T'"
  3555           by (elim wt_elim_cases) simp
  3556         with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'" 
  3557           by simp
  3558         from eval _ this
  3559         show ?thesis
  3560           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3561       qed
  3562     }
  3563     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3564       by simp_all      
  3565     ultimately show ?case by (intro conjI)
  3566   next
  3567     case (NewA s0 elT s1 e i s2 a s3 Env T A) 
  3568     note G = \<open>prg Env = G\<close>
  3569     from NewA.prems obtain
  3570       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3571       by (elim da_elim_cases)
  3572     from NewA.prems obtain 
  3573       wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
  3574       wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
  3575       by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
  3576     note halloc = \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3\<close>
  3577     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  3578       by (rule dom_locals_eval_mono_elim) (rule NewA.hyps)
  3579     with da_e obtain A' where
  3580                 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" 
  3581         and  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3582         and  brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
  3583       by (rule da_weakenE) simp
  3584     note \<open>PROP ?Hyp (In1l e) s1 s2\<close>
  3585     with wt_size da_e' G obtain 
  3586       nrmAss_A': "?NormalAssigned s2 A'" and
  3587       brkAss_A': "?BreakAssigned s1 s2 A'"
  3588       by simp
  3589     have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  3590     proof -
  3591       have "dom (locals (store s2)) 
  3592              \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"
  3593         by (simp)
  3594       also have "\<dots> \<subseteq> dom (locals (store s3))"
  3595         by (rule dom_locals_halloc_mono) (rule NewA.hyps)
  3596       finally show ?thesis .
  3597     qed 
  3598     have "?NormalAssigned s3 A"
  3599     proof 
  3600       assume normal_s3: "normal s3"
  3601       show "nrm A \<subseteq> dom (locals (store s3))"
  3602       proof -
  3603         from halloc normal_s3 
  3604         have "normal (abupd (check_neg i) s2)"
  3605           by cases simp_all
  3606         hence "normal s2"
  3607           by (cases s2) simp
  3608         with nrmAss_A' nrm_A_A' s2_s3 show ?thesis
  3609           by blast
  3610       qed
  3611     qed
  3612     moreover
  3613     {
  3614       fix j have "abrupt s3 \<noteq> Some (Jump j)"
  3615       proof -
  3616         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
  3617           unfolding G by (rule eval.NewA NewA.hyps)+
  3618         from NewA.prems 
  3619         obtain T' where  "T=Inl T'"
  3620           by (elim wt_elim_cases) simp
  3621         with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'" 
  3622           by simp
  3623         from eval _ this
  3624         show ?thesis
  3625           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3626       qed
  3627     }
  3628     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
  3629       by simp_all
  3630     ultimately show ?case by (intro conjI)
  3631   next
  3632     case (Cast s0 e v s1 s2 cT Env T A)
  3633     note G = \<open>prg Env = G\<close>
  3634     from Cast.prems obtain
  3635       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3636       by (elim da_elim_cases)
  3637     from Cast.prems obtain eT where
  3638       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3639       by (elim wt_elim_cases) 
  3640     note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>
  3641     with wt_e da_e G obtain 
  3642       nrmAss_A: "?NormalAssigned s1 A" and
  3643       brkAss_A: "?BreakAssigned (Norm s0) s1 A"
  3644       by simp
  3645     note s2 = \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
  3646     hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  3647       by simp
  3648     have "?NormalAssigned s2 A"
  3649     proof 
  3650       assume "normal s2"
  3651       with s2 have "normal s1"
  3652         by (cases s1) simp
  3653       with nrmAss_A s1_s2 
  3654       show "nrm A \<subseteq> dom (locals (store s2))"
  3655         by blast
  3656     qed
  3657     moreover
  3658     {
  3659       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3660       proof -
  3661         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
  3662           unfolding G by (rule eval.Cast Cast.hyps)+
  3663         from Cast.prems 
  3664         obtain T' where  "T=Inl T'"
  3665           by (elim wt_elim_cases) simp
  3666         with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'" 
  3667           by simp
  3668         from eval _ this
  3669         show ?thesis
  3670           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3671       qed
  3672     }
  3673     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3674       by simp_all
  3675     ultimately show ?case by (intro conjI)
  3676   next
  3677     case (Inst s0 e v s1 b iT Env T A)
  3678     note G = \<open>prg Env = G\<close>
  3679     from Inst.prems obtain
  3680       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3681       by (elim da_elim_cases)
  3682     from Inst.prems obtain eT where
  3683       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3684       by (elim wt_elim_cases) 
  3685     note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>
  3686     with wt_e da_e G obtain 
  3687       "?NormalAssigned s1 A" and
  3688       "?BreakAssigned (Norm s0) s1 A" and
  3689       "?ResAssigned (Norm s0) s1"
  3690       by simp
  3691     thus ?case by (intro conjI)
  3692   next
  3693     case (Lit s v Env T A)
  3694     from Lit.prems
  3695     have "nrm A = dom (locals (store ((Norm s)::state)))"
  3696       by (elim da_elim_cases) simp
  3697     thus ?case by simp
  3698   next
  3699     case (UnOp s0 e v s1 unop Env T A)
  3700     note G = \<open>prg Env = G\<close>
  3701     from UnOp.prems obtain
  3702       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3703       by (elim da_elim_cases)
  3704     from UnOp.prems obtain eT where
  3705       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3706       by (elim wt_elim_cases) 
  3707     note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>
  3708     with wt_e da_e G obtain 
  3709       "?NormalAssigned s1 A" and
  3710       "?BreakAssigned (Norm s0) s1 A" and
  3711       "?ResAssigned (Norm s0) s1"
  3712       by simp
  3713     thus ?case by (intro conjI)
  3714   next
  3715     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 Env T A)
  3716     note G = \<open>prg Env = G\<close>
  3717     from BinOp.hyps 
  3718     have 
  3719       eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
  3720       by (simp only: G) (rule eval.BinOp)
  3721     have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  3722                   \<subseteq> dom (locals (store s1))"
  3723       by (rule dom_locals_eval_mono_elim) (rule BinOp)
  3724     also have s1_s2: "dom (locals (store s1)) \<subseteq>  dom (locals (store s2))"
  3725       by (rule dom_locals_eval_mono_elim) (rule BinOp)
  3726     finally 
  3727     have s0_s2: "dom (locals (store ((Norm s0)::state))) 
  3728                   \<subseteq> dom (locals (store s2))" .
  3729     from BinOp.prems obtain e1T e2T
  3730       where wt_e1: "Env\<turnstile>e1\<Colon>-e1T" 
  3731        and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
  3732        and  wt_binop: "wt_binop (prg Env) binop e1T e2T"
  3733        and  T: "T=Inl (PrimT (binop_type binop))"
  3734       by (elim wt_elim_cases) simp
  3735     have "?NormalAssigned s2 A"
  3736     proof 
  3737       assume normal_s2: "normal s2"
  3738       have   normal_s1: "normal s1"
  3739         by (rule eval_no_abrupt_lemma [rule_format]) (rule BinOp.hyps, rule normal_s2)
  3740       show "nrm A \<subseteq> dom (locals (store s2))"
  3741       proof (cases "binop=CondAnd")
  3742         case True
  3743         note CondAnd = this
  3744         from BinOp.prems obtain
  3745            nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  3746                             \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3747                                  assigns_if False (BinOp CondAnd e1 e2))"
  3748           by (elim da_elim_cases) (simp_all add: CondAnd)
  3749         from T BinOp.prems CondAnd
  3750         have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"
  3751           by (simp)
  3752         with eval normal_s2
  3753         have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) 
  3754                                  (BinOp binop e1 e2)
  3755                         \<subseteq> dom (locals (store s2))"
  3756           by (rule assigns_if_good_approx) 
  3757         have "(assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3758                          assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"
  3759         proof (cases "the_Bool (eval_binop binop v1 v2)")
  3760           case True
  3761           with ass_if CondAnd  
  3762           have "assigns_if True (BinOp CondAnd e1 e2) 
  3763                  \<subseteq> dom (locals (store s2))"
  3764             by simp
  3765           thus ?thesis by blast
  3766         next
  3767           case False
  3768           with ass_if CondAnd
  3769           have "assigns_if False (BinOp CondAnd e1 e2) 
  3770                  \<subseteq> dom (locals (store s2))"
  3771             by (simp only: False)
  3772           thus ?thesis by blast
  3773         qed
  3774         with s0_s2
  3775         have "dom (locals (store ((Norm s0)::state))) 
  3776                 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3777                    assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"
  3778           by (rule Un_least)
  3779         thus ?thesis by (simp only: nrm_A)
  3780       next
  3781         case False
  3782         note notCondAnd = this
  3783         show ?thesis
  3784         proof (cases "binop=CondOr")
  3785           case True
  3786           note CondOr = this
  3787           from BinOp.prems obtain
  3788             nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  3789                              \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3790                                  assigns_if False (BinOp CondOr e1 e2))"
  3791             by (elim da_elim_cases) (simp_all add: CondOr)
  3792           from T BinOp.prems CondOr
  3793           have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"
  3794             by (simp)
  3795           with eval normal_s2
  3796           have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) 
  3797                                  (BinOp binop e1 e2)
  3798                           \<subseteq> dom (locals (store s2))"
  3799             by (rule assigns_if_good_approx) 
  3800           have "(assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3801                          assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"
  3802           proof (cases "the_Bool (eval_binop binop v1 v2)")
  3803             case True
  3804             with ass_if CondOr 
  3805             have "assigns_if True (BinOp CondOr e1 e2) 
  3806                     \<subseteq> dom (locals (store s2))"
  3807               by (simp)
  3808             thus ?thesis by blast
  3809           next
  3810             case False
  3811             with ass_if CondOr
  3812             have "assigns_if False (BinOp CondOr e1 e2) 
  3813                     \<subseteq> dom (locals (store s2))"
  3814               by (simp)
  3815             thus ?thesis by blast
  3816           qed
  3817           with s0_s2
  3818           have "dom (locals (store ((Norm s0)::state))) 
  3819                  \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3820                     assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"
  3821             by (rule Un_least)
  3822           thus ?thesis by (simp only: nrm_A)
  3823         next
  3824           case False
  3825           with notCondAnd obtain notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
  3826             by simp
  3827           from BinOp.prems obtain E1
  3828             where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"  
  3829              and  da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
  3830             by (elim da_elim_cases) (simp_all add: notAndOr)
  3831           note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1\<close>
  3832           with wt_e1 da_e1 G normal_s1
  3833           obtain "?NormalAssigned s1 E1"  
  3834             by simp
  3835           with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover
  3836           with da_e2 obtain A' 
  3837             where  da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
  3838                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3839             by (rule da_weakenE) iprover
  3840           from notAndOr have "need_second_arg binop v1" by simp
  3841           with BinOp.hyps 
  3842           have "PROP ?Hyp (In1l e2) s1 s2" by simp
  3843           with wt_e2 da_e2' G
  3844           obtain "?NormalAssigned s2 A'"  
  3845             by simp
  3846           with nrm_A_A' normal_s2
  3847           show "nrm A \<subseteq> dom (locals (store s2))" 
  3848             by blast
  3849         qed
  3850       qed
  3851     qed
  3852     moreover
  3853     {
  3854       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3855       proof -
  3856         from BinOp.prems T 
  3857         have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"
  3858           by simp
  3859         from eval _ this
  3860         show ?thesis
  3861           by (rule eval_expression_no_jump) (simp_all add: G wf) 
  3862       qed
  3863     }
  3864     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3865       by simp_all
  3866     ultimately show ?case by (intro conjI) 
  3867   next
  3868     case (Super s Env T A)
  3869     from Super.prems
  3870     have "nrm A = dom (locals (store ((Norm s)::state)))"
  3871       by (elim da_elim_cases) simp
  3872     thus ?case by simp
  3873   next
  3874     case (Acc s0 v w upd s1 Env T A)
  3875     show ?case
  3876     proof (cases "\<exists> vn. v = LVar vn")
  3877       case True
  3878       then obtain vn where vn: "v=LVar vn"..
  3879       from Acc.prems
  3880       have "nrm A = dom (locals (store ((Norm s0)::state)))"
  3881         by (simp only: vn) (elim da_elim_cases,simp_all)
  3882       moreover
  3883       from \<open>G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1\<close>
  3884       have "s1=Norm s0"
  3885         by (simp only: vn) (elim eval_elim_cases,simp)
  3886       ultimately show ?thesis by simp
  3887     next
  3888       case False
  3889       note G = \<open>prg Env = G\<close>
  3890       from False Acc.prems
  3891       have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"
  3892         by (elim da_elim_cases) simp_all 
  3893       from Acc.prems obtain vT where
  3894         wt_v: "Env\<turnstile>v\<Colon>=vT"
  3895         by (elim wt_elim_cases) 
  3896       note \<open>PROP ?Hyp (In2 v) (Norm s0) s1\<close>
  3897       with wt_v da_v G obtain 
  3898         "?NormalAssigned s1 A" and
  3899         "?BreakAssigned (Norm s0) s1 A" and
  3900         "?ResAssigned (Norm s0) s1"
  3901         by simp
  3902       thus ?thesis by (intro conjI)
  3903     qed
  3904   next
  3905     case (Ass s0 var w upd s1 e v s2 Env T A)
  3906     note G = \<open>prg Env = G\<close>
  3907     from Ass.prems obtain varT eT where
  3908       wt_var: "Env\<turnstile>var\<Colon>=varT" and
  3909       wt_e:   "Env\<turnstile>e\<Colon>-eT"
  3910       by (elim wt_elim_cases) simp
  3911     have eval_var: "prg Env\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" 
  3912       using Ass.hyps by (simp only: G)
  3913     have "?NormalAssigned (assign upd v s2) A"
  3914     proof 
  3915       assume normal_ass_s2: "normal (assign upd v s2)"
  3916       from normal_ass_s2 
  3917       have normal_s2: "normal s2"
  3918         by (cases s2) (simp add: assign_def Let_def)
  3919       hence normal_s1: "normal s1"
  3920         by - (rule eval_no_abrupt_lemma [rule_format], rule Ass.hyps)
  3921       note hyp_var = \<open>PROP ?Hyp (In2 var) (Norm s0) s1\<close>
  3922       note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2\<close>
  3923       show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"
  3924       proof (cases "\<exists> vn. var = LVar vn")
  3925         case True
  3926         then obtain vn where vn: "var=LVar vn"..
  3927         from Ass.prems obtain E where
  3928           da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  3929           nrm_A: "nrm A = nrm E \<union> {vn}"
  3930           by (elim da_elim_cases) (insert vn,auto)
  3931         obtain E' where
  3932           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and
  3933           E_E': "nrm E \<subseteq> nrm E'"
  3934         proof -
  3935           have "dom (locals (store ((Norm s0)::state))) 
  3936                   \<subseteq> dom (locals (store s1))"
  3937             by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
  3938           with da_e show thesis
  3939             by (rule da_weakenE) (rule that)
  3940         qed
  3941         from G eval_var vn 
  3942         have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1" 
  3943           by simp
  3944         then have upd: "upd = snd (lvar vn (store s1))"
  3945           by cases (cases "lvar vn (store s1)",simp)
  3946         have "nrm E \<subseteq> dom (locals (store (assign upd v s2)))"
  3947         proof -
  3948           from hyp_e wt_e da_e' G normal_s2
  3949           have "nrm E' \<subseteq> dom (locals (store s2))"
  3950             by simp
  3951           also
  3952           from upd
  3953           have "dom (locals (store s2))  \<subseteq> dom (locals (store (upd v s2)))"
  3954             by (simp add: lvar_def) blast
  3955           hence "dom (locals (store s2)) 
  3956                      \<subseteq> dom (locals (store (assign upd v s2)))"
  3957             by (rule dom_locals_assign_mono)
  3958           finally
  3959           show ?thesis using E_E' 
  3960             by blast
  3961         qed
  3962         moreover
  3963         from upd normal_s2
  3964         have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
  3965           by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)
  3966         ultimately
  3967         show "nrm A \<subseteq> \<dots>"
  3968           by (rule Un_least [elim_format]) (simp add: nrm_A)
  3969       next
  3970         case False
  3971         from Ass.prems obtain V where
  3972           da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and
  3973           da_e:   "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3974           by (elim da_elim_cases) (insert False,simp+)
  3975         from hyp_var wt_var da_var G normal_s1
  3976         have "nrm V \<subseteq> dom (locals (store s1))"
  3977           by simp
  3978         with da_e obtain A' 
  3979           where  da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
  3980                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3981           by (rule da_weakenE) iprover
  3982         from hyp_e wt_e da_e' G normal_s2
  3983         obtain "nrm A' \<subseteq> dom (locals (store s2))"   
  3984           by simp
  3985         with nrm_A_A' have "nrm A \<subseteq> \<dots>" 
  3986           by blast
  3987         also have "\<dots> \<subseteq> dom (locals (store (assign upd v s2)))"
  3988         proof -
  3989           from eval_var normal_s1
  3990           have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"
  3991             by (cases rule: dom_locals_eval_mono_elim)
  3992                (cases s2, simp)
  3993           thus ?thesis
  3994             by (rule dom_locals_assign_mono)
  3995         qed
  3996         finally show ?thesis .
  3997       qed
  3998     qed
  3999     moreover 
  4000     {
  4001       fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"
  4002       proof -
  4003         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
  4004           by (simp only: G) (rule eval.Ass Ass.hyps)+
  4005         from Ass.prems 
  4006         obtain T' where  "T=Inl T'"
  4007           by (elim wt_elim_cases) simp
  4008         with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp
  4009         from eval _ this
  4010         show ?thesis
  4011           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4012       qed
  4013     }
  4014     hence "?BreakAssigned (Norm s0) (assign upd v s2) A"
  4015       and "?ResAssigned (Norm s0) (assign upd v s2)"       
  4016       by simp_all
  4017     ultimately show ?case by (intro conjI)
  4018   next
  4019     case (Cond s0 e0 b s1 e1 e2 v s2 Env T A)
  4020     note G = \<open>prg Env = G\<close>
  4021     have "?NormalAssigned s2 A"
  4022     proof 
  4023       assume normal_s2: "normal s2"
  4024       show "nrm A \<subseteq> dom (locals (store s2))"
  4025       proof (cases "Env\<turnstile>(e0 ? e1 : e2)\<Colon>-(PrimT Boolean)")
  4026         case True
  4027         with Cond.prems 
  4028         have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  4029                              \<union> (assigns_if True  (e0 ? e1 : e2) \<inter> 
  4030                                  assigns_if False (e0 ? e1 : e2))"
  4031           by (elim da_elim_cases) simp_all
  4032         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"
  4033           unfolding G by (rule eval.Cond Cond.hyps)+
  4034         from eval 
  4035         have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"
  4036           by (rule dom_locals_eval_mono_elim)
  4037         moreover
  4038         from eval normal_s2 True
  4039         have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2)
  4040                         \<subseteq> dom (locals (store s2))"
  4041           by (rule assigns_if_good_approx)
  4042         have "assigns_if True  (e0 ? e1:e2) \<inter> assigns_if False (e0 ? e1:e2)
  4043                \<subseteq> dom (locals (store s2))"
  4044         proof (cases "the_Bool v")
  4045           case True 
  4046           from ass_if 
  4047           have "assigns_if True  (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"
  4048             by (simp only: True)
  4049           thus ?thesis by blast
  4050         next
  4051           case False 
  4052           from ass_if 
  4053           have "assigns_if False  (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"
  4054             by (simp only: False)
  4055           thus ?thesis by blast
  4056         qed
  4057         ultimately show "nrm A \<subseteq> dom (locals (store s2))"
  4058           by (simp only: nrm_A) (rule Un_least)
  4059       next
  4060         case False
  4061         with Cond.prems obtain E1 E2 where
  4062          da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  4063                          \<union> assigns_if True e0) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
  4064          da_e2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  4065                         \<union> assigns_if False e0) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2" and
  4066          nrm_A: "nrm A = nrm E1 \<inter> nrm E2"
  4067           by (elim da_elim_cases) simp_all
  4068         from Cond.prems obtain e1T e2T where
  4069           wt_e0: "Env\<turnstile>e0\<Colon>- PrimT Boolean" and
  4070           wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
  4071           wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
  4072           by (elim wt_elim_cases)
  4073         have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  4074                        \<subseteq> dom (locals (store s1))"
  4075           by (rule dom_locals_eval_mono_elim) (rule Cond.hyps)
  4076         have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
  4077           unfolding G by (rule Cond.hyps)
  4078         have normal_s1: "normal s1"
  4079           by (rule eval_no_abrupt_lemma [rule_format]) (rule Cond.hyps, rule normal_s2)
  4080         show ?thesis
  4081         proof (cases "the_Bool b")
  4082           case True
  4083           from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp
  4084           moreover
  4085           from eval_e0 normal_s1 wt_e0
  4086           have "assigns_if True e0 \<subseteq> dom (locals (store s1))"
  4087             by (rule assigns_if_good_approx [elim_format]) (simp only: True)
  4088           with s0_s1 
  4089           have "dom (locals (store ((Norm s0)::state))) 
  4090                  \<union> assigns_if True e0 \<subseteq> \<dots>"
  4091             by (rule Un_least)
  4092           with da_e1 obtain E1' where
  4093                   da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
  4094               nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"
  4095             by (rule da_weakenE) iprover
  4096           ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"
  4097             using wt_e1 G normal_s2 by simp 
  4098           with nrm_E1_E1' show ?thesis
  4099             by (simp only: nrm_A) blast
  4100         next
  4101           case False
  4102           from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp
  4103           moreover
  4104           from eval_e0 normal_s1 wt_e0
  4105           have "assigns_if False e0 \<subseteq> dom (locals (store s1))"
  4106             by (rule assigns_if_good_approx [elim_format]) (simp only: False)
  4107           with s0_s1 
  4108           have "dom (locals (store ((Norm s0)::state))) 
  4109                  \<union> assigns_if False e0 \<subseteq> \<dots>"
  4110             by (rule Un_least)
  4111           with da_e2 obtain E2' where
  4112                   da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
  4113               nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"
  4114             by (rule da_weakenE) iprover
  4115           ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"
  4116             using wt_e2 G normal_s2 by simp 
  4117           with nrm_E2_E2' show ?thesis
  4118             by (simp only: nrm_A) blast
  4119         qed
  4120       qed
  4121     qed
  4122     moreover
  4123     {
  4124       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  4125       proof -
  4126         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
  4127           unfolding G by (rule eval.Cond Cond.hyps)+
  4128         from Cond.prems 
  4129         obtain T' where  "T=Inl T'"
  4130           by (elim wt_elim_cases) simp
  4131         with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp
  4132         from eval _ this
  4133         show ?thesis
  4134           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4135       qed
  4136     } 
  4137     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  4138       by simp_all
  4139     ultimately show ?case by (intro conjI)
  4140   next
  4141     case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
  4142            Env T A)
  4143     note G = \<open>prg Env = G\<close>
  4144     have "?NormalAssigned (restore_lvars s2 s4) A"
  4145     proof 
  4146       assume normal_restore_lvars: "normal (restore_lvars s2 s4)"
  4147       show "nrm A \<subseteq> dom (locals (store (restore_lvars s2 s4)))"
  4148       proof -
  4149         from Call.prems obtain E where
  4150              da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  4151           da_args: "Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A" 
  4152           by (elim da_elim_cases)
  4153         from Call.prems obtain eT argsT where
  4154              wt_e: "Env\<turnstile>e\<Colon>-eT" and
  4155           wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
  4156           by (elim wt_elim_cases)
  4157         note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2\<close>
  4158         note s3' = \<open>s3' = check_method_access G accC statT mode 
  4159                                            \<lparr>name=mn,parTs=pTs\<rparr> a s3\<close>
  4160         have normal_s2: "normal s2"
  4161         proof -
  4162           from normal_restore_lvars have "normal s4"
  4163             by simp
  4164           then have "normal s3'"
  4165             by - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
  4166           with s3' have "normal s3"
  4167             by (cases s3) (simp add: check_method_access_def Let_def)
  4168           with s3 show "normal s2"
  4169             by (cases s2) (simp add: init_lvars_def Let_def)
  4170         qed
  4171         then have normal_s1: "normal s1"
  4172           by  - (rule eval_no_abrupt_lemma [rule_format], rule Call.hyps)
  4173         note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>
  4174         with da_e wt_e G normal_s1
  4175         have "nrm E \<subseteq> dom (locals (store s1))"
  4176           by simp
  4177         with da_args obtain A' where
  4178           da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
  4179           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4180           by (rule da_weakenE) iprover
  4181         note \<open>PROP ?Hyp (In3 args) s1 s2\<close>
  4182         with da_args' wt_args G normal_s2
  4183         have "nrm A' \<subseteq> dom (locals (store s2))"
  4184           by simp
  4185         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4186           by blast
  4187         also have "\<dots> \<subseteq> dom (locals (store (restore_lvars s2 s4)))"
  4188           by (cases s4) simp
  4189         finally show ?thesis .
  4190       qed
  4191     qed
  4192     moreover
  4193     {
  4194       fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"
  4195       proof -
  4196         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
  4197                             \<rightarrow> (restore_lvars s2 s4)"
  4198           unfolding G by (rule eval.Call Call)+
  4199         from Call.prems 
  4200         obtain T' where  "T=Inl T'"
  4201           by (elim wt_elim_cases) simp
  4202         with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'" 
  4203           by simp
  4204         from eval _ this
  4205         show ?thesis
  4206           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4207       qed
  4208     } 
  4209     hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"
  4210       and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"
  4211       by simp_all
  4212     ultimately show ?case by (intro conjI)
  4213   next
  4214     case (Methd s0 D sig v s1 Env T A)
  4215     note G = \<open>prg Env = G\<close>
  4216     from Methd.prems obtain m where
  4217        m:      "methd (prg Env) D sig = Some m" and
  4218        da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state)))) 
  4219                   \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A"
  4220       by - (erule da_elim_cases)
  4221     from Methd.prems m obtain
  4222       isCls: "is_class (prg Env) D" and
  4223       wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"
  4224       by - (erule wt_elim_cases,simp)
  4225     note \<open>PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1\<close>
  4226     moreover
  4227     from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"
  4228       using isCls m G by (simp add: body_def2)
  4229     moreover 
  4230     from da_body have "Env\<turnstile>(dom (locals (store ((Norm s0)::state)))) 
  4231                           \<guillemotright>\<langle>body G D sig\<rangle>\<guillemotright> A"
  4232       using isCls m G by (simp add: body_def2)
  4233     ultimately show ?case
  4234       using G by simp
  4235   next
  4236     case (Body s0 D s1 c s2 s3 Env T A)
  4237     note G = \<open>prg Env = G\<close>
  4238     from Body.prems 
  4239     have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  4240       by (elim da_elim_cases) simp
  4241     have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
  4242                         \<rightarrow>abupd (absorb Ret) s3"
  4243       unfolding G by (rule eval.Body Body.hyps)+
  4244     hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
  4245       by  (simp only: nrm_A) (rule dom_locals_eval_mono_elim)
  4246     hence "?NormalAssigned (abupd (absorb Ret) s3) A"
  4247       by simp
  4248     moreover
  4249     from eval have "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
  4250       by (rule Body_no_jump) simp
  4251     hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and
  4252           "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)"
  4253       by simp_all
  4254     ultimately show ?case by (intro conjI)
  4255   next
  4256     case (LVar s vn Env T A)
  4257     from LVar.prems
  4258     have "nrm A = dom (locals (store ((Norm s)::state)))"
  4259       by (elim da_elim_cases) simp
  4260     thus ?case by simp
  4261   next
  4262     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC Env T A)
  4263     note G = \<open>prg Env = G\<close>
  4264     have "?NormalAssigned s3 A"
  4265     proof 
  4266       assume normal_s3: "normal s3"
  4267       show "nrm A \<subseteq> dom (locals (store s3))"
  4268       proof -
  4269         note fvar = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close> and
  4270           s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
  4271         from FVar.prems
  4272         have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  4273           by (elim da_elim_cases)
  4274         from FVar.prems obtain eT where
  4275           wt_e: "Env\<turnstile>e\<Colon>-eT"
  4276           by (elim wt_elim_cases)
  4277         have "(dom (locals (store ((Norm s0)::state)))) 
  4278                \<subseteq> dom (locals (store s1))"
  4279           by (rule dom_locals_eval_mono_elim) (rule FVar.hyps)
  4280         with da_e obtain A' where
  4281           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
  4282           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4283           by (rule da_weakenE) iprover
  4284         have normal_s2: "normal s2"
  4285         proof -
  4286           from normal_s3 s3 
  4287           have "normal s2'"
  4288             by (cases s2') (simp add: check_field_access_def Let_def)
  4289           with fvar 
  4290           show "normal s2"
  4291             by (cases s2) (simp add: fvar_def2)
  4292         qed
  4293         note \<open>PROP ?Hyp (In1l e) s1 s2\<close>
  4294         with da_e' wt_e G normal_s2
  4295         have "nrm A' \<subseteq> dom (locals (store s2))"
  4296           by simp
  4297         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4298           by blast
  4299         also have "\<dots> \<subseteq> dom (locals (store s3))"
  4300         proof -
  4301           from fvar have "s2' = snd (fvar statDeclC stat fn a s2)" 
  4302             by (cases "fvar statDeclC stat fn a s2") simp
  4303           hence "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  4304             by (simp) (rule dom_locals_fvar_mono)
  4305           also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"
  4306             by (cases s2') (simp add: check_field_access_def Let_def)
  4307           finally show ?thesis .
  4308         qed
  4309         finally show ?thesis .
  4310       qed
  4311     qed
  4312     moreover
  4313     {
  4314       fix j have "abrupt s3 \<noteq> Some (Jump j)"
  4315       proof -
  4316         obtain w upd where v: "(w,upd)=v"
  4317           by (cases v) auto
  4318         have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
  4319           by (simp only: G v) (rule eval.FVar FVar.hyps)+
  4320         from FVar.prems 
  4321         obtain T' where  "T=Inl T'"
  4322           by (elim wt_elim_cases) simp
  4323         with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'" 
  4324           by simp
  4325         from eval _ this
  4326         show ?thesis
  4327           by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
  4328       qed
  4329     } 
  4330     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
  4331       by simp_all
  4332     ultimately show ?case by (intro conjI)
  4333   next
  4334     case (AVar s0 e1 a s1 e2 i s2 v s2' Env T A)
  4335     note G = \<open>prg Env = G\<close>
  4336     have "?NormalAssigned s2' A"
  4337     proof 
  4338       assume normal_s2': "normal s2'"
  4339       show "nrm A \<subseteq> dom (locals (store s2'))"
  4340       proof -
  4341         note avar = \<open>(v, s2') = avar G i a s2\<close>
  4342         from AVar.prems obtain E1 where
  4343           da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
  4344           da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A" 
  4345           by (elim da_elim_cases)
  4346         from AVar.prems obtain e1T e2T where
  4347              wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
  4348              wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
  4349           by (elim wt_elim_cases)
  4350         from avar normal_s2' 
  4351         have normal_s2: "normal s2"
  4352           by (cases s2) (simp add: avar_def2)
  4353         hence "normal s1"
  4354           by - (rule eval_no_abrupt_lemma [rule_format], rule AVar, rule normal_s2)
  4355         moreover note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1\<close>
  4356         ultimately have "nrm E1 \<subseteq> dom (locals (store s1))" 
  4357           using da_e1 wt_e1 G by simp
  4358         with da_e2 obtain A' where
  4359           da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
  4360           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4361           by (rule da_weakenE) iprover
  4362         note \<open>PROP ?Hyp (In1l e2) s1 s2\<close>
  4363         with da_e2' wt_e2 G normal_s2
  4364         have "nrm A' \<subseteq> dom (locals (store s2))"
  4365           by simp
  4366         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4367           by blast
  4368         also have "\<dots> \<subseteq> dom (locals (store s2'))"
  4369         proof -
  4370            from avar have "s2' = snd (avar G i a s2)" 
  4371             by (cases "(avar G i a s2)") simp
  4372           thus "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  4373             by (simp) (rule dom_locals_avar_mono)
  4374         qed
  4375         finally show ?thesis .
  4376       qed
  4377     qed
  4378     moreover
  4379     {
  4380       fix j have "abrupt s2' \<noteq> Some (Jump j)"
  4381       proof -
  4382         obtain w upd where v: "(w,upd)=v"
  4383           by (cases v) auto
  4384         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
  4385           unfolding G v by (rule eval.AVar AVar.hyps)+
  4386         from AVar.prems 
  4387         obtain T' where  "T=Inl T'"
  4388           by (elim wt_elim_cases) simp
  4389         with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'" 
  4390           by simp
  4391         from eval _ this
  4392         show ?thesis
  4393           by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
  4394       qed
  4395     } 
  4396     hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"
  4397       by simp_all
  4398     ultimately show ?case by (intro conjI)
  4399   next
  4400     case (Nil s0 Env T A)
  4401     from Nil.prems
  4402     have "nrm A = dom (locals (store ((Norm s0)::state)))"
  4403       by (elim da_elim_cases) simp
  4404     thus ?case by simp
  4405   next 
  4406     case (Cons s0 e v s1 es vs s2 Env T A)
  4407     note G = \<open>prg Env = G\<close>
  4408     have "?NormalAssigned s2 A"
  4409     proof 
  4410       assume normal_s2: "normal s2"
  4411       show "nrm A \<subseteq> dom (locals (store s2))"
  4412       proof -
  4413         from Cons.prems obtain E where
  4414           da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  4415           da_es: "Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A" 
  4416           by (elim da_elim_cases)
  4417         from Cons.prems obtain eT esT where
  4418              wt_e: "Env\<turnstile>e\<Colon>-eT" and
  4419              wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"
  4420           by (elim wt_elim_cases)
  4421         have "normal s1"
  4422           by - (rule eval_no_abrupt_lemma [rule_format], rule Cons.hyps, rule normal_s2)
  4423         moreover note \<open>PROP ?Hyp (In1l e) (Norm s0) s1\<close>
  4424         ultimately have "nrm E \<subseteq> dom (locals (store s1))" 
  4425           using da_e wt_e G by simp
  4426         with da_es obtain A' where
  4427           da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
  4428           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4429           by (rule da_weakenE) iprover
  4430         note \<open>PROP ?Hyp (In3 es) s1 s2\<close>
  4431         with da_es' wt_es G normal_s2
  4432         have "nrm A' \<subseteq> dom (locals (store s2))"
  4433           by simp
  4434         with nrm_A_A' show "nrm A \<subseteq> dom (locals (store s2))"
  4435           by blast
  4436       qed
  4437     qed
  4438     moreover
  4439     {
  4440       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  4441       proof -
  4442         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
  4443           unfolding G by (rule eval.Cons Cons.hyps)+
  4444         from Cons.prems 
  4445         obtain T' where  "T=Inr T'"
  4446           by (elim wt_elim_cases) simp
  4447         with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'" 
  4448           by simp
  4449         from eval _ this
  4450         show ?thesis
  4451           by (rule eval_expression_list_no_jump) (simp_all add: G wf)
  4452       qed
  4453     } 
  4454     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  4455       by simp_all
  4456     ultimately show ?case by (intro conjI)
  4457   qed
  4458 qed
  4459 
  4460 lemma da_good_approxE:
  4461   assumes
  4462     "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" and "Env\<turnstile>t\<Colon>T" and
  4463     "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A" and "wf_prog (prg Env)"
  4464   obtains
  4465     "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and
  4466     "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
  4467            \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and
  4468     "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))"
  4469   using assms by - (drule (3) da_good_approx, simp)
  4470 
  4471 
  4472 (* Same as above but with explicit environment; 
  4473    It would be nicer to find a "normalized" way to right down those things
  4474    in Bali.
  4475 *)
  4476 lemma da_good_approxE':
  4477   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  4478      and    wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"
  4479      and    da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"
  4480      and    wf: "wf_prog G"
  4481   obtains "normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1))" and
  4482     "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
  4483                        \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and
  4484     "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
  4485         \<Longrightarrow> Result \<in> dom (locals (store s1))"
  4486 proof -
  4487   from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp
  4488   moreover note wt da
  4489   moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
  4490   ultimately show thesis
  4491     using that by (rule da_good_approxE) iprover+
  4492 qed
  4493 
  4494 declare [[simproc add: wt_expr wt_var wt_exprs wt_stmt]]
  4495 
  4496 end