src/HOL/Bali/DefiniteAssignmentCorrect.thy

tuned proofs: avoid implicit prems;

(* $Id$ *)

header {* Correctness of Definite Assignment *}

theory DefiniteAssignmentCorrect imports WellForm Eval begin

ML {*
Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
*}

lemma sxalloc_no_jump:
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
           no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
   shows "abrupt s1 \<noteq> Some (Jump j)"
using sxalloc no_jmp
by cases simp_all

lemma sxalloc_no_jump':
  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and
          jump:  "abrupt s1 = Some (Jump j)"
 shows "abrupt s0 = Some (Jump j)"
using sxalloc jump
by cases simp_all

lemma halloc_no_jump:
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
           no_jmp: "abrupt s0 \<noteq> Some (Jump j)"
   shows "abrupt s1 \<noteq> Some (Jump j)"
using halloc no_jmp
by cases simp_all

lemma halloc_no_jump':
  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
          jump:  "abrupt s1 = Some (Jump j)"
  shows "abrupt s0 = Some (Jump j)"
using halloc jump
by cases simp_all

lemma Body_no_jump: 
   assumes eval: "G\<turnstile>s0 \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
           jump: "abrupt s0 \<noteq> Some (Jump j)"
   shows "abrupt s1 \<noteq> Some (Jump j)"
proof (cases "normal s0")
  case True
  with eval obtain s0' where eval': "G\<turnstile>Norm s0' \<midarrow>Body D c-\<succ>v\<rightarrow>s1" and
                             s0: "s0 = Norm s0'"
    by (cases s0) simp
  from eval' obtain s2 where
     s1: "s1 = abupd (absorb Ret)
             (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or>
                     abrupt s2 = Some (Jump (Cont l))
              then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)"
    by cases simp
  show ?thesis
  proof (cases "\<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
                   abrupt s2 = Some (Jump (Cont l))")
    case True
    with s1 have "abrupt s1 = Some (Error CrossMethodJump)"
      by (cases s2) simp
    thus ?thesis by simp
  next
    case False
    with s1 have "s1=abupd (absorb Ret) s2"
      by simp
    with False show ?thesis
      by (cases s2,cases j) (auto simp add: absorb_def)
  qed
next
  case False
  with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Body D c-\<succ>v\<rightarrow>s1"
                                 "s0 = (Some abr, s0')"
    by (cases s0) fastsimp
  with this jump
  show ?thesis
    by (cases) (simp)
qed

lemma Methd_no_jump: 
   assumes eval: "G\<turnstile>s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1" and
           jump: "abrupt s0 \<noteq> Some (Jump j)"
   shows "abrupt s1 \<noteq> Some (Jump j)"
proof (cases "normal s0")
  case True
   with eval obtain s0' where "G\<turnstile>Norm s0' \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1" 
                              "s0 = Norm s0'"
    by (cases s0) simp
  then obtain D' body where "G\<turnstile>s0 \<midarrow>Body D' body-\<succ>v\<rightarrow>s1"
    by (cases) (simp add: body_def2)
  from this jump
  show ?thesis
    by (rule Body_no_jump)
next
  case False
  with eval obtain s0' abr where "G\<turnstile>(Some abr,s0') \<midarrow>Methd D sig-\<succ>v\<rightarrow>s1"
                                 "s0 = (Some abr, s0')"
    by (cases s0) fastsimp
  with this jump
  show ?thesis
    by (cases) (simp)
qed

lemma jumpNestingOkS_mono: 
  assumes jumpNestingOk_l': "jumpNestingOkS jmps' c" 
      and      subset: "jmps' \<subseteq> jmps"
 shows "jumpNestingOkS jmps c"
proof -
    have True and True and 
       "\<And> jmps' jmps. \<lbrakk>jumpNestingOkS jmps' c; jmps' \<subseteq> jmps\<rbrakk> \<Longrightarrow> jumpNestingOkS jmps c" 
       and True
  proof (induct rule: var_expr_stmt.inducts)
    case (Lab j c jmps' jmps)
    note jmpOk = `jumpNestingOkS jmps' (j\<bullet> c)`
    note jmps = `jmps' \<subseteq> jmps`
    with jmpOk have "jumpNestingOkS ({j} \<union> jmps') c" by simp
    moreover from jmps have "({j} \<union> jmps') \<subseteq> ({j} \<union> jmps)" by auto
    ultimately
    have "jumpNestingOkS ({j} \<union> jmps) c"
      by (rule Lab.hyps)
    thus ?case 
      by simp
  next
    case (Jmp j jmps' jmps) 
    thus ?case 
      by (cases j) auto
  next
    case (Comp c1 c2 jmps' jmps)
    from Comp.prems 
    have "jumpNestingOkS jmps c1" by - (rule Comp.hyps,auto)
    moreover from Comp.prems
    have "jumpNestingOkS jmps c2" by - (rule Comp.hyps,auto)
    ultimately show ?case
      by simp
  next
    case (If_ e c1 c2 jmps' jmps)
    from If_.prems 
    have "jumpNestingOkS jmps c1" by - (rule If_.hyps,auto)
    moreover from If_.prems 
    have "jumpNestingOkS jmps c2" by - (rule If_.hyps,auto)
    ultimately show ?case
      by simp
  next
    case (Loop l e c jmps' jmps)
    from `jumpNestingOkS jmps' (l\<bullet> While(e) c)`
    have "jumpNestingOkS ({Cont l} \<union> jmps') c" by simp
    moreover
    from `jmps' \<subseteq> jmps`
    have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps" by auto
    ultimately
    have "jumpNestingOkS ({Cont l} \<union> jmps) c"
      by (rule Loop.hyps)
    thus ?case by simp
  next
    case (TryC c1 C vn c2 jmps' jmps)
    from TryC.prems 
    have "jumpNestingOkS jmps c1" by - (rule TryC.hyps,auto)
    moreover from TryC.prems 
    have "jumpNestingOkS jmps c2" by - (rule TryC.hyps,auto)
    ultimately show ?case
      by simp
  next
    case (Fin c1 c2 jmps' jmps)
    from Fin.prems 
    have "jumpNestingOkS jmps c1" by - (rule Fin.hyps,auto)
    moreover from Fin.prems 
    have "jumpNestingOkS jmps c2" by - (rule Fin.hyps,auto)
    ultimately show ?case
      by simp
  qed (simp_all)
  with jumpNestingOk_l' subset
  show ?thesis
    by iprover
qed
   
corollary jumpNestingOk_mono: 
  assumes jmpOk: "jumpNestingOk jmps' t" 
     and subset: "jmps' \<subseteq> jmps"
  shows  "jumpNestingOk jmps t"
proof (cases t)
  case (In1 expr_stmt)
  show ?thesis
  proof (cases expr_stmt)
    case (Inl e)
    with In1 show ?thesis by simp
  next
    case (Inr s)
    with In1 jmpOk subset show ?thesis by (auto intro: jumpNestingOkS_mono)
  qed
qed (simp_all)

lemma assign_abrupt_propagation: 
 assumes f_ok: "abrupt (f n s) \<noteq> x"
   and    ass: "abrupt (assign f n s) = x"
  shows "abrupt s = x"
proof (cases x)
  case None
  with ass show ?thesis
    by (cases s) (simp add: assign_def Let_def)
next
  case (Some xcpt)
  from f_ok
  obtain xf sf where "f n s = (xf,sf)"
    by (cases "f n s")
  with Some ass f_ok show ?thesis
    by (cases s) (simp add: assign_def Let_def)
qed
 
lemma wt_init_comp_ty': 
"is_acc_type (prg Env) (pid (cls Env)) T \<Longrightarrow> Env\<turnstile>init_comp_ty T\<Colon>\<surd>"
apply (unfold init_comp_ty_def)
apply (clarsimp simp add: accessible_in_RefT_simp 
                          is_acc_type_def is_acc_class_def)
done

lemma fvar_upd_no_jump: 
      assumes upd: "upd = snd (fst (fvar statDeclC stat fn a s'))"
        and noJmp: "abrupt s \<noteq> Some (Jump j)"
        shows "abrupt (upd val s) \<noteq> Some (Jump j)"
proof (cases "stat")
  case True
  with noJmp upd
  show ?thesis
    by (cases s) (simp add: fvar_def2)
next
  case False
  with noJmp upd
  show ?thesis
    by (cases s) (simp add: fvar_def2)
qed


lemma avar_state_no_jump: 
  assumes jmp: "abrupt (snd (avar G i a s)) = Some (Jump j)"
  shows "abrupt s = Some (Jump j)"
proof (cases "normal s")
  case True with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
next
  case False with jmp show ?thesis by (auto simp add: avar_def2 abrupt_if_def)
qed

lemma avar_upd_no_jump: 
      assumes upd: "upd = snd (fst (avar G i a s'))"
        and noJmp: "abrupt s \<noteq> Some (Jump j)"
        shows "abrupt (upd val s) \<noteq> Some (Jump j)"
using upd noJmp
by (cases s) (simp add: avar_def2 abrupt_if_def)


text {* 
The next theorem expresses: If jumps (breaks, continues, returns) are nested
correctly, we won't find an unexpected jump in the result state of the 
evaluation. For exeample, a break can't leave its enclosing loop, an return
cant leave its enclosing method.
To proove this, the method call is critical. Allthough the
wellformedness of the whole program guarantees that the jumps (breaks,continues
and returns) are nested
correctly in all method bodies, the call rule alone does not guarantee that I
will call a method or even a class that is part of the program due to dynamic
binding! To be able to enshure this we need a kind of conformance of the
state, like in the typesafety proof. But then we will redo the typesafty
proof here. It would be nice if we could find an easy precondition that will
guarantee that all calls will actually call classes and methods of the current
program, which can be instantiated in the typesafty proof later on.
To fix this problem, I have instrumented the semantic definition of a call
to filter out any breaks in the state and to throw an error instead. 

To get an induction hypothesis which is strong enough to perform the
proof, we can't just 
assume @{term jumpNestingOk} for the empty set and conlcude, that no jump at 
all will be in the resulting state,  because the set is altered by 
the statements @{term Lab} and @{term While}. 

The wellformedness of the program is used to enshure that for all
classinitialisations and methods the nesting of jumps is wellformed, too.
*}  
theorem jumpNestingOk_eval:
  assumes eval: "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
     and jmpOk: "jumpNestingOk jmps t" 
     and wt: "Env\<turnstile>t\<Colon>T" 
     and wf: "wf_prog G"
     and  G: "prg Env = G"
     and no_jmp: "\<forall>j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"
                    (is "?Jmp jmps s0")
  shows  "(\<forall>j. fst s1 = Some (Jump j) \<longrightarrow> j \<in> jmps) \<and>
                 (normal s1 \<longrightarrow>
                  (\<forall> w upd. v=In2 (w,upd)
                   \<longrightarrow>   (\<forall> s j val.
                          abrupt s \<noteq> Some (Jump j) \<longrightarrow>
                          abrupt (upd val s) \<noteq> Some (Jump j))))"
        (is "?Jmp jmps s1 \<and> ?Upd v s1")  
proof -
  let ?HypObj = "\<lambda> t s0 s1 v.
       (\<forall> jmps T Env. 
          ?Jmp jmps s0 \<longrightarrow> jumpNestingOk jmps t \<longrightarrow> Env\<turnstile>t\<Colon>T \<longrightarrow> prg Env=G\<longrightarrow>
          ?Jmp jmps s1 \<and> ?Upd v s1)"
  -- {* Variable @{text ?HypObj} is the following goal spelled in terms of
        the object logic, instead of the meta logic. It is needed in some
        cases of the induction were, the atomize-rulify process of induct 
        does not work fine, because the eval rules mix up object and meta
        logic. See for example the case for the loop. *} 
  from eval 
  have "\<And> jmps T Env. \<lbrakk>?Jmp jmps s0; jumpNestingOk jmps t; Env\<turnstile>t\<Colon>T;prg Env=G\<rbrakk>
            \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1" 
        (is "PROP ?Hyp t s0 s1 v")
  -- {* We need to abstract over @{term jmps} since @{term jmps} are extended
        during analysis of @{term Lab}. Also we need to abstract over 
        @{term T} and @{term Env} since they are altered in various
        typing judgements. *}    
  proof (induct)   
    case Abrupt thus ?case by simp 
  next
    case Skip thus ?case by simp
  next
    case Expr thus ?case by (elim wt_elim_cases) simp
  next
    case (Lab s0 c s1 jmp jmps T Env) 
    note jmpOK = `jumpNestingOk jmps (In1r (jmp\<bullet> c))`
    note G = `prg Env = G`
    have wt_c: "Env\<turnstile>c\<Colon>\<surd>" 
      using Lab.prems by (elim wt_elim_cases)
    { 
      fix j
      assume ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)"
      have "j\<in>jmps"          
      proof -
        from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
          by (cases s1) (simp add: absorb_def)
        note hyp_c = `PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>`
        from ab_s1 have "j \<noteq> jmp" 
          by (cases s1) (simp add: absorb_def)
        moreover have "j \<in> {jmp} \<union> jmps"
        proof -
          from jmpOK 
          have "jumpNestingOk ({jmp} \<union> jmps) (In1r c)" by simp
          with wt_c jmp_s1 G hyp_c
          show ?thesis
            by - (rule hyp_c [THEN conjunct1,rule_format],simp)
        qed
        ultimately show ?thesis
          by simp
      qed
    }
    thus ?case by simp
  next
    case (Comp s0 c1 s1 c2 s2 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (c1;; c2))`
    note G = `prg Env = G`
    from Comp.prems obtain
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
      by (elim wt_elim_cases)
    {
      fix j
      assume abr_s2: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        have jmp: "?Jmp jmps s1"
        proof -
          note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>`
          with wt_c1 jmpOk G 
          show ?thesis by simp
        qed
        moreover note hyp_c2 = `PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)`
        have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
        moreover note wt_c2 G abr_s2
        ultimately show "j \<in> jmps"
          by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
      qed
    } thus ?case by simp
  next
    case (If s0 e b s1 c1 c2 s2 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (If(e) c1 Else c2))`
    note G = `prg Env = G`
    from If.prems obtain 
              wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
      wt_then_else: "Env\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
      by (elim wt_elim_cases) simp
    { 
      fix j
      assume jmp: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
        with wt_e G have "?Jmp jmps s1" 
          by simp
        moreover note hyp_then_else =
          `PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>`
        have "jumpNestingOk jmps (In1r (if the_Bool b then c1 else c2))"
          using jmpOk by (cases "the_Bool b") simp_all
        moreover note wt_then_else G jmp
        ultimately show "j\<in> jmps" 
          by (rule hyp_then_else [THEN conjunct1,rule_format (no_asm)])
      qed
    }
    thus ?case by simp
  next
    case (Loop s0 e b s1 c s2 l s3 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (l\<bullet> While(e) c))`
    note G = `prg Env = G`
    note wt = `Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
    then obtain 
              wt_e: "Env\<turnstile>e\<Colon>-PrimT Boolean" and 
              wt_c: "Env\<turnstile>c\<Colon>\<surd>"
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt s3 = Some (Jump j)" 
      have "j\<in>jmps"
      proof -
        note `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)`
        with wt_e G have jmp_s1: "?Jmp jmps s1" 
          by simp
        show ?thesis
	proof (cases "the_Bool b")
          case False
          from Loop.hyps
          have "s3=s1"
            by (simp (no_asm_use) only: if_False False) 
          with jmp_s1 jmp have "j \<in> jmps" by simp
          thus ?thesis by simp
        next
          case True
          from Loop.hyps 
            (* Because of the mixture of object and pure logic in the rule 
               eval.If the atomization-rulification of the induct method 
               leaves the hypothesis in object logic *)
          have "?HypObj (In1r c) s1 s2 (\<diamondsuit>::vals)"
            apply (simp (no_asm_use) only: True if_True )
            apply (erule conjE)+
            apply assumption
            done
          note hyp_c = this [rule_format (no_asm)]
          moreover from jmpOk have "jumpNestingOk ({Cont l} \<union> jmps) (In1r c)"
            by simp
          moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
          ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
            using wt_c G by iprover
          have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
          proof -
            {
      	      fix j'
      	      assume abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')"
      	      have "j' \<in> jmps"
      	      proof (cases "j' = Cont l")
      		case True
      		with abs show ?thesis
      		  by (cases s2) (simp add: absorb_def)
      	      next
      		case False 
      		with abs have "abrupt s2 = Some (Jump j')"
      		  by (cases s2) (simp add: absorb_def) 
      		with jmp_s2 False show ?thesis
      		  by simp
      	      qed
            }
            thus ?thesis by simp
          qed
          moreover
          from Loop.hyps
          have "?HypObj (In1r (l\<bullet> While(e) c)) 
                        (abupd (absorb (Cont l)) s2) s3 (\<diamondsuit>::vals)"
            apply (simp (no_asm_use) only: True if_True)
            apply (erule conjE)+
            apply assumption
            done
          note hyp_w = this [rule_format (no_asm)]
          note jmpOk wt G jmp 
          ultimately show "j\<in> jmps" 
            by (rule hyp_w [THEN conjunct1,rule_format (no_asm)])
        qed
      qed
    }
    thus ?case by simp
  next
    case (Jmp s j jmps T Env) thus ?case by simp
  next
    case (Throw s0 e a s1 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (Throw e))`
    note G = `prg Env = G`
    from Throw.prems obtain Te where 
      wt_e: "Env\<turnstile>e\<Colon>-Te" 
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        from `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
        have "?Jmp jmps s1" using wt_e G by simp
        moreover
        from jmp 
        have "abrupt s1 = Some (Jump j)"
          by (cases s1) (simp add: throw_def abrupt_if_def)
        ultimately show "j \<in> jmps" by simp
      qed
    }
    thus ?case by simp
  next
    case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))`
    note G = `prg Env = G`
    from Try.prems obtain 
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and  
      wt_c2: "Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>\<turnstile>c2\<Colon>\<surd>"
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt s3 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note `PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)`
        with jmpOk wt_c1 G
        have jmp_s1: "?Jmp jmps s1" by simp
        note s2 = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
        show "j \<in> jmps"
        proof (cases "G,s2\<turnstile>catch C")
          case False
          from Try.hyps have "s3=s2" 
	    by (simp (no_asm_use) only: False if_False)
          with jmp have "abrupt s1 = Some (Jump j)"
            using sxalloc_no_jump' [OF s2] by simp
          with jmp_s1 
          show ?thesis by simp
        next
          case True
          with Try.hyps 
          have "?HypObj (In1r c2) (new_xcpt_var vn s2) s3 (\<diamondsuit>::vals)"
            apply (simp (no_asm_use) only: True if_True simp_thms)
            apply (erule conjE)+
            apply assumption
            done
          note hyp_c2 = this [rule_format (no_asm)]
          from jmp_s1 sxalloc_no_jump' [OF s2] 
          have "?Jmp jmps s2"
            by simp
          hence "?Jmp jmps (new_xcpt_var vn s2)"
            by (cases s2) simp
          moreover have "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
          moreover note wt_c2
          moreover from G 
          have "prg (Env\<lparr>lcl := lcl Env(VName vn\<mapsto>Class C)\<rparr>) = G"
            by simp
          moreover note jmp
          ultimately show ?thesis 
            by (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)])
        qed
      qed
    }
    thus ?case by simp
  next
    case (Fin s0 c1 x1 s1 c2 s2 s3 jmps T Env)
    note jmpOk = `jumpNestingOk jmps (In1r (c1 Finally c2))`
    note G = `prg Env = G`
    from Fin.prems obtain 
      wt_c1: "Env\<turnstile>c1\<Colon>\<surd>" and wt_c2: "Env\<turnstile>c2\<Colon>\<surd>"
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt s3 = Some (Jump j)" 
      have "j \<in> jmps"
      proof (cases "x1=Some (Jump j)")
        case True
        note hyp_c1 = `PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>`
        with True jmpOk wt_c1 G show ?thesis 
          by - (rule hyp_c1 [THEN conjunct1,rule_format (no_asm)],simp_all)
      next
        case False
        note hyp_c2 = `PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>`
        note `s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
        with False jmp have "abrupt s2 = Some (Jump j)"
          by (cases s2) (simp add: abrupt_if_def)
        with jmpOk wt_c2 G show ?thesis 
          by - (rule hyp_c2 [THEN conjunct1,rule_format (no_asm)],simp_all)
      qed
    }
    thus ?case by simp
  next
    case (Init C c s0 s3 s1 s2 jmps T Env)
    note `jumpNestingOk jmps (In1r (Init C))`
    note G = `prg Env = G`
    note `the (class G C) = c`
    with Init.prems have c: "class G C = Some c"
      by (elim wt_elim_cases) auto
    {
      fix j
      assume jmp: "abrupt s3 = (Some (Jump j))" 
      have "j\<in>jmps"
      proof (cases "inited C (globs s0)") 
        case True
        with Init.hyps have "s3=Norm s0"
          by simp
        with jmp
        have "False" by simp thus ?thesis ..
      next
        case False
        from wf c G
        have wf_cdecl: "wf_cdecl G (C,c)"
          by (simp add: wf_prog_cdecl)
        from Init.hyps
        have "?HypObj (In1r (if C = Object then Skip else Init (super c))) 
                            (Norm ((init_class_obj G C) s0)) s1 (\<diamondsuit>::vals)"
          apply (simp (no_asm_use) only: False if_False simp_thms)
          apply (erule conjE)+
          apply assumption
          done
        note hyp_s1 = this [rule_format (no_asm)]
        from wf_cdecl G have
          wt_super: "Env\<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
          by (cases "C=Object")
             (auto dest: wf_cdecl_supD is_acc_classD) 
        from hyp_s1 [OF _ _ wt_super G]
        have "?Jmp jmps s1" 
          by simp
        hence jmp_s1: "?Jmp jmps ((set_lvars empty) s1)" by (cases s1) simp
        from False Init.hyps
        have "?HypObj (In1r (init c)) ((set_lvars empty) s1) s2 (\<diamondsuit>::vals)" 
          apply (simp (no_asm_use) only: False if_False simp_thms)
          apply (erule conjE)+
          apply assumption
          done
        note hyp_init_c = this [rule_format (no_asm)] 
        from wf_cdecl 
        have wt_init_c: "\<lparr>prg = G, cls = C, lcl = empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
          by (rule wf_cdecl_wt_init)
        from wf_cdecl have "jumpNestingOkS {} (init c)" 
          by (cases rule: wf_cdeclE)
        hence "jumpNestingOkS jmps (init c)"
          by (rule jumpNestingOkS_mono) simp
        moreover 
        have "abrupt s2 = Some (Jump j)"
        proof -
          from False Init.hyps 
          have "s3 = (set_lvars (locals (store s1))) s2"  by simp
          with jmp show ?thesis by (cases s2) simp
        qed
        ultimately show ?thesis
          using hyp_init_c [OF jmp_s1 _ wt_init_c]
          by simp
      qed
    }
    thus ?case by simp
  next
    case (NewC s0 C s1 a s2 jmps T Env)
    {
      fix j
      assume jmp: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps"
      proof - 
        note `prg Env = G`
        moreover note hyp_init = `PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>`
        moreover from wf NewC.prems 
        have "Env\<turnstile>(Init C)\<Colon>\<surd>"
          by (elim wt_elim_cases) (drule is_acc_classD,simp)
        moreover 
        have "abrupt s1 = Some (Jump j)"
        proof -
          from `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2` and jmp show ?thesis
            by (rule halloc_no_jump')
        qed
        ultimately show "j \<in> jmps" 
          by - (rule hyp_init [THEN conjunct1,rule_format (no_asm)],auto)
      qed
    }
    thus ?case by simp
  next
    case (NewA s0 elT s1 e i s2 a s3 jmps T Env)
    {
      fix j
      assume jmp: "abrupt s3 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
	note G = `prg Env = G`
        from NewA.prems 
        obtain wt_init: "Env\<turnstile>init_comp_ty elT\<Colon>\<surd>" and 
               wt_size: "Env\<turnstile>e\<Colon>-PrimT Integer"
          by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
        note `PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>`
        with wt_init G 
        have "?Jmp jmps s1" 
          by (simp add: init_comp_ty_def)
        moreover
        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 i)`
        have "abrupt s2 = Some (Jump j)"
        proof -
          note `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
          moreover note jmp
          ultimately 
          have "abrupt (abupd (check_neg i) s2) = Some (Jump j)"
            by (rule halloc_no_jump')
          thus ?thesis by (cases s2) auto
        qed
        ultimately show "j\<in>jmps" using wt_size G 
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)],simp_all)
      qed
    }
    thus ?case by simp
  next
    case (Cast s0 e v s1 s2 cT jmps T Env)
    {
      fix j
      assume jmp: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
        note `prg Env = G`
        moreover from Cast.prems
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
        moreover 
        have "abrupt s1 = Some (Jump j)"
        proof -
          note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1`
          moreover note jmp
          ultimately show ?thesis by (cases s1) (simp add: abrupt_if_def)
        qed
        ultimately show ?thesis 
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
      qed
    }
    thus ?case by simp
  next
    case (Inst s0 e v s1 b eT jmps T Env)
    {
      fix j
      assume jmp: "abrupt s1 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
        note `prg Env = G`
        moreover from Inst.prems
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
        moreover note jmp
        ultimately show "j\<in>jmps" 
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all)
      qed
    }
    thus ?case by simp
  next
    case Lit thus ?case by simp
  next
    case (UnOp s0 e v s1 unop jmps T Env)
    {
      fix j
      assume jmp: "abrupt s1 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)`
        note `prg Env = G`
        moreover from UnOp.prems
        obtain eT where "Env\<turnstile>e\<Colon>-eT" by (elim wt_elim_cases)
        moreover note jmp
        ultimately show  "j\<in>jmps" 
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all) 
      qed
    }
    thus ?case by simp
  next
    case (BinOp s0 e1 v1 s1 binop e2 v2 s2 jmps T Env)
    {
      fix j
      assume jmp: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note G = `prg Env = G`
        from BinOp.prems
        obtain e1T e2T where 
          wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and
          wt_e2: "Env\<turnstile>e2\<Colon>-e2T" 
          by (elim wt_elim_cases)
        note `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)`
        with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
        note hyp_e2 =
          `PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
                     s1 s2 (In1 v2)`
        show "j\<in>jmps"
        proof (cases "need_second_arg binop v1")
          case True with jmp_s1 wt_e2 jmp G
          show ?thesis 
            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
        next
          case False with jmp_s1 jmp G
          show ?thesis 
            by - (rule hyp_e2 [THEN conjunct1,rule_format (no_asm)],auto)
        qed
      qed
    }
    thus ?case by simp
  next
    case Super thus ?case by simp
  next
    case (Acc s0 va v f s1 jmps T Env)
    {
      fix j
      assume jmp: "abrupt s1 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_va = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))`
        note `prg Env = G`
        moreover from Acc.prems
        obtain vT where "Env\<turnstile>va\<Colon>=vT" by (elim wt_elim_cases)
        moreover note jmp
        ultimately show "j\<in>jmps" 
          by - (rule hyp_va [THEN conjunct1,rule_format (no_asm)], simp_all)
      qed
    }
    thus ?case by simp
  next
    case (Ass s0 va w f s1 e v s2 jmps T Env)
    note G = `prg Env = G`
    from Ass.prems
    obtain vT eT where
      wt_va: "Env\<turnstile>va\<Colon>=vT" and
       wt_e: "Env\<turnstile>e\<Colon>-eT"
      by (elim wt_elim_cases)
    note hyp_v = `PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))`
    note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 v)`
    {
      fix j
      assume jmp: "abrupt (assign f v s2) = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        have "abrupt s2 = Some (Jump j)"
        proof (cases "normal s2")
          case True
          from `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2` and True have nrm_s1: "normal s1" 
            by (rule eval_no_abrupt_lemma [rule_format]) 
          with nrm_s1 wt_va G True
          have "abrupt (f v s2) \<noteq> Some (Jump j)"
            using hyp_v [THEN conjunct2,rule_format (no_asm)]
            by simp
          from this jmp
          show ?thesis
            by (rule assign_abrupt_propagation)
        next
          case False with jmp 
          show ?thesis by (cases s2) (simp add: assign_def Let_def)
        qed
        moreover from wt_va G
        have "?Jmp jmps s1"
          by - (rule hyp_v [THEN conjunct1],simp_all)
        ultimately show ?thesis using G 
          by - (rule hyp_e [THEN conjunct1,rule_format (no_asm)], simp_all, rule wt_e)
      qed
    }
    thus ?case by simp
  next
    case (Cond s0 e0 b s1 e1 e2 v s2 jmps T Env)
    note G = `prg Env = G`
    note hyp_e0 = `PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)`
    note hyp_e1_e2 = `PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)`
    from Cond.prems
    obtain e1T e2T
      where wt_e0: "Env\<turnstile>e0\<Colon>-PrimT Boolean"
       and  wt_e1: "Env\<turnstile>e1\<Colon>-e1T"
       and  wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt s2 = Some (Jump j)"
      have "j\<in>jmps" 
      proof -
        from wt_e0 G 
        have jmp_s1: "?Jmp jmps s1"
          by - (rule hyp_e0 [THEN conjunct1],simp_all)
        show ?thesis
        proof (cases "the_Bool b")
          case True
          with jmp_s1 wt_e1 G jmp
          show ?thesis
            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
        next
          case False
          with jmp_s1 wt_e2 G jmp
          show ?thesis
            by-(rule hyp_e1_e2 [THEN conjunct1,rule_format (no_asm)],simp_all)
        qed
      qed
    }
    thus ?case by simp
  next
    case (Call s0 e a s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4
               jmps T Env)
    note G = `prg Env = G`
    from Call.prems
    obtain eT argsT 
      where wt_e: "Env\<turnstile>e\<Colon>-eT" and wt_args: "Env\<turnstile>args\<Colon>\<doteq>argsT"
      by (elim wt_elim_cases)
    {
      fix j
      assume jmp: "abrupt ((set_lvars (locals (store s2))) s4) 
                     = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_e = `PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)`
        from wt_e G 
        have jmp_s1: "?Jmp jmps s1"
          by - (rule hyp_e [THEN conjunct1],simp_all)
        note hyp_args = `PROP ?Hyp (In3 args) s1 s2 (In3 vs)`
        have "abrupt s2 = Some (Jump j)"
        proof -
          note `G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4`
          moreover
          from jmp have "abrupt s4 = Some (Jump j)"
            by (cases s4) simp
          ultimately have "abrupt s3' = Some (Jump j)"
            by - (rule ccontr,drule (1) Methd_no_jump,simp)
          moreover note `s3' = check_method_access G accC statT mode 
                              \<lparr>name = mn, parTs = pTs\<rparr> a s3`
          ultimately have "abrupt s3 = Some (Jump j)"
            by (cases s3) 
               (simp add: check_method_access_def abrupt_if_def Let_def)
          moreover 
          note `s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2`
          ultimately show ?thesis
            by (cases s2) (auto simp add: init_lvars_def2)
        qed
        with jmp_s1 wt_args G
        show ?thesis
          by - (rule hyp_args [THEN conjunct1,rule_format (no_asm)], simp_all)
      qed
    }
    thus ?case by simp
  next
    case (Methd s0 D sig v s1 jmps T Env)
    from `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
    have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
      by (rule eval.Methd)
    hence "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
      by (rule Methd_no_jump) simp
    thus ?case by simp
  next
    case (Body s0 D s1 c s2 s3 jmps T Env)
    have "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
           \<rightarrow> abupd (absorb Ret) s3"
      by (rule eval.Body) (rule Body)+
    hence "\<And> j. abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump j)"
      by (rule Body_no_jump) simp
    thus ?case by simp
  next
    case LVar
    thus ?case by (simp add: lvar_def Let_def)
  next
    case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC jmps T Env)
    note G = `prg Env = G`
    from wf FVar.prems 
    obtain  statC f where
      wt_e: "Env\<turnstile>e\<Colon>-Class statC" and
      accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)"
      by  (elim wt_elim_cases) simp
    have wt_init: "Env\<turnstile>Init statDeclC\<Colon>\<surd>"
    proof -
      from wf wt_e G 
      have "is_class (prg Env) statC"
        by (auto dest: ty_expr_is_type type_is_class)
      with wf accfield G
      have "is_class (prg Env) statDeclC"
        by (auto dest!: accfield_fields dest: fields_declC)
      thus ?thesis
        by simp
    qed
    note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
    {
      fix j
      assume jmp: "abrupt s3 = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_init = `PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>`
        from G wt_init 
        have "?Jmp jmps s1"
          by - (rule hyp_init [THEN conjunct1],auto)
        moreover
        note hyp_e = `PROP ?Hyp (In1l e) s1 s2 (In1 a)`
        have "abrupt s2 = Some (Jump j)"
        proof -
          note `s3 = check_field_access G accC statDeclC fn stat a s2'`
          with jmp have "abrupt s2' = Some (Jump j)"
            by (cases s2') 
               (simp add: check_field_access_def abrupt_if_def Let_def)
         with fvar show "abrupt s2 =  Some (Jump j)"
            by (cases s2) (simp add: fvar_def2 abrupt_if_def)
        qed
        ultimately show ?thesis
          using G wt_e
          by - (rule hyp_e [THEN conjunct1, rule_format (no_asm)],simp_all)
      qed
    }
    moreover
    from fvar obtain upd w
      where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
              v: "v=(w,upd)"
      by (cases "fvar statDeclC stat fn a s2") simp
    {
      fix j val fix s::state
      assume "normal s3"
      assume no_jmp: "abrupt s \<noteq> Some (Jump j)"
      with upd
      have "abrupt (upd val s) \<noteq> Some (Jump j)"
        by (rule fvar_upd_no_jump)
    }
    ultimately show ?case using v by simp
  next
    case (AVar s0 e1 a s1 e2 i s2 v s2' jmps T Env)
    note G = `prg Env = G`
    from AVar.prems 
    obtain  e1T e2T where
      wt_e1: "Env\<turnstile>e1\<Colon>-e1T" and wt_e2: "Env\<turnstile>e2\<Colon>-e2T"
      by  (elim wt_elim_cases) simp
    note avar = `(v, s2') = avar G i a s2`
    {
      fix j
      assume jmp: "abrupt s2' = Some (Jump j)"
      have "j\<in>jmps"
      proof -
        note hyp_e1 = `PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)`
        from G wt_e1
        have "?Jmp jmps s1"
          by - (rule hyp_e1 [THEN conjunct1], auto)
        moreover
        note hyp_e2 = `PROP ?Hyp (In1l e2) s1 s2 (In1 i)`
        have "abrupt s2 = Some (Jump j)"
        proof -
          from avar have "s2' = snd (avar G i a s2)"
            by (cases "avar G i a s2") simp
          with jmp show ?thesis by - (rule avar_state_no_jump,simp) 
        qed  
        ultimately show ?thesis
          using wt_e2 G
          by - (rule hyp_e2 [THEN conjunct1, rule_format (no_asm)],simp_all)