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