src/HOL/Bali/DefiniteAssignmentCorrect.thy
author nipkow
Sat Feb 08 14:46:22 2003 +0100 (2003-02-08)
changeset 13811 f39f67982854
parent 13690 ac335b2f4a39
child 14030 cd928c0ac225
permissions -rw-r--r--
adjusted dom rules
     1 header {* Correctness of Definite Assignment *}
     2 
     3 theory DefiniteAssignmentCorrect = WellForm + Eval:
     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.induct)
   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 rules
   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  "?Jmp jmps s1 \<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 rules
   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 [consumes 1]: 
  1615   assumes   eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1616     hyps: "\<lbrakk>dom (locals (store s0)) \<subseteq> dom (locals (store s1));
  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)))\<rbrakk> \<Longrightarrow> P"
  1620  shows "P"
  1621 using eval
  1622 proof (rule dom_locals_eval_mono [THEN conjE])
  1623 qed (rule hyps,auto)
  1624 
  1625 lemma halloc_no_abrupt:
  1626   assumes halloc: "G\<turnstile>s0\<midarrow>halloc oi\<succ>a\<rightarrow>s1" and
  1627           normal: "normal s1"
  1628   shows "normal s0"
  1629 proof -
  1630   from halloc normal show ?thesis
  1631     by cases simp_all
  1632 qed
  1633  
  1634 lemma sxalloc_mono_no_abrupt:
  1635   assumes sxalloc: "G\<turnstile>s0\<midarrow>sxalloc\<rightarrow>s1" and
  1636            normal: "normal s1"
  1637   shows "normal s0"
  1638 proof -
  1639   from sxalloc normal show ?thesis
  1640     by cases simp_all
  1641 qed
  1642    
  1643 lemma union_subseteqI: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A; B' \<subseteq> B\<rbrakk>  \<Longrightarrow>   A' \<union> B' \<subseteq> C"
  1644   by blast
  1645 
  1646 lemma union_subseteqIl: "\<lbrakk>A \<union> B \<subseteq> C; A' \<subseteq> A\<rbrakk>  \<Longrightarrow>   A' \<union> B \<subseteq> C"
  1647   by blast
  1648 
  1649 lemma union_subseteqIr: "\<lbrakk>A \<union> B \<subseteq> C; B' \<subseteq> B\<rbrakk>  \<Longrightarrow>   A \<union> B' \<subseteq> C"
  1650   by blast
  1651 
  1652 lemma subseteq_union_transl [trans]: "\<lbrakk>A \<subseteq> B; B \<union> C \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"
  1653   by blast
  1654 
  1655 lemma subseteq_union_transr [trans]: "\<lbrakk>A \<subseteq> B; C \<union> B \<subseteq> D\<rbrakk> \<Longrightarrow> A \<union> C \<subseteq> D"
  1656   by blast
  1657 
  1658 lemma union_subseteq_weaken: "\<lbrakk>A \<union> B \<subseteq> C; \<lbrakk>A \<subseteq> C; B \<subseteq> C\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"  
  1659   by blast
  1660 
  1661 lemma assigns_good_approx: 
  1662   assumes
  1663       eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1664     normal: "normal s1" 
  1665   shows "assigns t \<subseteq> dom (locals (store s1))"
  1666 proof -
  1667   from eval normal show ?thesis
  1668   proof (induct)
  1669     case Abrupt thus ?case by simp 
  1670   next -- {* For statements its trivial, since then @{term "assigns t = {}"} *}
  1671     case Skip show ?case by simp
  1672   next
  1673     case Expr show ?case by simp 
  1674   next
  1675     case Lab show ?case by simp
  1676   next
  1677     case Comp show ?case by simp
  1678   next
  1679     case If show ?case by simp
  1680   next
  1681     case Loop show ?case by simp
  1682   next
  1683     case Jmp show ?case by simp
  1684   next
  1685     case Throw show ?case by simp
  1686   next
  1687     case Try show ?case by simp 
  1688   next
  1689     case Fin show ?case by simp
  1690   next
  1691     case Init show ?case by simp 
  1692   next
  1693     case NewC show ?case by simp
  1694   next
  1695     case (NewA T a e i s0 s1 s2 s3)
  1696     have halloc: "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1697     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1698     proof -
  1699       from NewA
  1700       have "normal (abupd (check_neg i) s2)"
  1701 	by - (erule halloc_no_abrupt [rule_format])
  1702       hence "normal s2" by (cases s2) simp
  1703       with NewA.hyps
  1704       show ?thesis by rules
  1705     qed
  1706     also
  1707     from halloc 
  1708     have "\<dots> \<subseteq>  dom (locals (store s3))"
  1709       by (rule dom_locals_halloc_mono [elim_format]) simp
  1710     finally show ?case by simp 
  1711   next
  1712     case (Cast T e s0 s1 s2 v)
  1713     hence "normal s1" by (cases s1,simp)
  1714     with Cast.hyps
  1715     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1716       by simp
  1717     also
  1718     from Cast.hyps
  1719     have "\<dots> \<subseteq> dom (locals (store s2))"
  1720       by simp
  1721     finally 
  1722     show ?case
  1723       by simp
  1724   next
  1725     case Inst thus ?case by simp
  1726   next
  1727     case Lit thus ?case by simp
  1728   next
  1729     case UnOp thus ?case by simp
  1730   next
  1731     case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
  1732     hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) 
  1733     with BinOp.hyps
  1734     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
  1735       by rules
  1736     also
  1737     have "\<dots>  \<subseteq> dom (locals (store s2))"
  1738     proof -
  1739       have "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  1740                       else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)" .
  1741       thus ?thesis
  1742 	by (rule dom_locals_eval_mono_elim)
  1743     qed
  1744     finally have s2: "assigns (In1l e1) \<subseteq> dom (locals (store s2))" .
  1745     show ?case
  1746     proof (cases "binop=CondAnd \<or> binop=CondOr")
  1747       case True
  1748       with s2 show ?thesis by simp 
  1749     next
  1750       case False
  1751       with BinOp 
  1752       have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1753 	by (simp add: need_second_arg_def)
  1754       with s2
  1755       show ?thesis using False by (simp add: Un_subset_iff)
  1756     qed
  1757   next
  1758     case Super thus ?case by simp
  1759   next
  1760     case Acc thus ?case by simp
  1761   next 
  1762     case (Ass e f s0 s1 s2 v va w)
  1763     have  nrm_ass_s2: "normal (assign f v s2)" .
  1764     hence nrm_s2: "normal s2"
  1765       by (cases s2, simp add: assign_def Let_def)
  1766     with Ass.hyps 
  1767     have nrm_s1: "normal s1"
  1768       by - (erule eval_no_abrupt_lemma [rule_format]) 
  1769     with Ass.hyps
  1770     have "assigns (In2 va) \<subseteq> dom (locals (store s1))" 
  1771       by rules
  1772     also
  1773     from Ass.hyps
  1774     have "\<dots> \<subseteq> dom (locals (store s2))"
  1775       by - (erule dom_locals_eval_mono_elim)
  1776     also
  1777     from nrm_s2 Ass.hyps
  1778     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1779       by rules
  1780     ultimately
  1781     have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq>  dom (locals (store s2))"
  1782       by (rule Un_least)
  1783     also
  1784     from Ass.hyps nrm_s1
  1785     have "\<dots>  \<subseteq> dom (locals (store (f v s2)))"
  1786       by - (erule dom_locals_eval_mono_elim, cases s2,simp)
  1787     then
  1788     have "dom (locals (store s2))  \<subseteq> dom (locals (store (assign f v s2)))"
  1789       by (rule dom_locals_assign_mono)
  1790     finally
  1791     have va_e: " assigns (In2 va) \<union> assigns (In1l e)
  1792                   \<subseteq> dom (locals (snd (assign f v s2)))" .
  1793     show ?case
  1794     proof (cases "\<exists> n. va = LVar n")
  1795       case False
  1796       with va_e show ?thesis 
  1797 	by (simp add: Un_assoc)
  1798     next
  1799       case True
  1800       then obtain n where va: "va = LVar n"
  1801 	by blast
  1802       with Ass.hyps 
  1803       have "G\<turnstile>Norm s0 \<midarrow>LVar n=\<succ>(w,f)\<rightarrow> s1" 
  1804 	by simp
  1805       hence "(w,f) = lvar n s0"
  1806 	by (rule eval_elim_cases) simp
  1807       with nrm_ass_s2
  1808       have "n \<in> dom (locals (store (assign f v s2)))"
  1809 	by (cases s2) (simp add: assign_def Let_def lvar_def)
  1810       with va_e True va 
  1811       show ?thesis by (simp add: Un_assoc)
  1812     qed
  1813   next
  1814     case (Cond b e0 e1 e2 s0 s1 s2 v) 
  1815     hence "normal s1"
  1816       by - (erule eval_no_abrupt_lemma [rule_format])
  1817     with Cond.hyps
  1818     have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"
  1819       by rules
  1820     also from Cond.hyps
  1821     have "\<dots> \<subseteq> dom (locals (store s2))"
  1822       by - (erule dom_locals_eval_mono_elim)
  1823     finally have e0: "assigns (In1l e0) \<subseteq> dom (locals (store s2))" .
  1824     show ?case
  1825     proof (cases "the_Bool b")
  1826       case True
  1827       with Cond 
  1828       have "assigns (In1l e1) \<subseteq> dom (locals (store s2))"
  1829 	by simp
  1830       hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>" 
  1831 	by blast
  1832       with e0
  1833       have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2) 
  1834              \<subseteq> dom (locals (store s2))"
  1835 	by (rule Un_least)
  1836       thus ?thesis using True by simp 
  1837     next
  1838       case False
  1839       with Cond 
  1840       have " assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1841 	by simp
  1842       hence "assigns (In1l e1) \<inter> assigns (In1l e2) \<subseteq> \<dots>"
  1843 	by blast
  1844       with e0
  1845       have "assigns (In1l e0) \<union> assigns (In1l e1) \<inter> assigns (In1l e2) 
  1846              \<subseteq> dom (locals (store s2))"
  1847 	by (rule Un_least)
  1848       thus ?thesis using False by simp 
  1849     qed
  1850   next
  1851     case (Call D a' accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs)
  1852     have nrm_s2: "normal s2"
  1853     proof -
  1854       have "normal ((set_lvars (locals (snd s2))) s4)" .
  1855       hence normal_s4: "normal s4" by simp
  1856       hence "normal s3'" using Call.hyps
  1857 	by - (erule eval_no_abrupt_lemma [rule_format]) 
  1858       moreover have  
  1859        "s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3".
  1860       ultimately have "normal s3"
  1861 	by (cases s3) (simp add: check_method_access_def Let_def) 
  1862       moreover
  1863       have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2" .
  1864       ultimately show "normal s2"
  1865 	by (cases s2) (simp add: init_lvars_def2)
  1866     qed
  1867     hence "normal s1" using Call.hyps
  1868       by - (erule eval_no_abrupt_lemma [rule_format])
  1869     with Call.hyps
  1870     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1871       by rules
  1872     also from Call.hyps
  1873     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1874       by - (erule dom_locals_eval_mono_elim)
  1875     also
  1876     from nrm_s2 Call.hyps
  1877     have "assigns (In3 args) \<subseteq> dom (locals (store s2))"
  1878       by rules
  1879     ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"
  1880       by (rule Un_least)
  1881     also 
  1882     have "\<dots> \<subseteq> dom (locals (store ((set_lvars (locals (store s2))) s4)))"
  1883       by (cases s4) simp
  1884     finally show ?case
  1885       by simp
  1886   next
  1887     case Methd thus ?case by simp
  1888   next
  1889     case Body thus ?case by simp
  1890   next
  1891     case LVar thus ?case by simp
  1892   next
  1893     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
  1894     have s3:  "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  1895     have avar: "(v, s2') = fvar statDeclC stat fn a s2" .
  1896     have nrm_s2: "normal s2"
  1897     proof -
  1898       have "normal s3" .
  1899       with s3 have "normal s2'"
  1900 	by (cases s2') (simp add: check_field_access_def Let_def)
  1901       with avar show "normal s2"
  1902 	by (cases s2) (simp add: fvar_def2)
  1903     qed
  1904     with FVar.hyps 
  1905     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
  1906       by rules
  1907     also
  1908     have "\<dots> \<subseteq>  dom (locals (store s2'))"
  1909     proof -
  1910       from avar
  1911       have "s2' = snd (fvar statDeclC stat fn a s2)"
  1912 	by (cases "fvar statDeclC stat fn a s2") simp
  1913       thus ?thesis
  1914 	by simp (rule dom_locals_fvar_mono)
  1915     qed
  1916     also from s3
  1917     have "\<dots> \<subseteq>  dom (locals (store s3))"
  1918       by (cases s2') (simp add: check_field_access_def Let_def)
  1919     finally show ?case
  1920       by simp
  1921   next
  1922     case (AVar a e1 e2 i s0 s1 s2 s2' v)
  1923     have avar: "(v, s2') = avar G i a s2" .
  1924     have nrm_s2: "normal s2"
  1925     proof -
  1926       have "normal s2'" .
  1927       with avar
  1928       show ?thesis by (cases s2) (simp add: avar_def2)
  1929     qed
  1930     with AVar.hyps 
  1931     have "normal s1"
  1932       by - (erule eval_no_abrupt_lemma [rule_format])
  1933     with AVar.hyps
  1934     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
  1935       by rules
  1936     also from AVar.hyps
  1937     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1938       by - (erule dom_locals_eval_mono_elim)
  1939     also
  1940     from AVar.hyps nrm_s2
  1941     have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
  1942       by rules
  1943     ultimately
  1944     have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"
  1945       by (rule Un_least)
  1946     also
  1947     have "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  1948     proof -
  1949       from avar have "s2' = snd (avar G i a s2)"
  1950 	by (cases "avar G i a s2") simp
  1951       thus ?thesis
  1952 	by simp (rule dom_locals_avar_mono)
  1953     qed
  1954     finally  
  1955     show ?case
  1956       by simp
  1957   next
  1958     case Nil show ?case by simp
  1959   next
  1960     case (Cons e es s0 s1 s2 v vs)
  1961     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
  1962     proof -
  1963       from Cons
  1964       have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
  1965       with Cons.hyps show ?thesis by rules
  1966     qed
  1967     also from Cons.hyps
  1968     have "\<dots> \<subseteq>  dom (locals (store s2))"
  1969       by - (erule dom_locals_eval_mono_elim)
  1970     also from Cons
  1971     have "assigns (In3 es) \<subseteq> dom (locals (store s2))"
  1972       by rules
  1973     ultimately
  1974     have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"
  1975       by (rule Un_least)
  1976     thus ?case
  1977       by simp
  1978   qed
  1979 qed
  1980 
  1981 corollary assignsE_good_approx:
  1982   assumes
  1983       eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and
  1984     normal: "normal s1"
  1985   shows "assignsE e \<subseteq> dom (locals (store s1))"
  1986 proof -
  1987 from eval normal show ?thesis
  1988   by (rule assigns_good_approx [elim_format]) simp
  1989 qed
  1990 
  1991 corollary assignsV_good_approx:
  1992   assumes
  1993      eval: "prg Env\<turnstile> s0 \<midarrow>v=\<succ>vf\<rightarrow> s1" and
  1994    normal: "normal s1"
  1995   shows "assignsV v \<subseteq> dom (locals (store s1))"
  1996 proof -
  1997 from eval normal show ?thesis
  1998   by (rule assigns_good_approx [elim_format]) simp
  1999 qed
  2000    
  2001 corollary assignsEs_good_approx:
  2002   assumes
  2003       eval: "prg Env\<turnstile> s0 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s1" and
  2004     normal: "normal s1" 
  2005   shows "assignsEs es \<subseteq> dom (locals (store s1))"
  2006 proof -
  2007 from eval normal show ?thesis
  2008   by (rule assigns_good_approx [elim_format]) simp
  2009 qed
  2010 
  2011 lemma constVal_eval: 
  2012  assumes const: "constVal e = Some c" and
  2013           eval: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s"
  2014   shows "v = c \<and> normal s"
  2015 proof -
  2016   have  True and 
  2017         "\<And> c v s0 s. \<lbrakk> constVal e = Some c; G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s\<rbrakk> 
  2018                       \<Longrightarrow> v = c \<and> normal s"
  2019         and True and True
  2020   proof (induct  rule: var_expr_stmt.induct)
  2021     case NewC hence False by simp thus ?case ..
  2022   next
  2023     case NewA hence False by simp thus ?case ..
  2024   next
  2025     case Cast hence False by simp thus ?case ..
  2026   next
  2027     case Inst hence False by simp thus ?case ..
  2028   next
  2029     case (Lit val c v s0 s)
  2030     have "constVal (Lit val) = Some c" .
  2031     moreover
  2032     have "G\<turnstile>Norm s0 \<midarrow>Lit val-\<succ>v\<rightarrow> s" .
  2033     then obtain "v=val" and "normal s"
  2034       by cases simp
  2035     ultimately show "v=c \<and> normal s" by simp
  2036   next
  2037     case (UnOp unop e c v s0 s)
  2038     have const: "constVal (UnOp unop e) = Some c" .
  2039     then obtain ce where ce: "constVal e = Some ce" by simp
  2040     have "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>v\<rightarrow> s" .
  2041     then obtain ve where ve: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>ve\<rightarrow> s" and
  2042                           v: "v = eval_unop unop ve" 
  2043       by cases simp
  2044     from ce ve
  2045     obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
  2046       by (rule UnOp.hyps [elim_format]) rules
  2047     from eq_ve_ce const ce v 
  2048     have "v=c" 
  2049       by simp
  2050     from this nrm_s
  2051     show ?case ..
  2052   next
  2053     case (BinOp binop e1 e2 c v s0 s)
  2054     have const: "constVal (BinOp binop e1 e2) = Some c" .
  2055     then obtain c1 c2 where c1: "constVal e1 = Some c1" and
  2056                             c2: "constVal e2 = Some c2" and
  2057                              c: "c = eval_binop binop c1 c2"
  2058       by simp
  2059     have "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>v\<rightarrow> s" .
  2060     then obtain v1 s1 v2
  2061       where v1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
  2062             v2: "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  2063                                else In1r Skip)\<succ>\<rightarrow> (In1 v2, s)" and
  2064              v: "v = eval_binop binop v1 v2"
  2065       by cases simp
  2066     from c1 v1
  2067     obtain eq_v1_c1: "v1 = c1" and 
  2068              nrm_s1: "normal s1"
  2069       by (rule BinOp.hyps [elim_format]) rules
  2070     show ?case
  2071     proof (cases "need_second_arg binop v1")
  2072       case True
  2073       with v2 nrm_s1  obtain s1' 
  2074 	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s" 
  2075 	by (cases s1) simp
  2076       with c2 obtain "v2 = c2" "normal s"
  2077 	by (rule BinOp.hyps [elim_format]) rules
  2078       with c c1 c2 eq_v1_c1 v 
  2079       show ?thesis by simp
  2080     next
  2081       case False
  2082       with nrm_s1 v2
  2083       have "s=s1"
  2084 	by (cases s1) (auto elim!: eval_elim_cases)
  2085       moreover
  2086       from False c v eq_v1_c1  
  2087       have "v = c"
  2088 	by (simp add: eval_binop_arg2_indep)
  2089       ultimately 
  2090       show ?thesis
  2091 	using nrm_s1 by simp
  2092     qed  (* hallo ehco *)
  2093   next
  2094     case Super hence False by simp thus ?case ..
  2095   next
  2096     case Acc hence False by simp thus ?case ..
  2097   next
  2098     case Ass hence False by simp thus ?case ..
  2099   next
  2100     case (Cond b e1 e2 c v s0 s)
  2101     have c: "constVal (b ? e1 : e2) = Some c" .
  2102     then obtain cb c1 c2 where
  2103       cb: "constVal b  = Some cb" and
  2104       c1: "constVal e1 = Some c1" and
  2105       c2: "constVal e2 = Some c2"
  2106       by (auto split: bool.splits)
  2107     have "G\<turnstile>Norm s0 \<midarrow>b ? e1 : e2-\<succ>v\<rightarrow> s" .
  2108     then obtain vb s1
  2109       where     vb: "G\<turnstile>Norm s0 \<midarrow>b-\<succ>vb\<rightarrow> s1" and
  2110             eval_v: "G\<turnstile>s1 \<midarrow>(if the_Bool vb then e1 else e2)-\<succ>v\<rightarrow> s"
  2111       by cases simp 
  2112     from cb vb
  2113     obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"
  2114       by (rule Cond.hyps [elim_format]) rules 
  2115     show ?case
  2116     proof (cases "the_Bool vb")
  2117       case True
  2118       with c cb c1 eq_vb_cb 
  2119       have "c = c1"
  2120 	by simp
  2121       moreover
  2122       from True eval_v nrm_s1 obtain s1' 
  2123 	where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"
  2124 	by (cases s1) simp
  2125       with c1 obtain "c1 = v" "normal s"
  2126 	by (rule Cond.hyps [elim_format]) rules 
  2127       ultimately show ?thesis by simp
  2128     next
  2129       case False
  2130       with c cb c2 eq_vb_cb 
  2131       have "c = c2"
  2132 	by simp
  2133       moreover
  2134       from False eval_v nrm_s1 obtain s1' 
  2135 	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"
  2136 	by (cases s1) simp
  2137       with c2 obtain "c2 = v" "normal s"
  2138 	by (rule Cond.hyps [elim_format]) rules 
  2139       ultimately show ?thesis by simp
  2140     qed
  2141   next
  2142     case Call hence False by simp thus ?case ..
  2143   qed simp_all
  2144   with const eval
  2145   show ?thesis
  2146     by rules
  2147 qed
  2148   
  2149 lemmas constVal_eval_elim = constVal_eval [THEN conjE]
  2150 
  2151 lemma eval_unop_type: 
  2152   "typeof dt (eval_unop unop v) = Some (PrimT (unop_type unop))"
  2153   by (cases unop) simp_all
  2154 
  2155 lemma eval_binop_type:
  2156   "typeof dt (eval_binop binop v1 v2) = Some (PrimT (binop_type binop))"
  2157   by (cases binop) simp_all
  2158 
  2159 lemma constVal_Boolean: 
  2160  assumes const: "constVal e = Some c" and
  2161             wt: "Env\<turnstile>e\<Colon>-PrimT Boolean"
  2162   shows "typeof empty_dt c = Some (PrimT Boolean)"
  2163 proof - 
  2164   have True and 
  2165        "\<And> c. \<lbrakk>constVal e = Some c;Env\<turnstile>e\<Colon>-PrimT Boolean\<rbrakk> 
  2166                 \<Longrightarrow> typeof empty_dt c = Some (PrimT Boolean)"
  2167        and True and True 
  2168   proof (induct rule: var_expr_stmt.induct)
  2169     case NewC hence False by simp thus ?case ..
  2170   next
  2171     case NewA hence False by simp thus ?case ..
  2172   next
  2173     case Cast hence False by simp thus ?case ..
  2174   next
  2175     case Inst hence False by simp thus ?case ..
  2176   next
  2177     case (Lit v c)
  2178     have "constVal (Lit v) = Some c" .
  2179     hence "c=v" by simp
  2180     moreover have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
  2181     hence "typeof empty_dt v = Some (PrimT Boolean)"
  2182       by cases simp
  2183     ultimately show ?case by simp
  2184   next
  2185     case (UnOp unop e c)
  2186     have "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
  2187     hence "Boolean = unop_type unop" by cases simp
  2188     moreover have "constVal (UnOp unop e) = Some c" .
  2189     then obtain ce where "c = eval_unop unop ce" by auto
  2190     ultimately show ?case by (simp add: eval_unop_type)
  2191   next
  2192     case (BinOp binop e1 e2 c)
  2193     have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
  2194     hence "Boolean = binop_type binop" by cases simp
  2195     moreover have "constVal (BinOp binop e1 e2) = Some c" .
  2196     then obtain c1 c2 where "c = eval_binop binop c1 c2" by auto
  2197     ultimately show ?case by (simp add: eval_binop_type)
  2198   next
  2199     case Super hence False by simp thus ?case ..
  2200   next
  2201     case Acc hence False by simp thus ?case ..
  2202   next
  2203     case Ass hence False by simp thus ?case ..
  2204   next
  2205     case (Cond b e1 e2 c)
  2206     have c: "constVal (b ? e1 : e2) = Some c" .
  2207     then obtain cb c1 c2 where
  2208       cb: "constVal b  = Some cb" and
  2209       c1: "constVal e1 = Some c1" and
  2210       c2: "constVal e2 = Some c2"
  2211       by (auto split: bool.splits)
  2212     have wt: "Env\<turnstile>b ? e1 : e2\<Colon>-PrimT Boolean" .
  2213     then
  2214     obtain T1 T2
  2215       where "Env\<turnstile>b\<Colon>-PrimT Boolean" and
  2216             wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2217             wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2218       by cases (auto dest: widen_Boolean2)
  2219     show ?case
  2220     proof (cases "the_Bool cb")
  2221       case True
  2222       from c1 wt_e1 
  2223       have  "typeof empty_dt c1 = Some (PrimT Boolean)" 
  2224 	by (rule Cond.hyps)
  2225       with True c cb c1 show ?thesis by simp
  2226     next
  2227       case False
  2228       from c2 wt_e2 
  2229       have "typeof empty_dt c2 = Some (PrimT Boolean)" 
  2230 	by (rule Cond.hyps)
  2231       with False c cb c2 show ?thesis by simp
  2232     qed
  2233   next
  2234     case Call hence False by simp thus ?case ..
  2235   qed simp_all
  2236   with const wt
  2237   show ?thesis
  2238     by rules
  2239 qed	
  2240       
  2241 lemma assigns_if_good_approx:
  2242   assumes
  2243      eval: "prg Env\<turnstile> s0 \<midarrow>e-\<succ>b\<rightarrow> s1"   and
  2244    normal: "normal s1" and
  2245      bool: "Env\<turnstile> e\<Colon>-PrimT Boolean"
  2246   shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  2247 proof -
  2248   -- {* To properly perform induction on the evaluation relation we have to
  2249         generalize the lemma to terms not only expressions. *}
  2250   { fix t val
  2251    assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
  2252    assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
  2253    assume expr:  "\<exists> expr. t=In1l expr"
  2254    have "assigns_if (the_Bool (the_In1 val)) (the_In1l t) 
  2255                 \<subseteq> dom (locals (store s1))"
  2256    using eval' normal bool' expr
  2257    proof (induct)
  2258      case Abrupt thus ?case by simp
  2259    next
  2260      case (NewC C a s0 s1 s2)
  2261      have "Env\<turnstile>NewC C\<Colon>-PrimT Boolean" .
  2262      hence False 
  2263        by cases simp
  2264      thus ?case ..
  2265    next
  2266      case (NewA T a e i s0 s1 s2 s3)
  2267      have "Env\<turnstile>New T[e]\<Colon>-PrimT Boolean" .
  2268      hence False 
  2269        by cases simp
  2270      thus ?case ..
  2271    next
  2272      case (Cast T e s0 s1 s2 b)
  2273      have s2: "s2 = abupd (raise_if (\<not> prg Env,snd s1\<turnstile>b fits T) ClassCast) s1".
  2274      have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))" 
  2275      proof -
  2276        have "normal s2" .
  2277        with s2 have "normal s1"
  2278 	 by (cases s1) simp
  2279        moreover
  2280        have "Env\<turnstile>Cast T e\<Colon>-PrimT Boolean" .
  2281        hence "Env\<turnstile>e\<Colon>- PrimT Boolean" 
  2282 	 by (cases) (auto dest: cast_Boolean2)
  2283        ultimately show ?thesis 
  2284 	 by (rule Cast.hyps [elim_format]) auto
  2285      qed
  2286      also from s2 
  2287      have "\<dots> \<subseteq> dom (locals (store s2))"
  2288        by simp
  2289      finally show ?case by simp
  2290    next
  2291      case (Inst T b e s0 s1 v)
  2292      have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" and "normal s1" .
  2293      hence "assignsE e \<subseteq> dom (locals (store s1))"
  2294        by (rule assignsE_good_approx)
  2295      thus ?case
  2296        by simp
  2297    next
  2298      case (Lit s v)
  2299      have "Env\<turnstile>Lit v\<Colon>-PrimT Boolean" .
  2300      hence "typeof empty_dt v = Some (PrimT Boolean)"
  2301        by cases simp
  2302      then obtain b where "v=Bool b"
  2303        by (cases v) (simp_all add: empty_dt_def)
  2304      thus ?case
  2305        by simp
  2306    next
  2307      case (UnOp e s0 s1 unop v)
  2308      have bool: "Env\<turnstile>UnOp unop e\<Colon>-PrimT Boolean" .
  2309      hence bool_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" 
  2310        by cases (cases unop,simp_all)
  2311      show ?case
  2312      proof (cases "constVal (UnOp unop e)")
  2313        case None
  2314        have "normal s1" .
  2315        moreover note bool_e
  2316        ultimately have "assigns_if (the_Bool v) e \<subseteq> dom (locals (store s1))"
  2317 	 by (rule UnOp.hyps [elim_format]) auto
  2318        moreover
  2319        from bool have "unop = UNot"
  2320 	 by cases (cases unop, simp_all)
  2321        moreover note None
  2322        ultimately 
  2323        have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) 
  2324               \<subseteq> dom (locals (store s1))"
  2325 	 by simp
  2326        thus ?thesis by simp
  2327      next
  2328        case (Some c)
  2329        moreover
  2330        have "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
  2331        hence "prg Env\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<rightarrow> s1" 
  2332 	 by (rule eval.UnOp)
  2333        with Some
  2334        have "eval_unop unop v=c"
  2335 	 by (rule constVal_eval_elim) simp
  2336        moreover
  2337        from Some bool
  2338        obtain b where "c=Bool b"
  2339 	 by (rule constVal_Boolean [elim_format])
  2340 	    (cases c, simp_all add: empty_dt_def)
  2341        ultimately
  2342        have "assigns_if (the_Bool (eval_unop unop v)) (UnOp unop e) = {}"
  2343 	 by simp
  2344        thus ?thesis by simp
  2345      qed
  2346    next
  2347      case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
  2348      have bool: "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean" .
  2349      show ?case
  2350      proof (cases "constVal (BinOp binop e1 e2)") 
  2351        case (Some c)
  2352        moreover
  2353        from BinOp.hyps
  2354        have
  2355 	 "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
  2356 	 by - (rule eval.BinOp) 
  2357        with Some
  2358        have "eval_binop binop v1 v2=c"
  2359 	 by (rule constVal_eval_elim) simp
  2360        moreover
  2361        from Some bool
  2362        obtain b where "c = Bool b"
  2363 	 by (rule constVal_Boolean [elim_format])
  2364 	    (cases c, simp_all add: empty_dt_def)
  2365        ultimately
  2366        have "assigns_if (the_Bool (eval_binop binop v1 v2)) (BinOp binop e1 e2) 
  2367              = {}"
  2368 	 by simp 
  2369        thus ?thesis by simp
  2370      next
  2371        case None
  2372        show ?thesis
  2373        proof (cases "binop=CondAnd \<or> binop=CondOr")
  2374 	 case True
  2375 	 from bool obtain bool_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2376                           bool_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2377 	   using True by cases auto
  2378 	 have "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s1))"
  2379 	 proof -
  2380 	   from BinOp have "normal s1"
  2381 	     by - (erule eval_no_abrupt_lemma [rule_format])
  2382 	   from this bool_e1
  2383 	   show ?thesis
  2384 	     by (rule BinOp.hyps [elim_format]) auto
  2385 	 qed
  2386 	 also
  2387 	 from BinOp.hyps
  2388 	 have "\<dots> \<subseteq> dom (locals (store s2))"
  2389 	   by - (erule dom_locals_eval_mono_elim,simp)
  2390 	 finally
  2391 	 have e1_s2: "assigns_if (the_Bool v1) e1 \<subseteq> dom (locals (store s2))".
  2392 	 from True show ?thesis
  2393 	 proof
  2394 	   assume condAnd: "binop = CondAnd"
  2395 	   show ?thesis
  2396 	   proof (cases "the_Bool (eval_binop binop v1 v2)")
  2397 	     case True
  2398 	     with condAnd 
  2399 	     have need_second: "need_second_arg binop v1"
  2400 	       by (simp add: need_second_arg_def)
  2401 	     have "normal s2" . 
  2402 	     hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2403 	       by (rule BinOp.hyps [elim_format]) 
  2404                   (simp add: need_second bool_e2)+
  2405 	     with e1_s2
  2406 	     have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2407 		    \<subseteq> dom (locals (store s2))"
  2408 	       by (rule Un_least)
  2409 	     with True condAnd None show ?thesis
  2410 	       by simp
  2411 	   next
  2412 	     case False
  2413 	     note binop_False = this
  2414 	     show ?thesis
  2415 	     proof (cases "need_second_arg binop v1")
  2416 	       case True
  2417 	       with binop_False condAnd
  2418 	       obtain "the_Bool v1=True" and "the_Bool v2 = False"
  2419 		 by (simp add: need_second_arg_def)
  2420 	       moreover
  2421 	       have "normal s2" . 
  2422 	       hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2423 		 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
  2424 	       with e1_s2
  2425 	       have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2426 		      \<subseteq> dom (locals (store s2))"
  2427 		 by (rule Un_least)
  2428 	       moreover note binop_False condAnd None
  2429 	       ultimately show ?thesis
  2430 		 by auto
  2431 	     next
  2432 	       case False
  2433 	       with binop_False condAnd
  2434 	       have "the_Bool v1=False"
  2435 		 by (simp add: need_second_arg_def)
  2436 	       with e1_s2 
  2437 	       show ?thesis
  2438 		 using binop_False condAnd None by auto
  2439 	     qed
  2440 	   qed
  2441 	 next
  2442 	   assume condOr: "binop = CondOr"
  2443 	   show ?thesis
  2444 	   proof (cases "the_Bool (eval_binop binop v1 v2)")
  2445 	     case False
  2446 	     with condOr 
  2447 	     have need_second: "need_second_arg binop v1"
  2448 	       by (simp add: need_second_arg_def)
  2449 	     have "normal s2" . 
  2450 	     hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2451 	       by (rule BinOp.hyps [elim_format]) 
  2452                   (simp add: need_second bool_e2)+
  2453 	     with e1_s2
  2454 	     have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2455 		    \<subseteq> dom (locals (store s2))"
  2456 	       by (rule Un_least)
  2457 	     with False condOr None show ?thesis
  2458 	       by simp
  2459 	   next
  2460 	     case True
  2461 	     note binop_True = this
  2462 	     show ?thesis
  2463 	     proof (cases "need_second_arg binop v1")
  2464 	       case True
  2465 	       with binop_True condOr
  2466 	       obtain "the_Bool v1=False" and "the_Bool v2 = True"
  2467 		 by (simp add: need_second_arg_def)
  2468 	       moreover
  2469 	       have "normal s2" . 
  2470 	       hence "assigns_if (the_Bool v2) e2 \<subseteq> dom (locals (store s2))"
  2471 		 by (rule BinOp.hyps [elim_format]) (simp add: True bool_e2)+
  2472 	       with e1_s2
  2473 	       have "assigns_if (the_Bool v1) e1 \<union> assigns_if (the_Bool v2) e2
  2474 		      \<subseteq> dom (locals (store s2))"
  2475 		 by (rule Un_least)
  2476 	       moreover note binop_True condOr None
  2477 	       ultimately show ?thesis
  2478 		 by auto
  2479 	     next
  2480 	       case False
  2481 	       with binop_True condOr
  2482 	       have "the_Bool v1=True"
  2483 		 by (simp add: need_second_arg_def)
  2484 	       with e1_s2 
  2485 	       show ?thesis
  2486 		 using binop_True condOr None by auto
  2487 	     qed
  2488 	   qed
  2489 	 qed  
  2490        next
  2491 	 case False
  2492 	 have "\<not> (binop = CondAnd \<or> binop = CondOr)" .
  2493 	 from BinOp.hyps
  2494 	 have
  2495 	  "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>eval_binop binop v1 v2\<rightarrow> s2"
  2496 	   by - (rule eval.BinOp)  
  2497 	 moreover have "normal s2" .
  2498 	 ultimately
  2499 	 have "assignsE (BinOp binop e1 e2) \<subseteq> dom (locals (store s2))"
  2500 	   by (rule assignsE_good_approx)
  2501 	 with False None
  2502 	 show ?thesis 
  2503 	   by simp
  2504        qed
  2505      qed
  2506    next     
  2507      case Super 
  2508      have "Env\<turnstile>Super\<Colon>-PrimT Boolean" .
  2509      hence False 
  2510        by cases simp
  2511      thus ?case ..
  2512    next
  2513      case (Acc f s0 s1 v va)
  2514      have "prg Env\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<rightarrow> s1"  and "normal s1".
  2515      hence "assignsV va \<subseteq> dom (locals (store s1))"
  2516        by (rule assignsV_good_approx)
  2517      thus ?case by simp
  2518    next
  2519      case (Ass e f s0 s1 s2 v va w)
  2520      hence "prg Env\<turnstile>Norm s0 \<midarrow>va := e-\<succ>v\<rightarrow> assign f v s2"
  2521        by - (rule eval.Ass)
  2522      moreover have "normal (assign f v s2)" .
  2523      ultimately 
  2524      have "assignsE (va := e) \<subseteq> dom (locals (store (assign f v s2)))"
  2525        by (rule assignsE_good_approx)
  2526      thus ?case by simp
  2527    next
  2528      case (Cond b e0 e1 e2 s0 s1 s2 v)
  2529      have "Env\<turnstile>e0 ? e1 : e2\<Colon>-PrimT Boolean" .
  2530      then obtain wt_e1: "Env\<turnstile>e1\<Colon>-PrimT Boolean" and
  2531                  wt_e2: "Env\<turnstile>e2\<Colon>-PrimT Boolean"
  2532        by cases (auto dest: widen_Boolean2)
  2533      have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  2534      have e0_s2: "assignsE e0 \<subseteq> dom (locals (store s2))"
  2535      proof -
  2536        note eval_e0 
  2537        moreover
  2538        have "normal s2" .
  2539        with Cond.hyps have "normal s1"
  2540 	 by - (erule eval_no_abrupt_lemma [rule_format],simp)
  2541        ultimately
  2542        have "assignsE e0 \<subseteq> dom (locals (store s1))"
  2543 	 by (rule assignsE_good_approx)
  2544        also
  2545        from Cond
  2546        have "\<dots> \<subseteq> dom (locals (store s2))"
  2547 	 by - (erule dom_locals_eval_mono [elim_format],simp)
  2548        finally show ?thesis .
  2549      qed
  2550      show ?case
  2551      proof (cases "constVal e0")
  2552        case None
  2553        have "assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2 
  2554 	      \<subseteq> dom (locals (store s2))"
  2555        proof (cases "the_Bool b")
  2556 	 case True
  2557 	 have "normal s2" .
  2558 	 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
  2559 	   by (rule Cond.hyps [elim_format]) (simp_all add: wt_e1 True)
  2560 	 thus ?thesis
  2561 	   by blast
  2562        next
  2563 	 case False
  2564 	 have "normal s2" .
  2565 	 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
  2566 	   by (rule Cond.hyps [elim_format]) (simp_all add: wt_e2 False)
  2567 	 thus ?thesis
  2568 	   by blast
  2569        qed
  2570        with e0_s2
  2571        have "assignsE e0 \<union> 
  2572              (assigns_if (the_Bool v) e1 \<inter>  assigns_if (the_Bool v) e2)
  2573 	       \<subseteq> dom (locals (store s2))"
  2574 	 by (rule Un_least)
  2575        with None show ?thesis
  2576 	 by simp
  2577      next
  2578        case (Some c)
  2579        from this eval_e0 have eq_b_c: "b=c" 
  2580 	 by (rule constVal_eval_elim) 
  2581        show ?thesis
  2582        proof (cases "the_Bool c")
  2583 	 case True
  2584 	 have "normal s2" .
  2585 	 hence "assigns_if (the_Bool v) e1 \<subseteq> dom (locals (store s2))"    
  2586 	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c True)
  2587 	 with e0_s2
  2588 	 have "assignsE e0 \<union> assigns_if (the_Bool v) e1  \<subseteq> \<dots>"
  2589 	   by (rule Un_least)
  2590 	 with Some True show ?thesis
  2591 	   by simp
  2592        next
  2593 	 case False
  2594 	 have "normal s2" .
  2595 	 hence "assigns_if (the_Bool v) e2 \<subseteq> dom (locals (store s2))"    
  2596 	   by (rule Cond.hyps [elim_format]) (simp_all add: eq_b_c False)
  2597 	 with e0_s2
  2598 	 have "assignsE e0 \<union> assigns_if (the_Bool v) e2  \<subseteq> \<dots>"
  2599 	   by (rule Un_least)
  2600 	 with Some False show ?thesis
  2601 	   by simp
  2602        qed
  2603      qed
  2604    next
  2605      case (Call D a accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs)
  2606      hence
  2607      "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v\<rightarrow> 
  2608                        (set_lvars (locals (store s2)) s4)"
  2609        by - (rule eval.Call)
  2610      hence "assignsE ({accC,statT,mode}e\<cdot>mn( {pTs}args)) 
  2611               \<subseteq>  dom (locals (store ((set_lvars (locals (store s2))) s4)))"
  2612        by (rule assignsE_good_approx)
  2613      thus ?case by simp
  2614    next
  2615      case Methd show ?case by simp
  2616    next
  2617      case Body show ?case by simp
  2618    qed simp+ -- {* all the statements and variables *}
  2619  }
  2620  note generalized = this
  2621  from eval bool show ?thesis
  2622    by (rule generalized [elim_format]) simp+
  2623 qed
  2624 
  2625 lemma assigns_if_good_approx': 
  2626   assumes   eval: "G\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1"  
  2627      and  normal: "normal s1" 
  2628      and    bool: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>- (PrimT Boolean)"
  2629   shows "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  2630 proof -
  2631   from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
  2632   from this normal bool show ?thesis
  2633     by (rule assigns_if_good_approx)
  2634 qed
  2635 
  2636  
  2637 lemma subset_Intl: "A \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C" 
  2638   by blast
  2639 
  2640 lemma subset_Intr: "B \<subseteq> C \<Longrightarrow> A \<inter> B \<subseteq> C" 
  2641   by blast
  2642 
  2643 lemma da_good_approx: 
  2644   assumes  eval: "prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  2645            wt: "Env\<turnstile>t\<Colon>T"     (is "?Wt Env t T") and
  2646            da: "Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"  (is "?Da Env s0 t A") and 
  2647            wf: "wf_prog (prg Env)" 
  2648      shows "(normal s1 \<longrightarrow> (nrm A \<subseteq>  dom (locals (store s1)))) \<and>
  2649             (\<forall> l. abrupt s1 = Some (Jump (Break l)) \<and> normal s0 
  2650                        \<longrightarrow> (brk A l \<subseteq> dom (locals (store s1)))) \<and>
  2651             (abrupt s1 = Some (Jump Ret) \<and> normal s0 
  2652                        \<longrightarrow> Result \<in> dom (locals (store s1)))"
  2653      (is "?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1")
  2654 proof -
  2655   note inj_term_simps [simp]
  2656   obtain G where G: "prg Env = G" by (cases Env) simp
  2657   with eval have eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by simp
  2658   from G wf have wf: "wf_prog G" by simp
  2659   let ?HypObj = "\<lambda> t s0 s1.
  2660       \<forall> Env T A. ?Wt Env t T \<longrightarrow>  ?Da Env s0 t A \<longrightarrow> prg Env = G 
  2661        \<longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned  s0 s1"
  2662   -- {* Goal in object logic variant *} 
  2663   from eval
  2664   show "\<And> Env T A. \<lbrakk>?Wt Env t T; ?Da Env s0 t A; prg Env = G\<rbrakk> 
  2665         \<Longrightarrow> ?NormalAssigned s1 A \<and> ?BreakAssigned s0 s1 A \<and> ?ResAssigned s0 s1"
  2666         (is "PROP ?Hyp t s0 s1")
  2667   proof (induct)
  2668     case (Abrupt s t xc Env T A)
  2669     have da: "Env\<turnstile> dom (locals s) \<guillemotright>t\<guillemotright> A" using Abrupt.prems by simp 
  2670     have "?NormalAssigned (Some xc,s) A" 
  2671       by simp
  2672     moreover
  2673     have "?BreakAssigned (Some xc,s) (Some xc,s) A"
  2674       by simp
  2675     moreover have "?ResAssigned (Some xc,s) (Some xc,s)"
  2676       by simp
  2677     ultimately show ?case by (intro conjI)
  2678   next
  2679     case (Skip s Env T A)
  2680     have da: "Env\<turnstile> dom (locals (store (Norm s))) \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A" 
  2681       using Skip.prems by simp
  2682     hence "nrm A = dom (locals (store (Norm s)))"
  2683       by (rule da_elim_cases) simp
  2684     hence "?NormalAssigned (Norm s) A"
  2685       by auto
  2686     moreover
  2687     have "?BreakAssigned (Norm s) (Norm s) A" 
  2688       by simp
  2689     moreover have "?ResAssigned (Norm s) (Norm s)"
  2690       by simp
  2691     ultimately show ?case by (intro conjI)
  2692   next
  2693     case (Expr e s0 s1 v Env T A)
  2694     from Expr.prems
  2695     show "?NormalAssigned s1 A \<and> ?BreakAssigned (Norm s0) s1 A 
  2696            \<and> ?ResAssigned (Norm s0) s1"
  2697       by (elim wt_elim_cases da_elim_cases) 
  2698          (rule Expr.hyps, auto)
  2699   next 
  2700     case (Lab c j s0 s1 Env T A)
  2701     have G: "prg Env = G" .
  2702     from Lab.prems
  2703     obtain C l where
  2704       da_c: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
  2705          A: "nrm A = nrm C \<inter> (brk C) l" "brk A = rmlab l (brk C)" and
  2706          j: "j = Break l"
  2707       by - (erule da_elim_cases, simp)
  2708     from Lab.prems
  2709     have wt_c: "Env\<turnstile>c\<Colon>\<surd>"
  2710       by - (erule wt_elim_cases, simp)
  2711     from wt_c da_c G and Lab.hyps
  2712     have norm_c: "?NormalAssigned s1 C" and 
  2713           brk_c: "?BreakAssigned (Norm s0) s1 C" and
  2714           res_c: "?ResAssigned (Norm s0) s1"
  2715       by simp_all
  2716     have "?NormalAssigned (abupd (absorb j) s1) A"
  2717     proof
  2718       assume normal: "normal (abupd (absorb j) s1)"
  2719       show "nrm A \<subseteq> dom (locals (store (abupd (absorb j) s1)))"
  2720       proof (cases "abrupt s1")
  2721 	case None
  2722 	with norm_c A 
  2723 	show ?thesis
  2724 	  by auto
  2725       next
  2726 	case Some
  2727 	with normal j 
  2728 	have "abrupt s1 = Some (Jump (Break l))"
  2729 	  by (auto dest: absorb_Some_NoneD)
  2730 	with brk_c A
  2731   	show ?thesis
  2732 	  by auto
  2733       qed
  2734     qed
  2735     moreover 
  2736     have "?BreakAssigned (Norm s0) (abupd (absorb j) s1) A"
  2737     proof -
  2738       {
  2739 	fix l'
  2740 	assume break: "abrupt (abupd (absorb j) s1) = Some (Jump (Break l'))"
  2741 	with j 
  2742 	have "l\<noteq>l'"
  2743 	  by (cases s1) (auto dest!: absorb_Some_JumpD)
  2744 	hence "(rmlab l (brk C)) l'= (brk C) l'"
  2745 	  by (simp)
  2746 	with break brk_c A
  2747 	have 
  2748           "(brk A l' \<subseteq> dom (locals (store (abupd (absorb j) s1))))"
  2749 	  by (cases s1) auto
  2750       }
  2751       then show ?thesis
  2752 	by simp
  2753     qed
  2754     moreover
  2755     from res_c have "?ResAssigned (Norm s0) (abupd (absorb j) s1)"
  2756       by (cases s1) (simp add: absorb_def)
  2757     ultimately show ?case by (intro conjI)
  2758   next
  2759     case (Comp c1 c2 s0 s1 s2 Env T A)
  2760     have G: "prg Env = G" .
  2761     from Comp.prems
  2762     obtain C1 C2
  2763       where da_c1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and 
  2764             da_c2: "Env\<turnstile> nrm C1 \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  2765                 A: "nrm A = nrm C2" "brk A = (brk C1) \<Rightarrow>\<inter> (brk C2)"
  2766       by (elim da_elim_cases) simp
  2767     from Comp.prems
  2768     obtain wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  2769            wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
  2770       by (elim wt_elim_cases) simp
  2771     have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
  2772     with wt_c1 da_c1 G 
  2773     obtain nrm_c1: "?NormalAssigned s1 C1" and 
  2774            brk_c1: "?BreakAssigned (Norm s0) s1 C1" and
  2775            res_c1: "?ResAssigned (Norm s0) s1"
  2776       by simp
  2777     show ?case
  2778     proof (cases "normal s1")
  2779       case True
  2780       with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by rules
  2781       with da_c2 obtain C2' 
  2782 	where  da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  2783                nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
  2784                brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  2785         by (rule da_weakenE) rules
  2786       have "PROP ?Hyp (In1r c2) s1 s2" .
  2787       with wt_c2 da_c2' G
  2788       obtain nrm_c2': "?NormalAssigned s2 C2'" and 
  2789              brk_c2': "?BreakAssigned s1 s2 C2'" and
  2790              res_c2 : "?ResAssigned s1 s2" 
  2791 	by simp
  2792       from nrm_c2' nrm_c2 A
  2793       have "?NormalAssigned s2 A" 
  2794 	by blast
  2795       moreover from brk_c2' brk_c2 A
  2796       have "?BreakAssigned s1 s2 A" 
  2797 	by fastsimp
  2798       with True 
  2799       have "?BreakAssigned (Norm s0) s2 A" by simp
  2800       moreover from res_c2 True
  2801       have "?ResAssigned (Norm s0) s2"
  2802 	by simp
  2803       ultimately show ?thesis by (intro conjI)
  2804     next
  2805       case False
  2806       have "G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2" .
  2807       with False have eq_s1_s2: "s2=s1" by auto
  2808       with False have "?NormalAssigned s2 A" by blast
  2809       moreover
  2810       have "?BreakAssigned (Norm s0) s2 A"
  2811       proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")
  2812 	case True
  2813 	then obtain l where l: "abrupt s1 = Some (Jump (Break l))" .. 
  2814 	with brk_c1
  2815 	have "brk C1 l \<subseteq> dom (locals (store s1))"
  2816 	  by simp
  2817 	with A eq_s1_s2 
  2818 	have "brk A l \<subseteq> dom (locals (store s2))" 
  2819 	  by auto
  2820 	with l eq_s1_s2
  2821 	show ?thesis by simp
  2822       next
  2823 	case False
  2824 	with eq_s1_s2 show ?thesis by simp
  2825       qed
  2826       moreover from False res_c1 eq_s1_s2
  2827       have "?ResAssigned (Norm s0) s2"
  2828 	by simp
  2829       ultimately show ?thesis by (intro conjI)
  2830     qed
  2831   next
  2832 -- {* 
  2833 \par
  2834 *} (* dummy text command to break paragraph for latex;
  2835               large paragraphs exhaust memory of debian pdflatex *)
  2836     case (If b c1 c2 e s0 s1 s2 Env T A)
  2837     have G: "prg Env = G" .
  2838     with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
  2839     from If.prems
  2840     obtain E C1 C2 where
  2841       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  2842      da_c1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2843                    \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
  2844      da_c2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2845                    \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  2846      A: "nrm A = nrm C1 \<inter> nrm C2"  "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
  2847       by (elim da_elim_cases) 
  2848     from If.prems
  2849     obtain 
  2850        wt_e:  "Env\<turnstile>e\<Colon>- PrimT Boolean" and 
  2851        wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  2852        wt_c2: "Env\<turnstile>c2\<Colon>\<surd>" 
  2853       by (elim wt_elim_cases)
  2854     from wt_e da_e G
  2855     obtain nrm_s1: "?NormalAssigned s1 E" and 
  2856            brk_s1: "?BreakAssigned (Norm s0) s1 E" and
  2857            res_s1: "?ResAssigned (Norm s0) s1"
  2858       by (elim If.hyps [elim_format]) simp+
  2859     from If.hyps have
  2860      s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2861       by (elim dom_locals_eval_mono_elim)
  2862     show ?case
  2863     proof (cases "normal s1")
  2864       case True
  2865       note normal_s1 = this 
  2866       show ?thesis
  2867       proof (cases "the_Bool b")
  2868 	case True
  2869 	from eval_e normal_s1 wt_e
  2870 	have "assigns_if True e \<subseteq> dom (locals (store s1))"
  2871 	  by (rule assigns_if_good_approx [elim_format]) (simp add: True)
  2872 	with s0_s1
  2873 	have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"
  2874 	  by (rule Un_least)
  2875 	with da_c1 obtain C1'
  2876 	  where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
  2877 	        nrm_c1: "nrm C1 \<subseteq> nrm C1'"                  and
  2878                 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"
  2879           by (rule da_weakenE) rules
  2880 	from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp
  2881 	with wt_c1 da_c1'
  2882 	obtain nrm_c1': "?NormalAssigned s2 C1'" and 
  2883                brk_c1': "?BreakAssigned s1 s2 C1'" and
  2884                res_c1: "?ResAssigned s1 s2"
  2885 	  using G by simp
  2886 	from nrm_c1' nrm_c1 A
  2887 	have "?NormalAssigned s2 A" 
  2888 	  by blast
  2889 	moreover from brk_c1' brk_c1 A
  2890 	have "?BreakAssigned s1 s2 A" 
  2891 	  by fastsimp
  2892 	with normal_s1
  2893 	have "?BreakAssigned (Norm s0) s2 A" by simp
  2894 	moreover from res_c1 normal_s1 have "?ResAssigned (Norm s0) s2"
  2895 	  by simp
  2896 	ultimately show ?thesis by (intro conjI)
  2897       next
  2898 	case False
  2899 	from eval_e normal_s1 wt_e
  2900 	have "assigns_if False e \<subseteq> dom (locals (store s1))"
  2901 	  by (rule assigns_if_good_approx [elim_format]) (simp add: False)
  2902 	with s0_s1
  2903 	have "dom (locals (store ((Norm s0)::state)))\<union> assigns_if False e \<subseteq> \<dots>"
  2904 	  by (rule Un_least)
  2905 	with da_c2 obtain C2'
  2906 	  where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  2907 	        nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
  2908                 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  2909           by (rule da_weakenE) rules
  2910 	from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp
  2911 	with wt_c2 da_c2'
  2912 	obtain nrm_c2': "?NormalAssigned s2 C2'" and 
  2913                brk_c2': "?BreakAssigned s1 s2 C2'" and
  2914 	       res_c2: "?ResAssigned s1 s2"
  2915 	  using G by simp
  2916 	from nrm_c2' nrm_c2 A
  2917 	have "?NormalAssigned s2 A" 
  2918 	  by blast
  2919 	moreover from brk_c2' brk_c2 A
  2920 	have "?BreakAssigned s1 s2 A" 
  2921 	  by fastsimp
  2922 	with normal_s1
  2923 	have "?BreakAssigned (Norm s0) s2 A" by simp
  2924 	moreover from res_c2 normal_s1 have "?ResAssigned (Norm s0) s2"
  2925 	  by simp
  2926 	ultimately show ?thesis by (intro conjI)
  2927       qed
  2928     next
  2929       case False 
  2930       then obtain abr where abr: "abrupt s1 = Some abr"
  2931 	by (cases s1) auto
  2932       moreover
  2933       from eval_e _ wt_e have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"
  2934 	by (rule eval_expression_no_jump) (simp_all add: G wf)
  2935       moreover
  2936       have "s2 = s1"
  2937       proof -
  2938 	have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2" .
  2939         with abr show ?thesis  
  2940 	  by (cases s1) simp
  2941       qed
  2942       ultimately show ?thesis using res_s1 by simp
  2943     qed
  2944   next
  2945 -- {* 
  2946 \par
  2947 *} (* dummy text command to break paragraph for latex;
  2948               large paragraphs exhaust memory of debian pdflatex *)
  2949     case (Loop b c e l s0 s1 s2 s3 Env T A)
  2950     have G: "prg Env = G" .
  2951     with Loop.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" 
  2952       by (simp (no_asm_simp))
  2953     from Loop.prems
  2954     obtain E C where
  2955       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  2956       da_c: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2957                    \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C" and
  2958      A: "nrm A = nrm C \<inter> 
  2959               (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)"
  2960         "brk A = brk C"
  2961       by (elim da_elim_cases) 
  2962     from Loop.prems
  2963     obtain 
  2964        wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
  2965        wt_c: "Env\<turnstile>c\<Colon>\<surd>"
  2966       by (elim wt_elim_cases)
  2967     from wt_e da_e G
  2968     obtain res_s1: "?ResAssigned (Norm s0) s1"  
  2969       by (elim Loop.hyps [elim_format]) simp+
  2970     from Loop.hyps have
  2971       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2972       by (elim dom_locals_eval_mono_elim)
  2973     show ?case
  2974     proof (cases "normal s1")
  2975       case True
  2976       note normal_s1 = this
  2977       show ?thesis
  2978       proof (cases "the_Bool b")
  2979 	case True  
  2980 	with Loop.hyps obtain
  2981           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  2982           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  2983 	  by simp
  2984 	from Loop.hyps True 
  2985 	have "?HypObj (In1r c) s1 s2" by simp
  2986 	note hyp_c = this [rule_format]
  2987 	from Loop.hyps True
  2988 	have "?HypObj (In1r (l\<bullet> While(e) c)) (abupd (absorb (Cont l)) s2) s3"
  2989 	  by simp
  2990 	note hyp_while = this [rule_format]
  2991 	from eval_e normal_s1 wt_e
  2992 	have "assigns_if True e \<subseteq> dom (locals (store s1))"
  2993 	  by (rule assigns_if_good_approx [elim_format]) (simp add: True)
  2994 	with s0_s1
  2995 	have "dom (locals (store ((Norm s0)::state))) \<union> assigns_if True e \<subseteq> \<dots>"
  2996 	  by (rule Un_least)
  2997 	with da_c obtain C'
  2998 	  where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
  2999 	     nrm_C_C': "nrm C \<subseteq> nrm C'"                  and
  3000              brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"
  3001           by (rule da_weakenE) rules
  3002 	from hyp_c wt_c da_c'
  3003 	obtain nrm_C': "?NormalAssigned s2 C'" and 
  3004           brk_C': "?BreakAssigned s1 s2 C'" and
  3005           res_s2: "?ResAssigned s1 s2"
  3006 	  using G by simp
  3007 	show ?thesis
  3008 	proof (cases "normal s2 \<or> abrupt s2 = Some (Jump (Cont l))")
  3009 	  case True
  3010 	  from Loop.prems obtain
  3011 	    wt_while: "Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" and
  3012             da_while: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) 
  3013                            \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A"
  3014 	    by simp
  3015 	  have "dom (locals (store ((Norm s0)::state)))
  3016                   \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  3017 	  proof -
  3018 	    note s0_s1
  3019 	    also from eval_c 
  3020 	    have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  3021 	      by (rule dom_locals_eval_mono_elim)
  3022 	    also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  3023 	      by simp
  3024 	    finally show ?thesis .
  3025 	  qed
  3026 	  with da_while obtain A'
  3027 	    where 
  3028 	    da_while': "Env\<turnstile> dom (locals (store (abupd (absorb (Cont l)) s2))) 
  3029                        \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'" 
  3030 	    and  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3031             and  brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
  3032 	    by (rule da_weakenE) simp
  3033 	  with wt_while hyp_while
  3034 	  obtain nrm_A': "?NormalAssigned s3 A'" and
  3035                  brk_A': "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A'" and
  3036                  res_s3: "?ResAssigned (abupd (absorb (Cont l)) s2) s3"
  3037 	    using G by simp 
  3038 	  from nrm_A_A' nrm_A'
  3039 	  have "?NormalAssigned s3 A" 
  3040 	    by blast
  3041 	  moreover 
  3042 	  have "?BreakAssigned (Norm s0) s3 A" 
  3043 	  proof -
  3044 	    from brk_A_A' brk_A' 
  3045 	    have "?BreakAssigned (abupd (absorb (Cont l)) s2) s3 A" 
  3046 	      by fastsimp
  3047 	    moreover
  3048 	    from True have "normal (abupd (absorb (Cont l)) s2)"
  3049 	      by (cases s2) auto
  3050 	    ultimately show ?thesis
  3051 	      by simp
  3052 	  qed
  3053 	  moreover from res_s3 True have "?ResAssigned (Norm s0) s3"
  3054 	    by auto
  3055 	  ultimately show ?thesis by (intro conjI)
  3056 	next
  3057 	  case False
  3058 	  then obtain abr where 
  3059 	    "abrupt s2 = Some abr" and
  3060 	    "abrupt (abupd (absorb (Cont l)) s2) = Some abr"
  3061 	    by auto
  3062 	  with eval_while 
  3063 	  have eq_s3_s2: "s3=s2"
  3064 	    by auto
  3065 	  with nrm_C_C' nrm_C' A
  3066 	  have "?NormalAssigned s3 A"
  3067 	    by fastsimp
  3068 	  moreover
  3069 	  from eq_s3_s2 brk_C_C' brk_C' normal_s1 A
  3070 	  have "?BreakAssigned (Norm s0) s3 A"
  3071 	    by fastsimp
  3072 	  moreover 
  3073 	  from eq_s3_s2 res_s2 normal_s1 have "?ResAssigned (Norm s0) s3"
  3074 	    by simp
  3075 	  ultimately show ?thesis by (intro conjI)
  3076 	qed
  3077       next
  3078 	case False
  3079 	with Loop.hyps have eq_s3_s1: "s3=s1"
  3080 	  by simp
  3081 	from eq_s3_s1 res_s1 
  3082 	have res_s3: "?ResAssigned (Norm s0) s3"
  3083 	  by simp
  3084 	from eval_e True wt_e
  3085 	have "assigns_if False e \<subseteq> dom (locals (store s1))"
  3086 	  by (rule assigns_if_good_approx [elim_format]) (simp add: False)
  3087 	with s0_s1
  3088 	have "dom (locals (store ((Norm s0)::state)))\<union>assigns_if False e \<subseteq> \<dots>"
  3089 	  by (rule Un_least)
  3090 	hence "nrm C \<inter> 
  3091                (dom (locals (store ((Norm s0)::state))) \<union> assigns_if False e)
  3092                \<subseteq> dom (locals (store s1))"
  3093 	  by (rule subset_Intr)
  3094 	with normal_s1 A eq_s3_s1
  3095 	have "?NormalAssigned s3 A"
  3096 	  by simp
  3097 	moreover
  3098 	from normal_s1 eq_s3_s1
  3099 	have "?BreakAssigned (Norm s0) s3 A"
  3100 	  by simp
  3101 	moreover note res_s3
  3102 	ultimately show ?thesis by (intro conjI)
  3103       qed
  3104     next
  3105       case False
  3106       then obtain abr where abr: "abrupt s1 = Some abr"
  3107 	by (cases s1) auto
  3108       moreover
  3109       from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  3110 	by (rule eval_expression_no_jump) (simp_all add: wf G)
  3111       moreover
  3112       have eq_s3_s1: "s3=s1"
  3113       proof (cases "the_Bool b")
  3114 	case True  
  3115 	with Loop.hyps obtain
  3116           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  3117           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  3118 	  by simp
  3119 	from eval_c abr have "s2=s1" by auto
  3120 	moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  3121 	  by (cases s1) (simp add: absorb_def)
  3122 	ultimately show ?thesis
  3123 	  using eval_while abr
  3124 	  by auto
  3125       next
  3126 	case False
  3127 	with Loop.hyps show ?thesis by simp
  3128       qed
  3129       moreover
  3130       from eq_s3_s1 res_s1 
  3131       have res_s3: "?ResAssigned (Norm s0) s3"
  3132 	by simp
  3133       ultimately show ?thesis
  3134 	by simp 
  3135     qed
  3136   next 
  3137     case (Jmp j s Env T A)
  3138     have "?NormalAssigned (Some (Jump j),s) A" by simp
  3139     moreover
  3140     from Jmp.prems
  3141     obtain ret: "j = Ret \<longrightarrow> Result \<in> dom (locals (store (Norm s)))" and
  3142            brk: "brk A = (case j of
  3143                            Break l \<Rightarrow> \<lambda> k. if k=l 
  3144                                      then dom (locals (store ((Norm s)::state)))
  3145                                      else UNIV     
  3146                          | Cont l  \<Rightarrow> \<lambda> k. UNIV
  3147                          | Ret     \<Rightarrow> \<lambda> k. UNIV)"
  3148       by (elim da_elim_cases) simp
  3149     from brk have "?BreakAssigned (Norm s) (Some (Jump j),s) A"
  3150       by simp
  3151     moreover from ret have "?ResAssigned (Norm s) (Some (Jump j),s)"
  3152       by simp
  3153     ultimately show ?case by (intro conjI)
  3154   next
  3155     case (Throw a e s0 s1 Env T A)
  3156     have G: "prg Env = G" .
  3157     from Throw.prems obtain E where 
  3158       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E"
  3159       by (elim da_elim_cases)
  3160     from Throw.prems
  3161       obtain eT where wt_e: "Env\<turnstile>e\<Colon>-eT"
  3162 	by (elim wt_elim_cases)
  3163     have "?NormalAssigned (abupd (throw a) s1) A"
  3164       by (cases s1) (simp add: throw_def)
  3165     moreover
  3166     have "?BreakAssigned (Norm s0) (abupd (throw a) s1) A"
  3167     proof -
  3168       from G Throw.hyps have eval_e: "prg Env\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1" 
  3169 	by (simp (no_asm_simp))
  3170       from eval_e _ wt_e 
  3171       have "\<And> l. abrupt s1 \<noteq> Some (Jump (Break l))"
  3172 	by (rule eval_expression_no_jump) (simp_all add: wf G) 
  3173       hence "\<And> l. abrupt (abupd (throw a) s1) \<noteq> Some (Jump (Break l))"
  3174 	by (cases s1) (simp add: throw_def abrupt_if_def)
  3175       thus ?thesis
  3176 	by simp
  3177     qed
  3178     moreover
  3179     from wt_e da_e G have "?ResAssigned (Norm s0) s1"
  3180       by (elim Throw.hyps [elim_format]) simp+
  3181     hence "?ResAssigned (Norm s0) (abupd (throw a) s1)"
  3182       by (cases s1) (simp add: throw_def abrupt_if_def)
  3183     ultimately show ?case by (intro conjI)
  3184   next
  3185     case (Try C c1 c2 s0 s1 s2 s3 vn Env T A)
  3186     have G: "prg Env = G" .
  3187     from Try.prems obtain C1 C2 where
  3188       da_c1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1"  and
  3189       da_c2:
  3190        "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
  3191         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  3192       A: "nrm A = nrm C1 \<inter> nrm C2" "brk A = brk C1 \<Rightarrow>\<inter> brk C2"
  3193       by (elim da_elim_cases) simp
  3194     from Try.prems obtain 
  3195       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  3196       wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
  3197       by (elim wt_elim_cases)
  3198     have sxalloc: "prg Env\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" using Try.hyps G 
  3199       by (simp (no_asm_simp))
  3200     have "PROP ?Hyp (In1r c1) (Norm s0) s1" .
  3201     with wt_c1 da_c1 G
  3202     obtain nrm_C1: "?NormalAssigned s1 C1" and
  3203            brk_C1: "?BreakAssigned (Norm s0) s1 C1" and
  3204            res_s1: "?ResAssigned (Norm s0) s1"
  3205       by simp
  3206     show ?case
  3207     proof (cases "normal s1")
  3208       case True
  3209       with nrm_C1 have "nrm C1 \<inter> nrm C2 \<subseteq> dom (locals (store s1))"
  3210 	by auto
  3211       moreover
  3212       have "s3=s1"
  3213       proof -
  3214 	from sxalloc True have eq_s2_s1: "s2=s1"
  3215 	  by (cases s1) (auto elim: sxalloc_elim_cases)
  3216 	with True have "\<not>  G,s2\<turnstile>catch C"
  3217 	  by (simp add: catch_def)
  3218 	with Try.hyps have "s3=s2"
  3219 	  by simp
  3220 	with eq_s2_s1 show ?thesis by simp
  3221       qed
  3222       ultimately show ?thesis
  3223 	using True A res_s1 by simp
  3224     next
  3225       case False
  3226       note not_normal_s1 = this
  3227       show ?thesis
  3228       proof (cases "\<exists> l. abrupt s1 = Some (Jump (Break l))")
  3229 	case True
  3230 	then obtain l where l: "abrupt s1 = Some (Jump (Break l))"
  3231 	  by auto
  3232 	with brk_C1 have "(brk C1 \<Rightarrow>\<inter> brk C2) l \<subseteq> dom (locals (store s1))"
  3233 	  by auto
  3234 	moreover have "s3=s1"
  3235 	proof -
  3236 	  from sxalloc l have eq_s2_s1: "s2=s1"
  3237 	    by (cases s1) (auto elim: sxalloc_elim_cases)
  3238 	  with l have "\<not>  G,s2\<turnstile>catch C"
  3239 	    by (simp add: catch_def)
  3240 	  with Try.hyps have "s3=s2"
  3241 	    by simp
  3242 	  with eq_s2_s1 show ?thesis by simp
  3243 	qed
  3244 	ultimately show ?thesis
  3245 	  using l A res_s1 by simp
  3246       next
  3247 	case False
  3248 	note abrupt_no_break = this
  3249 	show ?thesis
  3250 	proof (cases "G,s2\<turnstile>catch C")
  3251 	  case True
  3252 	  with Try.hyps have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3"
  3253             by simp
  3254           note hyp_c2 = this [rule_format]
  3255           have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  3256                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  3257           proof -
  3258             have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  3259             hence "dom (locals (store ((Norm s0)::state))) 
  3260                     \<subseteq> dom (locals (store s1))"
  3261               by (rule dom_locals_eval_mono_elim)
  3262             also
  3263             from sxalloc
  3264             have "\<dots> \<subseteq> dom (locals (store s2))"
  3265               by (rule dom_locals_sxalloc_mono)
  3266             also 
  3267             have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  3268               by (cases s2) (simp add: new_xcpt_var_def, blast) 
  3269             also
  3270             have "{VName vn} \<subseteq> \<dots>"
  3271               by (cases s2) simp
  3272             ultimately show ?thesis
  3273               by (rule Un_least)
  3274           qed
  3275           with da_c2 
  3276           obtain C2' where
  3277             da_C2': "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>
  3278                      \<turnstile> dom (locals (store (new_xcpt_var vn s2))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
  3279            and nrm_C2': "nrm C2 \<subseteq> nrm C2'" 
  3280            and brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  3281             by (rule da_weakenE) simp
  3282           from wt_c2 da_C2' G and hyp_c2
  3283           obtain nrmAss_C2: "?NormalAssigned s3 C2'" and
  3284                  brkAss_C2: "?BreakAssigned (new_xcpt_var vn s2) s3 C2'" and
  3285                  resAss_s3: "?ResAssigned (new_xcpt_var vn s2) s3"
  3286             by simp
  3287           from nrmAss_C2 nrm_C2' A 
  3288           have "?NormalAssigned s3 A"
  3289             by auto
  3290           moreover
  3291           have "?BreakAssigned (Norm s0) s3 A"
  3292           proof -
  3293             from brkAss_C2 have "?BreakAssigned (Norm s0) s3 C2'"
  3294               by (cases s2) (auto simp add: new_xcpt_var_def)
  3295             with brk_C2' A show ?thesis 
  3296               by fastsimp
  3297           qed
  3298 	  moreover
  3299 	  from resAss_s3 have "?ResAssigned (Norm s0) s3"
  3300 	    by (cases s2) ( simp add: new_xcpt_var_def)
  3301           ultimately show ?thesis by (intro conjI)
  3302         next
  3303           case False
  3304           with Try.hyps 
  3305           have eq_s3_s2: "s3=s2" by simp
  3306           moreover from sxalloc not_normal_s1 abrupt_no_break
  3307           obtain "\<not> normal s2" 
  3308                  "\<forall> l. abrupt s2 \<noteq> Some (Jump (Break l))"
  3309             by - (rule sxalloc_cases,auto)
  3310 	  ultimately obtain 
  3311 	    "?NormalAssigned s3 A" and "?BreakAssigned (Norm s0) s3 A"
  3312 	    by (cases s2) auto
  3313 	  moreover have "?ResAssigned (Norm s0) s3"
  3314 	  proof (cases "abrupt s1 = Some (Jump Ret)")
  3315 	    case True
  3316 	    with sxalloc have "s2=s1"
  3317 	      by (elim sxalloc_cases) auto
  3318 	    with res_s1 eq_s3_s2 show ?thesis by simp
  3319 	  next
  3320 	    case False
  3321 	    with sxalloc
  3322 	    have "abrupt s2 \<noteq> Some (Jump Ret)"
  3323 	      by (rule sxalloc_no_jump) 
  3324 	    with eq_s3_s2 show ?thesis
  3325 	      by simp
  3326 	  qed
  3327           ultimately show ?thesis by (intro conjI)
  3328         qed
  3329       qed
  3330     qed
  3331   next
  3332 -- {* 
  3333 \par
  3334 *} (* dummy text command to break paragraph for latex;
  3335               large paragraphs exhaust memory of debian pdflatex *)
  3336     case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A)
  3337     have G: "prg Env = G" .
  3338     from Fin.prems obtain C1 C2 where 
  3339       da_C1: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1" and
  3340       da_C2: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2" and
  3341       nrm_A: "nrm A = nrm C1 \<union> nrm C2" and
  3342       brk_A: "brk A = ((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) \<Rightarrow>\<inter> (brk C2)"
  3343       by (elim da_elim_cases) simp
  3344     from Fin.prems obtain 
  3345       wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and
  3346       wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
  3347       by (elim wt_elim_cases)
  3348     have "PROP ?Hyp (In1r c1) (Norm s0) (x1,s1)" .
  3349     with wt_c1 da_C1 G
  3350     obtain nrmAss_C1: "?NormalAssigned (x1,s1) C1" and
  3351            brkAss_C1: "?BreakAssigned (Norm s0) (x1,s1) C1" and
  3352            resAss_s1: "?ResAssigned (Norm s0) (x1,s1)"
  3353       by simp
  3354     obtain nrmAss_C2: "?NormalAssigned s2 C2" and
  3355            brkAss_C2: "?BreakAssigned (Norm s1) s2 C2" and
  3356            resAss_s2: "?ResAssigned (Norm s1) s2"
  3357     proof -
  3358       from Fin.hyps
  3359       have "dom (locals (store ((Norm s0)::state))) 
  3360              \<subseteq> dom (locals (store (x1,s1)))"
  3361         by - (rule dom_locals_eval_mono_elim) 
  3362       with da_C2 obtain C2'
  3363         where
  3364         da_C2': "Env\<turnstile> dom (locals (store (x1,s1))) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
  3365         nrm_C2': "nrm C2 \<subseteq> nrm C2'" and
  3366         brk_C2': "\<forall> l. brk C2 l \<subseteq> brk C2' l"
  3367         by (rule da_weakenE) simp
  3368       have "PROP ?Hyp (In1r c2) (Norm s1) s2" .
  3369       with wt_c2 da_C2' G
  3370       obtain nrmAss_C2': "?NormalAssigned s2 C2'" and
  3371              brkAss_C2': "?BreakAssigned (Norm s1) s2 C2'" and
  3372 	     resAss_s2': "?ResAssigned (Norm s1) s2"
  3373         by simp
  3374       from nrmAss_C2' nrm_C2' have "?NormalAssigned s2 C2"
  3375         by blast
  3376       moreover
  3377       from brkAss_C2' brk_C2' have "?BreakAssigned (Norm s1) s2 C2"
  3378         by fastsimp
  3379       ultimately
  3380       show ?thesis
  3381         using that resAss_s2' by simp
  3382     qed
  3383     have s3: "s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
  3384                        else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  3385     have s1_s2: "dom (locals s1) \<subseteq> dom (locals (store s2))"
  3386     proof -  
  3387       have "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
  3388       thus ?thesis
  3389         by (rule dom_locals_eval_mono_elim) simp
  3390     qed
  3391 
  3392     have "?NormalAssigned s3 A"
  3393     proof 
  3394       assume normal_s3: "normal s3"
  3395       show "nrm A \<subseteq> dom (locals (snd s3))"
  3396       proof -
  3397         have "nrm C1 \<subseteq> dom (locals (snd s3))"
  3398         proof -
  3399           from normal_s3 s3
  3400           have "normal (x1,s1)"
  3401             by (cases s2) (simp add: abrupt_if_def)
  3402           with normal_s3 nrmAss_C1 s3 s1_s2
  3403           show ?thesis
  3404             by fastsimp
  3405         qed
  3406         moreover 
  3407         have "nrm C2 \<subseteq> dom (locals (snd s3))"
  3408         proof -
  3409           from normal_s3 s3
  3410           have "normal s2"
  3411             by (cases s2) (simp add: abrupt_if_def)
  3412           with normal_s3 nrmAss_C2 s3 s1_s2
  3413           show ?thesis
  3414             by fastsimp
  3415         qed
  3416         ultimately have "nrm C1 \<union> nrm C2 \<subseteq> \<dots>"
  3417           by (rule Un_least)
  3418         with nrm_A show ?thesis
  3419           by simp
  3420       qed
  3421     qed
  3422     moreover
  3423     {
  3424       fix l assume brk_s3: "abrupt s3 = Some (Jump (Break l))"
  3425       have "brk A l \<subseteq> dom (locals (store s3))"
  3426       proof (cases "normal s2")
  3427         case True
  3428         with brk_s3 s3 
  3429         have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  3430           by simp
  3431         have "brk C1 l \<subseteq> dom (locals (store s3))"
  3432         proof -
  3433           from True brk_s3 s3 have "x1=Some (Jump (Break l))"
  3434             by (cases s2) (simp add: abrupt_if_def)
  3435           with brkAss_C1 s1_s2 s2_s3
  3436           show ?thesis
  3437             by simp (blast intro: subset_trans)
  3438         qed
  3439         moreover from True nrmAss_C2 s2_s3
  3440         have "nrm C2 \<subseteq> dom (locals (store s3))"
  3441           by - (rule subset_trans, simp_all)
  3442         ultimately 
  3443         have "((brk C1) \<Rightarrow>\<union>\<^sub>\<forall> (nrm C2)) l \<subseteq> \<dots>"
  3444           by blast
  3445         with brk_A show ?thesis
  3446           by simp blast
  3447       next
  3448         case False
  3449         note not_normal_s2 = this
  3450         have "s3=s2"
  3451         proof (cases "normal (x1,s1)")
  3452           case True with not_normal_s2 s3 show ?thesis
  3453             by (cases s2) (simp add: abrupt_if_def)
  3454         next
  3455           case False with not_normal_s2 s3 brk_s3 show ?thesis
  3456             by (cases s2) (simp add: abrupt_if_def)
  3457         qed
  3458         with brkAss_C2 brk_s3
  3459         have "brk C2 l \<subseteq> dom (locals (store s3))"
  3460           by simp
  3461         with brk_A show ?thesis
  3462           by simp blast
  3463       qed
  3464     }
  3465     hence "?BreakAssigned (Norm s0) s3 A"
  3466       by simp
  3467     moreover
  3468     {
  3469       assume abr_s3: "abrupt s3 = Some (Jump Ret)"
  3470       have "Result \<in> dom (locals (store s3))"
  3471       proof (cases "x1 = Some (Jump Ret)")
  3472 	case True
  3473 	note ret_x1 = this
  3474 	with resAss_s1 have res_s1: "Result \<in> dom (locals s1)"
  3475 	  by simp
  3476 	moreover have "dom (locals (store ((Norm s1)::state))) 
  3477                          \<subseteq> dom (locals (store s2))"
  3478 	  by (rule dom_locals_eval_mono_elim)
  3479 	ultimately have "Result \<in> dom (locals (store s2))"
  3480 	  by - (rule subsetD,auto)
  3481 	with res_s1 s3 show ?thesis
  3482 	  by simp
  3483       next
  3484 	case False
  3485 	with s3 abr_s3 obtain  "abrupt s2 = Some (Jump Ret)" and "s3=s2"
  3486 	  by (cases s2) (simp add: abrupt_if_def)
  3487 	with resAss_s2 show ?thesis
  3488 	  by simp
  3489       qed
  3490     }
  3491     hence "?ResAssigned (Norm s0) s3"
  3492       by simp
  3493     ultimately show ?case by (intro conjI)
  3494   next 
  3495     case (Init C c s0 s1 s2 s3 Env T A)
  3496     have G: "prg Env = G" .
  3497     from Init.hyps
  3498     have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Init C\<rightarrow> s3"
  3499       apply (simp only: G) 
  3500       apply (rule eval.Init, assumption)
  3501       apply (cases "inited C (globs s0) ")
  3502       apply   simp
  3503       apply (simp only: if_False )
  3504       apply (elim conjE,intro conjI,assumption+,simp)
  3505       done (* auto or simp alone always do too much *)
  3506     have "the (class G C) = c" .
  3507     with Init.prems 
  3508     have c: "class G C = Some c"
  3509       by (elim wt_elim_cases) auto
  3510     from Init.prems obtain
  3511        nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  3512       by (elim da_elim_cases) simp
  3513     show ?case
  3514     proof (cases "inited C (globs s0)")
  3515       case True
  3516       with Init.hyps have "s3=Norm s0" by simp
  3517       thus ?thesis
  3518 	using nrm_A by simp
  3519     next
  3520       case False
  3521       from Init.hyps False G
  3522       obtain eval_initC: 
  3523               "prg Env\<turnstile>Norm ((init_class_obj G C) s0) 
  3524                        \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  3525              eval_init: "prg Env\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  3526              s3: "s3=(set_lvars (locals (store s1))) s2"
  3527 	by simp
  3528       have "?NormalAssigned s3 A"
  3529       proof
  3530 	show "nrm A \<subseteq> dom (locals (store s3))"
  3531 	proof -
  3532 	  from nrm_A have "nrm A \<subseteq> dom (locals (init_class_obj G C s0))"
  3533 	    by simp
  3534 	  also from eval_initC have "\<dots> \<subseteq> dom (locals (store s1))"
  3535 	    by (rule dom_locals_eval_mono_elim) simp
  3536 	  also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"
  3537 	    by (cases s1) (cases s2, simp add: init_lvars_def2)
  3538 	  finally show ?thesis .
  3539 	qed
  3540       qed
  3541       moreover
  3542       from eval 
  3543       have "\<And> j. abrupt s3 \<noteq> Some (Jump j)"
  3544 	by (rule eval_statement_no_jump) (auto simp add: wf c G)
  3545       then obtain "?BreakAssigned (Norm s0) s3 A" 
  3546               and "?ResAssigned (Norm s0) s3"
  3547 	by simp
  3548       ultimately show ?thesis by (intro conjI)
  3549     qed
  3550   next 
  3551     case (NewC C a s0 s1 s2 Env T A)
  3552     have G: "prg Env = G" .
  3553     from NewC.prems
  3554     obtain A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  3555               "brk A = (\<lambda> l. UNIV)"
  3556       by (elim da_elim_cases) simp
  3557     from wf NewC.prems 
  3558     have wt_init: "Env\<turnstile>(Init C)\<Colon>\<surd>"
  3559       by  (elim wt_elim_cases) (drule is_acc_classD,simp)
  3560     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s2))"
  3561     proof -
  3562       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  3563         by (rule dom_locals_eval_mono_elim)
  3564       also
  3565       have "\<dots> \<subseteq> dom (locals (store s2))"
  3566         by (rule dom_locals_halloc_mono)
  3567       finally show ?thesis .
  3568     qed
  3569     with A have "?NormalAssigned s2 A"
  3570       by simp
  3571     moreover
  3572     {
  3573       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3574       proof -
  3575         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
  3576 	  by (simp only: G) (rule eval.NewC)
  3577         from NewC.prems 
  3578         obtain T' where  "T=Inl T'"
  3579           by (elim wt_elim_cases) simp
  3580         with NewC.prems have "Env\<turnstile>NewC C\<Colon>-T'" 
  3581           by simp
  3582         from eval _ this
  3583         show ?thesis
  3584           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3585       qed
  3586     }
  3587     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3588       by simp_all      
  3589     ultimately show ?case by (intro conjI)
  3590   next
  3591 -- {* 
  3592 \par
  3593 *} (* dummy text command to break paragraph for latex;
  3594               large paragraphs exhaust memory of debian pdflatex *)
  3595     case (NewA elT a e i s0 s1 s2 s3 Env T A) 
  3596     have G: "prg Env = G" .
  3597     from NewA.prems obtain
  3598       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3599       by (elim da_elim_cases)
  3600     from NewA.prems obtain 
  3601       wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
  3602       wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
  3603       by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
  3604     have halloc:"G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow>s3".
  3605     have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  3606       by (rule dom_locals_eval_mono_elim)
  3607     with da_e obtain A' where
  3608                 da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" 
  3609         and  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3610         and  brk_A_A': "\<forall> l. brk A l \<subseteq> brk A' l"
  3611       by (rule da_weakenE) simp
  3612     have "PROP ?Hyp (In1l e) s1 s2" .
  3613     with wt_size da_e' G obtain 
  3614       nrmAss_A': "?NormalAssigned s2 A'" and
  3615       brkAss_A': "?BreakAssigned s1 s2 A'"
  3616       by simp
  3617     have s2_s3: "dom (locals (store s2)) \<subseteq> dom (locals (store s3))"
  3618     proof -
  3619       have "dom (locals (store s2)) 
  3620              \<subseteq> dom (locals (store (abupd (check_neg i) s2)))"
  3621         by (simp)
  3622       also have "\<dots> \<subseteq> dom (locals (store s3))"
  3623         by (rule dom_locals_halloc_mono)
  3624       finally show ?thesis .
  3625     qed 
  3626     have "?NormalAssigned s3 A"
  3627     proof 
  3628       assume normal_s3: "normal s3"
  3629       show "nrm A \<subseteq> dom (locals (store s3))"
  3630       proof -
  3631         from halloc normal_s3 
  3632         have "normal (abupd (check_neg i) s2)"
  3633           by cases simp_all
  3634         hence "normal s2"
  3635           by (cases s2) simp
  3636         with nrmAss_A' nrm_A_A' s2_s3 show ?thesis
  3637           by blast
  3638       qed
  3639     qed
  3640     moreover
  3641     {
  3642       fix j have "abrupt s3 \<noteq> Some (Jump j)"
  3643       proof -
  3644         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>New elT[e]-\<succ>Addr a\<rightarrow> s3"
  3645 	  by (simp only: G) (rule eval.NewA)
  3646         from NewA.prems 
  3647         obtain T' where  "T=Inl T'"
  3648           by (elim wt_elim_cases) simp
  3649         with NewA.prems have "Env\<turnstile>New elT[e]\<Colon>-T'" 
  3650           by simp
  3651         from eval _ this
  3652         show ?thesis
  3653           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3654       qed
  3655     }
  3656     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
  3657       by simp_all
  3658     ultimately show ?case by (intro conjI)
  3659   next
  3660     case (Cast cT e s0 s1 s2 v Env T A)
  3661     have G: "prg Env = G" .
  3662     from Cast.prems obtain
  3663       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3664       by (elim da_elim_cases)
  3665     from Cast.prems obtain eT where
  3666       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3667       by (elim wt_elim_cases) 
  3668     have "PROP ?Hyp (In1l e) (Norm s0) s1" .
  3669     with wt_e da_e G obtain 
  3670       nrmAss_A: "?NormalAssigned s1 A" and
  3671       brkAss_A: "?BreakAssigned (Norm s0) s1 A"
  3672       by simp
  3673     have s2: "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1" .
  3674     hence s1_s2: "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  3675       by simp
  3676     have "?NormalAssigned s2 A"
  3677     proof 
  3678       assume "normal s2"
  3679       with s2 have "normal s1"
  3680         by (cases s1) simp
  3681       with nrmAss_A s1_s2 
  3682       show "nrm A \<subseteq> dom (locals (store s2))"
  3683         by blast
  3684     qed
  3685     moreover
  3686     {
  3687       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3688       proof -
  3689         have eval: "prg Env\<turnstile> Norm s0 \<midarrow>Cast cT e-\<succ>v\<rightarrow> s2"
  3690 	  by (simp only: G) (rule eval.Cast)
  3691         from Cast.prems 
  3692         obtain T' where  "T=Inl T'"
  3693           by (elim wt_elim_cases) simp
  3694         with Cast.prems have "Env\<turnstile>Cast cT e\<Colon>-T'" 
  3695           by simp
  3696         from eval _ this
  3697         show ?thesis
  3698           by (rule eval_expression_no_jump) (simp_all add: G wf)
  3699       qed
  3700     }
  3701     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3702       by simp_all
  3703     ultimately show ?case by (intro conjI)
  3704   next
  3705     case (Inst iT b e s0 s1 v Env T A)
  3706     have G: "prg Env = G" .
  3707     from Inst.prems obtain
  3708       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3709       by (elim da_elim_cases)
  3710     from Inst.prems obtain eT where
  3711       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3712       by (elim wt_elim_cases) 
  3713     have "PROP ?Hyp (In1l e) (Norm s0) s1" .
  3714     with wt_e da_e G obtain 
  3715       "?NormalAssigned s1 A" and
  3716       "?BreakAssigned (Norm s0) s1 A" and
  3717       "?ResAssigned (Norm s0) s1"
  3718       by simp
  3719     thus ?case by (intro conjI)
  3720   next
  3721     case (Lit s v Env T A)
  3722     from Lit.prems
  3723     have "nrm A = dom (locals (store ((Norm s)::state)))"
  3724       by (elim da_elim_cases) simp
  3725     thus ?case by simp
  3726   next
  3727     case (UnOp e s0 s1 unop v Env T A)
  3728      have G: "prg Env = G" .
  3729     from UnOp.prems obtain
  3730       da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  3731       by (elim da_elim_cases)
  3732     from UnOp.prems obtain eT where
  3733       wt_e: "Env\<turnstile>e\<Colon>-eT"
  3734       by (elim wt_elim_cases) 
  3735     have "PROP ?Hyp (In1l e) (Norm s0) s1" .
  3736     with wt_e da_e G obtain 
  3737       "?NormalAssigned s1 A" and
  3738       "?BreakAssigned (Norm s0) s1 A" and
  3739       "?ResAssigned (Norm s0) s1"
  3740       by simp
  3741     thus ?case by (intro conjI)
  3742   next
  3743     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 Env T A)
  3744     have G: "prg Env = G". 
  3745     from BinOp.hyps 
  3746     have 
  3747      eval: "prg Env\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
  3748       by (simp only: G) (rule eval.BinOp)
  3749     have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  3750                   \<subseteq> dom (locals (store s1))"
  3751       by (rule dom_locals_eval_mono_elim)
  3752     also have s1_s2: "dom (locals (store s1)) \<subseteq>  dom (locals (store s2))"
  3753       by (rule dom_locals_eval_mono_elim)
  3754     finally 
  3755     have s0_s2: "dom (locals (store ((Norm s0)::state))) 
  3756                   \<subseteq> dom (locals (store s2))" . 
  3757     from BinOp.prems obtain e1T e2T
  3758       where wt_e1: "Env\<turnstile>e1\<Colon>-e1T" 
  3759        and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
  3760        and  wt_binop: "wt_binop (prg Env) binop e1T e2T"
  3761        and  T: "T=Inl (PrimT (binop_type binop))"
  3762       by (elim wt_elim_cases) simp
  3763     have "?NormalAssigned s2 A"
  3764     proof 
  3765       assume normal_s2: "normal s2"
  3766       have   normal_s1: "normal s1"
  3767         by (rule eval_no_abrupt_lemma [rule_format])
  3768       show "nrm A \<subseteq> dom (locals (store s2))"
  3769       proof (cases "binop=CondAnd")
  3770         case True
  3771         note CondAnd = this
  3772         from BinOp.prems obtain
  3773            nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  3774                             \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3775                                  assigns_if False (BinOp CondAnd e1 e2))"
  3776           by (elim da_elim_cases) (simp_all add: CondAnd)
  3777         from T BinOp.prems CondAnd
  3778         have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"
  3779           by (simp)
  3780         with eval normal_s2
  3781         have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) 
  3782                                  (BinOp binop e1 e2)
  3783                         \<subseteq> dom (locals (store s2))"
  3784           by (rule assigns_if_good_approx) 
  3785         have "(assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3786                          assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"
  3787         proof (cases "the_Bool (eval_binop binop v1 v2)")
  3788           case True
  3789           with ass_if CondAnd  
  3790           have "assigns_if True (BinOp CondAnd e1 e2) 
  3791                  \<subseteq> dom (locals (store s2))"
  3792 	    by simp
  3793           thus ?thesis by blast
  3794         next
  3795           case False
  3796           with ass_if CondAnd
  3797           have "assigns_if False (BinOp CondAnd e1 e2) 
  3798                  \<subseteq> dom (locals (store s2))"
  3799             by (simp only: False)
  3800           thus ?thesis by blast
  3801         qed
  3802         with s0_s2
  3803         have "dom (locals (store ((Norm s0)::state))) 
  3804                 \<union> (assigns_if True (BinOp CondAnd e1 e2) \<inter> 
  3805                    assigns_if False (BinOp CondAnd e1 e2)) \<subseteq> \<dots>"
  3806           by (rule Un_least)
  3807         thus ?thesis by (simp only: nrm_A)
  3808       next
  3809         case False
  3810         note notCondAnd = this
  3811         show ?thesis
  3812         proof (cases "binop=CondOr")
  3813           case True
  3814           note CondOr = this
  3815           from BinOp.prems obtain
  3816             nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  3817                              \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3818                                  assigns_if False (BinOp CondOr e1 e2))"
  3819             by (elim da_elim_cases) (simp_all add: CondOr)
  3820           from T BinOp.prems CondOr
  3821           have "Env\<turnstile>BinOp binop e1 e2\<Colon>-PrimT Boolean"
  3822             by (simp)
  3823           with eval normal_s2
  3824           have ass_if: "assigns_if (the_Bool (eval_binop binop v1 v2)) 
  3825                                  (BinOp binop e1 e2)
  3826                           \<subseteq> dom (locals (store s2))"
  3827             by (rule assigns_if_good_approx) 
  3828           have "(assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3829                          assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"
  3830           proof (cases "the_Bool (eval_binop binop v1 v2)")
  3831             case True
  3832             with ass_if CondOr 
  3833             have "assigns_if True (BinOp CondOr e1 e2) 
  3834                     \<subseteq> dom (locals (store s2))"
  3835               by (simp)
  3836             thus ?thesis by blast
  3837           next
  3838             case False
  3839             with ass_if CondOr
  3840             have "assigns_if False (BinOp CondOr e1 e2) 
  3841                     \<subseteq> dom (locals (store s2))"
  3842               by (simp)
  3843             thus ?thesis by blast
  3844           qed
  3845           with s0_s2
  3846           have "dom (locals (store ((Norm s0)::state))) 
  3847                  \<union> (assigns_if True (BinOp CondOr e1 e2) \<inter> 
  3848                     assigns_if False (BinOp CondOr e1 e2)) \<subseteq> \<dots>"
  3849             by (rule Un_least)
  3850           thus ?thesis by (simp only: nrm_A)
  3851         next
  3852           case False
  3853           with notCondAnd obtain notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
  3854             by simp
  3855           from BinOp.prems obtain E1
  3856             where da_e1: "Env\<turnstile> dom (locals (snd (Norm s0))) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1"  
  3857              and  da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A"
  3858             by (elim da_elim_cases) (simp_all add: notAndOr)
  3859           have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
  3860           with wt_e1 da_e1 G normal_s1
  3861           obtain "?NormalAssigned s1 E1"  
  3862             by simp
  3863           with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by rules
  3864           with da_e2 obtain A' 
  3865             where  da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
  3866                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  3867             by (rule da_weakenE) rules
  3868           from notAndOr have "need_second_arg binop v1" by simp
  3869           with BinOp.hyps 
  3870           have "PROP ?Hyp (In1l e2) s1 s2" by simp
  3871           with wt_e2 da_e2' G
  3872           obtain "?NormalAssigned s2 A'"  
  3873             by simp
  3874           with nrm_A_A' normal_s2
  3875           show "nrm A \<subseteq> dom (locals (store s2))" 
  3876             by blast
  3877         qed
  3878       qed
  3879     qed
  3880     moreover
  3881     {
  3882       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  3883       proof -
  3884         from BinOp.prems T 
  3885         have "Env\<turnstile>In1l (BinOp binop e1 e2)\<Colon>Inl (PrimT (binop_type binop))"
  3886           by simp
  3887         from eval _ this
  3888         show ?thesis
  3889           by (rule eval_expression_no_jump) (simp_all add: G wf) 
  3890       qed
  3891     }
  3892     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  3893       by simp_all
  3894     ultimately show ?case by (intro conjI) 
  3895   next
  3896 -- {* 
  3897 \par
  3898 *} (* dummy text command to break paragraph for latex;
  3899               large paragraphs exhaust memory of debian pdflatex *)
  3900     case (Super s Env T A)
  3901     from Super.prems
  3902     have "nrm A = dom (locals (store ((Norm s)::state)))"
  3903       by (elim da_elim_cases) simp
  3904     thus ?case by simp
  3905   next
  3906     case (Acc upd s0 s1 w v Env T A)
  3907     show ?case
  3908     proof (cases "\<exists> vn. v = LVar vn")
  3909       case True
  3910       then obtain vn where vn: "v=LVar vn"..
  3911       from Acc.prems
  3912       have "nrm A = dom (locals (store ((Norm s0)::state)))"
  3913         by (simp only: vn) (elim da_elim_cases,simp_all)
  3914       moreover have "G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1" .
  3915       hence "s1=Norm s0"
  3916         by (simp only: vn) (elim eval_elim_cases,simp)
  3917       ultimately show ?thesis by simp
  3918     next
  3919       case False
  3920       have G: "prg Env = G" .
  3921       from False Acc.prems
  3922       have da_v: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>v\<rangle>\<guillemotright> A"
  3923         by (elim da_elim_cases) simp_all 
  3924       from Acc.prems obtain vT where
  3925         wt_v: "Env\<turnstile>v\<Colon>=vT"
  3926         by (elim wt_elim_cases) 
  3927       have "PROP ?Hyp (In2 v) (Norm s0) s1" .
  3928       with wt_v da_v G obtain 
  3929         "?NormalAssigned s1 A" and
  3930         "?BreakAssigned (Norm s0) s1 A" and
  3931 	"?ResAssigned (Norm s0) s1"
  3932         by simp
  3933       thus ?thesis by (intro conjI)
  3934     qed
  3935   next
  3936     case (Ass e upd s0 s1 s2 v var w Env T A)
  3937     have G: "prg Env = G" .
  3938     from Ass.prems obtain varT eT where
  3939       wt_var: "Env\<turnstile>var\<Colon>=varT" and
  3940       wt_e:   "Env\<turnstile>e\<Colon>-eT"
  3941       by (elim wt_elim_cases) simp
  3942     have eval_var: "prg Env\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1" 
  3943       using Ass.hyps by (simp only: G)
  3944     have "?NormalAssigned (assign upd v s2) A"
  3945     proof 
  3946       assume normal_ass_s2: "normal (assign upd v s2)"
  3947       from normal_ass_s2 
  3948       have normal_s2: "normal s2"
  3949         by (cases s2) (simp add: assign_def Let_def)
  3950       hence normal_s1: "normal s1"
  3951         by - (rule eval_no_abrupt_lemma [rule_format])
  3952       have hyp_var: "PROP ?Hyp (In2 var) (Norm s0) s1" .
  3953       have hyp_e: "PROP ?Hyp (In1l e) s1 s2" .
  3954       show "nrm A \<subseteq> dom (locals (store (assign upd v s2)))"
  3955       proof (cases "\<exists> vn. var = LVar vn")
  3956 	case True
  3957 	then obtain vn where vn: "var=LVar vn"..
  3958 	from Ass.prems obtain E where
  3959 	  da_e: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  3960 	  nrm_A: "nrm A = nrm E \<union> {vn}"
  3961 	  by (elim da_elim_cases) (insert vn,auto)
  3962 	obtain E' where
  3963 	  da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'" and
  3964 	  E_E': "nrm E \<subseteq> nrm E'"
  3965 	proof -
  3966 	  have "dom (locals (store ((Norm s0)::state))) 
  3967                   \<subseteq> dom (locals (store s1))"
  3968 	    by (rule dom_locals_eval_mono_elim)
  3969 	  with da_e show ?thesis
  3970 	    by (rule da_weakenE)
  3971 	qed
  3972 	from G eval_var vn 
  3973 	have eval_lvar: "G\<turnstile>Norm s0 \<midarrow>LVar vn=\<succ>(w, upd)\<rightarrow> s1" 
  3974 	  by simp
  3975 	then have upd: "upd = snd (lvar vn (store s1))"
  3976 	  by cases (cases "lvar vn (store s1)",simp)
  3977 	have "nrm E \<subseteq> dom (locals (store (assign upd v s2)))"
  3978 	proof -
  3979 	  from hyp_e wt_e da_e' G normal_s2
  3980 	  have "nrm E' \<subseteq> dom (locals (store s2))"
  3981 	    by simp
  3982 	  also
  3983 	  from upd
  3984 	  have "dom (locals (store s2))  \<subseteq> dom (locals (store (upd v s2)))"
  3985 	    by (simp add: lvar_def) blast
  3986 	  hence "dom (locals (store s2)) 
  3987 	             \<subseteq> dom (locals (store (assign upd v s2)))"
  3988 	    by (rule dom_locals_assign_mono)
  3989 	  finally
  3990 	  show ?thesis using E_E' 
  3991 	    by blast
  3992 	qed
  3993 	moreover
  3994 	from upd normal_s2
  3995 	have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
  3996 	  by (auto simp add: assign_def Let_def lvar_def upd split: split_split)
  3997 	ultimately
  3998 	show "nrm A \<subseteq> \<dots>"
  3999 	  by (rule Un_least [elim_format]) (simp add: nrm_A)
  4000       next
  4001 	case False
  4002 	from Ass.prems obtain V where
  4003 	  da_var: "Env\<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>var\<rangle>\<guillemotright> V" and
  4004 	  da_e:   "Env\<turnstile> nrm V \<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  4005 	  by (elim da_elim_cases) (insert False,simp+)
  4006         from hyp_var wt_var da_var G normal_s1
  4007         have "nrm V \<subseteq> dom (locals (store s1))"
  4008           by simp
  4009         with da_e obtain A' 
  4010           where  da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
  4011                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
  4012           by (rule da_weakenE) rules
  4013         from hyp_e wt_e da_e' G normal_s2
  4014         obtain "nrm A' \<subseteq> dom (locals (store s2))"   
  4015           by simp
  4016         with nrm_A_A' have "nrm A \<subseteq> \<dots>" 
  4017           by blast
  4018         also have "\<dots> \<subseteq> dom (locals (store (assign upd v s2)))"
  4019         proof -
  4020           from eval_var normal_s1
  4021           have "dom (locals (store s2)) \<subseteq> dom (locals (store (upd v s2)))"
  4022             by (cases rule: dom_locals_eval_mono_elim)
  4023                (cases s2, simp)
  4024           thus ?thesis
  4025             by (rule dom_locals_assign_mono)
  4026         qed
  4027         finally show ?thesis .
  4028       qed
  4029     qed
  4030     moreover 
  4031     {
  4032       fix j have "abrupt (assign upd v s2) \<noteq> Some (Jump j)"
  4033       proof -
  4034         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<rightarrow> (assign upd v s2)"
  4035           by (simp only: G) (rule eval.Ass)
  4036         from Ass.prems 
  4037         obtain T' where  "T=Inl T'"
  4038           by (elim wt_elim_cases) simp
  4039         with Ass.prems have "Env\<turnstile>var:=e\<Colon>-T'" by simp
  4040         from eval _ this
  4041         show ?thesis
  4042           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4043       qed
  4044     }
  4045     hence "?BreakAssigned (Norm s0) (assign upd v s2) A"
  4046       and "?ResAssigned (Norm s0) (assign upd v s2)"       
  4047       by simp_all
  4048     ultimately show ?case by (intro conjI)
  4049   next
  4050 -- {* 
  4051 \par
  4052 *} (* dummy text command to break paragraph for latex;
  4053               large paragraphs exhaust memory of debian pdflatex *)
  4054     case (Cond b e0 e1 e2 s0 s1 s2 v Env T A)
  4055     have G: "prg Env = G" .
  4056     have "?NormalAssigned s2 A"
  4057     proof 
  4058       assume normal_s2: "normal s2"
  4059       show "nrm A \<subseteq> dom (locals (store s2))"
  4060       proof (cases "Env\<turnstile>(e0 ? e1 : e2)\<Colon>-(PrimT Boolean)")
  4061         case True
  4062         with Cond.prems 
  4063         have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state))) 
  4064                              \<union> (assigns_if True  (e0 ? e1 : e2) \<inter> 
  4065                                  assigns_if False (e0 ? e1 : e2))"
  4066           by (elim da_elim_cases) simp_all
  4067         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>(e0 ? e1 : e2)-\<succ>v\<rightarrow> s2"
  4068           by (simp only: G) (rule eval.Cond)
  4069         from eval 
  4070         have "dom (locals (store ((Norm s0)::state)))\<subseteq>dom (locals (store s2))"
  4071           by (rule dom_locals_eval_mono_elim)
  4072         moreover
  4073         from eval normal_s2 True
  4074         have ass_if: "assigns_if (the_Bool v) (e0 ? e1 : e2)
  4075                         \<subseteq> dom (locals (store s2))"
  4076           by (rule assigns_if_good_approx)
  4077         have "assigns_if True  (e0 ? e1:e2) \<inter> assigns_if False (e0 ? e1:e2)
  4078                \<subseteq> dom (locals (store s2))"
  4079         proof (cases "the_Bool v")
  4080           case True 
  4081           from ass_if 
  4082           have "assigns_if True  (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"
  4083             by (simp only: True)
  4084           thus ?thesis by blast
  4085         next
  4086           case False 
  4087           from ass_if 
  4088           have "assigns_if False  (e0 ? e1:e2) \<subseteq> dom (locals (store s2))"
  4089             by (simp only: False)
  4090           thus ?thesis by blast
  4091         qed
  4092         ultimately show "nrm A \<subseteq> dom (locals (store s2))"
  4093           by (simp only: nrm_A) (rule Un_least)
  4094       next
  4095         case False
  4096         with Cond.prems obtain E1 E2 where
  4097          da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  4098                          \<union> assigns_if True e0) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
  4099          da_e2: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  4100                         \<union> assigns_if False e0) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2" and
  4101          nrm_A: "nrm A = nrm E1 \<inter> nrm E2"
  4102           by (elim da_elim_cases) simp_all
  4103         from Cond.prems obtain e1T e2T where
  4104           wt_e0: "Env\<turnstile>e0\<Colon>- PrimT Boolean" and
  4105           wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
  4106           wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
  4107           by (elim wt_elim_cases)
  4108         have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  4109                        \<subseteq> dom (locals (store s1))"
  4110           by (rule dom_locals_eval_mono_elim)
  4111         have eval_e0: "prg Env\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" by (simp only: G)
  4112         have normal_s1: "normal s1"
  4113           by (rule eval_no_abrupt_lemma [rule_format])
  4114         show ?thesis
  4115         proof (cases "the_Bool b")
  4116           case True
  4117           from True Cond.hyps have "PROP ?Hyp (In1l e1) s1 s2" by simp
  4118           moreover
  4119           from eval_e0 normal_s1 wt_e0
  4120           have "assigns_if True e0 \<subseteq> dom (locals (store s1))"
  4121             by (rule assigns_if_good_approx [elim_format]) (simp only: True)
  4122           with s0_s1 
  4123           have "dom (locals (store ((Norm s0)::state))) 
  4124                  \<union> assigns_if True e0 \<subseteq> \<dots>"
  4125             by (rule Un_least)
  4126           with da_e1 obtain E1' where
  4127                   da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
  4128               nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"
  4129             by (rule da_weakenE) rules
  4130           ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"
  4131             using wt_e1 G normal_s2 by simp 
  4132           with nrm_E1_E1' show ?thesis
  4133             by (simp only: nrm_A) blast
  4134         next
  4135           case False
  4136           from False Cond.hyps have "PROP ?Hyp (In1l e2) s1 s2" by simp
  4137           moreover
  4138           from eval_e0 normal_s1 wt_e0
  4139           have "assigns_if False e0 \<subseteq> dom (locals (store s1))"
  4140             by (rule assigns_if_good_approx [elim_format]) (simp only: False)
  4141           with s0_s1 
  4142           have "dom (locals (store ((Norm s0)::state))) 
  4143                  \<union> assigns_if False e0 \<subseteq> \<dots>"
  4144             by (rule Un_least)
  4145           with da_e2 obtain E2' where
  4146                   da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
  4147               nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"
  4148             by (rule da_weakenE) rules
  4149           ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"
  4150             using wt_e2 G normal_s2 by simp 
  4151           with nrm_E2_E2' show ?thesis
  4152             by (simp only: nrm_A) blast
  4153         qed
  4154       qed
  4155     qed
  4156     moreover
  4157     {
  4158       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  4159       proof -
  4160         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
  4161           by (simp only: G) (rule eval.Cond)
  4162         from Cond.prems 
  4163         obtain T' where  "T=Inl T'"
  4164           by (elim wt_elim_cases) simp
  4165         with Cond.prems have "Env\<turnstile>e0 ? e1 : e2\<Colon>-T'" by simp
  4166         from eval _ this
  4167         show ?thesis
  4168           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4169       qed
  4170     } 
  4171     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  4172       by simp_all
  4173     ultimately show ?case by (intro conjI)
  4174   next
  4175     case (Call D a accC args e mn mode pTs s0 s1 s2 s3 s3' s4 statT v vs 
  4176            Env T A)
  4177     have G: "prg Env = G" .
  4178     have "?NormalAssigned (restore_lvars s2 s4) A"
  4179     proof 
  4180       assume normal_restore_lvars: "normal (restore_lvars s2 s4)"
  4181       show "nrm A \<subseteq> dom (locals (store (restore_lvars s2 s4)))"
  4182       proof -
  4183         from Call.prems obtain E where
  4184              da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  4185           da_args: "Env\<turnstile> nrm E \<guillemotright>\<langle>args\<rangle>\<guillemotright> A" 
  4186           by (elim da_elim_cases)
  4187         from Call.prems obtain eT argsT where
  4188              wt_e: "Env\<turnstile>e\<Colon>-eT" and
  4189           wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
  4190           by (elim wt_elim_cases)
  4191         have s3: "s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a vs s2" .
  4192         have s3': "s3' = check_method_access G accC statT mode 
  4193                                            \<lparr>name=mn,parTs=pTs\<rparr> a s3" .
  4194         have normal_s2: "normal s2"
  4195         proof -
  4196           from normal_restore_lvars have "normal s4"
  4197             by simp
  4198           then have "normal s3'"
  4199             by - (rule eval_no_abrupt_lemma [rule_format])
  4200           with s3' have "normal s3"
  4201             by (cases s3) (simp add: check_method_access_def Let_def)
  4202           with s3 show "normal s2"
  4203             by (cases s2) (simp add: init_lvars_def Let_def)
  4204         qed
  4205         then have normal_s1: "normal s1"
  4206           by  - (rule eval_no_abrupt_lemma [rule_format])
  4207         have "PROP ?Hyp (In1l e) (Norm s0) s1" .
  4208         with da_e wt_e G normal_s1
  4209         have "nrm E \<subseteq> dom (locals (store s1))"
  4210           by simp
  4211         with da_args obtain A' where
  4212           da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
  4213           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4214           by (rule da_weakenE) rules
  4215         have "PROP ?Hyp (In3 args) s1 s2" .
  4216         with da_args' wt_args G normal_s2
  4217         have "nrm A' \<subseteq> dom (locals (store s2))"
  4218           by simp
  4219         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4220           by blast
  4221         also have "\<dots> \<subseteq> dom (locals (store (restore_lvars s2 s4)))"
  4222           by (cases s4) simp
  4223         finally show ?thesis .
  4224       qed
  4225     qed
  4226     moreover
  4227     {
  4228       fix j have "abrupt (restore_lvars s2 s4) \<noteq> Some (Jump j)"
  4229       proof -
  4230         have eval: "prg Env\<turnstile>Norm s0 \<midarrow>({accC,statT,mode}e\<cdot>mn( {pTs}args))-\<succ>v
  4231                             \<rightarrow> (restore_lvars s2 s4)"
  4232           by (simp only: G) (rule eval.Call)
  4233         from Call.prems 
  4234         obtain T' where  "T=Inl T'"
  4235           by (elim wt_elim_cases) simp
  4236         with Call.prems have "Env\<turnstile>({accC,statT,mode}e\<cdot>mn( {pTs}args))\<Colon>-T'" 
  4237           by simp
  4238         from eval _ this
  4239         show ?thesis
  4240           by (rule eval_expression_no_jump) (simp_all add: G wf)
  4241       qed
  4242     } 
  4243     hence "?BreakAssigned (Norm s0) (restore_lvars s2 s4) A"
  4244       and "?ResAssigned (Norm s0) (restore_lvars s2 s4)"
  4245       by simp_all
  4246     ultimately show ?case by (intro conjI)
  4247   next
  4248     case (Methd D s0 s1 sig v Env T A)
  4249     have G: "prg Env = G". 
  4250     from Methd.prems obtain m where
  4251        m:      "methd (prg Env) D sig = Some m" and
  4252        da_body: "Env\<turnstile>(dom (locals (store ((Norm s0)::state)))) 
  4253                   \<guillemotright>\<langle>Body (declclass m) (stmt (mbody (mthd m)))\<rangle>\<guillemotright> A"
  4254       by - (erule da_elim_cases)
  4255     from Methd.prems m obtain
  4256       isCls: "is_class (prg Env) D" and
  4257       wt_body: "Env \<turnstile>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<Colon>T"
  4258       by - (erule wt_elim_cases,simp)
  4259     have "PROP ?Hyp (In1l (body G D sig)) (Norm s0) s1" .
  4260     moreover
  4261     from wt_body have "Env\<turnstile>In1l (body G D sig)\<Colon>T"
  4262       using isCls m G by (simp add: body_def2)
  4263     moreover 
  4264     from da_body have "Env\<turnstile>(dom (locals (store ((Norm s0)::state)))) 
  4265                           \<guillemotright>\<langle>body G D sig\<rangle>\<guillemotright> A"
  4266       using isCls m G by (simp add: body_def2)
  4267     ultimately show ?case
  4268       using G by simp
  4269   next
  4270     case (Body D c s0 s1 s2 s3 Env T A)
  4271     have G: "prg Env = G" .
  4272     from Body.prems 
  4273     have nrm_A: "nrm A = dom (locals (store ((Norm s0)::state)))"
  4274       by (elim da_elim_cases) simp
  4275     have eval: "prg Env\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
  4276                         \<rightarrow>abupd (absorb Ret) s3"
  4277       by (simp only: G) (rule eval.Body)
  4278     hence "nrm A \<subseteq> dom (locals (store (abupd (absorb Ret) s3)))"
  4279       by  (simp only: nrm_A) (rule dom_locals_eval_mono_elim)
  4280     hence "?NormalAssigned (abupd (absorb Ret) s3) A"
  4281       by simp
  4282     moreover
  4283     from eval have "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
  4284       by (rule Body_no_jump) simp
  4285     hence "?BreakAssigned (Norm s0) (abupd (absorb Ret) s3) A" and
  4286           "?ResAssigned (Norm s0) (abupd (absorb Ret) s3)"
  4287       by simp_all
  4288     ultimately show ?case by (intro conjI)
  4289   next
  4290 -- {* 
  4291 \par
  4292 *} (* dummy text command to break paragraph for latex;
  4293               large paragraphs exhaust memory of debian pdflatex *)
  4294     case (LVar s vn Env T A)
  4295     from LVar.prems
  4296     have "nrm A = dom (locals (store ((Norm s)::state)))"
  4297       by (elim da_elim_cases) simp
  4298     thus ?case by simp
  4299   next
  4300     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v Env T A)
  4301     have G: "prg Env = G" .
  4302     have "?NormalAssigned s3 A"
  4303     proof 
  4304       assume normal_s3: "normal s3"
  4305       show "nrm A \<subseteq> dom (locals (store s3))"
  4306       proof -
  4307         have fvar: "(v, s2') = fvar statDeclC stat fn a s2" and
  4308                s3: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  4309         from FVar.prems
  4310         have da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> A"
  4311           by (elim da_elim_cases)
  4312         from FVar.prems obtain eT where
  4313           wt_e: "Env\<turnstile>e\<Colon>-eT"
  4314           by (elim wt_elim_cases)
  4315         have "(dom (locals (store ((Norm s0)::state)))) 
  4316                \<subseteq> dom (locals (store s1))"
  4317           by (rule dom_locals_eval_mono_elim)
  4318         with da_e obtain A' where
  4319           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
  4320           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4321           by (rule da_weakenE) rules
  4322         have normal_s2: "normal s2"
  4323         proof -
  4324           from normal_s3 s3 
  4325           have "normal s2'"
  4326             by (cases s2') (simp add: check_field_access_def Let_def)
  4327           with fvar 
  4328           show "normal s2"
  4329             by (cases s2) (simp add: fvar_def2)
  4330         qed
  4331         have "PROP ?Hyp (In1l e) s1 s2" . 
  4332         with da_e' wt_e G normal_s2
  4333         have "nrm A' \<subseteq> dom (locals (store s2))"
  4334           by simp
  4335         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4336           by blast
  4337         also have "\<dots> \<subseteq> dom (locals (store s3))"
  4338         proof -
  4339           from fvar have "s2' = snd (fvar statDeclC stat fn a s2)" 
  4340             by (cases "fvar statDeclC stat fn a s2") simp
  4341           hence "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  4342             by (simp) (rule dom_locals_fvar_mono)
  4343           also from s3 have "\<dots> \<subseteq> dom (locals (store s3))"
  4344             by (cases s2') (simp add: check_field_access_def Let_def)
  4345           finally show ?thesis .
  4346         qed
  4347         finally show ?thesis .
  4348       qed
  4349     qed
  4350     moreover
  4351     {
  4352       fix j have "abrupt s3 \<noteq> Some (Jump j)"
  4353       proof -
  4354         obtain w upd where v: "(w,upd)=v"
  4355           by (cases v) auto
  4356         have eval: "prg Env\<turnstile>Norm s0\<midarrow>({accC,statDeclC,stat}e..fn)=\<succ>(w,upd)\<rightarrow>s3"
  4357           by (simp only: G v) (rule eval.FVar)
  4358         from FVar.prems 
  4359         obtain T' where  "T=Inl T'"
  4360           by (elim wt_elim_cases) simp
  4361         with FVar.prems have "Env\<turnstile>({accC,statDeclC,stat}e..fn)\<Colon>=T'" 
  4362           by simp
  4363         from eval _ this
  4364         show ?thesis
  4365           by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
  4366       qed
  4367     } 
  4368     hence "?BreakAssigned (Norm s0) s3 A" and "?ResAssigned (Norm s0) s3"
  4369       by simp_all
  4370     ultimately show ?case by (intro conjI)
  4371   next
  4372     case (AVar a e1 e2 i s0 s1 s2 s2' v Env T A)
  4373     have G: "prg Env = G" .
  4374     have "?NormalAssigned s2' A"
  4375     proof 
  4376       assume normal_s2': "normal s2'"
  4377       show "nrm A \<subseteq> dom (locals (store s2'))"
  4378       proof -
  4379         have avar: "(v, s2') = avar G i a s2" .
  4380         from AVar.prems obtain E1 where
  4381           da_e1: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1" and
  4382           da_e2: "Env\<turnstile> nrm E1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A" 
  4383           by (elim da_elim_cases)
  4384         from AVar.prems obtain e1T e2T where
  4385              wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
  4386              wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
  4387           by (elim wt_elim_cases)
  4388         from avar normal_s2' 
  4389         have normal_s2: "normal s2"
  4390           by (cases s2) (simp add: avar_def2)
  4391         hence "normal s1"
  4392           by - (rule eval_no_abrupt_lemma [rule_format])
  4393         moreover have "PROP ?Hyp (In1l e1) (Norm s0) s1" .
  4394         ultimately have "nrm E1 \<subseteq> dom (locals (store s1))" 
  4395           using da_e1 wt_e1 G by simp
  4396         with da_e2 obtain A' where
  4397           da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
  4398           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4399           by (rule da_weakenE) rules
  4400         have "PROP ?Hyp (In1l e2) s1 s2" .
  4401         with da_e2' wt_e2 G normal_s2
  4402         have "nrm A' \<subseteq> dom (locals (store s2))"
  4403           by simp
  4404         with nrm_A_A' have "nrm A \<subseteq> dom (locals (store s2))"
  4405           by blast
  4406         also have "\<dots> \<subseteq> dom (locals (store s2'))"
  4407         proof -
  4408            from avar have "s2' = snd (avar G i a s2)" 
  4409             by (cases "(avar G i a s2)") simp
  4410           thus "dom (locals (store s2)) \<subseteq>  dom (locals (store s2'))"
  4411             by (simp) (rule dom_locals_avar_mono)
  4412         qed
  4413         finally show ?thesis .
  4414       qed
  4415     qed
  4416     moreover
  4417     {
  4418       fix j have "abrupt s2' \<noteq> Some (Jump j)"
  4419       proof -
  4420         obtain w upd where v: "(w,upd)=v"
  4421           by (cases v) auto
  4422         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e1.[e2])=\<succ>(w,upd)\<rightarrow>s2'"
  4423           by  (simp only: G v) (rule eval.AVar)
  4424         from AVar.prems 
  4425         obtain T' where  "T=Inl T'"
  4426           by (elim wt_elim_cases) simp
  4427         with AVar.prems have "Env\<turnstile>(e1.[e2])\<Colon>=T'" 
  4428           by simp
  4429         from eval _ this
  4430         show ?thesis
  4431           by (rule eval_var_no_jump [THEN conjunct1]) (simp_all add: G wf)
  4432       qed
  4433     } 
  4434     hence "?BreakAssigned (Norm s0) s2' A" and "?ResAssigned (Norm s0) s2'"
  4435       by simp_all
  4436     ultimately show ?case by (intro conjI)
  4437   next
  4438     case (Nil s0 Env T A)
  4439     from Nil.prems
  4440     have "nrm A = dom (locals (store ((Norm s0)::state)))"
  4441       by (elim da_elim_cases) simp
  4442     thus ?case by simp
  4443   next 
  4444     case (Cons e es s0 s1 s2 v vs Env T A)
  4445     have G: "prg Env = G" .
  4446     have "?NormalAssigned s2 A"
  4447     proof 
  4448       assume normal_s2: "normal s2"
  4449       show "nrm A \<subseteq> dom (locals (store s2))"
  4450       proof -
  4451         from Cons.prems obtain E where
  4452           da_e: "Env\<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>\<langle>e\<rangle>\<guillemotright> E" and
  4453           da_es: "Env\<turnstile> nrm E \<guillemotright>\<langle>es\<rangle>\<guillemotright> A" 
  4454           by (elim da_elim_cases)
  4455         from Cons.prems obtain eT esT where
  4456              wt_e: "Env\<turnstile>e\<Colon>-eT" and
  4457              wt_es: "Env\<turnstile>es\<Colon>\<doteq>esT"
  4458           by (elim wt_elim_cases)
  4459         have "normal s1"
  4460           by - (rule eval_no_abrupt_lemma [rule_format])
  4461         moreover have "PROP ?Hyp (In1l e) (Norm s0) s1" .
  4462         ultimately have "nrm E \<subseteq> dom (locals (store s1))" 
  4463           using da_e wt_e G by simp
  4464         with da_es obtain A' where
  4465           da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
  4466           nrm_A_A': "nrm A \<subseteq> nrm A'"
  4467           by (rule da_weakenE) rules
  4468         have "PROP ?Hyp (In3 es) s1 s2" .
  4469         with da_es' wt_es G normal_s2
  4470         have "nrm A' \<subseteq> dom (locals (store s2))"
  4471           by simp
  4472         with nrm_A_A' show "nrm A \<subseteq> dom (locals (store s2))"
  4473           by blast
  4474       qed
  4475     qed
  4476     moreover
  4477     {
  4478       fix j have "abrupt s2 \<noteq> Some (Jump j)"
  4479       proof -
  4480         have eval: "prg Env\<turnstile>Norm s0\<midarrow>(e # es)\<doteq>\<succ>v#vs\<rightarrow>s2"
  4481           by (simp only: G) (rule eval.Cons)
  4482         from Cons.prems 
  4483         obtain T' where  "T=Inr T'"
  4484           by (elim wt_elim_cases) simp
  4485         with Cons.prems have "Env\<turnstile>(e # es)\<Colon>\<doteq>T'" 
  4486           by simp
  4487         from eval _ this
  4488         show ?thesis
  4489           by (rule eval_expression_list_no_jump) (simp_all add: G wf)
  4490       qed
  4491     } 
  4492     hence "?BreakAssigned (Norm s0) s2 A" and "?ResAssigned (Norm s0) s2"
  4493       by simp_all
  4494     ultimately show ?case by (intro conjI)
  4495   qed
  4496 qed
  4497 
  4498 lemma da_good_approxE [consumes 4]:
  4499   "\<lbrakk>prg Env\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1); Env\<turnstile>t\<Colon>T; Env\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A;
  4500    wf_prog (prg Env);
  4501    \<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
  4502      \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
  4503            \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
  4504      \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))
  4505    \<rbrakk> \<Longrightarrow> P
  4506   \<rbrakk> \<Longrightarrow> P"
  4507 by (drule (3) da_good_approx) simp
  4508 
  4509 
  4510 (* Same as above but with explicit environment; 
  4511    It would be nicer to find a "normalized" way to right down those things
  4512    in Bali.
  4513 *)
  4514 lemma da_good_approxE' [consumes 4]:
  4515   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  4516      and    wt: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T"
  4517      and    da: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>t\<guillemotright> A"
  4518      and    wf: "wf_prog G"
  4519      and  elim: "\<lbrakk>normal s1 \<Longrightarrow> nrm A \<subseteq> dom (locals (store s1));
  4520                  \<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
  4521                        \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1));
  4522                   \<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>
  4523                   \<Longrightarrow>Result \<in> dom (locals (store s1))
  4524                  \<rbrakk> \<Longrightarrow> P"
  4525   shows "P"
  4526 proof -
  4527   from eval have "prg \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)" by simp
  4528   moreover note wt da
  4529   moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
  4530   ultimately show ?thesis
  4531     using elim by (rule da_good_approxE) rules+
  4532 qed
  4533 
  4534 ML {*
  4535 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
  4536 *}
  4537 end