Quelle DefiniteAssignmentCorrect.thy Sprache: Isabelle

subsection \<open>Correctness of Definite Assignment\<close>

theory DefiniteAssignmentCorrect imports WellForm Eval begin

declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]

lemma sxalloc_no_jump:
  assumes sxalloc: "G\s0 \sxalloc\ s1" and
           no_jmp: "abrupt s0 \ Some (Jump j)"
   shows "abrupt s1 \ Some (Jump j)"
using sxalloc no_jmp
by cases simp_all

lemma sxalloc_no_jump':
  assumes sxalloc: "G\s0 \sxalloc\ 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\s0 \halloc oi\a\ s1" and
           no_jmp: "abrupt s0 \ Some (Jump j)"
   shows "abrupt s1 \ Some (Jump j)"
using halloc no_jmp
by cases simp_all

lemma halloc_no_jump':
  assumes halloc: "G\s0 \halloc oi\a\ 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\s0 \Body D c-\v\s1" and
           jump: "abrupt s0 \ Some (Jump j)"
   shows "abrupt s1 \ Some (Jump j)"
proof (cases "normal s0")
  case True
  with eval obtain s0' where eval': "G\Norm s0' \Body D c-\v\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 "\l. abrupt s2 = Some (Jump (Break l)) \
                   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\(Some abr,s0') \Body D c-\v\s1"
                                 "s0 = (Some abr, s0')"
    by (cases s0) fastforce
  with this jump
  show ?thesis
    by (cases) (simp)
qed

lemma Methd_no_jump:
   assumes eval: "G\s0 \Methd D sig-\v\ s1" and
           jump: "abrupt s0 \ Some (Jump j)"
   shows "abrupt s1 \ Some (Jump j)"
proof (cases "normal s0")
  case True
   with eval obtain s0' where "G\Norm s0' \Methd D sig-\v\s1"
                              "s0 = Norm s0'"
    by (cases s0) simp
  then obtain D' body where "G\s0 \Body D' body-\v\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\(Some abr,s0') \Methd D sig-\v\s1"
                                 "s0 = (Some abr, s0')"
    by (cases s0) fastforce
  with this jump
  show ?thesis
    by (cases) (simp)
qed

lemma jumpNestingOkS_mono:
  assumes jumpNestingOk_l': "jumpNestingOkS jmps' c"
      and      subset: "jmps' \ jmps"
shows "jumpNestingOkS jmps c"
proof -
    have True and True and
       "\ jmps' jmps. \jumpNestingOkS jmps' c; jmps' \ jmps\ \ jumpNestingOkS jmps c"
  proof (induct rule: var.induct expr.induct stmt.induct)
    case (Lab j c jmps' jmps)
    note jmpOk = \<open>jumpNestingOkS jmps' (j\<bullet> c)\<close>
    note jmps = \<open>jmps' \<subseteq> jmps\<close>
    with jmpOk have "jumpNestingOkS ({j} \ jmps') c" by simp
    moreover from jmps have "({j} \ jmps') \ ({j} \ jmps)" by auto
    ultimately
    have "jumpNestingOkS ({j} \ 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)
    have "jumpNestingOkS jmps c1" by (rule Comp.hyps) (use Comp.prems in auto)
    moreover
    have "jumpNestingOkS jmps c2" by (rule Comp.hyps) (use Comp.prems in auto)
    ultimately show ?case by simp
  next
    case (If' e c1 c2 jmps' jmps)
    have "jumpNestingOkS jmps c1" by (rule If'.hyps) (use If'.prems in auto)
    moreover
    have "jumpNestingOkS jmps c2" by (rule If'.hyps) (use If'.prems in auto)
    ultimately show ?case by simp
  next
    case (Loop l e c jmps' jmps)
    from \<open>jumpNestingOkS jmps' (l\<bullet> While(e) c)\<close> have "jumpNestingOkS ({Cont l} \<union> jmps') c"
      by simp
    moreover
    from \<open>jmps' \<subseteq> jmps\<close> have "{Cont l} \<union> jmps'  \<subseteq> {Cont l} \<union> jmps"
      by auto
    ultimately have "jumpNestingOkS ({Cont l} \ jmps) c"
      by (rule Loop.hyps)
    thus ?case by simp
  next
    case (TryC c1 C vn c2 jmps' jmps)
    have "jumpNestingOkS jmps c1" by (rule TryC.hyps) (use TryC.prems in auto)
    moreover
    have "jumpNestingOkS jmps c2" by (rule TryC.hyps) (use TryC.prems in auto)
    ultimately show ?case
      by simp
  next
    case (Fin c1 c2 jmps' jmps)
    have "jumpNestingOkS jmps c1" by (rule Fin.hyps) (use Fin.prems in auto)
    moreover
    have "jumpNestingOkS jmps c2" by (rule Fin.hyps) (use Fin.prems in 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' \ 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) \ 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 \ Env\init_comp_ty T\\"
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 \ Some (Jump j)"
        shows "abrupt (upd val s) \ 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 \ Some (Jump j)"
        shows "abrupt (upd val s) \ Some (Jump j)"
using upd noJmp
by (cases s) (simp add: avar_def2 abrupt_if_def)

text \<open>
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>\<open>jumpNestingOk\<close> 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>\<open>Lab\<close> and \<^term>\<open>While\<close>.

The wellformedness of the program is used to enshure that for all
classinitialisations and methods the nesting of jumps is wellformed, too.
\<close>
theorem jumpNestingOk_eval:
  assumes eval: "G\ s0 \t\\ (v,s1)"
     and jmpOk: "jumpNestingOk jmps t"
     and wt: "Env\t\T"
     and wf: "wf_prog G"
     and  G: "prg Env = G"
     and no_jmp: "\j. abrupt s0 = Some (Jump j) \ j \ jmps"
                    (is "?Jmp jmps s0")
  shows  "(\j. fst s1 = Some (Jump j) \ j \ jmps) \
                 (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 \ ?Upd v s1")
proof -
  let ?HypObj = "\ 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)"
  \<comment> \<open>Variable \<open>?HypObj\<close> 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.\<close>
  from eval
  have "\ jmps T Env. \?Jmp jmps s0; jumpNestingOk jmps t; Env\t\T;prg Env=G\
            \<Longrightarrow> ?Jmp jmps s1 \<and> ?Upd v s1"
        (is "PROP ?Hyp t s0 s1 v")
  \<comment> \<open>We need to abstract over \<^term>\<open>jmps\<close> since \<^term>\<open>jmps\<close> are extended
        during analysis of \<^term>\<open>Lab\<close>. Also we need to abstract over
        \<^term>\<open>T\<close> and \<^term>\<open>Env\<close> since they are altered in various
        typing judgements.\<close>
  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 = \<open>jumpNestingOk jmps (In1r (jmp\<bullet> c))\<close>
    note G = \<open>prg Env = G\<close>
    have wt_c: "Env\c\\"
      using Lab.prems by (elim wt_elim_cases)
    have "j\jmps" if ab_s1: "abrupt (abupd (absorb jmp) s1) = Some (Jump j)" for j
    proof -
      from ab_s1 have jmp_s1: "abrupt s1 = Some (Jump j)"
        by (cases s1) (simp add: absorb_def)
      note hyp_c = \<open>PROP ?Hyp (In1r c) (Norm s0) s1 \<diamondsuit>\<close>
      from ab_s1 have "j \ jmp"
        by (cases s1) (simp add: absorb_def)
      moreover have "j \ {jmp} \ jmps"
      proof -
        from jmpOK
        have "jumpNestingOk ({jmp} \ 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 = \<open>jumpNestingOk jmps (In1r (c1;; c2))\<close>
    note G = \<open>prg Env = G\<close>
    from Comp.prems obtain
      wt_c1: "Env\c1\\" and wt_c2: "Env\c2\\"
      by (elim wt_elim_cases)
    have "j\jmps" if abr_s2: "abrupt s2 = Some (Jump j)" for j
    proof -
      have jmp: "?Jmp jmps s1"
      proof -
        note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 \<diamondsuit>\<close>
        with wt_c1 jmpOk G
        show ?thesis by simp
      qed
      moreover note hyp_c2 = \<open>PROP ?Hyp (In1r c2) s1 s2 (\<diamondsuit>::vals)\<close>
      have jmpOk': "jumpNestingOk jmps (In1r c2)" using jmpOk by simp
      moreover note wt_c2 G abr_s2
      ultimately show "j \ 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 = \<open>jumpNestingOk jmps (In1r (If(e) c1 Else c2))\<close>
    note G = \<open>prg Env = G\<close>
    from If.prems obtain
              wt_e: "Env\e\-PrimT Boolean" and
      wt_then_else: "Env\(if the_Bool b then c1 else c2)\\"
      by (elim wt_elim_cases) simp
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    proof -
      note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
      with wt_e G have "?Jmp jmps s1"
        by simp
      moreover note hyp_then_else =
        \<open>PROP ?Hyp (In1r (if the_Bool b then c1 else c2)) s1 s2 \<diamondsuit>\<close>
      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\ 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 = \<open>jumpNestingOk jmps (In1r (l\<bullet> While(e) c))\<close>
    note G = \<open>prg Env = G\<close>
    note wt = \<open>Env\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T\<close>
    then obtain
              wt_e: "Env\e\-PrimT Boolean" and
              wt_c: "Env\c\\"
      by (elim wt_elim_cases)
    have "j\jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
    proof -
      note \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 b)\<close>
      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 \ 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 (\::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} \ jmps) (In1r c)"
          by simp
        moreover from jmp_s1 have "?Jmp ({Cont l} \ jmps) s1" by simp
        ultimately have jmp_s2: "?Jmp ({Cont l} \ jmps) s2"
          using wt_c G by iprover
        have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
        proof -
          have "j' \ jmps" if abs: "abrupt (abupd (absorb (Cont l)) s2)=Some (Jump j')" for j'
          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\ 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\ 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 = \<open>jumpNestingOk jmps (In1r (Throw e))\<close>
    note G = \<open>prg Env = G\<close>
    from Throw.prems obtain Te where
      wt_e: "Env\e\-Te"
      by (elim wt_elim_cases)
    have "j\jmps" if jmp: "abrupt (abupd (throw a) s1) = Some (Jump j)" for j
    proof -
      from \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
      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 \ jmps" by simp
    qed
    thus ?case by simp
  next
    case (Try s0 c1 s1 s2 C vn c2 s3 jmps T Env)
    note jmpOk = \<open>jumpNestingOk jmps (In1r (Try c1 Catch(C vn) c2))\<close>
    note G = \<open>prg Env = G\<close>
    from Try.prems obtain
      wt_c1: "Env\c1\\" and
      wt_c2: "Env\lcl := (lcl Env)(VName vn\Class C)\\c2\\"
      by (elim wt_elim_cases)
    have "j\jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
    proof -
      note \<open>PROP ?Hyp (In1r c1) (Norm s0) s1 (\<diamondsuit>::vals)\<close>
      with jmpOk wt_c1 G
      have jmp_s1: "?Jmp jmps s1" by simp
      note s2 = \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
      show "j \ jmps"
      proof (cases "G,s2\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 (\::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\lcl := (lcl Env)(VName vn\Class C)\) = 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 = \<open>jumpNestingOk jmps (In1r (c1 Finally c2))\<close>
    note G = \<open>prg Env = G\<close>
    from Fin.prems obtain
      wt_c1: "Env\c1\\" and wt_c2: "Env\c2\\"
      by (elim wt_elim_cases)
    have "j \ jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
    proof (cases "x1=Some (Jump j)")
      case True
      note hyp_c1 = \<open>PROP ?Hyp (In1r c1) (Norm s0) (x1,s1) \<diamondsuit>\<close>
      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 = \<open>PROP ?Hyp (In1r c2) (Norm s1) s2 \<diamondsuit>\<close>
      note \<open>s3 = (if \<exists>err. x1 = Some (Error err) then (x1, s1)
                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)\<close>
      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 \<open>jumpNestingOk jmps (In1r (Init C))\<close>
    note G = \<open>prg Env = G\<close>
    note \<open>the (class G C) = c\<close>
    with Init.prems have c: "class G C = Some c"
      by (elim wt_elim_cases) auto
    have "j\jmps" if jmp: "abrupt s3 = (Some (Jump j))" for j
    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\(if C = Object then Skip else Init (super c))\\"
        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 Map.empty) s1)" by (cases s1) simp
      from False Init.hyps
      have "?HypObj (In1r (init c)) ((set_lvars Map.empty) s1) s2 (\::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: "\prg = G, cls = C, lcl = Map.empty\\init c\\"
        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)
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    proof -
      note \<open>prg Env = G\<close>
      moreover note hyp_init = \<open>PROP ?Hyp (In1r (Init C)) (Norm s0) s1 \<diamondsuit>\<close>
      moreover from wf NewC.prems
      have "Env\(Init C)\\"
        by (elim wt_elim_cases) (drule is_acc_classD,simp)
      moreover
      have "abrupt s1 = Some (Jump j)"
      proof -
        from \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close> and jmp show ?thesis
          by (rule halloc_no_jump')
      qed
      ultimately show "j \ 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)
    have "j\jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
    proof -
      note G = \<open>prg Env = G\<close>
      from NewA.prems
      obtain wt_init: "Env\init_comp_ty elT\\" and
        wt_size: "Env\e\-PrimT Integer"
        by (elim wt_elim_cases) (auto dest:  wt_init_comp_ty')
      note \<open>PROP ?Hyp (In1r (init_comp_ty elT)) (Norm s0) s1 \<diamondsuit>\<close>
      with wt_init G
      have "?Jmp jmps s1"
        by (simp add: init_comp_ty_def)
      moreover
      note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 i)\<close>
      have "abrupt s2 = Some (Jump j)"
      proof -
        note \<open>G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3\<close>
        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\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)
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    proof -
      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
      note \<open>prg Env = G\<close>
      moreover from Cast.prems
      obtain eT where "Env\e\-eT" by (elim wt_elim_cases)
      moreover
      have "abrupt s1 = Some (Jump j)"
      proof -
        note \<open>s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits cT) ClassCast) s1\<close>
        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)
    have "j\jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
    proof -
      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
      note \<open>prg Env = G\<close>
      moreover from Inst.prems
      obtain eT where "Env\e\-eT" by (elim wt_elim_cases)
      moreover note jmp
      ultimately show "j\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)
    have "j\jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
    proof -
      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
      note \<open>prg Env = G\<close>
      moreover from UnOp.prems obtain eT where "Env\e\-eT" by (elim wt_elim_cases)
      moreover note jmp
      ultimately show "j\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)
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    proof -
      note G = \<open>prg Env = G\<close>
      from BinOp.prems
      obtain e1T e2T where
        wt_e1: "Env\e1\-e1T" and
        wt_e2: "Env\e2\-e2T"
        by (elim wt_elim_cases)
      note \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 v1)\<close>
      with G wt_e1 have jmp_s1: "?Jmp jmps s1" by simp
      note hyp_e2 =
        \<open>PROP ?Hyp (if need_second_arg binop v1 then In1l e2 else In1r Skip)
                     s1 s2 (In1 v2)\<close>
      show "j\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)
    have "j\jmps" if jmp: "abrupt s1 = Some (Jump j)" for j
    proof -
      note hyp_va = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (v,f))\<close>
      note \<open>prg Env = G\<close>
      moreover from Acc.prems
      obtain vT where "Env\va\=vT" by (elim wt_elim_cases)
      moreover note jmp
      ultimately show "j\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 = \<open>prg Env = G\<close>
    from Ass.prems
    obtain vT eT where
      wt_va: "Env\va\=vT" and
       wt_e: "Env\e\-eT"
      by (elim wt_elim_cases)
    note hyp_v = \<open>PROP ?Hyp (In2 va) (Norm s0) s1 (In2 (w,f))\<close>
    note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 v)\<close>
    have "j\jmps" if jmp: "abrupt (assign f v s2) = Some (Jump j)" for j
    proof -
      have "abrupt s2 = Some (Jump j)"
      proof (cases "normal s2")
        case True
        from \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close> 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) \ 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 = \<open>prg Env = G\<close>
    note hyp_e0 = \<open>PROP ?Hyp (In1l e0) (Norm s0) s1 (In1 b)\<close>
    note hyp_e1_e2 = \<open>PROP ?Hyp (In1l (if the_Bool b then e1 else e2)) s1 s2 (In1 v)\<close>
    from Cond.prems
    obtain e1T e2T
      where wt_e0: "Env\e0\-PrimT Boolean"
       and  wt_e1: "Env\e1\-e1T"
       and  wt_e2: "Env\e2\-e2T"
      by (elim wt_elim_cases)
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    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 = \<open>prg Env = G\<close>
    from Call.prems
    obtain eT argsT
      where wt_e: "Env\e\-eT" and wt_args: "Env\args\\argsT"
      by (elim wt_elim_cases)
    have "j\jmps" if jmp: "abrupt ((set_lvars (locals (store s2))) s4) = Some (Jump j)" for j
    proof -
      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 a)\<close>
      from wt_e G
      have jmp_s1: "?Jmp jmps s1"
        by - (rule hyp_e [THEN conjunct1],simp_all)
      note hyp_args = \<open>PROP ?Hyp (In3 args) s1 s2 (In3 vs)\<close>
      have "abrupt s2 = Some (Jump j)"
      proof -
        note \<open>G\<turnstile>s3' \<midarrow>Methd D \<lparr>name = mn, parTs = pTs\<rparr>-\<succ>v\<rightarrow> s4\<close>
        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 \<open>s3' = check_method_access G accC statT mode
                              \<lparr>name = mn, parTs = pTs\<rparr> a s3\<close>
        ultimately have "abrupt s3 = Some (Jump j)"
          by (cases s3)
            (simp add: check_method_access_def abrupt_if_def Let_def)
        moreover
        note \<open>s3 = init_lvars G D \<lparr>name=mn, parTs=pTs\<rparr> mode a vs s2\<close>
        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 \<open>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<close>
    have "G\Norm s0 \Methd D sig-\v\ s1"
      by (rule eval.Methd)
    hence "\ j. abrupt s1 \ 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\Norm s0 \Body D c-\the (locals (store s2) Result)
           \<rightarrow> abupd (absorb Ret) s3"
      by (rule eval.Body) (rule Body)+
    hence "\ j. abrupt (abupd (absorb Ret) s3) \ 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 = \<open>prg Env = G\<close>
    from wf FVar.prems
    obtain  statC f where
      wt_e: "Env\e\-Class statC" and
      accfield: "accfield (prg Env) accC statC fn = Some (statDeclC,f)"
      by  (elim wt_elim_cases) simp
    have wt_init: "Env\Init statDeclC\\"
    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 = \<open>(v, s2') = fvar statDeclC stat fn a s2\<close>
    have "j\jmps" if jmp: "abrupt s3 = Some (Jump j)" for j
    proof -
      note hyp_init = \<open>PROP ?Hyp (In1r (Init statDeclC)) (Norm s0) s1 \<diamondsuit>\<close>
      have "?Jmp jmps s1"
        by (rule hyp_init [THEN conjunct1]) (use G wt_init in auto)
      moreover
      note hyp_e = \<open>PROP ?Hyp (In1l e) s1 s2 (In1 a)\<close>
      have "abrupt s2 = Some (Jump j)"
      proof -
        note \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
        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, use surjective_pairing in blast)
    have "abrupt (upd val s) \ Some (Jump j)"
      if "abrupt s \ Some (Jump j)"
      for j val and s::state
      using upd that 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 = \<open>prg Env = G\<close>
    from AVar.prems
    obtain  e1T e2T where
      wt_e1: "Env\e1\-e1T" and wt_e2: "Env\e2\-e2T"
      by  (elim wt_elim_cases) simp
    note avar = \<open>(v, s2') = avar G i a s2\<close>
    have "j\jmps" if jmp: "abrupt s2' = Some (Jump j)" for j
    proof -
      note hyp_e1 = \<open>PROP ?Hyp (In1l e1) (Norm s0) s1 (In1 a)\<close>
      from G wt_e1
      have "?Jmp jmps s1"
        by - (rule hyp_e1 [THEN conjunct1], auto)
      moreover
      note hyp_e2 = \<open>PROP ?Hyp (In1l e2) s1 s2 (In1 i)\<close>
      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)
    qed
    moreover
    from avar obtain upd w
      where upd: "upd = snd (fst (avar G i a s2))" and
              v: "v=(w,upd)"
      by (cases "avar G i a s2")
        (simp, use surjective_pairing in blast)
    have "abrupt (upd val s) \ Some (Jump j)" if "abrupt s \ Some (Jump j)"
      for j val and s::state
      using upd that by (rule avar_upd_no_jump)
    ultimately show ?case using v by simp
  next
    case Nil
    thus ?case by simp
  next
    case (Cons s0 e v s1 es vs s2 jmps T Env)
    note G = \<open>prg Env = G\<close>
    from Cons.prems obtain eT esT
      where wt_e: "Env\e\-eT" and wt_e2: "Env\es\\esT"
      by  (elim wt_elim_cases) simp
    have "j\jmps" if jmp: "abrupt s2 = Some (Jump j)" for j
    proof -
      note hyp_e = \<open>PROP ?Hyp (In1l e) (Norm s0) s1 (In1 v)\<close>
      from G wt_e
      have "?Jmp jmps s1"
        by - (rule hyp_e [THEN conjunct1],simp_all)
      moreover
      note hyp_es = \<open>PROP ?Hyp (In3 es) s1 s2 (In3 vs)\<close>
      ultimately show ?thesis
        using wt_e2 G jmp
        by - (rule hyp_es [THEN conjunct1, rule_format (no_asm)],
            (assumption|simp (no_asm_simp))+)
    qed
    thus ?case by simp
  qed
  note generalized = this
  from no_jmp jmpOk wt G
  show ?thesis
    by (rule generalized)
qed

lemmas jumpNestingOk_evalE = jumpNestingOk_eval [THEN conjE,rule_format]

lemma jumpNestingOk_eval_no_jump:
assumes    eval: "prg Env\ s0 \t\\ (v,s1)" and
           jmpOk: "jumpNestingOk {} t" and
          no_jmp: "abrupt s0 \ Some (Jump j)" and
              wt: "Env\t\T" and
              wf: "wf_prog (prg Env)"
shows "abrupt s1 \ Some (Jump j) \
        (normal s1 \<longrightarrow> v=In2 (w,upd)
         \<longrightarrow> abrupt s \<noteq> Some (Jump j')
         \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j'))"
proof (cases "\ j'. abrupt s0 = Some (Jump j')")
  case True
  then obtain j' where jmp: "abrupt s0 = Some (Jump j')" ..
  with no_jmp have "j'\j" by simp
  with eval jmp have "s1=s0" by auto
  with no_jmp jmp show ?thesis by simp
next
  case False
  obtain G where G: "prg Env = G"
    by (cases Env) simp
  from G eval have "G\ s0 \t\\ (v,s1)" by simp
  moreover note jmpOk wt
  moreover from G wf have "wf_prog G" by simp
  moreover note G
  moreover from False have "\ j. abrupt s0 = Some (Jump j) \ j \ {}"
    by simp
  ultimately show ?thesis
    apply (rule jumpNestingOk_evalE)
    apply assumption
    apply simp
    apply fastforce
    done
qed

lemmas jumpNestingOk_eval_no_jumpE
       = jumpNestingOk_eval_no_jump [THEN conjE,rule_format]

corollary eval_expression_no_jump:
  assumes eval: "prg Env\s0 \e-\v\ s1" and
        no_jmp: "abrupt s0 \ Some (Jump j)" and
        wt: "Env\e\-T" and
        wf: "wf_prog (prg Env)"
  shows "abrupt s1 \ Some (Jump j)"
using eval _ no_jmp wt wf
by (rule jumpNestingOk_eval_no_jumpE, simp_all)

corollary eval_var_no_jump:
  assumes eval: "prg Env\s0 \var=\(w,upd)\ s1" and
        no_jmp: "abrupt s0 \ Some (Jump j)" and
        wt: "Env\var\=T" and
        wf: "wf_prog (prg Env)"
  shows "abrupt s1 \ Some (Jump j) \
         (normal s1 \<longrightarrow>
          (abrupt s \<noteq> Some (Jump j')
           \<longrightarrow> abrupt (upd val s) \<noteq> Some (Jump j')))"
apply (rule_tac upd="upd" and val="val" and s="s" and w="w" and j'=j'
         in jumpNestingOk_eval_no_jumpE [OF eval _ no_jmp wt wf])
by simp_all

lemmas eval_var_no_jumpE = eval_var_no_jump [THEN conjE,rule_format]

corollary eval_statement_no_jump:
  assumes eval: "prg Env\s0 \c\ s1" and
         jmpOk: "jumpNestingOkS {} c" and
        no_jmp: "abrupt s0 \ Some (Jump j)" and
        wt: "Env\c\\" and
        wf: "wf_prog (prg Env)"
  shows "abrupt s1 \ Some (Jump j)"
using eval _ no_jmp wt wf
by (rule jumpNestingOk_eval_no_jumpE) (simp_all add: jmpOk)

corollary eval_expression_list_no_jump:
  assumes eval: "prg Env\s0 \es\\v\ s1" and
        no_jmp: "abrupt s0 \ Some (Jump j)" and
        wt: "Env\es\\T" and
        wf: "wf_prog (prg Env)"
  shows "abrupt s1 \ Some (Jump j)"
using eval _ no_jmp wt wf
by (rule jumpNestingOk_eval_no_jumpE, simp_all)

(* ### FIXME: Do i need this *)
lemma union_subseteq_elim [elim]: "\A \ B \ C; \A \ C; B \ C\ \ P\ \ P"
  by blast

lemma dom_locals_halloc_mono:
  assumes halloc: "G\s0\halloc oi\a\s1"
  shows "dom (locals (store s0)) \ dom (locals (store s1))"
proof -
  from halloc show ?thesis
    by cases simp_all
qed

lemma dom_locals_sxalloc_mono:
  assumes sxalloc: "G\s0\sxalloc\s1"
  shows "dom (locals (store s0)) \ dom (locals (store s1))"
proof -
  from sxalloc show ?thesis
  proof (cases)
    case Norm thus ?thesis by simp
  next
    case Jmp thus ?thesis by simp
  next
    case Error thus ?thesis by simp
  next
    case XcptL thus ?thesis by simp
  next
    case SXcpt thus ?thesis
      by - (drule dom_locals_halloc_mono,simp)
  qed
qed


lemma dom_locals_assign_mono:
assumes f_ok: "dom (locals (store s)) \ dom (locals (store (f n s)))"
   shows  "dom (locals (store s)) \ dom (locals (store (assign f n s)))"
proof (cases "normal s")
  case False thus ?thesis
    by (cases s) (auto simp add: assign_def Let_def)
next
  case True
  then obtain s' where s': "s = (None,s')"
    by auto
  moreover
  obtain x1 s1 where "f n s = (x1,s1)"
    by (cases "f n s")
  ultimately
  show ?thesis
    using f_ok
    by (simp add: assign_def Let_def)
qed

(*
lemma dom_locals_init_lvars_mono:
"dom (locals (store s))
   \<subseteq> dom (locals (store (init_lvars G D sig mode a vs s)))"
proof (cases "mode = Static")
  case True
  thus ?thesis
    apply (cases s)
    apply (simp add: init_lvars_def Let_def)
*)

lemma dom_locals_lvar_mono:
"dom (locals (store s)) \ dom (locals (store (snd (lvar vn s') val s)))"
by (simp add: lvar_def) blast

lemma dom_locals_fvar_vvar_mono:
"dom (locals (store s))
  \<subseteq> dom (locals (store (snd (fst (fvar statDeclC stat fn a s')) val s)))"
proof (cases stat)
  case True
  thus ?thesis
    by (cases s) (simp add: fvar_def2)
next
  case False
  thus ?thesis
    by (cases s) (simp add: fvar_def2)
qed

lemma dom_locals_fvar_mono:
"dom (locals (store s))
  \<subseteq> dom (locals (store (snd (fvar statDeclC stat fn a s))))"
proof (cases stat)
  case True
  thus ?thesis
    by (cases s) (simp add: fvar_def2)
next
  case False
  thus ?thesis
    by (cases s) (simp add: fvar_def2)
qed

lemma dom_locals_avar_vvar_mono:
"dom (locals (store s))
  \<subseteq> dom (locals (store (snd (fst (avar G i a s')) val s)))"
by (cases s, simp add: avar_def2)

lemma dom_locals_avar_mono:
"dom (locals (store s))
  \<subseteq> dom (locals (store (snd (avar G i a s))))"
by (cases s, simp add: avar_def2)

  text \<open>
Since assignments are modelled as functions from states to states, we
  must take into account these functions. They  appear only in the assignment
  rule and as result from evaluating a variable. Thats why we need the
  complicated second part of the conjunction in the goal.
The reason for the very generic way to treat assignments was the aim
to omit redundancy. There is only one evaluation rule for each kind of
variable (locals, fields, arrays). These rules are used for both accessing
variables and updating variables. Thats why the evaluation rules for variables
result in a pair consisting of a value and an update function. Of course we
could also think of a pair of a value and a reference in the store, instead of
the generic update function. But as only array updates can cause a special
exception (if the types mismatch) and not array reads we then have to introduce
two different rules to handle array reads and updates\<close>
lemma dom_locals_eval_mono:
  assumes   eval: "G\ s0 \t\\ (v,s1)"
  shows "dom (locals (store s0)) \ dom (locals (store s1)) \
         (\<forall> vv. v=In2 vv \<and> normal s1
            \<longrightarrow> (\<forall> s val. dom (locals (store s))
                           \<subseteq> dom (locals (store ((snd vv) val s)))))"
proof -
  from eval show ?thesis
  proof (induct)
    case Abrupt thus ?case by simp
  next
    case Skip thus ?case by simp
  next
    case Expr thus ?case by simp
  next
    case Lab thus ?case by simp
  next
    case (Comp s0 c1 s1 c2 s2)
    from Comp.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from Comp.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    finally show ?case by simp
  next
    case (If s0 e b s1 c1 c2 s2)
    from If.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from If.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    finally show ?case by simp
  next
    case (Loop s0 e b s1 c s2 l s3)
    show ?case
    proof (cases "the_Bool b")
      case True
      with Loop.hyps
      obtain
        s0_s1:
        "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))" and
        s1_s2: "dom (locals (store s1)) \ dom (locals (store s2))" and
        s2_s3: "dom (locals (store s2)) \ dom (locals (store s3))"
        by simp
      note s0_s1 also note s1_s2 also note s2_s3
      finally show ?thesis
        by simp
    next
      case False
      with Loop.hyps show ?thesis
        by simp
    qed
  next
    case Jmp thus ?case by simp
  next
    case Throw thus ?case by simp
  next
    case (Try s0 c1 s1 s2 C vn c2 s3)
    then
    have s0_s1: "dom (locals (store ((Norm s0)::state)))
                  \<subseteq> dom (locals (store s1))" by simp
    from \<open>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2\<close>
    have s1_s2: "dom (locals (store s1)) \ dom (locals (store s2))"
      by (rule dom_locals_sxalloc_mono)
    thus ?case
    proof (cases "G,s2\catch C")
      case True
      note s0_s1 also note s1_s2
      also
      from True Try.hyps
      have "dom (locals (store (new_xcpt_var vn s2)))
              \<subseteq> dom (locals (store s3))"
        by simp
      hence "dom (locals (store s2)) \ dom (locals (store s3))"
        by (cases s2, simp )
      finally show ?thesis by simp
    next
      case False
      note s0_s1 also note s1_s2
      finally
      show ?thesis
        using False Try.hyps by simp
    qed
  next
    case (Fin s0 c1 x1 s1 c2 s2 s3)
    show ?case
    proof (cases "\err. x1 = Some (Error err)")
      case True
      with Fin.hyps show ?thesis
        by simp
    next
      case False
      from Fin.hyps
      have "dom (locals (store ((Norm s0)::state)))
             \<subseteq> dom (locals (store (x1, s1)))"
        by simp
      hence "dom (locals (store ((Norm s0)::state)))
              \<subseteq> dom (locals (store ((Norm s1)::state)))"
        by simp
      also
      from Fin.hyps
      have "\ \ dom (locals (store s2))"
        by simp
      finally show ?thesis
        using Fin.hyps by simp
    qed
  next
    case (Init C c s0 s3 s1 s2)
    show ?case
    proof (cases "inited C (globs s0)")
      case True
      with Init.hyps show ?thesis by simp
    next
      case False
      with Init.hyps
      obtain s0_s1: "dom (locals (store (Norm ((init_class_obj G C) s0))))
                     \<subseteq> dom (locals (store s1))" and
             s3: "s3 = (set_lvars (locals (snd s1))) s2"
        by simp
      from s0_s1
      have "dom (locals (store (Norm s0))) \ dom (locals (store s1))"
        by (cases s0) simp
      with s3
      have "dom (locals (store (Norm s0))) \ dom (locals (store s3))"
        by (cases s2) simp
      thus ?thesis by simp
    qed
  next
    case (NewC s0 C s1 a s2)
    note halloc = \<open>G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2\<close>
    from NewC.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from halloc
    have "\ \ dom (locals (store s2))" by (rule dom_locals_halloc_mono)
    finally show ?case by simp
  next
    case (NewA s0 T s1 e i s2 a s3)
    note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
    from NewA.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from NewA.hyps
    have "\ \ dom (locals (store s2))" by simp
    also
    from halloc
    have "\ \ dom (locals (store s3))"
      by (rule dom_locals_halloc_mono [elim_format]) simp
    finally show ?case by simp
  next
    case Cast thus ?case by simp
  next
    case Inst thus ?case by simp
  next
    case Lit thus ?case by simp
  next
    case UnOp thus ?case by simp
  next
    case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
    from BinOp.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from BinOp.hyps
    have "\ \ dom (locals (store s2))" by simp
    finally show ?case by simp
  next
    case Super thus ?case by simp
  next
    case Acc thus ?case by simp
  next
    case (Ass s0 va w f s1 e v s2)
    from Ass.hyps
    have s0_s1:
      "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    show ?case
    proof (cases "normal s1")
      case True
      with Ass.hyps
      have ass_ok:
        "\ s val. dom (locals (store s)) \ dom (locals (store (f val s)))"
        by simp
      note s0_s1
      also
      from Ass.hyps
      have "dom (locals (store s1)) \ dom (locals (store s2))"
        by simp
      also
      from ass_ok
      have "\ \ dom (locals (store (assign f v s2)))"
        by (rule dom_locals_assign_mono [where f = f])
      finally show ?thesis by simp
    next
      case False
      with \<open>G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2\<close>
      have "s2=s1"
        by auto
      with s0_s1 False
      have "dom (locals (store ((Norm s0)::state)))
            \<subseteq> dom (locals (store (assign f v s2)))"
        by simp
      thus ?thesis
        by simp
    qed
  next
    case (Cond s0 e0 b s1 e1 e2 v s2)
    from Cond.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from Cond.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    finally show ?case by simp
  next
    case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
    note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
    from Call.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from Call.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    also
    have "\ \ dom (locals (store ((set_lvars (locals (store s2))) s4)))"
      by (cases s4) simp
    finally show ?case by simp
  next
    case Methd thus ?case by simp
  next
    case (Body s0 D s1 c s2 s3)
    from Body.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from Body.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    also
    have "\ \ dom (locals (store (abupd (absorb Ret) s2)))"
      by simp
    also
    have "\ \ dom (locals (store (abupd (absorb Ret) s3)))"
    proof -
      from \<open>s3 =
         (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)\<close>
      show ?thesis
        by simp
    qed
    finally show ?case by simp
  next
    case LVar
    thus ?case
      using dom_locals_lvar_mono
      by simp
  next
    case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
    from FVar.hyps
    obtain s2': "s2' = snd (fvar statDeclC stat fn a s2)" and
             v: "v = fst (fvar statDeclC stat fn a s2)"
      by (cases "fvar statDeclC stat fn a s2" ) simp
    from v
    have "\s val. dom (locals (store s))
                          \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")
      by (simp add: dom_locals_fvar_vvar_mono)
    hence v_ok: "(\vv. In2 v = In2 vv \ normal s3 \ ?V_ok)"
      by - (intro strip, simp)
    note s3 = \<open>s3 = check_field_access G accC statDeclC fn stat a s2'\<close>
    from FVar.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from FVar.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    also
    from s2'
    have "\ \ dom (locals (store s2'))"
      by (simp add: dom_locals_fvar_mono)
    also
    from s3
    have "\ \ dom (locals (store s3))"
      by (simp add: check_field_access_def Let_def)
    finally
    show ?case
      using v_ok
      by simp
  next
    case (AVar s0 e1 a s1 e2 i s2 v s2')
    from AVar.hyps
    obtain s2': "s2' = snd (avar G i a s2)" and
             v: "v = fst (avar G i a s2)"
      by (cases "avar G i a s2") simp
    from v
    have "\s val. dom (locals (store s))
                          \<subseteq> dom (locals (store (snd v val s)))" (is "?V_ok")
      by (simp add: dom_locals_avar_vvar_mono)
    hence v_ok: "(\vv. In2 v = In2 vv \ normal s2' \ ?V_ok)"
      by - (intro strip, simp)
    from AVar.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from AVar.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    also
    from s2'
    have "\ \ dom (locals (store s2'))"
      by (simp add: dom_locals_avar_mono)
    finally
    show ?case using v_ok by simp
  next
    case Nil thus ?case by simp
  next
    case (Cons s0 e v s1 es vs s2)
    from Cons.hyps
    have "dom (locals (store ((Norm s0)::state))) \ dom (locals (store s1))"
      by simp
    also
    from Cons.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    finally show ?case by simp
  qed
qed

lemma dom_locals_eval_mono_elim:
  assumes   eval: "G\ s0 \t\\ (v,s1)"
  obtains "dom (locals (store s0)) \ dom (locals (store s1))" and
    "\ vv s val. \v=In2 vv; normal s1\
                        \<Longrightarrow> dom (locals (store s))
                             \<subseteq> dom (locals (store ((snd vv) val s)))"
  using eval by (rule dom_locals_eval_mono [THEN conjE]) (rule that, auto)

lemma halloc_no_abrupt:
  assumes halloc: "G\s0\halloc oi\a\s1" and
          normal: "normal s1"
  shows "normal s0"
proof -
  from halloc normal show ?thesis
    by cases simp_all
qed

lemma sxalloc_mono_no_abrupt:
  assumes sxalloc: "G\s0\sxalloc\s1" and
           normal: "normal s1"
  shows "normal s0"
proof -
  from sxalloc normal show ?thesis
    by cases simp_all
qed

lemma union_subseteqI: "\A \ B \ C; A' \ A; B' \ B\ \ A' \ B' \ C"
  by blast

lemma union_subseteqIl: "\A \ B \ C; A' \ A\ \ A' \ B \ C"
  by blast

lemma union_subseteqIr: "\A \ B \ C; B' \ B\ \ A \ B' \ C"
  by blast

lemma subseteq_union_transl [trans]: "\A \ B; B \ C \ D\ \ A \ C \ D"
  by blast

lemma subseteq_union_transr [trans]: "\A \ B; C \ B \ D\ \ A \ C \ D"
  by blast

lemma union_subseteq_weaken: "\A \ B \ C; \A \ C; B \ C\ \ P \ \ P"
  by blast

lemma assigns_good_approx:
  assumes
      eval: "G\ s0 \t\\ (v,s1)" and
    normal: "normal s1"
  shows "assigns t \ dom (locals (store s1))"
proof -
  from eval normal show ?thesis
  proof (induct)
    case Abrupt thus ?case by simp
  next \<comment> \<open>For statements its trivial, since then \<^term>\<open>assigns t = {}\<close>\<close>
    case Skip show ?case by simp
  next
    case Expr show ?case by simp
  next
    case Lab show ?case by simp
  next
    case Comp show ?case by simp
  next
    case If show ?case by simp
  next
    case Loop show ?case by simp
  next
    case Jmp show ?case by simp
  next
    case Throw show ?case by simp
  next
    case Try show ?case by simp
  next
    case Fin show ?case by simp
  next
    case Init show ?case by simp
  next
    case NewC show ?case by simp
  next
    case (NewA s0 T s1 e i s2 a s3)
    note halloc = \<open>G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3\<close>
    have "assigns (In1l e) \ dom (locals (store s2))"
    proof -
      from NewA
      have "normal (abupd (check_neg i) s2)"
        by - (erule halloc_no_abrupt [rule_format])
      hence "normal s2" by (cases s2) simp
      with NewA.hyps
      show ?thesis by iprover
    qed
    also
    from halloc
    have "\ \ dom (locals (store s3))"
      by (rule dom_locals_halloc_mono [elim_format]) simp
    finally show ?case by simp
  next
    case (Cast s0 e v s1 s2 T)
    hence "normal s1" by (cases s1,simp)
    with Cast.hyps
    have "assigns (In1l e) \ dom (locals (store s1))"
      by simp
    also
    from Cast.hyps
    have "\ \ dom (locals (store s2))"
      by simp
    finally
    show ?case
      by simp
  next
    case Inst thus ?case by simp
  next
    case Lit thus ?case by simp
  next
    case UnOp thus ?case by simp
  next
    case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
    hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
    with BinOp.hyps
    have "assigns (In1l e1) \ dom (locals (store s1))"
      by iprover
    also
    have "\ \ dom (locals (store s2))"
    proof -
      note \<open>G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
                      else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)\<close>
      thus ?thesis
        by (rule dom_locals_eval_mono_elim)
    qed
    finally have s2: "assigns (In1l e1) \ dom (locals (store s2))" .
    show ?case
    proof (cases "binop=CondAnd \ binop=CondOr")
      case True
      with s2 show ?thesis by simp
    next
      case False
      with BinOp
      have "assigns (In1l e2) \ dom (locals (store s2))"
        by (simp add: need_second_arg_def)
      with s2
      show ?thesis using False by simp
    qed
  next
    case Super thus ?case by simp
  next
    case Acc thus ?case by simp
  next
    case (Ass s0 va w f s1 e v s2)
    note nrm_ass_s2 = \<open>normal (assign f v s2)\<close>
    hence nrm_s2: "normal s2"
      by (cases s2, simp add: assign_def Let_def)
    with Ass.hyps
    have nrm_s1: "normal s1"
      by - (erule eval_no_abrupt_lemma [rule_format])
    with Ass.hyps
    have "assigns (In2 va) \ dom (locals (store s1))"
      by iprover
    also
    from Ass.hyps
    have "\ \ dom (locals (store s2))"
      by - (erule dom_locals_eval_mono_elim)
    also
    from nrm_s2 Ass.hyps
    have "assigns (In1l e) \ dom (locals (store s2))"
      by iprover
    ultimately
    have "assigns (In2 va) \ assigns (In1l e) \ dom (locals (store s2))"
      by (rule Un_least)
    also
    from Ass.hyps nrm_s1
    have "\ \ dom (locals (store (f v s2)))"
      by - (erule dom_locals_eval_mono_elim, cases s2,simp)
    then
    have "dom (locals (store s2)) \ dom (locals (store (assign f v s2)))"
      by (rule dom_locals_assign_mono)
    finally
    have va_e: " assigns (In2 va) \ assigns (In1l e)
                  \<subseteq> dom (locals (snd (assign f v s2)))" .
    show ?case
    proof (cases "\ n. va = LVar n")
      case False
      with va_e show ?thesis
        by (simp add: Un_assoc)
    next
      case True
      then obtain n where va: "va = LVar n"
        by blast
      with Ass.hyps
      have "G\Norm s0 \LVar n=\(w,f)\ s1"
        by simp
      hence "(w,f) = lvar n s0"
        by (rule eval_elim_cases) simp
      with nrm_ass_s2
      have "n \ dom (locals (store (assign f v s2)))"
        by (cases s2) (simp add: assign_def Let_def lvar_def)
      with va_e True va
      show ?thesis by (simp add: Un_assoc)
    qed
  next
    case (Cond s0 e0 b s1 e1 e2 v s2)
    hence "normal s1"
      by - (erule eval_no_abrupt_lemma [rule_format])
    with Cond.hyps
    have "assigns (In1l e0) \ dom (locals (store s1))"
      by iprover
    also from Cond.hyps
    have "\ \ dom (locals (store s2))"
      by - (erule dom_locals_eval_mono_elim)
    finally have e0: "assigns (In1l e0) \ dom (locals (store s2))" .
    show ?case
    proof (cases "the_Bool b")
      case True
      with Cond
      have "assigns (In1l e1) \ dom (locals (store s2))"
        by simp
      hence "assigns (In1l e1) \ assigns (In1l e2) \ \"
        by blast
      with e0
      have "assigns (In1l e0) \ assigns (In1l e1) \ assigns (In1l e2)
             \<subseteq> dom (locals (store s2))"
        by (rule Un_least)
      thus ?thesis using True by simp
    next
      case False
      with Cond
      have " assigns (In1l e2) \ dom (locals (store s2))"
        by simp
      hence "assigns (In1l e1) \ assigns (In1l e2) \ \"
        by blast
      with e0
      have "assigns (In1l e0) \ assigns (In1l e1) \ assigns (In1l e2)
             \<subseteq> dom (locals (store s2))"
        by (rule Un_least)
      thus ?thesis using False by simp
    qed
  next
    case (Call s0 e a' s1 args vs s2 D mode statT mn pTs s3 s3' accC v s4)
    have nrm_s2: "normal s2"
    proof -
      from \<open>normal ((set_lvars (locals (snd s2))) s4)\<close>
      have normal_s4: "normal s4" by simp
      hence "normal s3'" using Call.hyps
        by - (erule eval_no_abrupt_lemma [rule_format])
      moreover note
       \<open>s3' = check_method_access G accC statT mode \<lparr>name=mn, parTs=pTs\<rparr> a' s3\<close>
      ultimately have "normal s3"
        by (cases s3) (simp add: check_method_access_def Let_def)
      moreover
      note s3 = \<open>s3 = init_lvars G D \<lparr>name = mn, parTs = pTs\<rparr> mode a' vs s2\<close>
      ultimately show "normal s2"
        by (cases s2) (simp add: init_lvars_def2)
    qed
    hence "normal s1" using Call.hyps
      by - (erule eval_no_abrupt_lemma [rule_format])
    with Call.hyps
    have "assigns (In1l e) \ dom (locals (store s1))"
      by iprover
    also from Call.hyps
    have "\ \ dom (locals (store s2))"
      by - (erule dom_locals_eval_mono_elim)
    also
    from nrm_s2 Call.hyps
    have "assigns (In3 args) \ dom (locals (store s2))"
      by iprover
    ultimately have "assigns (In1l e) \ assigns (In3 args) \ \"
      by (rule Un_least)
    also
--> --------------------

--> maximum size reached

--> --------------------

quality96%

¤ Dauer der Verarbeitung: 0.40 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.