Theory Evaln

(*  Title:      HOL/Bali/Evaln.thy
    Author:     David von Oheimb and Norbert Schirmer
*)
subsection ‹Operational evaluation (big-step) semantics of Java expressions and 
          statements
›

theory Evaln imports TypeSafe begin


text ‹
Variant of termeval relation with counter for bounded recursive depth. 
In principal termevaln could replace termeval.

Validity of the axiomatic semantics builds on termevaln. 
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 termeval. 
So sometimes we have to switch between termevaln and termeval and vice 
versa. To make
this switch easy termevaln also does all the technical accessibility tests 
termcheck_field_access and termcheck_method_access like termeval. 
If it would omit them termevaln and termeval would only be equivalent 
for welltyped, and definitely assigned terms.
›

inductive
  evaln :: "[prog, state, term, nat, vals, state]  bool"
    ("__ _≻─_ '(_, _')" [61,61,80,61,0,0] 60)
  and evarn :: "[prog, state, var, vvar, nat, state]  bool"
    ("__ _=≻__ _" [61,61,90,61,61,61] 60)
  and eval_n:: "[prog, state, expr, val, nat, state]  bool"
    ("__ _-≻__ _" [61,61,80,61,61,61] 60)
  and evalsn :: "[prog, state, expr list, val  list, nat, state]  bool"
    ("__ _≐≻__ _" [61,61,61,61,61,61] 60)
  and execn     :: "[prog, state, stmt, nat, state]  bool"
    ("__ __ _"     [61,61,65,   61,61] 60)
  for G :: prog
where

  "Gs c     n    s'  Gs In1r  c≻─n (    ,  s')"
| "Gs e-≻v  n    s'  Gs In1l e≻─n (In1 v ,  s')"
| "Gs e=≻vf n    s'  Gs In2  e≻─n (In2 vf,  s')"
| "Gs e≐≻v  n    s'  Gs In3  e≻─n (In3 v ,  s')"

― ‹propagation of abrupt completion›

| Abrupt:   "G(Some xc,s) t≻─n (undefined3 t,(Some xc,s))"


― ‹evaluation of variables›

| LVar: "GNorm s LVar vn=≻lvar vn sn Norm s"

| FVar: "GNorm s0 Init statDeclCn s1; Gs1 e-≻an s2;
          (v,s2') = fvar statDeclC stat fn a s2;
          s3 = check_field_access G accC statDeclC fn stat a s2' 
          GNorm s0 {accC,statDeclC,stat}e..fn=≻vn s3"

| AVar: "G Norm s0 e1-≻an s1 ; Gs1 e2-≻in s2; 
          (v,s2') = avar G i a s2 
                      GNorm s0 e1.[e2]=≻vn s2'"




― ‹evaluation of expressions›

| NewC: "GNorm s0 Init Cn s1;
          G     s1 ─halloc (CInst C)a s2 
                                  GNorm s0 NewC C-≻Addr an s2"

| NewA: "GNorm s0 init_comp_ty Tn s1; Gs1 e-≻i'n s2; 
          Gabupd (check_neg i') s2 ─halloc (Arr T (the_Intg i'))a s3 
                                GNorm s0 New T[e]-≻Addr an s3"

| Cast: "GNorm s0 e-≻vn s1;
          s2 = abupd (raise_if (¬G,snd s1v fits T) ClassCast) s1 
                                GNorm s0 Cast T e-≻vn s2"

| Inst: "GNorm s0 e-≻vn s1;
          b = (vNull  G,store s1v fits RefT T) 
                              GNorm s0 e InstOf T-≻Bool bn s1"

| Lit:                     "GNorm s Lit v-≻vn Norm s"

| UnOp: "GNorm s0 e-≻vn s1 
          GNorm s0 UnOp unop e-≻(eval_unop unop v)n s1"

| BinOp: "GNorm s0 e1-≻v1n s1; 
           Gs1 (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
            ≻─n (In1 v2,s2) 
          GNorm s0 BinOp binop e1 e2-≻(eval_binop binop v1 v2)n s2"

| Super:                   "GNorm s Super-≻val_this sn Norm s"

| Acc:  "GNorm s0 va=≻(v,f)n s1 
                                  GNorm s0 Acc va-≻vn s1"

| Ass:  "GNorm s0 va=≻(w,f)n s1;
          G     s1 e-≻v     n s2 
                                   GNorm s0 va:=e-≻vn assign f v s2"

| Cond: "GNorm s0 e0-≻bn s1;
          G     s1 (if the_Bool b then e1 else e2)-≻vn s2 
                            GNorm s0 e0 ? e1 : e2-≻vn s2"

| Call: 
  "GNorm s0 e-≻a'n s1; Gs1 args≐≻vsn 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;
    Gs3'Methd D name=mn,parTs=pTs-≻vn s4
   
    
    GNorm s0 {accC,statT,mode}emn({pTs}args)-≻vn (restore_lvars s2 s4)"

| Methd:"GNorm s0 body G D sig-≻vn s1 
                                GNorm s0 Methd D sig-≻vSuc n s1"

| Body: "GNorm s0Init Dn s1; Gs1 cn 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)
         GNorm s0 Body D c
          -≻the (locals (store s2) Result)nabupd (absorb Ret) s3"

― ‹evaluation of expression lists›

| Nil:
                                "GNorm s0 []≐≻[]n Norm s0"

| Cons: "GNorm s0 e -≻ v n s1;
          G     s1 es≐≻vsn s2 
                             GNorm s0 e#es≐≻v#vsn s2"


― ‹execution of statements›

| Skip:                             "GNorm s Skipn Norm s"

| Expr: "GNorm s0 e-≻vn s1 
                                  GNorm s0 Expr en s1"

| Lab:  "GNorm s0 c n s1 
                             GNorm s0 l cn abupd (absorb l) s1"

| Comp: "GNorm s0 c1 n s1;
          G     s1 c2 n s2 
                                 GNorm s0 c1;; c2n s2"

| If:   "GNorm s0 e-≻bn s1;
          G     s1(if the_Bool b then c1 else c2)n s2 
                       GNorm s0 If(e) c1 Else c2 n s2"

| Loop: "GNorm s0 e-≻bn s1;
          if the_Bool b 
             then (Gs1 cn s2  
                   G(abupd (absorb (Cont l)) s2) l While(e) cn s3)
             else s3 = s1 
                              GNorm s0 l While(e) cn s3"
  
| Jmp: "GNorm s Jmp jn (Some (Jump j), s)"
  
| Throw:"GNorm s0 e-≻a'n s1 
                                 GNorm s0 Throw en abupd (throw a') s1"

| Try:  "GNorm s0 c1n s1; Gs1 ─sxalloc→ s2;
          if G,s2⊢catch tn then Gnew_xcpt_var vn s2 c2n s3 else s3 = s2
          
                  GNorm s0 Try c1 Catch(tn vn) c2n s3"

| Fin:  "GNorm s0 c1n (x1,s1);
          GNorm s1 c2n s2;
          s3=(if ( err. x1=Some (Error err)) 
              then (x1,s1) 
              else abupd (abrupt_if (x1None) x1) s2) 
              GNorm s0 c1 Finally c2n s3"
  
| Init: "the (class G C) = c;
          if inited C (globs s0) then s3 = Norm s0
          else (GNorm (init_class_obj G C s0)
                  (if C = Object then Skip else Init (super c))n s1 
                Gset_lvars Map.empty s1 init cn s2  
                s3 = restore_lvars s1 s2)
          
                 GNorm s0 Init Cn s3"
monos
  if_bool_eq_conj


declare if_split     [split del] if_split_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]
setup map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")

inductive_cases evaln_cases: "Gs t≻─n (v, s')"

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

declare if_split     [split] if_split_asm     [split] 
        option.split [split] option.split_asm [split]
        not_None_eq [simp] 
        split_paired_All [simp] split_paired_Ex [simp]
declaration K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))

lemma evaln_Inj_elim: "Gs t≻─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   (rename_tac a, 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 termIn1l into terms) always evaluates to ordinary values 
 (injection termIn1 into generalised values termvals). 
›

lemma evaln_expr_eq: "Gs In1l t≻─n (w, s') = (v. w=In1 v  Gs t-≻v n s')"
  by (auto, frule evaln_Inj_elim, auto)

lemma evaln_var_eq: "Gs In2 t≻─n (w, s') = (vf. w=In2 vf  Gs t=≻vfn s')"
  by (auto, frule evaln_Inj_elim, auto)

lemma evaln_exprs_eq: "Gs In3 t≻─n (w, s') = (vs. w=In3 vs  Gs t≐≻vsn s')"
  by (auto, frule evaln_Inj_elim, auto)

lemma evaln_stmt_eq: "Gs In1r t≻─n (w, s') = (w=  Gs t n s')"
  by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)

simproc_setup evaln_expr ("Gs In1l t≻─n (w, s')") = K (K (fn ct =>
    (case Thm.term_of ct of
      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    | _ => SOME (mk_meta_eq @{thm evaln_expr_eq}))))

simproc_setup evaln_var ("Gs In2 t≻─n (w, s')") = K (K (fn ct =>
    (case Thm.term_of ct of
      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    | _ => SOME (mk_meta_eq @{thm evaln_var_eq}))))

simproc_setup evaln_exprs ("Gs In3 t≻─n (w, s')") = K (K (fn ct =>
    (case Thm.term_of ct of
      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq}))))

simproc_setup evaln_stmt ("Gs In1r t≻─n (w, s')") = K (K (fn ct =>
    (case Thm.term_of ct of
      (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
    | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq}))))

ML ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate context @{thm evaln.Abrupt})
declare evaln_AbruptIs [intro!]

lemma evaln_Callee: "GNorm sIn1l (Callee l e)≻─n (v,s') = False"
proof -
  { fix s t v s'
    assume eval: "Gs t≻─n (v,s')" and
         normal: "normal s" and
         callee: "t=In1l (Callee l e)"
    then have "False" by induct auto
  }
  then show ?thesis
    by (cases s') fastforce 
qed

lemma evaln_InsInitE: "GNorm sIn1l (InsInitE c e)≻─n (v,s') = False"
proof -
  { fix s t v s'
    assume eval: "Gs t≻─n (v,s')" and
         normal: "normal s" and
         callee: "t=In1l (InsInitE c e)"
    then have "False" by induct auto
  }
  then show ?thesis
    by (cases s') fastforce
qed

lemma evaln_InsInitV: "GNorm sIn2 (InsInitV c w)≻─n (v,s') = False"
proof -
  { fix s t v s'
    assume eval: "Gs t≻─n (v,s')" and
         normal: "normal s" and
         callee: "t=In2 (InsInitV c w)"
    then have "False" by induct auto
  }  
  then show ?thesis
    by (cases s') fastforce
qed

lemma evaln_FinA: "GNorm sIn1r (FinA a c)≻─n (v,s') = False"
proof -
  { fix s t v s'
    assume eval: "Gs t≻─n (v,s')" and
         normal: "normal s" and
         callee: "t=In1r (FinA a c)"
    then have "False" by induct auto
  } 
  then show ?thesis
    by (cases s') fastforce
qed

lemma evaln_abrupt_lemma: "Gs e≻─n (v,s')  
 fst s = Some xc  s' = s  v = undefined3 e"
apply (erule evaln_cases , auto)
done

lemma evaln_abrupt: 
 "s'. G(Some xc,s) e≻─n (w,s') = (s' = (Some xc,s)   
  w=undefined3 e  G(Some xc,s) e≻─n (undefined3 e,(Some xc,s)))"
apply auto
apply (frule evaln_abrupt_lemma, auto)+
done

simproc_setup evaln_abrupt ("G(Some xc,s) e≻─n (w,s')") = K (K (fn ct =>
    (case Thm.term_of ct of
      (_ $ _ $ _ $ _ $ _ $ _ $ (Const (const_namePair, _) $ (Const (const_nameSome,_) $ _)$ _))
        => NONE
    | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))))

lemma evaln_LitI: "Gs Lit v-≻(if normal s then v else undefined)n s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Lit)

lemma CondI: 
 "s1. Gs e-≻bn s1; Gs1 (if the_Bool b then e1 else e2)-≻vn s2  
  Gs e ? e1 : e2-≻(if normal s1 then v else undefined)n s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Cond)

lemma evaln_SkipI [intro!]: "Gs Skipn s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Skip)

lemma evaln_ExprI: "Gs e-≻vn s'  Gs Expr en s'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Expr)

lemma evaln_CompI: "Gs c1n s1; Gs1 c2n s2  Gs c1;; c2n s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Comp)

lemma evaln_IfI: 
 "Gs e-≻vn s1; Gs1 (if the_Bool v then c1 else c2)n s2  
  Gs If(e) c1 Else c2n s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.If)

lemma evaln_SkipD [dest!]: "Gs Skipn s'  s' = s" 
by (erule evaln_cases, auto)

lemma evaln_Skip_eq [simp]: "Gs Skipn s' = (s = s')"
apply auto
done




subsubsection ‹evaln implies eval›

lemma evaln_eval:  
  assumes evaln: "Gs0 t≻─n (v,s1)" 
  shows "Gs0 t≻→ (v,s1)"
using evaln 
proof (induct)
  case (Loop s0 e b n s1 c s2 l s3)
  note GNorm s0 e-≻b s1
  moreover
  have "if the_Bool b
        then (Gs1 c s2)  
             Gabupd (absorb (Cont l)) s2 l While(e) c s3
        else s3 = s1"
    using Loop.hyps by simp
  ultimately show ?case by (rule eval.Loop)
next
  case (Try s0 c1 n s1 s2 C vn c2 s3)
  note GNorm s0 c1 s1
  moreover
  note Gs1 ─sxalloc→ s2
  moreover
  have "if G,s2⊢catch C then Gnew_xcpt_var vn s2 c2 s3 else s3 = s2"
    using Try.hyps by simp
  ultimately show ?case by (rule eval.Try)
next
  case (Init C c s0 s3 n s1 s2)
  note the (class G C) = c
  moreover
  have "if inited C (globs s0) 
           then s3 = Norm s0
           else GNorm ((init_class_obj G C) s0) 
                  (if C = Object then Skip else Init (super c)) s1 
                G(set_lvars Map.empty) s1 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]: 
  "Gs t≻─n (w, s')  m. nm  Gs t≻─m (w, s')"
apply (erule evaln.induct)
apply (tactic ALLGOALS (EVERY' [strip_tac context,
  TRY o eresolve_tac context @{thms Suc_le_D_lemma},
  REPEAT o smp_tac context 1, 
  resolve_tac context @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac context]))
(* 3 subgoals *)
apply (auto split del: if_split)
done

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

lemma evaln_max2: "Gs1 t1≻─n1 (w1, s1'); Gs2 t2≻─n2 (w2, s2')  
             Gs1 t1≻─max n1 n2 (w1, s1')  Gs2 t2≻─max n1 n2 (w2, s2')"
by (fast intro: max.cobounded1 max.cobounded2)

corollary evaln_max2E [consumes 2]:
  "Gs1 t1≻─n1 (w1, s1'); Gs2 t2≻─n2 (w2, s2'); 
    Gs1 t1≻─max n1 n2 (w1, s1');Gs2 t2≻─max n1 n2 (w2, s2')   P   P"
by (drule (1) evaln_max2) simp


lemma evaln_max3: 
"Gs1 t1≻─n1 (w1, s1'); Gs2 t2≻─n2 (w2, s2'); Gs3 t3≻─n3 (w3, s3') 
 Gs1 t1≻─max (max n1 n2) n3 (w1, s1') 
 Gs2 t2≻─max (max n1 n2) n3 (w2, s2')  
 Gs3 t3≻─max (max n1 n2) n3 (w3, s3')"
apply (drule (1) evaln_max2, erule thin_rl)
apply (fast intro!: max.cobounded1 max.cobounded2)
done

corollary evaln_max3E: 
"Gs1 t1≻─n1 (w1, s1'); Gs2 t2≻─n2 (w2, s2'); Gs3 t3≻─n3 (w3, s3');
   Gs1 t1≻─max (max n1 n2) n3 (w1, s1');
    Gs2 t2≻─max (max n1 n2) n3 (w2, s2'); 
    Gs3 t3≻─max (max n1 n2) n3 (w3, s3')
     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 max.cobounded1)
  also
  have "max n2 n3  max n1 (max n2 n3)"
    by (rule max.cobounded2)
  finally
  show ?thesis .
qed

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

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

subsubsection ‹eval implies evaln›
lemma eval_evaln: 
  assumes eval: "Gs0 t≻→ (v,s1)"
  shows  "n. Gs0 t≻─n (v,s1)"
using eval 
proof (induct)
  case (Abrupt xc s t)
  obtain n where
    "G(Some xc, s) t≻─n (undefined3 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 s0 e v s1)
  then obtain n where
    "GNorm s0 e-≻vn s1"
    by (iprover)
  then have "GNorm s0 Expr en s1"
    by (rule evaln.Expr) 
  then show ?case ..
next
  case (Lab s0 c s1 l)
  then obtain n where
    "GNorm s0 cn s1"
    by (iprover)
  then have "GNorm s0 l cn abupd (absorb l) s1"
    by (rule evaln.Lab)
  then show ?case ..
next
  case (Comp s0 c1 s1 c2 s2)
  then obtain n1 n2 where
    "GNorm s0 c1n1 s1"
    "Gs1 c2n2 s2"
    by (iprover)
  then have "GNorm s0 c1;; c2max n1 n2 s2"
    by (blast intro: evaln.Comp dest: evaln_max2 )
  then show ?case ..
next
  case (If s0 e b s1 c1 c2 s2)
  then obtain n1 n2 where
    "GNorm s0 e-≻bn1 s1"
    "Gs1 (if the_Bool b then c1 else c2)n2 s2"
    by (iprover)
  then have "GNorm s0 If(e) c1 Else c2max n1 n2 s2"
    by (blast intro: evaln.If dest: evaln_max2)
  then show ?case ..
next
  case (Loop s0 e b s1 c s2 l s3)
  from Loop.hyps obtain n1 where
    "GNorm s0 e-≻bn1 s1"
    by (iprover)
  moreover from Loop.hyps obtain n2 where
    "if the_Bool b 
        then (Gs1 cn2 s2  
              G(abupd (absorb (Cont l)) s2)l While(e) cn2 s3)
        else s3 = s1"
    by simp (iprover intro: evaln_nonstrict max.cobounded1 max.cobounded2)
  ultimately
  have "GNorm s0 l While(e) cmax n1 n2 s3"
    apply -
    apply (rule evaln.Loop)
    apply   (iprover intro: evaln_nonstrict intro: max.cobounded1)
    apply   (auto intro: evaln_nonstrict intro: max.cobounded2)
    done
  then show ?case ..
next
  case (Jmp s j)
  fix n have "GNorm s Jmp jn (Some (Jump j), s)"
    by (rule evaln.Jmp)
  then show ?case ..
next
  case (Throw s0 e a s1)
  then obtain n where
    "GNorm s0 e-≻an s1"
    by (iprover)
  then have "GNorm s0 Throw en abupd (throw a) s1"
    by (rule evaln.Throw)
  then show ?case ..
next 
  case (Try s0 c1 s1 s2 catchC vn c2 s3)
  from Try.hyps obtain n1 where
    "GNorm s0 c1n1 s1"
    by (iprover)
  moreover 
  note sxalloc = Gs1 ─sxalloc→ s2
  moreover
  from Try.hyps obtain n2 where
    "if G,s2⊢catch catchC then Gnew_xcpt_var vn s2 c2n2 s3 else s3 = s2"
    by fastforce 
  ultimately
  have "GNorm s0 Try c1 Catch(catchC vn) c2max n1 n2 s3"
    by (auto intro!: evaln.Try max.cobounded1 max.cobounded2)
  then show ?case ..
next
  case (Fin s0 c1 x1 s1 c2 s2 s3)
  from Fin obtain n1 n2 where 
    "GNorm s0 c1n1 (x1, s1)"
    "GNorm s1 c2n2 s2"
    by iprover
  moreover
  note s3 = s3 = (if err. x1 = Some (Error err) 
                   then (x1, s1)
                   else abupd (abrupt_if (x1  None) x1) s2)
  ultimately 
  have 
    "GNorm s0 c1 Finally c2max n1 n2 s3"
    by (blast intro: evaln.Fin dest: evaln_max2)
  then show ?case ..
next
  case (Init C c s0 s3 s1 s2)
  note cls = the (class G C) = c
  moreover from Init.hyps obtain n where
      "if inited C (globs s0) then s3 = Norm s0
       else (GNorm (init_class_obj G C s0)
              (if C = Object then Skip else Init (super c))n s1 
                   Gset_lvars Map.empty s1 init cn s2  
                   s3 = restore_lvars s1 s2)"
    by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
  ultimately have "GNorm s0 Init Cn s3"
    by (rule evaln.Init)
  then show ?case ..
next
  case (NewC s0 C s1 a s2)
  then obtain n where 
    "GNorm s0 Init Cn s1"
    by (iprover)
  with NewC 
  have "GNorm s0 NewC C-≻Addr an s2"
    by (iprover intro: evaln.NewC)
  then show ?case ..
next
  case (NewA s0 T s1 e i s2 a s3)
  then obtain n1 n2 where 
    "GNorm s0 init_comp_ty Tn1 s1"
    "Gs1 e-≻in2 s2"      
    by (iprover)
  moreover
  note Gabupd (check_neg i) s2 ─halloc Arr T (the_Intg i)a s3
  ultimately
  have "GNorm s0 New T[e]-≻Addr amax n1 n2 s3"
    by (blast intro: evaln.NewA dest: evaln_max2)
  then show ?case ..
next
  case (Cast s0 e v s1 s2 castT)
  then obtain n where
    "GNorm s0 e-≻vn s1"
    by (iprover)
  moreover 
  note s2 = abupd (raise_if (¬ G,snd s1v fits castT) ClassCast) s1
  ultimately
  have "GNorm s0 Cast castT e-≻vn s2"
    by (rule evaln.Cast)
  then show ?case ..
next
  case (Inst s0 e v s1 b T)
  then obtain n where
    "GNorm s0 e-≻vn s1"
    by (iprover)
  moreover 
  note b = (v  Null  G,snd s1v fits RefT T)
  ultimately
  have "GNorm s0 e InstOf T-≻Bool bn s1"
    by (rule evaln.Inst)
  then show ?case ..
next
  case (Lit s v)
  fix n have "GNorm s Lit v-≻vn Norm s"
    by (rule evaln.Lit)
  then show ?case ..
next
  case (UnOp s0 e v s1 unop)
  then obtain n where
    "GNorm s0 e-≻vn s1"
    by (iprover)
  hence "GNorm s0 UnOp unop e-≻eval_unop unop vn s1"
    by (rule evaln.UnOp)
  then show ?case ..
next
  case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
  then obtain n1 n2 where 
    "GNorm s0 e1-≻v1n1 s1"
    "Gs1 (if need_second_arg binop v1 then In1l e2
               else In1r Skip)≻─n2 (In1 v2, s2)"    
    by (iprover)
  hence "GNorm s0 BinOp binop e1 e2-≻(eval_binop binop v1 v2)max n1 n2
           s2"
    by (blast intro!: evaln.BinOp dest: evaln_max2)
  then show ?case ..
next
  case (Super s )
  fix n have "GNorm s Super-≻val_this sn Norm s"
    by (rule evaln.Super)
  then show ?case ..
next
  case (Acc s0 va v f s1)
  then obtain n where
    "GNorm s0 va=≻(v, f)n s1"
    by (iprover)
  then
  have "GNorm s0 Acc va-≻vn s1"
    by (rule evaln.Acc)
  then show ?case ..
next
  case (Ass s0 var w f s1 e v s2)
  then obtain n1 n2 where 
    "GNorm s0 var=≻(w, f)n1 s1"
    "Gs1 e-≻vn2 s2"      
    by (iprover)
  then
  have "GNorm s0 var:=e-≻vmax n1 n2 assign f v s2"
    by (blast intro: evaln.Ass dest: evaln_max2)
  then show ?case ..
next
  case (Cond s0 e0 b s1 e1 e2 v s2)
  then obtain n1 n2 where 
    "GNorm s0 e0-≻bn1 s1"
    "Gs1 (if the_Bool b then e1 else e2)-≻vn2 s2"
    by (iprover)
  then
  have "GNorm s0 e0 ? e1 : e2-≻vmax n1 n2 s2"
    by (blast intro: evaln.Cond dest: evaln_max2)
  then show ?case ..
next
  case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
  then obtain n1 n2 where
    "GNorm s0 e-≻a'n1 s1"
    "Gs1 args≐≻vsn2 s2"
    by iprover
  moreover
  note invDeclC = invocation_declclass G mode (store s2) a' statT 
                       name=mn,parTs=pTs'
  moreover
  note s3 = init_lvars G invDeclC name=mn,parTs=pTs' mode a' vs s2
  moreover
  note s3'=check_method_access G accC' statT mode name=mn,parTs=pTs' a' s3
  moreover 
  from Call.hyps
  obtain m where 
    "Gs3' Methd invDeclC name=mn, parTs=pTs'-≻vm s4"
    by iprover
  ultimately
  have "GNorm s0 {accC',statT,mode}emn( {pTs'}args)-≻vmax n1 (max n2 m) 
            (set_lvars (locals (store s2))) s4"
    by (auto intro!: evaln.Call max.cobounded1 le_max3I1 le_max3I2)
  thus ?case ..
next
  case (Methd s0 D sig v s1)
  then obtain n where
    "GNorm s0 body G D sig-≻vn s1"
    by iprover
  then have "GNorm s0 Methd D sig-≻vSuc n s1"
    by (rule evaln.Methd)
  then show ?case ..
next
  case (Body s0 D s1 c s2 s3)
  from Body.hyps obtain n1 n2 where 
    evaln_init: "GNorm s0 Init Dn1 s1" and
    evaln_c: "Gs1 cn2 s2"
    by (iprover)
  moreover
  note 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
     "GNorm s0 Body D c-≻the (locals (store s2) Result)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
    "GNorm s LVar vn=≻lvar vn sn Norm s"
    by (iprover intro: evaln.LVar)
  then show ?case ..
next
  case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
  then obtain n1 n2 where
    "GNorm s0 Init statDeclCn1 s1"
    "Gs1 e-≻an2 s2"
    by iprover
  moreover
  note s3 = check_field_access G accC statDeclC fn stat a s2'
    and (v, s2') = fvar statDeclC stat fn a s2
  ultimately
  have "GNorm s0 {accC,statDeclC,stat}e..fn=≻vmax n1 n2 s3"
    by (iprover intro: evaln.FVar dest: evaln_max2)
  then show ?case ..
next
  case (AVar s0 e1 a s1 e2 i s2 v s2')
  then obtain n1 n2 where 
    "GNorm s0 e1-≻an1 s1"
    "Gs1 e2-≻in2 s2"      
    by iprover
  moreover 
  note (v, s2') = avar G i a s2
  ultimately 
  have "GNorm s0 e1.[e2]=≻vmax 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 s0 e v s1 es vs s2)
  then obtain n1 n2 where 
    "GNorm s0 e-≻vn1 s1"
    "Gs1 es≐≻vsn2 s2"      
    by iprover
  then
  have "GNorm s0 e # es≐≻v # vsmax n1 n2 s2"
    by (blast intro!: evaln.Cons dest: evaln_max2)
  then show ?case ..
qed

end