# Theory Evaln

Up to index of Isabelle/HOL/Bali

theory Evaln
imports TypeSafe
begin

    (*  Title:      HOL/Bali/Evaln.thy
        ID:         $Id: Evaln.thy,v 1.16 2005/09/22 21:56:23 nipkow Exp $
        Author:     David von Oheimb and Norbert Schirmer
    *)
    header {* Operational evaluation (big-step) semantics of Java expressions and
              statements
    *}

    theory Evaln imports TypeSafe begin

    text {*
    Variant of @{term eval} relation with counter for bounded recursive depth.
    In principal @{term evaln} could replace @{term eval}.

    Validity of the axiomatic semantics builds on @{term evaln}.
    For recursive method calls the axiomatic semantics rule assumes the method ok
    to derive a proof for the body. To prove the method rule sound we need to
    perform induction on the recursion depth.
    For the completeness proof of the axiomatic semantics the notion of the most
    general formula is used. The most general formula right now builds on the
    ordinary evaluation relation @{term eval}.
    So sometimes we have to switch between @{term evaln} and @{term eval} and vice
    versa. To make
    this switch easy @{term evaln} also does all the technical accessibility tests
    @{term check_field_access} and @{term check_method_access} like @{term eval}.
    If it would omit them @{term evaln} and @{term eval} would only be equivalent
    for welltyped, and definitely assigned terms.
    *}

    consts

      evaln :: "prog => (state × term × nat × vals × state) set"

    syntax

      evaln :: "[prog, state, term,        nat, vals * state] => bool"
                                    ("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
      evarn :: "[prog, state, var  , vvar        , nat, state] => bool"
                                    ("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
      eval_n:: "[prog, state, expr , val         , nat, state] => bool"
                                    ("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
      evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
                                    ("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
      execn :: "[prog, state, stmt ,               nat, state] => bool"
                                    ("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)

    syntax (xsymbols)

      evaln :: "[prog, state, term,         nat, vals × state] => bool"
                                    ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_-> _"   [61,61,80,   61,61] 60)
      evarn :: "[prog, state, var  , vvar         , nat, state] => bool"
                                    ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_-> _" [61,61,90,61,61,61] 60)
      eval_n:: "[prog, state, expr , val ,          nat, state] => bool"
                                    ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_-> _" [61,61,80,61,61,61] 60)
      evalsn:: "[prog, state, expr list, val  list, nat, state] => bool"
                                    ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_-> _" [61,61,61,61,61,61] 60)
      execn :: "[prog, state, stmt ,                nat, state] => bool"
                                    ("_\<turnstile>_ \<midarrow>_\<midarrow>_-> _"     [61,61,65,   61,61] 60)

    translations

      "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n->  w___s' " == "(s,t,n,w___s') ∈ evaln G"
      "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n-> (w,  s')" <= "(s,t,n,w,  s') ∈ evaln G"
      "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n-> (w,x,s')" <= "(s,t,n,w,x,s') ∈ evaln G"
      "G\<turnstile>s \<midarrow>c     \<midarrow>n-> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n-> (♦    ,x,s')"
      "G\<turnstile>s \<midarrow>c     \<midarrow>n->    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n-> (♦    ,  s')"
      "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n-> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n-> (In1 v ,x,s')"
      "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n->    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n-> (In1 v ,  s')"
      "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n-> (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n-> (In2 vf,x,s')"
      "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n->    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n-> (In2 vf,  s')"
      "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n-> (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n-> (In3 v ,x,s')"
      "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n->    s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n-> (In3 v ,  s')"

    inductive "evaln G" intros

    --{* propagation of abrupt completion *}

      Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n-> (arbitrary3 t,(Some xc,s))"

    --{* evaluation of variables *}

      LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n-> Norm s"

      FVar: "[|G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n-> s2;
              (v,s2') = fvar statDeclC stat fn a s2;
              s3 = check_field_access G accC statDeclC fn stat a s2'|] ==>
              G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n-> s3"

      AVar: "[|G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n-> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n-> s2;
              (v,s2') = avar G i a s2|] ==>
                          G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n-> s2'"

    --{* evaluation of expressions *}

      NewC: "[|G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n-> s1;
              G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a-> s2|] ==>
                                      G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n-> s2"

      NewA: "[|G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n-> s2;
              G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a-> s3|] ==>
                                    G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n-> s3"

      Cast: "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1;
              s2 = abupd (raise_if (¬G,snd s1\<turnstile>v fits T) ClassCast) s1|] ==>
                                    G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n-> s2"

      Inst: "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1;
              b = (v≠Null ∧ G,store s1\<turnstile>v fits RefT T)|] ==>
                                  G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n-> s1"

      Lit:                     "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n-> Norm s"

      UnOp: "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1|]
             ==> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n-> s1"

      BinOp: "[|G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n-> s1;
               G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
                \<succ>\<midarrow>n-> (In1 v2,s2)|]
             ==> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n-> s2"

      Super:                   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n-> Norm s"

      Acc:  "[|G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n-> s1|] ==>
                                      G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n-> s1"

      Ass:  "[|G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n-> s1;
              G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n-> s2|] ==>
                                       G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n-> assign f v s2"

      Cond: "[|G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n-> s1;
              G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n-> s2|] ==>
                                G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n-> s2"

      Call:
      "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n-> s2;
        D = invocation_declclass G mode (store s2) a' statT (|name=mn,parTs=pTs|)),;
        s3=init_lvars G D (|name=mn,parTs=pTs|)), mode a' vs s2;
        s3' = check_method_access G accC statT mode (|name=mn,parTs=pTs|)), a' s3;
        G\<turnstile>s3'\<midarrow>Methd D (|name=mn,parTs=pTs|)),-\<succ>v\<midarrow>n-> s4
       |]
       ==>
        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e·mn({pTs}args)-\<succ>v\<midarrow>n-> (restore_lvars s2 s4)"

      Methd:"[|G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n-> s1|] ==>
                                    G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n-> s1"

      Body: "[|G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n-> s2;
              s3 = (if (∃ l. abrupt s2 = Some (Jump (Break l)) ∨
                             abrupt s2 = Some (Jump (Cont l)))
                      then abupd (λ x. Some (Error CrossMethodJump)) s2
                      else s2)|]==>
             G\<turnstile>Norm s0 \<midarrow>Body D c
              -\<succ>the (locals (store s2) Result)\<midarrow>n->abupd (absorb Ret) s3"

    --{* evaluation of expression lists *}

      Nil:
                                    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n-> Norm s0"

      Cons: "[|G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n-> s1;
              G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n-> s2|] ==>
                                 G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n-> s2"

    --{* execution of statements *}

      Skip:                             "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n-> Norm s"

      Expr: "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1|] ==>
                                      G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n-> s1"

      Lab:  "[|G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n-> s1|] ==>
                                 G\<turnstile>Norm s0 \<midarrow>l• c\<midarrow>n-> abupd (absorb l) s1"

      Comp: "[|G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n-> s1;
              G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n-> s2|] ==>
                                     G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n-> s2"

      If:   "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n-> s1;
              G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n-> s2|] ==>
                           G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n-> s2"

      Loop: "[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n-> s1;
              if the_Bool b
                 then (G\<turnstile>s1 \<midarrow>c\<midarrow>n-> s2 ∧
                       G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l• While(e) c\<midarrow>n-> s3)
                 else s3 = s1|] ==>
                                  G\<turnstile>Norm s0 \<midarrow>l• While(e) c\<midarrow>n-> s3"

      Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n-> (Some (Jump j), s)"

      Throw:"[|G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n-> s1|] ==>
                                     G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n-> abupd (throw a') s1"

      Try:  "[|G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>sxalloc-> s2;
              if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n-> s3 else s3 = s2|]
              ==>
                      G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n-> s3"

      Fin:  "[|G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n-> (x1,s1);
              G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n-> s2;
              s3=(if (∃ err. x1=Some (Error err))
                  then (x1,s1)
                  else abupd (abrupt_if (x1≠None) x1) s2)|] ==>
                  G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n-> s3"

      Init: "[|the (class G C) = c;
              if inited C (globs s0) then s3 = Norm s0
              else (G\<turnstile>Norm (init_class_obj G C s0)
                      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n-> s1 ∧
                    G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n-> s2 ∧
                    s3 = restore_lvars s1 s2)|]
              ==>
                     G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n-> s3"
    monos
      if_def2

    declare split_if     [split del] split_if_asm     [split del]
            option.split [split del] option.split_asm [split del]
            not_None_eq [simp del]
            split_paired_All [simp del] split_paired_Ex [simp del]
    ML_setup {*
    simpset_ref() := simpset() delloop "split_all_tac"
    *}
    inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> vs'"

    inductive_cases evaln_elim_cases:
            "G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (l• c)                    \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (l• While(e) c)           \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e·mn({pT}p)) \<succ>\<midarrow>n-> vs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n-> xs'"
            "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n-> xs'"

    declare split_if     [split] split_if_asm     [split]
            option.split [split] option.split_asm [split]
            not_None_eq [simp]
            split_paired_All [simp] split_paired_Ex [simp]
    ML_setup {*
    simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
    *}
    lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> (w,s') ==> case t of In1 ec =>
      (case ec of Inl e => (∃v. w = In1 v) | Inr c => w = ♦)
      | In2 e => (∃v. w = In2 v) | In3 e => (∃v. w = In3 v)"
    apply (erule evaln_cases , auto)
    apply (induct_tac "t")
    apply   (induct_tac "a")
    apply auto
    done

    text {* The following simplification procedures set up the proper injections of
     terms and their corresponding values in the evaluation relation:
     E.g. an expression
     (injection @{term In1l} into terms) always evaluates to ordinary values
     (injection @{term In1} into generalised values @{term vals}).
    *}

    ML_setup {*
    fun enf nam inj rhs =
    let
      val name = "evaln_" ^ nam ^ "_eq"
      val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n-> (w, s')"
      val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
            (K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
      fun is_Inj (Const (inj,_) $ _) = true
        | is_Inj _                   = false
      fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $
        (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
    in
      cond_simproc name lhs pred (thm name)
    end;

    val evaln_expr_proc = enf "expr" "In1l" "∃v.  w=In1 v  ∧ G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n-> s'";
    val evaln_var_proc  = enf "var"  "In2"  "∃vf. w=In2 vf ∧ G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n-> s'";
    val evaln_exprs_proc= enf "exprs""In3"  "∃vs. w=In3 vs ∧ G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n-> s'";
    val evaln_stmt_proc = enf "stmt" "In1r" "     w=♦      ∧ G\<turnstile>s \<midarrow>t     \<midarrow>n-> s'";
    Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];

    bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
    *}
    declare evaln_AbruptIs [intro!]

    lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n-> (v,s') = False"
    proof -
      { fix s t v s'
        assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> (v,s')" and
             normal: "normal s" and
             callee: "t=In1l (Callee l e)"
        then have "False"
        proof (induct)
        qed (auto)
      }
      then show ?thesis
        by (cases s') fastsimp
    qed

    lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n-> (v,s') = False"
    proof -
      { fix s t v s'
        assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> (v,s')" and
             normal: "normal s" and
             callee: "t=In1l (InsInitE c e)"
        then have "False"
        proof (induct)
        qed (auto)
      }
      then show ?thesis
        by (cases s') fastsimp
    qed

    lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n-> (v,s') = False"
    proof -
      { fix s t v s'
        assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> (v,s')" and
             normal: "normal s" and
             callee: "t=In2 (InsInitV c w)"
        then have "False"
        proof (induct)
        qed (auto)
      }
      then show ?thesis
        by (cases s') fastsimp
    qed

    lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n-> (v,s') = False"
    proof -
      { fix s t v s'
        assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> (v,s')" and
             normal: "normal s" and
             callee: "t=In1r (FinA a c)"
        then have "False"
        proof (induct)
        qed (auto)
      }
      then show ?thesis
        by (cases s') fastsimp
    qed

    lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n-> (v,s') ==>
     fst s = Some xc --> s' = s ∧ v = arbitrary3 e"
    apply (erule evaln_cases , auto)
    done

    lemma evaln_abrupt:
     "!!s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n-> (w,s') = (s' = (Some xc,s) ∧
      w=arbitrary3 e ∧ G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n-> (arbitrary3 e,(Some xc,s)))"
    apply auto
    apply (frule evaln_abrupt_lemma, auto)+
    done

    ML {*
    local
      fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
        | is_Some _ = false
      fun pred (_ $ (Const ("Pair",_) $
         _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
           (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
    in
      val evaln_abrupt_proc =
     cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n-> (w,s')" pred (thm "evaln_abrupt")
    end;
    Addsimprocs [evaln_abrupt_proc]
    *}

    lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n-> s"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.Lit)

    lemma CondI:
     "!!s1. [|G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n-> s2|] ==>
      G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n-> s2"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.Cond)

    lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n-> s"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.Skip)

    lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n-> s' ==> G\<turnstile>s \<midarrow>Expr e\<midarrow>n-> s'"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.Expr)

    lemma evaln_CompI: "[|G\<turnstile>s \<midarrow>c1\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n-> s2|] ==> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n-> s2"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.Comp)

    lemma evaln_IfI:
     "[|G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n-> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n-> s2|] ==>
      G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n-> s2"
    apply (case_tac "s", case_tac "a = None")
    by (auto intro!: evaln.If)

    lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n-> s' ==> s' = s"
    by (erule evaln_cases, auto)

    lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n-> s' = (s = s')"
    apply auto
    done

    section {* evaln implies eval *}

    lemma evaln_eval:
      assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n-> (v,s1)"
      shows "G\<turnstile>s0 \<midarrow>t\<succ>-> (v,s1)"
    using evaln
    proof (induct)
      case (Loop b c e l n s0 s1 s2 s3)
      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b-> s1".
      moreover
      have "if the_Bool b
            then (G\<turnstile>s1 \<midarrow>c-> s2) ∧
                 G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l• While(e) c-> s3
            else s3 = s1"
        using Loop.hyps by simp
      ultimately show ?case by (rule eval.Loop)
    next
      case (Try c1 c2 n s0 s1 s2 s3 C vn)
      have "G\<turnstile>Norm s0 \<midarrow>c1-> s1".
      moreover
      have "G\<turnstile>s1 \<midarrow>sxalloc-> s2".
      moreover
      have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2-> s3 else s3 = s2"
        using Try.hyps by simp
      ultimately show ?case by (rule eval.Try)
    next
      case (Init C c n s0 s1 s2 s3)
      have "the (class G C) = c".
      moreover
      have "if inited C (globs s0)
               then s3 = Norm s0
               else G\<turnstile>Norm ((init_class_obj G C) s0)
                      \<midarrow>(if C = Object then Skip else Init (super c))-> s1 ∧
                    G\<turnstile>(set_lvars empty) s1 \<midarrow>init c-> s2 ∧
                    s3 = (set_lvars (locals (store s1))) s2"
        using Init.hyps by simp
      ultimately show ?case by (rule eval.Init)
    qed (rule eval.intros,(assumption+ | assumption?))+

    lemma Suc_le_D_lemma: "[|Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
    apply (frule Suc_le_D)
    apply fast
    done

    lemma evaln_nonstrict [rule_format (no_asm), elim]:
      "!!ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n-> ws ==> ∀m. n≤m --> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m-> ws"
    apply (simp (no_asm_simp) only: split_tupled_all)
    apply (erule evaln.induct)
    apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
      REPEAT o smp_tac 1,
      resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
    (* 3 subgoals *)
    apply (auto split del: split_if)
    done

    lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]

    lemma evaln_max2: "[|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1-> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2-> ws2|] ==>
                 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2-> ws1 ∧ G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2-> ws2"
    by (fast intro: le_maxI1 le_maxI2)

    corollary evaln_max2E [consumes 2]:
      "[|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1-> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2-> ws2;
        [|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2-> ws1;G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2-> ws2 |] ==> P |] ==> P"
    by (drule (1) evaln_max2) simp

    lemma evaln_max3:
    "[|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1-> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2-> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3-> ws3|] ==>
     G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3-> ws1 ∧
     G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3-> ws2 ∧
     G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3-> ws3"
    apply (drule (1) evaln_max2, erule thin_rl)
    apply (fast intro!: le_maxI1 le_maxI2)
    done

    corollary evaln_max3E:
    "[|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1-> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2-> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3-> ws3;
       [|G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3-> ws1;
        G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3-> ws2;
        G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3-> ws3
       |] ==> P
      |] ==> P"
    by (drule (2) evaln_max3) simp

    lemma le_max3I1: "(n2::nat) ≤ max n1 (max n2 n3)"
    proof -
      have "n2 ≤ max n2 n3"
        by (rule le_maxI1)
      also
      have "max n2 n3 ≤ max n1 (max n2 n3)"
        by (rule le_maxI2)
      finally
      show ?thesis .
    qed

    lemma le_max3I2: "(n3::nat) ≤ max n1 (max n2 n3)"
    proof -
      have "n3 ≤ max n2 n3"
        by (rule le_maxI2)
      also
      have "max n2 n3 ≤ max n1 (max n2 n3)"
        by (rule le_maxI2)
      finally
      show ?thesis .
    qed

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

    section {* eval implies evaln *}
    lemma eval_evaln:
      assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>-> (v,s1)"
      shows  "∃n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n-> (v,s1)"
    using eval
    proof (induct)
      case (Abrupt s t xc)
      obtain n where
        "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n-> (arbitrary3 t, Some xc, s)"
        by (iprover intro: evaln.Abrupt)
      then show ?case ..
    next
      case Skip
      show ?case by (blast intro: evaln.Skip)
    next
      case (Expr e s0 s1 v)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1"
        by (iprover)
      then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n-> s1"
        by (rule evaln.Expr)
      then show ?case ..
    next
      case (Lab c l s0 s1)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n-> s1"
        by (iprover)
      then have "G\<turnstile>Norm s0 \<midarrow>l• c\<midarrow>n-> abupd (absorb l) s1"
        by (rule evaln.Lab)
      then show ?case ..
    next
      case (Comp c1 c2 s0 s1 s2)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2-> s2"
        by (iprover)
      then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2-> s2"
        by (blast intro: evaln.Comp dest: evaln_max2 )
      then show ?case ..
    next
      case (If b c1 c2 e s0 s1 s2)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2-> s2"
        by (iprover)
      then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2-> s2"
        by (blast intro: evaln.If dest: evaln_max2)
      then show ?case ..
    next
      case (Loop b c e l s0 s1 s2 s3)
      from Loop.hyps obtain n1 where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1-> s1"
        by (iprover)
      moreover from Loop.hyps obtain n2 where
        "if the_Bool b
            then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2-> s2 ∧
                  G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l• While(e) c\<midarrow>n2-> s3)
            else s3 = s1"
        by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>l• While(e) c\<midarrow>max n1 n2-> s3"
        apply -
        apply (rule evaln.Loop)
        apply   (iprover intro: evaln_nonstrict intro: le_maxI1)

        apply   (auto intro: evaln_nonstrict intro: le_maxI2)
        done
      then show ?case ..
    next
      case (Jmp j s)
      have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n-> (Some (Jump j), s)"
        by (rule evaln.Jmp)
      then show ?case ..
    next
      case (Throw a e s0 s1)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n-> s1"
        by (iprover)
      then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n-> abupd (throw a) s1"
        by (rule evaln.Throw)
      then show ?case ..
    next
      case (Try catchC c1 c2 s0 s1 s2 s3 vn)
      from Try.hyps obtain n1 where
        "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1-> s1"
        by (iprover)
      moreover
      have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc-> s2" .
      moreover
      from Try.hyps obtain n2 where
        "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2-> s3 else s3 = s2"
        by fastsimp
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2-> s3"
        by (auto intro!: evaln.Try le_maxI1 le_maxI2)
      then show ?case ..
    next
      case (Fin c1 c2 s0 s1 s2 s3 x1)
      from Fin obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1-> (x1, s1)"
        "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2-> s2"
        by iprover
      moreover
      have s3: "s3 = (if ∃err. x1 = Some (Error err)
                         then (x1, s1)
                         else abupd (abrupt_if (x1 ≠ None) x1) s2)" .
      ultimately
      have
        "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2-> s3"
        by (blast intro: evaln.Fin dest: evaln_max2)
      then show ?case ..
    next
      case (Init C c s0 s1 s2 s3)
      have     cls: "the (class G C) = c" .
      moreover from Init.hyps obtain n where
          "if inited C (globs s0) then s3 = Norm s0
           else (G\<turnstile>Norm (init_class_obj G C s0)
                  \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n-> s1 ∧
                       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n-> s2 ∧
                       s3 = restore_lvars s1 s2)"
        by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
      ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n-> s3"
        by (rule evaln.Init)
      then show ?case ..
    next
      case (NewC C a s0 s1 s2)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n-> s1"
        by (iprover)
      with NewC
      have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n-> s2"
        by (iprover intro: evaln.NewC)
      then show ?case ..
    next
      case (NewA T a e i s0 s1 s2 s3)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2-> s2"
        by (iprover)
      moreover
      have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a-> s3" .
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2-> s3"
        by (blast intro: evaln.NewA dest: evaln_max2)
      then show ?case ..
    next
      case (Cast castT e s0 s1 s2 v)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1"
        by (iprover)
      moreover
      have "s2 = abupd (raise_if (¬ G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n-> s2"
        by (rule evaln.Cast)
      then show ?case ..
    next
      case (Inst T b e s0 s1 v)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1"
        by (iprover)
      moreover
      have "b = (v ≠ Null ∧ G,snd s1\<turnstile>v fits RefT T)" .
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n-> s1"
        by (rule evaln.Inst)
      then show ?case ..
    next
      case (Lit s v)
      have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n-> Norm s"
        by (rule evaln.Lit)
      then show ?case ..
    next
      case (UnOp e s0 s1 unop v )
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n-> s1"
        by (iprover)
      hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n-> s1"
        by (rule evaln.UnOp)
      then show ?case ..
    next
      case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
                   else In1r Skip)\<succ>\<midarrow>n2-> (In1 v2, s2)"
        by (iprover)
      hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
              -> s2"
        by (blast intro!: evaln.BinOp dest: evaln_max2)
      then show ?case ..
    next
      case (Super s )
      have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n-> Norm s"
        by (rule evaln.Super)
      then show ?case ..
    next
    -- {*
    \par
    *} (* dummy text command to break paragraph for latex;
                  large paragraphs exhaust memory of debian pdflatex *)
      case (Acc f s0 s1 v va)
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n-> s1"
        by (iprover)
      then
      have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n-> s1"
        by (rule evaln.Acc)
      then show ?case ..
    next
      case (Ass e f s0 s1 s2 v var w)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2-> s2"
        by (iprover)
      then
      have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2-> assign f v s2"
        by (blast intro: evaln.Ass dest: evaln_max2)
      then show ?case ..
    next
      case (Cond b e0 e1 e2 s0 s1 s2 v)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2-> s2"
        by (iprover)
      then
      have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2-> s2"
        by (blast intro: evaln.Cond dest: evaln_max2)
      then show ?case ..
    next
      case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT
            v vs)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2-> s2"
        by iprover
      moreover
      have "invDeclC = invocation_declclass G mode (store s2) a' statT
                           (|name=mn,parTs=pTs'|))," .
      moreover
      have "s3 = init_lvars G invDeclC (|name=mn,parTs=pTs'|)), mode a' vs s2" .
      moreover
      have "s3'=check_method_access G accC' statT mode (|name=mn,parTs=pTs'|)), a' s3".
      moreover
      from Call.hyps
      obtain m where
        "G\<turnstile>s3' \<midarrow>Methd invDeclC (|name=mn, parTs=pTs'|)),-\<succ>v\<midarrow>m-> s4"
        by iprover
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e·mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)->
                (set_lvars (locals (store s2))) s4"
        by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
      thus ?case ..
    next
      case (Methd D s0 s1 sig v )
      then obtain n where
        "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n-> s1"
        by iprover
      then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n-> s1"
        by (rule evaln.Methd)
      then show ?case ..
    next
      case (Body D c s0 s1 s2 s3 )
      from Body.hyps obtain n1 n2 where
        evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1-> s1" and
        evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2-> s2"
        by (iprover)
      moreover
      have "s3 = (if ∃l. fst s2 = Some (Jump (Break l)) ∨
                         fst s2 = Some (Jump (Cont l))
                     then abupd (λx. Some (Error CrossMethodJump)) s2
                     else s2)".
      ultimately
      have
         "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
           -> abupd (absorb Ret) s3"
        by (iprover intro: evaln.Body dest: evaln_max2)
      then show ?case ..
    next
      case (LVar s vn )
      obtain n where
        "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n-> Norm s"
        by (iprover intro: evaln.LVar)
      then show ?case ..
    next
      case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2-> s2"
        by iprover
      moreover
      have "s3 = check_field_access G accC statDeclC fn stat a s2'"
           "(v, s2') = fvar statDeclC stat fn a s2" .
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2-> s3"
        by (iprover intro: evaln.FVar dest: evaln_max2)
      then show ?case ..
    next
      case (AVar a e1 e2 i s0 s1 s2 s2' v )
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2-> s2"
        by iprover
      moreover
      have "(v, s2') = avar G i a s2" .
      ultimately
      have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2-> s2'"
        by (blast intro!: evaln.AVar dest: evaln_max2)
      then show ?case ..
    next
      case (Nil s0)
      show ?case by (iprover intro: evaln.Nil)
    next
      case (Cons e es s0 s1 s2 v vs)
      then obtain n1 n2 where
        "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1-> s1"
        "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2-> s2"
        by iprover
      then
      have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2-> s2"
        by (blast intro!: evaln.Cons dest: evaln_max2)
      then show ?case ..
    qed

    end

lemmas evaln_cases:

      [| G|-s -t>-n-> vs';
         !!s xc. [| s = (Some xc, s); vs' = (arbitrary3 t, Some xc, s) |] ==> P;
         !!s vn.
            [| s = Norm s; t = In2 (LVar vn); vs' = (In2 (lvar vn s), Norm s) |]
            ==> P;
         !!a accC e fn s0 s1 s2 s2' stat statDeclC v.
            [| G|-Norm s0 -Init statDeclC-n-> s1; G|-s1 -e->a-n-> s2;
               (v, s2') = fvar statDeclC stat fn a s2; s = Norm s0;
               t = In2 ({accC,statDeclC,stat}e..fn);
               vs' = (In2 v, check_field_access G accC statDeclC fn stat a s2') |]
            ==> P;
         !!a e1 e2 i s0 s1 s2 s2' v.
            [| G|-Norm s0 -e1->a-n-> s1; G|-s1 -e2->i-n-> s2;
               (v, s2') = avar G i a s2; s = Norm s0; t = In2 (e1.[e2]);
               vs' = (In2 v, s2') |]
            ==> P;
         !!C a s0 s1 s2.
            [| G|-Norm s0 -Init C-n-> s1; G|-s1 -halloc CInst C>a-> s2; s = Norm s0;
               t = In1l (NewC C); vs' = (In1 (Addr a), s2) |]
            ==> P;
         !!T a e i' s0 s1 s2 s3.
            [| G|-Norm s0 -init_comp_ty T-n-> s1; G|-s1 -e->i'-n-> s2;
               G|-abupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3;
               s = Norm s0; t = In1l (New T[e]); vs' = (In1 (Addr a), s3) |]
            ==> P;
         !!T e s0 s1 v.
            [| G|-Norm s0 -e->v-n-> s1; s = Norm s0; t = In1l (Cast T e);
               vs' =
               (In1 v,
                abupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1) |]
            ==> P;
         !!T e s0 s1 v.
            [| G|-Norm s0 -e->v-n-> s1; s = Norm s0; t = In1l (e InstOf T);
               vs' =
               (In1 (Bool (v ≠ Null ∧ G,snd s1\<turnstile>v fits RefT T)), s1) |]
            ==> P;
         !!s v. [| s = Norm s; t = In1l (Lit v); vs' = (In1 v, Norm s) |] ==> P;
         !!e s0 s1 unop v.
            [| G|-Norm s0 -e->v-n-> s1; s = Norm s0; t = In1l (UnOp unop e);
               vs' = (In1 (eval_unop unop v), s1) |]
            ==> P;
         !!binop e1 e2 s0 s1 s2 v1 v2.
            [| G|-Norm s0 -e1->v1-n-> s1;
               G|-s1 -(if need_second_arg binop v1 then In1l e2
                       else In1r Skip)>-n-> (In1 v2, s2);
               s = Norm s0; t = In1l (BinOp binop e1 e2);
               vs' = (In1 (eval_binop binop v1 v2), s2) |]
            ==> P;
         !!s. [| s = Norm s; t = In1l Super; vs' = (In1 (val_this s), Norm s) |]
              ==> P;
         !!f s0 s1 v va.
            [| G|-Norm s0 -va=>(v, f)-n-> s1; s = Norm s0; t = In1l (Acc va);
               vs' = (In1 v, s1) |]
            ==> P;
         !!e f s0 s1 s2 v va w.
            [| G|-Norm s0 -va=>(w, f)-n-> s1; G|-s1 -e->v-n-> s2; s = Norm s0;
               t = In1l (va:=e); vs' = (In1 v, assign f v s2) |]
            ==> P;
         !!b e0 e1 e2 s0 s1 s2 v.
            [| G|-Norm s0 -e0->b-n-> s1;
               G|-s1 -(if the_Bool b then e1 else e2)->v-n-> s2; s = Norm s0;
               t = In1l (e0 ? e1 : e2); vs' = (In1 v, s2) |]
            ==> P;
         !!a' accC args e mn mode pTs s0 s1 s2 s4 statT v vs.
            [| G|-Norm s0 -e->a'-n-> s1; G|-s1 -args#>vs-n-> s2;
               G|-check_method_access G accC statT mode (| name = mn, parTs = pTs |)
                   a' (init_lvars G
                        (invocation_declclass G mode (snd s2) a' statT
                          (| name = mn, parTs = pTs |))
                        (| name = mn, parTs = pTs |) mode a' vs
                        s2) -Methd
                              (invocation_declclass G mode (snd s2) a' statT
                                (| name = mn, parTs = pTs |))
                              (| name = mn, parTs = pTs |)->v-n-> s4;
               s = Norm s0; t = In1l ({accC,statT,mode}e·mn( {pTs}args));
               vs' = (In1 v, (set_lvars (locals (snd s2))) s4) |]
            ==> P;
         !!D n s0 s1 sig v.
            [| G|-Norm s0 -body G D sig->v-n-> s1; s = Norm s0;
               t = In1l (Methd D sig); n = Suc n; vs' = (In1 v, s1) |]
            ==> P;
         !!D c s0 s1 s2.
            [| G|-Norm s0 -Init D-n-> s1; G|-s1 -c-n-> s2; s = Norm s0;
               t = In1l (Body D c);
               vs' =
               (In1 (the (locals (snd s2) Result)),
                abupd (absorb Ret)
                 (if ∃l. fst s2 = Some (Jump (Break l)) ∨
                         fst s2 = Some (Jump (Cont l))
                  then abupd (%x. Some (Error CrossMethodJump)) s2 else s2)) |]
            ==> P;
         !!s0. [| s = Norm s0; t = In3 []; vs' = (In3 [], Norm s0) |] ==> P;
         !!e es s0 s1 s2 v vs.
            [| G|-Norm s0 -e->v-n-> s1; G|-s1 -es#>vs-n-> s2; s = Norm s0;
               t = In3 (e # es); vs' = (In3 (v # vs), s2) |]
            ==> P;
         !!s. [| s = Norm s; t = In1r Skip; vs' = (dummy_res, Norm s) |] ==> P;
         !!e s0 s1 v.
            [| G|-Norm s0 -e->v-n-> s1; s = Norm s0; t = In1r (Expr e);
               vs' = (dummy_res, s1) |]
            ==> P;
         !!c l s0 s1.
            [| G|-Norm s0 -c-n-> s1; s = Norm s0; t = In1r (l• c);
               vs' = (dummy_res, abupd (absorb l) s1) |]
            ==> P;
         !!c1 c2 s0 s1 s2.
            [| G|-Norm s0 -c1-n-> s1; G|-s1 -c2-n-> s2; s = Norm s0;
               t = In1r (c1;; c2); vs' = (dummy_res, s2) |]
            ==> P;
         !!b c1 c2 e s0 s1 s2.
            [| G|-Norm s0 -e->b-n-> s1; G|-s1 -(if the_Bool b then c1 else c2)-n-> s2;
               s = Norm s0; t = In1r (If(e) c1 Else c2); vs' = (dummy_res, s2) |]
            ==> P;
         !!b c e l s0 s1 s2 s3.
            [| G|-Norm s0 -e->b-n-> s1;
               if the_Bool b
               then G|-s1 -c-n-> s2 ∧
                    G|-abupd (absorb (Cont l)) s2 -l• While(e) c-n-> s3
               else s3 = s1;
               s = Norm s0; t = In1r (l• While(e) c); vs' = (dummy_res, s3) |]
            ==> P;
         !!j s. [| s = Norm s; t = In1r (Jmp j);
                   vs' = (dummy_res, Some (Jump j), s) |]
                ==> P;
         !!a' e s0 s1.
            [| G|-Norm s0 -e->a'-n-> s1; s = Norm s0; t = In1r (Throw e);
               vs' = (dummy_res, abupd (throw a') s1) |]
            ==> P;
         !!c1 c2 s0 s1 s2 s3 tn vn.
            [| G|-Norm s0 -c1-n-> s1; G|-s1 -sxalloc-> s2;
               if G,s2\<turnstile>catch tn then G|-new_xcpt_var vn s2 -c2-n-> s3
               else s3 = s2;
               s = Norm s0; t = In1r (Try c1 Catch(tn vn) c2);
               vs' = (dummy_res, s3) |]
            ==> P;
         !!c1 c2 s0 s1 s2 x1.
            [| G|-Norm s0 -c1-n-> (x1, s1); G|-Norm s1 -c2-n-> s2; s = Norm s0;
               t = In1r (c1 Finally c2);
               vs' =
               (dummy_res,
                if ∃err. x1 = Some (Error err) then (x1, s1)
                else abupd (abrupt_if (x1 ≠ None) x1) s2) |]
            ==> P;
         !!C s0 s1 s2 s3.
            [| if inited C (globs s0) then s3 = Norm s0
               else G|-Norm ((init_class_obj G C)
                              s0) -(if C = Object then Skip
                                    else Init (super (the (class G C))))-n-> s1 ∧
                    G|-(set_lvars empty) s1 -init (the (class G C))-n-> s2 ∧
                    s3 = (set_lvars (locals (snd s1))) s2;
               s = Norm s0; t = In1r (Init C); vs' = (dummy_res, s3) |]
            ==> P |]
      ==> P

lemmas evaln_elim_cases:

      [| G|-(Some xc, s) -t>-n-> vs'; vs' = (arbitrary3 t, Some xc, s) ==> P |] ==> P

      [| G|-Norm s -In1r Skip>-n-> xs'; xs' = (dummy_res, Norm s) ==> P |] ==> P

      [| G|-Norm s -In1r (Jmp j)>-n-> xs';
         xs' = (dummy_res, Some (Jump j), s) ==> P |]
      ==> P

      [| G|-Norm s -In1r (l• c)>-n-> xs';
         !!s1. [| G|-Norm s -c-n-> s1; xs' = (dummy_res, abupd (absorb l) s1) |]
               ==> P |]
      ==> P

      [| G|-Norm s -In3 []>-n-> vs'; vs' = (In3 [], Norm s) ==> P |] ==> P

      [| G|-Norm s -In3 (e # es)>-n-> vs';
         !!s1 s2 v vs.
            [| G|-Norm s -e->v-n-> s1; G|-s1 -es#>vs-n-> s2;
               vs' = (In3 (v # vs), s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (Lit w)>-n-> vs'; vs' = (In1 w, Norm s) ==> P |] ==> P

      [| G|-Norm s -In1l (UnOp unop e)>-n-> vs';
         !!s1 v.
            [| G|-Norm s -e->v-n-> s1; vs' = (In1 (eval_unop unop v), s1) |] ==> P |]
      ==> P

      [| G|-Norm s -In1l (BinOp binop e1.0 e2.0)>-n-> vs';
         !!s1 s2 v1 v2.
            [| G|-Norm s -e1.0->v1-n-> s1;
               G|-s1 -(if need_second_arg binop v1 then In1l e2.0
                       else In1r Skip)>-n-> (In1 v2, s2);
               vs' = (In1 (eval_binop binop v1 v2), s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In2 (LVar vn)>-n-> vs'; vs' = (In2 (lvar vn s), Norm s) ==> P |]
      ==> P

      [| G|-Norm s -In1l (Cast T e)>-n-> vs';
         !!s1 v.
            [| G|-Norm s -e->v-n-> s1;
               vs' =
               (In1 v,
                abupd (raise_if (¬ G,snd s1\<turnstile>v fits T) ClassCast) s1) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (e InstOf T)>-n-> vs';
         !!s1 v.
            [| G|-Norm s -e->v-n-> s1;
               vs' =
               (In1 (Bool (v ≠ Null ∧ G,snd s1\<turnstile>v fits RefT T)), s1) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l Super>-n-> vs'; vs' = (In1 (val_this s), Norm s) ==> P |]
      ==> P

      [| G|-Norm s -In1l (Acc va)>-n-> vs';
         !!f s1 v. [| G|-Norm s -va=>(v, f)-n-> s1; vs' = (In1 v, s1) |] ==> P |]
      ==> P

      [| G|-Norm s -In1r (Expr e)>-n-> xs';
         !!s1 v. [| G|-Norm s -e->v-n-> s1; xs' = (dummy_res, s1) |] ==> P |]
      ==> P

      [| G|-Norm s -In1r (c1.0;; c2.0)>-n-> xs';
         !!s1 s2.
            [| G|-Norm s -c1.0-n-> s1; G|-s1 -c2.0-n-> s2; xs' = (dummy_res, s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (Methd C sig)>-n-> xs';
         !!n s1 v.
            [| G|-Norm s -body G C sig->v-n-> s1; n = Suc n; xs' = (In1 v, s1) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (Body D c)>-n-> xs';
         !!s1 s2.
            [| G|-Norm s -Init D-n-> s1; G|-s1 -c-n-> s2;
               xs' =
               (In1 (the (locals (snd s2) Result)),
                abupd (absorb Ret)
                 (if ∃l. fst s2 = Some (Jump (Break l)) ∨
                         fst s2 = Some (Jump (Cont l))
                  then abupd (%x. Some (Error CrossMethodJump)) s2 else s2)) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (e0.0 ? e1.0 : e2.0)>-n-> vs';
         !!b s1 s2 v.
            [| G|-Norm s -e0.0->b-n-> s1;
               G|-s1 -(if the_Bool b then e1.0 else e2.0)->v-n-> s2;
               vs' = (In1 v, s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (If(e) c1.0 Else c2.0)>-n-> xs';
         !!b s1 s2.
            [| G|-Norm s -e->b-n-> s1;
               G|-s1 -(if the_Bool b then c1.0 else c2.0)-n-> s2;
               xs' = (dummy_res, s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (l• While(e) c)>-n-> xs';
         !!b s1 s2 s3.
            [| G|-Norm s -e->b-n-> s1;
               if the_Bool b
               then G|-s1 -c-n-> s2 ∧
                    G|-abupd (absorb (Cont l)) s2 -l• While(e) c-n-> s3
               else s3 = s1;
               xs' = (dummy_res, s3) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (c1.0 Finally c2.0)>-n-> xs';
         !!s1 s2 x1.
            [| G|-Norm s -c1.0-n-> (x1, s1); G|-Norm s1 -c2.0-n-> s2;
               xs' =
               (dummy_res,
                if ∃err. x1 = Some (Error err) then (x1, s1)
                else abupd (abrupt_if (x1 ≠ None) x1) s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (Throw e)>-n-> xs';
         !!a' s1.
            [| G|-Norm s -e->a'-n-> s1; xs' = (dummy_res, abupd (throw a') s1) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (NewC C)>-n-> vs';
         !!a s1 s2.
            [| G|-Norm s -Init C-n-> s1; G|-s1 -halloc CInst C>a-> s2;
               vs' = (In1 (Addr a), s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (New T[e])>-n-> vs';
         !!a i' s1 s2 s3.
            [| G|-Norm s -init_comp_ty T-n-> s1; G|-s1 -e->i'-n-> s2;
               G|-abupd (check_neg i') s2 -halloc Arr T (the_Intg i')>a-> s3;
               vs' = (In1 (Addr a), s3) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l (va:=e)>-n-> vs';
         !!f s1 s2 v w.
            [| G|-Norm s -va=>(w, f)-n-> s1; G|-s1 -e->v-n-> s2;
               vs' = (In1 v, assign f v s2) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (Try c1.0 Catch(tn vn) c2.0)>-n-> xs';
         !!s1 s2 s3.
            [| G|-Norm s -c1.0-n-> s1; G|-s1 -sxalloc-> s2;
               if G,s2\<turnstile>catch tn then G|-new_xcpt_var vn s2 -c2.0-n-> s3
               else s3 = s2;
               xs' = (dummy_res, s3) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In2 ({accC,statDeclC,stat}e..fn)>-n-> vs';
         !!a s1 s2 s2' v.
            [| G|-Norm s -Init statDeclC-n-> s1; G|-s1 -e->a-n-> s2;
               (v, s2') = fvar statDeclC stat fn a s2;
               vs' = (In2 v, check_field_access G accC statDeclC fn stat a s2') |]
            ==> P |]
      ==> P

      [| G|-Norm s -In2 (e1.0.[e2.0])>-n-> vs';
         !!a i s1 s2 s2' v.
            [| G|-Norm s -e1.0->a-n-> s1; G|-s1 -e2.0->i-n-> s2;
               (v, s2') = avar G i a s2; vs' = (In2 v, s2') |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1l ({accC,statT,mode}e·mn( {pT}p))>-n-> vs';
         !!a' s1 s2 s4 v vs.
            [| G|-Norm s -e->a'-n-> s1; G|-s1 -p#>vs-n-> s2;
               G|-check_method_access G accC statT mode (| name = mn, parTs = pT |) a'
                   (init_lvars G
                     (invocation_declclass G mode (snd s2) a' statT
                       (| name = mn, parTs = pT |))
                     (| name = mn, parTs = pT |) mode a' vs
                     s2) -Methd
                           (invocation_declclass G mode (snd s2) a' statT
                             (| name = mn, parTs = pT |))
                           (| name = mn, parTs = pT |)->v-n-> s4;
               vs' = (In1 v, (set_lvars (locals (snd s2))) s4) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (Init C)>-n-> xs';
         !!s1 s2 s3.
            [| if inited C (globs s) then s3 = Norm s
               else G|-Norm ((init_class_obj G C)
                              s) -(if C = Object then Skip
                                   else Init (super (the (class G C))))-n-> s1 ∧
                    G|-(set_lvars empty) s1 -init (the (class G C))-n-> s2 ∧
                    s3 = (set_lvars (locals (snd s1))) s2;
               xs' = (dummy_res, s3) |]
            ==> P |]
      ==> P

      [| G|-Norm s -In1r (Init C)>-n-> xs';
         !!s1 s2 s3.
            [| if inited C (globs s) then s3 = Norm s
               else G|-Norm ((init_class_obj G C)
                              s) -(if C = Object then Skip
                                   else Init (super (the (class G C))))-n-> s1 ∧
                    G|-(set_lvars empty) s1 -init (the (class G C))-n-> s2 ∧
                    s3 = (set_lvars (locals (snd s1))) s2;
               xs' = (dummy_res, s3) |]
            ==> P |]
      ==> P

lemma evaln_Inj_elim:

      G|-s -t>-n-> (w, s')
      ==> case t of
          In1 ec => case ec of Inl e => ∃v. w = In1 v | Inr c => w = dummy_res
          | In2 e => ∃v. w = In2 v | In3 e => ∃v. w = In3 v

theorem evaln_expr_eq:

      G|-s -In1l t>-n-> (w, s') = (∃v. w = In1 v ∧ G|-s -t->v-n-> s')

theorem evaln_var_eq:

      G|-s -In2 t>-n-> (w, s') = (∃vf. w = In2 vf ∧ G|-s -t=>vf-n-> s')

theorem evaln_exprs_eq:

      G|-s -In3 t>-n-> (w, s') = (∃vs. w = In3 vs ∧ G|-s -t#>vs-n-> s')

theorem evaln_stmt_eq:

      G|-s -In1r t>-n-> (w, s') = (w = dummy_res ∧ G|-s -t-n-> s')

theorems evaln_AbruptIs:

      G|-(Some xc, s) -x->arbitrary-n-> (Some xc, s)

      G|-(Some xc, s) -x=>arbitrary-n-> (Some xc, s)

      G|-(Some xc, s) -x#>arbitrary-n-> (Some xc, s)

      G|-(Some xc, s) -x-n-> (Some xc, s)

lemma evaln_Callee:

      G|-Norm s -In1l (Callee l e)>-n-> (v, s') = False

lemma evaln_InsInitE:

      G|-Norm s -In1l (InsInitE c e)>-n-> (v, s') = False

lemma evaln_InsInitV:

      G|-Norm s -In2 (InsInitV c w)>-n-> (v, s') = False

lemma evaln_FinA:

      G|-Norm s -In1r (FinA a c)>-n-> (v, s') = False

lemma evaln_abrupt_lemma:

      G|-s -e>-n-> (v, s') ==> fst s = Some xc --> s' = s ∧ v = arbitrary3 e

lemma evaln_abrupt:

      G|-(Some xc, s) -e>-n-> (w, s') =
      (s' = (Some xc, s) ∧
       w = arbitrary3 e ∧ G|-(Some xc, s) -e>-n-> (arbitrary3 e, Some xc, s))

lemma evaln_LitI:

      G|-s -Lit v->(if normal s then v else arbitrary)-n-> s

lemma CondI:

      [| G|-s -e->b-n-> s1.0;
         G|-s1.0 -(if the_Bool b then e1.0 else e2.0)->v-n-> s2.0 |]
      ==> G|-s -e ? e1.0 : e2.0->(if normal s1.0 then v else arbitrary)-n-> s2.0

lemma evaln_SkipI:

      G|-s -Skip-n-> s

lemma evaln_ExprI:

      G|-s -e->v-n-> s' ==> G|-s -Expr e-n-> s'

lemma evaln_CompI:

      [| G|-s -c1.0-n-> s1.0; G|-s1.0 -c2.0-n-> s2.0 |] ==> G|-s -c1.0;; c2.0-n-> s2.0

lemma evaln_IfI:

      [| G|-s -e->v-n-> s1.0; G|-s1.0 -(if the_Bool v then c1.0 else c2.0)-n-> s2.0 |]
      ==> G|-s -If(e) c1.0 Else c2.0-n-> s2.0

lemma evaln_SkipD:

      G|-s -Skip-n-> s' ==> s' = s

lemma evaln_Skip_eq:

      G|-s -Skip-n-> s' = (s = s')

## evaln implies eval

lemma evaln_eval:

      G|-s0.0 -t>-n-> (v, s1.0) ==> G|-s0.0 -t>-> (v, s1.0)

lemma Suc_le_D_lemma:

      [| Suc n ≤ m'; !!m. n ≤ m ==> P (Suc m) |] ==> P m'

lemma evaln_nonstrict:

      [| G|-s -t>-n-> ws; n ≤ m |] ==> G|-s -t>-m-> ws

lemmas evaln_nonstrict_Suc:

      G|-s -t>-n-> ws ==> G|-s -t>-Suc n-> ws

lemmas evaln_nonstrict_Suc:

      G|-s -t>-n-> ws ==> G|-s -t>-Suc n-> ws

lemma evaln_max2:

      [| G|-s1.0 -t1.0>-n1.0-> ws1.0; G|-s2.0 -t2.0>-n2.0-> ws2.0 |]
      ==> G|-s1.0 -t1.0>-max n1.0 n2.0-> ws1.0 ∧ G|-s2.0 -t2.0>-max n1.0 n2.0-> ws2.0

corollary evaln_max2E:

      [| G|-s1.0 -t1.0>-n1.0-> ws1.0; G|-s2.0 -t2.0>-n2.0-> ws2.0;
         [| G|-s1.0 -t1.0>-max n1.0 n2.0-> ws1.0;
            G|-s2.0 -t2.0>-max n1.0 n2.0-> ws2.0 |]
         ==> P |]
      ==> P

lemma evaln_max3:

      [| G|-s1.0 -t1.0>-n1.0-> ws1.0; G|-s2.0 -t2.0>-n2.0-> ws2.0;
         G|-s3.0 -t3.0>-n3.0-> ws3.0 |]
      ==> G|-s1.0 -t1.0>-max (max n1.0 n2.0) n3.0-> ws1.0 ∧
          G|-s2.0 -t2.0>-max (max n1.0 n2.0) n3.0-> ws2.0 ∧
          G|-s3.0 -t3.0>-max (max n1.0 n2.0) n3.0-> ws3.0

corollary evaln_max3E:

      [| G|-s1.0 -t1.0>-n1.0-> ws1.0; G|-s2.0 -t2.0>-n2.0-> ws2.0;
         G|-s3.0 -t3.0>-n3.0-> ws3.0;
         [| G|-s1.0 -t1.0>-max (max n1.0 n2.0) n3.0-> ws1.0;
            G|-s2.0 -t2.0>-max (max n1.0 n2.0) n3.0-> ws2.0;
            G|-s3.0 -t3.0>-max (max n1.0 n2.0) n3.0-> ws3.0 |]
         ==> P |]
      ==> P

lemma le_max3I1:

      n2.0 ≤ max n1.0 (max n2.0 n3.0)

lemma le_max3I2:

      n3.0 ≤ max n1.0 (max n2.0 n3.0)

## eval implies evaln

lemma eval_evaln:

      G|-s0.0 -t>-> (v, s1.0) ==> ∃n. G|-s0.0 -t>-n-> (v, s1.0)