Quelle  Eval.thy

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

theory Eval imports State DeclConcepts begin

text ‹
 
 improvements over Java Specification 1.0:
 \begin{itemize}
 \item dynamic method lookup does not need to consider the return type
  (cf.15.11.4.4)
 \item throw raises a NullPointer exception if a null reference is given, and
  each throw of a standard exception yield a fresh exception object
  (was not specified)
 \item if there is not enough memory even to allocate an OutOfMemory exception,
  evaluation/execution fails, i.e. simply stops (was not specified)
 \item array assignment checks lhs (and may throw exceptions) before evaluating
  rhs
 \item fixed exact positions of class initializations
  (immediate at first active use)
 \end{itemize}
 
 design issues:
 \begin{itemize}
 \item evaluation vs. (single-step) transition semantics
  evaluation semantics chosen, because:
  \begin{itemize}
  \item[++] less verbose and therefore easier to read (and to handle in proofs)
  \item[+] more abstract
  \item[+] intermediate values (appearing in recursive rules) need not be
  stored explicitly, e.g. no call body construct or stack of invocation
  frames containing local variables and return addresses for method calls
  needed
  \item[+] convenient rule induction for subject reduction theorem
  \item[-] no interleaving (for parallelism) can be described
  \item[-] stating a property of infinite executions requires the meta-level
  argument that this property holds for any finite prefixes of it
  (e.g. stopped using a counter that is decremented to zero and then
  throwing an exception)
  \end{itemize}
 \item unified evaluation for variables, expressions, expression lists,
  statements
 \item the value entry in statement rules is redundant
 \item the value entry in rules is irrelevant in case of exceptions, but its full
  inclusion helps to make the rule structure independent of exception occurrence.
 \item as irrelevant value entries are ignored, it does not matter if they are
  unique.
  For simplicity, (fixed) arbitrary values are preferred over "free" values.
 \item the rule format is such that the start state may contain an exception.
  \begin{itemize}
  \item[++] faciliates exception handling
  \item[+] symmetry
  \end{itemize}
 \item the rules are defined carefully in order to be applicable even in not
  type-correct situations (yielding undefined values),
  e.g. ‹the_Addr (Val (Bool b)) = undefined›.
  \begin{itemize}
  \item[++] fewer rules
  \item[-] less readable because of auxiliary functions like ‹the_Addr›
  \end{itemize}
  Alternative: "defensive" evaluation throwing some InternalError exception
  in case of (impossible, for correct programs) type mismatches
 \item there is exactly one rule per syntactic construct
  \begin{itemize}
  \item[+] no redundancy in case distinctions
  \end{itemize}
 \item halloc fails iff there is no free heap address. When there is
  only one free heap address left, it returns an OutOfMemory exception.
  In this way it is guaranteed that when an OutOfMemory exception is thrown for
  the first time, there is a free location on the heap to allocate it.
 \item the allocation of objects that represent standard exceptions is deferred
  until execution of any enclosing catch clause, which is transparent to
  the program.
  \begin{itemize}
  \item[-] requires an auxiliary execution relation
  \item[++] avoids copies of allocation code and awkward case distinctions
  (whether there is enough memory to allocate the exception) in
  evaluation rules
  \end{itemize}
 \item unfortunately ‹new_Addr› is not directly executable because of
  Hilbert operator.
 \end{itemize}
 simplifications:
 \begin{itemize}
 \item local variables are initialized with default values
  (no definite assignment)
 \item garbage collection not considered, therefore also no finalizers
 \item stack overflow and memory overflow during class initialization not
  modelled
 \item exceptions in initializations not replaced by ExceptionInInitializerError
 \end{itemize}
 ›


type_synonym vvar = "val × (val ==> state ==> state)"
type_synonym vals = "(val, vvar, val list) sum3"
translations
  (type) "vvar" <= (type) "val × (val ==> state ==> state)"
  (type) "vals" <= (type) "(val, vvar, val list) sum3" 

text ‹To avoid redundancy and to reduce the number of rules, there is only
  one evaluation rule for each syntactic term. This is also true for variables
  (e.g. see the rules below for ‹LVar›, ‹FVar› and ‹AVar›).
  So evaluation of a variable must capture both possible further uses:
  read (rule ‹Acc›) or write (rule ‹Ass›) to the variable.
  Therefor a variable evaluates to a special value 🍋‹vvar›, which is
  a pair, consisting of the current value (for later read access) and an update
  function (for later write access). Because
  during assignment to an array variable an exception may occur if the types
  don't match, the update function is very generic: it transforms the
  full state. This generic update function causes some technical trouble during
  some proofs (e.g. type safety, correctness of definite assignment). There we
  need to prove some additional invariant on this update function to prove the
  assignment correct, since the update function could potentially alter the whole
  state in an arbitrary manner. This invariant must be carried around through
  the whole induction.
  So for future approaches it may be better not to take
  such a generic update function, but only to store the address and the kind
  of variable (array (+ element type), local variable or field) for later
  assignment.
 ›

abbreviation
  dummy_res :: "vals" (‹♢›)
  where "♢ == In1 Unit"

abbreviation (input)
  val_inj_vals (‹⌊_⌋🪙e› 1000)
  where "⌊e⌋🪙e == In1 e"

abbreviation (input)
  var_inj_vals  (‹⌊_⌋🪙v› 1000)
  where "⌊v⌋🪙v == In2 v"

abbreviation (input)
  lst_inj_vals  (‹⌊_⌋🪙l› 1000)
  where "⌊es⌋🪙l == In3 es"

definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 ==> vals" where
 "undefined3 = case_sum3 (In1 ∘ case_sum (λx. undefined) (λx. Unit))
                     (λx. In2 undefined) (λx. In3 undefined)"

lemma [simp]: "undefined3 (In1l x) = In1 undefined"
by (simp add: undefined3_def)

lemma [simp]: "undefined3 (In1r x) = ♢"
by (simp add: undefined3_def)

lemma [simp]: "undefined3 (In2 x) = In2 undefined"
by (simp add: undefined3_def)

lemma [simp]: "undefined3 (In3 x) = In3 undefined"
by (simp add: undefined3_def)


subsubsection "exception throwing and catching"

definition
  throw :: "val ==> abopt ==> abopt" where
  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"

lemma throw_def2: 
 "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
apply (unfold throw_def)
apply (simp (no_asm))
done

definition
  fits :: "prog ==> st ==> val ==> ty ==> bool" (‹_,_⊨_ fits _›[61,61,61,61]60)
  where "G,s⊨a' fits T = ((∃rt. T=RefT rt) ⟶ a'=Null ∨ G⊨obj_ty(lookup_obj s a')⪯T)"

lemma fits_Null [simp]: "G,s⊨Null fits T"
by (simp add: fits_def)


lemma fits_Addr_RefT [simp]:
  "G,s⊨Addr a fits RefT t = G⊨obj_ty (the (heap s a))⪯RefT t"
by (simp add: fits_def)

lemma fitsD: "∧X. G,s⊨a' fits T ==> (∃pt. T = PrimT pt) ∨
  (∃t. T = RefT t) ∧ a' = Null ∨
  (∃t. T = RefT t) ∧ a' ≠ Null ∧ G⊨obj_ty (lookup_obj s a')⪯T"
apply (unfold fits_def)
apply (case_tac "∃pt. T = PrimT pt")
apply  simp_all
apply (case_tac "T")
defer 
apply (case_tac "a' = Null")
apply  simp_all
done

definition
  catch :: "prog ==> state ==> qtname ==> bool" (‹_,_⊨catch _›[61,61,61]60) where
  "G,s⊨catch C = (∃xc. abrupt s=Some (Xcpt xc) ∧
                        G,store s⊨Addr (the_Loc xc) fits Class C)"

lemma catch_Norm [simp]: "¬G,Norm s⊨catch tn"
apply (unfold catch_def)
apply (simp (no_asm))
done

lemma catch_XcptLoc [simp]: 
  "G,(Some (Xcpt (Loc a)),s)⊨catch C = G,s⊨Addr a fits Class C"
apply (unfold catch_def)
apply (simp (no_asm))
done

lemma catch_Jump [simp]: "¬G,(Some (Jump j),s)⊨catch tn"
apply (unfold catch_def)
apply (simp (no_asm))
done

lemma catch_Error [simp]: "¬G,(Some (Error e),s)⊨catch tn"
apply (unfold catch_def)
apply (simp (no_asm))
done

definition
  new_xcpt_var :: "vname ==> state ==> state" where
  "new_xcpt_var vn = (λ(x,s). Norm (lupd(VName vn↦Addr (the_Loc (the_Xcpt (the x)))) s))"

lemma new_xcpt_var_def2 [simp]: 
 "new_xcpt_var vn (x,s) =
    Norm (lupd(VName vn↦Addr (the_Loc (the_Xcpt (the x)))) s)"
apply (unfold new_xcpt_var_def)
apply (simp (no_asm))
done



subsubsection "misc"

definition
  assign :: "('a ==> state ==> state) ==> 'a ==> state ==> state" where
 "assign f v = (λ(x,s). let (x',s') = (if x = None then f v else id) (x,s)
                        in (x',if x' = None then s' else s))"

(*
 lemma assign_Norm_Norm [simp]:
 "f v (abrupt=None,store=s) = (abrupt=None,store=s')
  ==> assign f v (abrupt=None,store=s) = (abrupt=None,store=s')"
 by (simp add: assign_def Let_def)
*)

lemma assign_Norm_Norm [simp]: 
"f v (Norm s) = Norm s' ==> assign f v (Norm s) = Norm s'"
by (simp add: assign_def Let_def)

(*
 lemma assign_Norm_Some [simp]:
  "[abrupt (f v (abrupt=None,store=s)) = Some y]
  ==> assign f v (abrupt=None,store=s) = (abrupt=Some y,store =s)"
 by (simp add: assign_def Let_def split_beta)
*)

lemma assign_Norm_Some [simp]: 
  "[abrupt (f v (Norm s)) = Some y]
   ==> assign f v (Norm s) = (Some y,s)"
by (simp add: assign_def Let_def split_beta)


lemma assign_Some [simp]: 
"assign f v (Some x,s) = (Some x,s)" 
by (simp add: assign_def Let_def split_beta)

lemma assign_Some1 [simp]:  "¬ normal s ==> assign f v s = s" 
by (auto simp add: assign_def Let_def split_beta)

lemma assign_supd [simp]: 
"assign (λv. supd (f v)) v (x,s)
  = (x, if x = None then f v s else s)"
apply auto
done

lemma assign_raise_if [simp]: 
  "assign (λv (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =
  (raise_if (b s v) xcpt x, if x=None ∧ ¬b s v then f v s else s)"
apply (case_tac "x = None")
apply auto
done


(*
 lemma assign_raise_if [simp]:
  "assign (λv s. (abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
  store = f v (store s))) v s =
  (abrupt=raise_if (b (store s) v) xcpt (abrupt s),
  store= if (abrupt s)=None ∧ ¬b (store s) v
  then f v (store s) else (store s))"
 apply (case_tac "abrupt s = None")
 apply auto
 done
*)

definition
  init_comp_ty :: "ty ==> stmt"
  where "init_comp_ty T = (if (∃C. T = Class C) then Init (the_Class T) else Skip)"

lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
apply (unfold init_comp_ty_def)
apply (simp (no_asm))
done

definition
  invocation_class :: "inv_mode ==> st ==> val ==> ref_ty ==> qtname" where
 "invocation_class m s a' statT =
    (case m of
       Static ==> if (∃ statC. statT = ClassT statC)
                    then the_Class (RefT statT)
                    else Object
     | SuperM ==> the_Class (RefT statT)
     | IntVir ==> obj_class (lookup_obj s a'))"

definition
  invocation_declclass :: "prog ==> inv_mode ==> st ==> val ==> ref_ty ==> sig ==> qtname" where
  "invocation_declclass G m s a' statT sig =
    declclass (the (dynlookup G statT
                                (invocation_class m s a' statT)
                                sig))" 
  
lemma invocation_class_IntVir [simp]: 
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
by (simp add: invocation_class_def)

lemma dynclass_SuperM [simp]: 
 "invocation_class SuperM s a' statT = the_Class (RefT statT)"
by (simp add: invocation_class_def)

lemma invocation_class_Static [simp]: 
  "invocation_class Static s a' statT = (if (∃ statC. statT = ClassT statC)
                                            then the_Class (RefT statT)
                                            else Object)"
by (simp add: invocation_class_def)

definition
  init_lvars :: "prog ==> qtname ==> sig ==> inv_mode ==> val ==> val list ==> state ==> state"
where
  "init_lvars G C sig mode a' pvs =
    (λ(x,s).
      let m = mthd (the (methd G C sig));
          l = λ k.
              (case k of
                 EName e
                   ==> (case e of
                         VNam v ==> (Map.empty ((pars m)[↦]pvs)) v
                       | Res ==> None)
               | This
                   ==> (if mode=Static then None else Some a'))
      in set_lvars l (if mode = Static then x else np a' x,s))"



lemma init_lvars_def2: 🍋 ‹better suited for simplification›
"init_lvars G C sig mode a' pvs (x,s) =
  set_lvars
    (λ k.
       (case k of
          EName e
            ==> (case e of
                  VNam v
                  ==> (Map.empty ((pars (mthd (the (methd G C sig))))[↦]pvs)) v
               | Res ==> None)
        | This
            ==> (if mode=Static then None else Some a')))
    (if mode = Static then x else np a' x,s)"
apply (unfold init_lvars_def)
apply (simp (no_asm) add: Let_def)
done

definition
  body :: "prog ==> qtname ==> sig ==> expr" where
 "body G C sig =
    (let m = the (methd G C sig)
     in Body (declclass m) (stmt (mbody (mthd m))))"

lemma body_def2: 🍋 ‹better suited for simplification›
"body G C sig = Body (declclass (the (methd G C sig)))
                      (stmt (mbody (mthd (the (methd G C sig)))))"
apply (unfold body_def Let_def)
apply auto
done

subsubsection "variables"

definition
  lvar :: "lname ==> st ==> vvar"
  where "lvar vn s = (the (locals s vn), λv. supd (lupd(vn↦v)))"

definition
  fvar :: "qtname ==> bool ==> vname ==> val ==> state ==> vvar × state" where
 "fvar C stat fn a' s =
   (let (oref,xf) = if stat then (Stat C,id)
                            else (Heap (the_Addr a'),np a');
                  n = Inl (fn,C);
                  f = (λv. supd (upd_gobj oref n v))
    in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"

definition
  avar :: "prog ==> val ==> val ==> state ==> vvar × state" where
  "avar G i' a' s =
    (let oref = Heap (the_Addr a');
              i = the_Intg i';
              n = Inr i;
       (T,k,cs) = the_Arr (globs (store s) oref);
              f = (λv (x,s). (raise_if (¬G,s⊨v fits T)
                                           ArrStore x
                              ,upd_gobj oref n v s))
     in ((the (cs n),f),abupd (raise_if (¬i in_bounds k) IndOutBound ∘ np a') s))"

lemma fvar_def2: 🍋 ‹better suited for simplification›
"fvar C stat fn a' s =
  ((the
     (values
      (the (globs (store s) (if stat then Stat C else Heap (the_Addr a'))))
      (Inl (fn,C)))
   ,(λv. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a'))
                        (Inl (fn,C))
                        v)))
  ,abupd (if stat then id else np a') s)
  "
apply (unfold fvar_def)
apply (simp (no_asm) add: Let_def split_beta)
done

lemma avar_def2: 🍋 ‹better suited for simplification›
"avar G i' a' s =
  ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a'))))))
           (Inr (the_Intg i')))
   ,(λv (x,s'). (raise_if (¬G,s'⊨v fits (fst(the_Arr (globs (store s)
                                                   (Heap (the_Addr a'))))))
                            ArrStore x
                 ,upd_gobj (Heap (the_Addr a'))
                               (Inr (the_Intg i')) v s')))
  ,abupd (raise_if (¬(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s)
                   (Heap (the_Addr a'))))))) IndOutBound ∘ np a')
          s)"
apply (unfold avar_def)
apply (simp (no_asm) add: Let_def split_beta)
done

definition
  check_field_access :: "prog ==> qtname ==> qtname ==> vname ==> bool ==> val ==> state ==> state" where
  "check_field_access G accC statDeclC fn stat a' s =
    (let oref = if stat then Stat statDeclC
                else Heap (the_Addr a');
         dynC = case oref of
                   Heap a ==> obj_class (the (globs (store s) oref))
                 | Stat C ==> C;
         f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
     in abupd
        (error_if (¬ G⊨Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
                  AccessViolation)
        s)"

definition
  check_method_access :: "prog ==> qtname ==> ref_ty ==> inv_mode ==> sig ==> val ==> state ==> state" where
  "check_method_access G accC statT mode sig a' s =
    (let invC = invocation_class mode (store s) a' statT;
       dynM = the (dynlookup G statT invC sig)
     in abupd
        (error_if (¬ G⊨Methd sig dynM in invC dyn_accessible_from accC)
                  AccessViolation)
        s)"
       
subsubsection "evaluation judgments"

inductive
  halloc :: "[prog,state,obj_tag,loc,state]==>bool" (‹_⊨_ ←-halloc _≻_→ _›[61,61,61,61,61]60) for G::prog
where 🍋 ‹allocating objects on the heap, cf. 12.5›

  Abrupt: 
  "G⊨(Some x,s) ←-halloc oi≻undefined→ (Some x,s)"

| New:    "[new_Addr (heap s) = Some a;
            (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
                       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))]
            ==>
            G⊨Norm s ←-halloc oi≻a→ (x,init_obj G oi' (Heap a) s)"

inductive sxalloc :: "[prog,state,state]==>bool" (‹_⊨_ ←-sxalloc→ _›[61,61,61]60) for G::prog
where 🍋 ‹allocating exception objects for
  standard exceptions (other than OutOfMemory)›

  Norm:  "G⊨ Norm s ←-sxalloc→ Norm s"

| Jmp:   "G⊨(Some (Jump j), s) ←-sxalloc→ (Some (Jump j), s)"

| Error: "G⊨(Some (Error e), s) ←-sxalloc→ (Some (Error e), s)"

| XcptL: "G⊨(Some (Xcpt (Loc a) ),s) ←-sxalloc→ (Some (Xcpt (Loc a)),s)"

| SXcpt: "[G⊨Norm s0 ←-halloc (CInst (SXcpt xn))≻a→ (x,s1)] ==>
          G⊨(Some (Xcpt (Std xn)),s0) ←-sxalloc→ (Some (Xcpt (Loc a)),s1)"


inductive
  eval :: "[prog,state,term,vals,state]==>bool" (‹_⊨_ ←-_≻→ '(_, _')›  [61,61,80,0,0]60)
  and exec ::"[prog,state,stmt ,state]==>bool"(‹_⊨_ ←-_→ _›   [61,61,65,   61]60)
  and evar ::"[prog,state,var ,vvar,state]==>bool"(‹_⊨_ ←-_=≻_→ _›[61,61,90,61,61]60)
  and eval'::"[prog,state,expr ,val ,state]==>bool"(‹_⊨_ ←-_-≻_→ _›[61,61,80,61,61]60)
  and evals::"[prog,state,expr list ,
                    val list ,state]==>bool"(‹_⊨_ ←-_≐≻_→ _›[61,61,61,61,61]60)
  for G::prog
where

  "G⊨s ←-c → s' ≡ G⊨s ←-In1r c≻→ (♢, s')"
| "G⊨s ←-e-≻v → s' ≡ G⊨s ←-In1l e≻→ (In1 v, s')"
| "G⊨s ←-e=≻vf→ s' ≡ G⊨s ←-In2 e≻→ (In2 vf, s')"
| "G⊨s ←-e≐≻v → s' ≡ G⊨s ←-In3 e≻→ (In3 v, s')"

🍋 ‹propagation of abrupt completion›

  🍋 ‹cf. 14.1, 15.5›
| Abrupt: 
   "G⊨(Some xc,s) ←-t≻→ (undefined3 t, (Some xc, s))"


🍋 ‹execution of statements›

  🍋 ‹cf. 14.5›
| Skip:                             "G⊨Norm s ←-Skip→ Norm s"

  🍋 ‹cf. 14.7›
| Expr: "[G⊨Norm s0 ←-e-≻v→ s1] ==>
                                  G⊨Norm s0 ←-Expr e→ s1"

| Lab:  "[G⊨Norm s0 ←-c → s1] ==>
                                G⊨Norm s0 ←-l∙ c→ abupd (absorb l) s1"
  🍋 ‹cf. 14.2›
| Comp: "[G⊨Norm s0 ←-c1 → s1;
          G⊨ s1 ←-c2 → s2] ==>
                                 G⊨Norm s0 ←-c1;; c2→ s2"

  🍋 ‹cf. 14.8.2›
| If:   "[G⊨Norm s0 ←-e-≻b→ s1;
          G⊨ s1←-(if the_Bool b then c1 else c2)→ s2] ==>
                       G⊨Norm s0 ←-If(e) c1 Else c2 → s2"

  🍋 ‹cf. 14.10, 14.10.1›
  
  🍋 ‹A continue jump from the while body 🍋‹c› is handled by
  this rule. If a continue jump with the proper label was invoked inside
  🍋‹c› this label (Cont l) is deleted out of the abrupt component of
  the state before the iterative evaluation of the while statement.
  A break jump is handled by the Lab Statement ‹Lab l (while…)›.›
| Loop: "[G⊨Norm s0 ←-e-≻b→ s1;
          if the_Bool b
             then (G⊨s1 ←-c→ s2 ∧
                   G⊨(abupd (absorb (Cont l)) s2) ←-l∙ While(e) c→ s3)
             else s3 = s1] ==>
                              G⊨Norm s0 ←-l∙ While(e) c→ s3"

| Jmp: "G⊨Norm s ←-Jmp j→ (Some (Jump j), s)"
   
  🍋 ‹cf. 14.16›
| Throw: "[G⊨Norm s0 ←-e-≻a'→ s1] ==>
                                 G⊨Norm s0 ←-Throw e→ abupd (throw a') s1"

  🍋 ‹cf. 14.18.1›
| Try:  "[G⊨Norm s0 ←-c1→ s1; G⊨s1 ←-sxalloc→ s2;
          if G,s2⊨catch C then G⊨new_xcpt_var vn s2 ←-c2→ s3 else s3 = s2] ==>
                  G⊨Norm s0 ←-Try c1 Catch(C vn) c2→ s3"

  🍋 ‹cf. 14.18.2›
| Fin:  "[G⊨Norm s0 ←-c1→ (x1,s1);
          G⊨Norm s1 ←-c2→ s2;
          s3=(if (∃ err. x1=Some (Error err))
              then (x1,s1)
              else abupd (abrupt_if (x1≠None) x1) s2) ]
          ==>
          G⊨Norm s0 ←-c1 Finally c2→ s3"
  🍋 ‹cf. 12.4.2, 8.5›
| Init: "[the (class G C) = c;
          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 c))→ s1 ∧
               G⊨set_lvars Map.empty s1 ←-init c→ s2 ∧ s3 = restore_lvars s1 s2)]
              ==>
                 G⊨Norm s0 ←-Init C→ s3"
   🍋 ‹This class initialisation rule is a little bit inaccurate. Look at the
  exact sequence:
  (1) The current class object (the static fields) are initialised
  (‹init_class_obj›),
  (2) the superclasses are initialised,
  (3) the static initialiser of the current class is invoked.
  More precisely we should expect another ordering, namely 2 1 3.
  But we can't just naively toggle 1 and 2. By calling
  ‹init_class_obj›
  before initialising the superclasses, we also implicitly record that
  we have started to initialise the current class (by setting an
  value for the class object). This becomes
  crucial for the completeness proof of the axiomatic semantics
  ‹AxCompl.thy›. Static initialisation requires an induction on
  the number of classes not yet initialised (or to be more precise,
  classes were the initialisation has not yet begun).
  So we could first assign a dummy value to the class before
  superclass initialisation and afterwards set the correct values.
  But as long as we don't take memory overflow into account
  when allocating class objects, we can leave things as they are for
  convenience.›
🍋 ‹evaluation of expressions›

  🍋 ‹cf. 15.8.1, 12.4.1›
| NewC: "[G⊨Norm s0 ←-Init C→ s1;
          G⊨ s1 ←-halloc (CInst C)≻a→ s2] ==>
                                  G⊨Norm s0 ←-NewC C-≻Addr a→ s2"

  🍋 ‹cf. 15.9.1, 12.4.1›
| NewA: "[G⊨Norm s0 ←-init_comp_ty T→ s1; G⊨s1 ←-e-≻i'→ s2;
          G⊨abupd (check_neg i') s2 ←-halloc (Arr T (the_Intg i'))≻a→ s3] ==>
                                G⊨Norm s0 ←-New T[e]-≻Addr a→ s3"

  🍋 ‹cf. 15.15›
| Cast: "[G⊨Norm s0 ←-e-≻v→ s1;
          s2 = abupd (raise_if (¬G,store s1⊨v fits T) ClassCast) s1] ==>
                                G⊨Norm s0 ←-Cast T e-≻v→ s2"

  🍋 ‹cf. 15.19.2›
| Inst: "[G⊨Norm s0 ←-e-≻v→ s1;
          b = (v≠Null ∧ G,store s1⊨v fits RefT T)] ==>
                              G⊨Norm s0 ←-e InstOf T-≻Bool b→ s1"

  🍋 ‹cf. 15.7.1›
| Lit:  "G⊨Norm s ←-Lit v-≻v→ Norm s"

| UnOp: "[G⊨Norm s0 ←-e-≻v→ s1]
         ==> G⊨Norm s0 ←-UnOp unop e-≻(eval_unop unop v)→ s1"
 
| BinOp: "[G⊨Norm s0 ←-e1-≻v1→ s1;
          G⊨s1 ←-(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
                ≻→ (In1 v2, s2)
          ]
         ==> G⊨Norm s0 ←-BinOp binop e1 e2-≻(eval_binop binop v1 v2)→ s2"
   
  🍋 ‹cf. 15.10.2›
| Super: "G⊨Norm s ←-Super-≻val_this s→ Norm s"

  🍋 ‹cf. 15.2›
| Acc:  "[G⊨Norm s0 ←-va=≻(v,f)→ s1] ==>
                                  G⊨Norm s0 ←-Acc va-≻v→ s1"

  🍋 ‹cf. 15.25.1›
| Ass:  "[G⊨Norm s0 ←-va=≻(w,f)→ s1;
          G⊨ s1 ←-e-≻v → s2] ==>
                                   G⊨Norm s0 ←-va:=e-≻v→ assign f v s2"

  🍋 ‹cf. 15.24›
| Cond: "[G⊨Norm s0 ←-e0-≻b→ s1;
          G⊨ s1 ←-(if the_Bool b then e1 else e2)-≻v→ s2] ==>
                            G⊨Norm s0 ←-e0 ? e1 : e2-≻v→ s2"


🍋 ‹The interplay of 🍋‹Call›, 🍋‹Methd› and 🍋‹Body›:
  Method invocation is split up into these three rules:
  \begin{itemize}
  \item [🍋‹Call›] Calculates the target address and evaluates the
  arguments of the method, and then performs dynamic
  or static lookup of the method, corresponding to the
  call mode. Then the 🍋‹Methd› rule is evaluated
  on the calculated declaration class of the method
  invocation.
  \item [🍋‹Methd›] A syntactic bridge for the folded method body.
  It is used by the axiomatic semantics to add the
  proper hypothesis for recursive calls of the method.
  \item [🍋‹Body›] An extra syntactic entity for the unfolded method
  body was introduced to properly trigger class
  initialisation. Without class initialisation we
  could just evaluate the body statement.
  \end{itemize}›
  🍋 ‹cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5›
| Call: 
  "[G⊨Norm s0 ←-e-≻a'→ s1; G⊨s1 ←-args≐≻vs→ 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⊨s3' ←-Methd D (name=mn,parTs=pTs)-≻v→ s4]
   ==>
       G⊨Norm s0 ←-{accC,statT,mode}e⋅mn({pTs}args)-≻v→ (restore_lvars s2 s4)"
🍋 ‹The accessibility check is after 🍋‹init_lvars›, to keep it simple.
  🍋‹init_lvars› already tests for the absence of a null-pointer
  reference in case of an instance method invocation.›

| Methd:        "[G⊨Norm s0 ←-body G D sig-≻v→ s1] ==>
                                G⊨Norm s0 ←-Methd D sig-≻v→ s1"
  
| Body: "[G⊨Norm s0 ←-Init D→ s1; G⊨s1 ←-c→ 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⊨Norm s0 ←-Body D c-≻the (locals (store s2) Result)
              →abupd (absorb Ret) s3"
  🍋 ‹cf. 14.15, 12.4.1›
  🍋 ‹We filter out a break/continue in 🍋‹s2›, so that we can proof
  definite assignment
  correct, without the need of conformance of the state. By this the
  different parts of the typesafety proof can be disentangled a little.›

🍋 ‹evaluation of variables›

  🍋 ‹cf. 15.13.1, 15.7.2›
| LVar: "G⊨Norm s ←-LVar vn=≻lvar vn s→ Norm s"

  🍋 ‹cf. 15.10.1, 12.4.1›
| FVar: "[G⊨Norm s0 ←-Init statDeclC→ s1; G⊨s1 ←-e-≻a→ s2;
          (v,s2') = fvar statDeclC stat fn a s2;
          s3 = check_field_access G accC statDeclC fn stat a s2' ] ==>
          G⊨Norm s0 ←-{accC,statDeclC,stat}e..fn=≻v→ s3"
 🍋 ‹The accessibility check is after 🍋‹fvar›, to keep it simple.
  🍋‹fvar› already tests for the absence of a null-pointer reference
  in case of an instance field›

  🍋 ‹cf. 15.12.1, 15.25.1›
| AVar: "[G⊨ Norm s0 ←-e1-≻a→ s1; G⊨s1 ←-e2-≻i→ s2;
          (v,s2') = avar G i a s2] ==>
                      G⊨Norm s0 ←-e1.[e2]=≻v→ s2'"


🍋 ‹evaluation of expression lists›

  🍋 ‹cf. 15.11.4.2›
| Nil:
                                    "G⊨Norm s0 ←-[]≐≻[]→ Norm s0"

  🍋 ‹cf. 15.6.4›
| Cons: "[G⊨Norm s0 ←-e -≻ v → s1;
          G⊨ s1 ←-es≐≻vs→ s2] ==>
                                   G⊨Norm s0 ←-e#es≐≻v#vs→ s2"

(* Rearrangement of premisses:
 [0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
  17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
  29(AVar),24(Call)]
*)

ML ‹
 ML_Thms.bind_thm ("eval_induct", rearrange_prems
 [0,1,2,8,4,30,31,27,15,16,
  17,18,19,20,21,3,5,25,26,23,6,
  7,11,9,13,14,12,22,10,28,
  29,24] @{thm eval.induct})
 ›


declare if_split     [split del] if_split_asm     [split del] 
        option.split [split del] option.split_asm [split del]
inductive_cases halloc_elim_cases: 
  "G⊨(Some xc,s) ←-halloc oi≻a→ s'"
  "G⊨(Norm s) ←-halloc oi≻a→ s'"

inductive_cases sxalloc_elim_cases:
        "G⊨ Norm s ←-sxalloc→ s'"
        "G⊨(Some (Jump j),s) ←-sxalloc→ s'"
        "G⊨(Some (Error e),s) ←-sxalloc→ s'"
        "G⊨(Some (Xcpt (Loc a )),s) ←-sxalloc→ s'"
        "G⊨(Some (Xcpt (Std xn)),s) ←-sxalloc→ s'"
inductive_cases sxalloc_cases: "G⊨s ←-sxalloc→ s'"

lemma sxalloc_elim_cases2: "[G⊨s ←-sxalloc→ s';
       ∧s. [s' = Norm s] ==> P;
       ∧j s. [s' = (Some (Jump j),s)] ==> P;
       ∧e s. [s' = (Some (Error e),s)] ==> P;
       ∧a s. [s' = (Some (Xcpt (Loc a)),s)] ==> P
      ] ==> P"
apply cut_tac 
apply (erule sxalloc_cases)
apply blast+
done

declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
declare split_paired_All [simp del] split_paired_Ex [simp del]
setup ‹map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")›

inductive_cases eval_cases: "G⊨s ←-t≻→ (v, s')"

inductive_cases eval_elim_cases [cases set]:
        "G⊨(Some xc,s) ←-t ≻→ (v, s')"
        "G⊨Norm s ←-In1r Skip ≻→ (x, s')"
        "G⊨Norm s ←-In1r (Jmp j) ≻→ (x, s')"
        "G⊨Norm s ←-In1r (l∙ c) ≻→ (x, s')"
        "G⊨Norm s ←-In3 ([]) ≻→ (v, s')"
        "G⊨Norm s ←-In3 (e#es) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (Lit w) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (UnOp unop e) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (BinOp binop e1 e2) ≻→ (v, s')"
        "G⊨Norm s ←-In2 (LVar vn) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (Cast T e) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (e InstOf T) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (Super) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (Acc va) ≻→ (v, s')"
        "G⊨Norm s ←-In1r (Expr e) ≻→ (x, s')"
        "G⊨Norm s ←-In1r (c1;; c2) ≻→ (x, s')"
        "G⊨Norm s ←-In1l (Methd C sig) ≻→ (x, s')"
        "G⊨Norm s ←-In1l (Body D c) ≻→ (x, s')"
        "G⊨Norm s ←-In1l (e0 ? e1 : e2) ≻→ (v, s')"
        "G⊨Norm s ←-In1r (If(e) c1 Else c2) ≻→ (x, s')"
        "G⊨Norm s ←-In1r (l∙ While(e) c) ≻→ (x, s')"
        "G⊨Norm s ←-In1r (c1 Finally c2) ≻→ (x, s')"
        "G⊨Norm s ←-In1r (Throw e) ≻→ (x, s')"
        "G⊨Norm s ←-In1l (NewC C) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (New T[e]) ≻→ (v, s')"
        "G⊨Norm s ←-In1l (Ass va e) ≻→ (v, s')"
        "G⊨Norm s ←-In1r (Try c1 Catch(tn vn) c2) ≻→ (x, s')"
        "G⊨Norm s ←-In2 ({accC,statDeclC,stat}e..fn) ≻→ (v, s')"
        "G⊨Norm s ←-In2 (e1.[e2]) ≻→ (v, s')"
        "G⊨Norm s ←-In1l ({accC,statT,mode}e⋅mn({pT}p)) ≻→ (v, s')"
        "G⊨Norm s ←-In1r (Init C) ≻→ (x, s')"
declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
declare split_paired_All [simp] split_paired_Ex [simp]
declaration ‹K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))›
declare if_split     [split] if_split_asm     [split] 
        option.split [split] option.split_asm [split]

lemma eval_Inj_elim: 
 "G⊨s ←-t≻→ (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 eval_cases)
apply 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 🍋‹In1l› i
 (injection 🍋‹In1› into generalised values 🍋‹vals›). 
›

lemma eval_expr_eq: "G⊨s ←-In1l t≻→ (w, s') = (∃v. w=In1 v ∧ G⊨s ←-t-≻v → s')"
  by (auto, frule eval_Inj_elim, auto)

lemma eval_var_eq: "G⊨s ←-In2 t≻→ (w, s') = (∃vf. w=In2 vf ∧ G⊨s ←-t=≻vf→ s')"
  by (auto, frule eval_Inj_elim, auto)

lemma eval_exprs_eq: "G⊨s ←-In3 t≻→ (w, s') = (∃vs. w=In3 vs ∧ G⊨s ←-t≐≻vs→ s')"
  by (auto, frule eval_Inj_elim, auto)

lemma eval_stmt_eq: "G⊨s ←-In1r t≻→ (w, s') = (w=♢ ∧ G⊨s ←-t → s')"
  by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)

simproc_setup eval_expr ("G⊨s ←-In1l t≻→ (w, s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
  | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))))›

simproc_setup eval_var ("G⊨s ←-In2 t≻→ (w, s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
  | _ => SOME (mk_meta_eq @{thm eval_var_eq}))))›

simproc_setup eval_exprs ("G⊨s ←-In3 t≻→ (w, s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
  | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))))›

simproc_setup eval_stmt ("G⊨s ←-In1r t≻→ (w, s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
  | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))))›

ML ‹
 ML_Thms.bind_thms ("AbruptIs", sum3_instantiate 🍋 @{thm eval.Abrupt})
 ›

declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]

text‹‹Callee›,\<open>InsInitE›, ‹InsInitV›, ‹FinA› are only
used in smallstep semantics, not in the bigstep semantics. So their is no
valid evaluation of these terms 
›


lemma eval_Callee: "G⊨Norm s←-Callee l e-≻v→ s' = False"
proof -
  have False
    if eval: "G⊨s ←-t≻→ (v,s')"
    and normal: "normal s"
    and callee: "t=In1l (Callee l e)"
    for s t v s'
    using that by induct auto
  then show ?thesis
    by (cases s') fastforce
qed


lemma eval_InsInitE: "G⊨Norm s←-InsInitE c e-≻v→ s' = False"
proof -
  have "False"
    if eval: "G⊨s ←-t≻→ (v,s')"
    and normal: "normal s"
    and callee: "t=In1l (InsInitE c e)"
    for s t v s'
    using that by induct auto
  then show ?thesis
    by (cases s') fastforce
qed

lemma eval_InsInitV: "G⊨Norm s←-InsInitV c w=≻v→ s' = False"
proof -
  have "False"
    if eval: "G⊨s ←-t≻→ (v,s')"
    and normal: "normal s"
    and callee: "t=In2 (InsInitV c w)"
    for s t v s'
    using that by induct auto
  then show ?thesis
    by (cases s') fastforce
qed

lemma eval_FinA: "G⊨Norm s←-FinA a c→ s' = False"
proof -
  have "False"
    if eval: "G⊨s ←-t≻→ (v,s')"
    and normal: "normal s"
    and callee: "t=In1r (FinA a c)"
    for s t v s'
    using that by induct auto
  then show ?thesis
    by (cases s') fastforce 
qed

lemma eval_no_abrupt_lemma: 
   "∧s s'. G⊨s ←-t≻→ (w,s') ==> normal s' ⟶ normal s"
by (erule eval_cases, auto)

lemma eval_no_abrupt: 
  "G⊨(x,s) ←-t≻→ (w,Norm s') =
        (x = None ∧ G⊨Norm s ←-t≻→ (w,Norm s'))"
apply auto
apply (frule eval_no_abrupt_lemma, auto)+
done

simproc_setup eval_no_abrupt ("G⊨(x,s) ←-e≻→ (w,Norm s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ (Const (🍋‹Pair›,
    | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))))
›


lemma eval_abrupt_lemma: 
  "G⊨s ←-t≻→ (v,s') ==> abrupt s=Some xc ⟶ s'= s ∧ v = undefined3 t"
by (erule eval_cases, auto)

lemma eval_abrupt: 
 " G⊨(Some xc,s) ←-t≻→ (w,s') =
     (s'=(Some xc,s) ∧ w=undefined3 t ∧
     G⊨(Some xc,s) ←-t≻→ (undefined3 t,(Some xc,s)))"
apply auto
apply (frule eval_abrupt_lemma, auto)+
done

simproc_setup eval_abrupt ("G⊨(Some xc,s) ←-e≻→ (w,s')") = ‹
  K (K (fn ct =>
  (case Thm.term_of ct of
  (_ $ _ $ _ $ _ $ _ $ (Const (🍋‹Pair›,
    | _ => SOME (mk_meta_eq @{thm eval_abrupt}))))
›

lemma LitI: "G⊨s ←-Lit v-≻(if normal s then v else undefined)→ s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Lit)

lemma SkipI [intro!]: "G⊨s ←-Skip→ s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Skip)

lemma ExprI: "G⊨s ←-e-≻v→ s' ==> G⊨s ←-Expr e→ s'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Expr)

lemma CompI: "[G⊨s ←-c1→ s1; G⊨s1 ←-c2→ s2] ==> G⊨s ←-c1;; c2→ s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Comp)

lemma CondI: 
  "∧s1. [G⊨s ←-e-≻b→ s1; G⊨s1 ←-(if the_Bool b then e1 else e2)-≻v→ s2] ==>
         G⊨s ←-e ? e1 : e2-≻(if normal s1 then v else undefined)→ s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Cond)

lemma IfI: "[G⊨s ←-e-≻v→ s1; G⊨s1 ←-(if the_Bool v then c1 else c2)→ s2]
                 ==> G⊨s ←-If(e) c1 Else c2→ s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.If)

lemma MethdI: "G⊨s ←-body G C sig-≻v→ s'
                ==> G⊨s ←-Methd C sig-≻v→ s'"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Methd)

lemma eval_Call: 
   "[G⊨Norm s0 ←-e-≻a'→ s1; G⊨s1 ←-ps≐≻pvs→ 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' pvs s2;
     s3' = check_method_access G accC statT mode (name=mn,parTs=pTs) a' s3;
     G⊨s3'←-Methd D (name=mn,parTs=pTs)-≻ v→ s4;
       s4' = restore_lvars s2 s4] ==>
       G⊨Norm s0 ←-{accC,statT,mode}e⋅mn({pTs}ps)-≻v→ s4'"
apply (drule eval.Call, assumption)
apply (rule HOL.refl)
apply simp+
done

lemma eval_Init: 
"[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))))→ s1 ∧
       G⊨set_lvars Map.empty s1 ←-(init (the (class G C)))→ s2 ∧
      s3 = restore_lvars s1 s2] ==>
  G⊨Norm s0 ←-Init C→ s3"
apply (rule eval.Init)
apply auto
done

lemma init_done: "initd C s ==> G⊨s ←-Init C→ s"
apply (case_tac "s", simp)
apply (case_tac "a")
apply  safe
apply (rule eval_Init)
apply   auto
done

lemma eval_StatRef: 
"G⊨s ←-StatRef rt-≻(if abrupt s=None then Null else undefined)→ s"
apply (case_tac "s", simp)
apply (case_tac "a = None")
apply (auto del: eval.Abrupt intro!: eval.intros)
done


lemma SkipD [dest!]: "G⊨s ←-Skip→ s' ==> s' = s" 
apply (erule eval_cases)
by auto

lemma Skip_eq [simp]: "G⊨s ←-Skip→ s' = (s = s')"
by auto

(*unused*)
lemma init_retains_locals [rule_format (no_asm)]: "G⊨s ←-t≻→ (w,s') ==>
  (∀C. t=In1r (Init C) ⟶ locals (store s) = locals (store s'))"
apply (erule eval.induct)
apply (simp (no_asm_use) split del: if_split_asm option.split_asm)+
apply auto
done

lemma halloc_xcpt [dest!]: 
  "∧s'. G⊨(Some xc,s) ←-halloc oi≻a→ s' ==> s'=(Some xc,s)"
apply (erule_tac halloc_elim_cases)
by auto

(*
 G⊨(x,(h,l)) ←-e≻v→ (x',(h',l'))) ==> l This = l' This"
 G⊨(x,(h,l)) ←-s → (x',(h',l'))) ==> l This = l' This"
*)

lemma eval_Methd: 
  "G⊨s ←-In1l(body G C sig)≻→ (w,s')
   ==> G⊨s ←-In1l(Methd C sig)≻→ (w,s')"
apply (case_tac "s")
apply (case_tac "a")
apply clarsimp+
apply (erule eval.Methd)
apply (drule eval_abrupt_lemma)
apply force
done

lemma eval_Body: "[G⊨Norm s0 ←-Init D→ s1; G⊨s1 ←-c→ s2;
                   res=the (locals (store s2) Result);
                   s3 = (if (∃ l. abrupt s2 = Some (Jump (Break l)) ∨
                                  abrupt s2 = Some (Jump (Cont l)))
                   then abupd (λ x. Some (Error CrossMethodJump)) s2
                   else s2);
                   s4=abupd (absorb Ret) s3] ==>
 G⊨Norm s0 ←-Body D c-≻res→s4"
by (auto elim: eval.Body)

lemma eval_binop_arg2_indep:
"¬ need_second_arg binop v1 ==> eval_binop binop v1 x = eval_binop binop v1 y"
by (cases binop)
   (simp_all add: need_second_arg_def)


lemma eval_BinOp_arg2_indepI:
  assumes eval_e1: "G⊨Norm s0 ←-e1-≻v1→ s1" and
          no_need: "¬ need_second_arg binop v1" 
  shows "G⊨Norm s0 ←-BinOp binop e1 e2-≻(eval_binop binop v1 v2)→ s1"
         (is "?EvalBinOp v2")
proof -
  from eval_e1 
  have "?EvalBinOp Unit" 
    by (rule eval.BinOp)
       (simp add: no_need)
  moreover
  from no_need 
  have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
    by (simp add: eval_binop_arg2_indep)
  ultimately
  show ?thesis
    by simp
qed


subsubsection "single valued"

lemma unique_halloc [rule_format (no_asm)]: 
  "G⊨s ←-halloc oi≻a → s' ==> G⊨s ←-halloc oi≻a' → s'' ⟶ a' = a ∧ s'' = s'"
apply (erule halloc.induct)
apply  (auto elim!: halloc_elim_cases split del: if_split if_split_asm)
apply (drule trans [THEN sym], erule sym) 
defer
apply (drule trans [THEN sym], erule sym)
apply auto
done


lemma single_valued_halloc: 
  "single_valued {((s,oi),(a,s')). G⊨s ←-halloc oi≻a → s'}"
apply (unfold single_valued_def)
by (clarsimp, drule (1) unique_halloc, auto)


lemma unique_sxalloc [rule_format (no_asm)]: 
  "G⊨s ←-sxalloc→ s' ==> G⊨s ←-sxalloc→ s'' ⟶ s'' = s'"
apply (erule sxalloc.induct)
apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
              split del: if_split if_split_asm)
done

lemma single_valued_sxalloc: "single_valued {(s,s'). G⊨s ←-sxalloc→ s'}"
apply (unfold single_valued_def)
apply (blast dest: unique_sxalloc)
done

lemma split_pairD: "(x,y) = p ==> x = fst p & y = snd p"
by auto



lemma unique_eval [rule_format (no_asm)]: 
  "G⊨s ←-t≻→ (w, s') ==> (∀w' s''. G⊨s ←-t≻→ (w', s'') ⟶ w' = w ∧ s'' = s')"
apply (erule eval_induct)
apply (tactic ‹ALLGOALS (EVERY'
  [strip_tac 🍋, rotate_tac ~1, eresolve_tac 🍋 @{thms eval_elim_cases}])›)
(* 31 subgoals *)
prefer 28 (* Try *) 
apply (simp (no_asm_use) only: split: if_split_asm)
(* 34 subgoals *)
prefer 30 (* Init *)
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
prefer 26 (* While *)
apply (simp (no_asm_use) only: split: if_split_asm, blast)
(* 36 subgoals *)
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
done

(* unused *)
lemma single_valued_eval: 
 "single_valued {((s, t), (v, s')). G⊨s ←-t≻→ (v, s')}"
apply (unfold single_valued_def)
by (clarify, drule (1) unique_eval, auto)

end