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