src/HOL/Bali/Eval.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62042 6c6ccf573479
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Bali/Eval.thy
     2     Author:     David von Oheimb
     3 *)
     4 subsection \<open>Operational evaluation (big-step) semantics of Java expressions and 
     5           statements
     6 \<close>
     7 
     8 theory Eval imports State DeclConcepts begin
     9 
    10 text \<open>
    11 
    12 improvements over Java Specification 1.0:
    13 \begin{itemize}
    14 \item dynamic method lookup does not need to consider the return type 
    15       (cf.15.11.4.4)
    16 \item throw raises a NullPointer exception if a null reference is given, and 
    17       each throw of a standard exception yield a fresh exception object 
    18       (was not specified)
    19 \item if there is not enough memory even to allocate an OutOfMemory exception,
    20   evaluation/execution fails, i.e. simply stops (was not specified)
    21 \item array assignment checks lhs (and may throw exceptions) before evaluating 
    22       rhs
    23 \item fixed exact positions of class initializations 
    24       (immediate at first active use)
    25 \end{itemize}
    26 
    27 design issues:
    28 \begin{itemize}
    29 \item evaluation vs. (single-step) transition semantics
    30   evaluation semantics chosen, because:
    31   \begin{itemize} 
    32   \item[++] less verbose and therefore easier to read (and to handle in proofs)
    33   \item[+]  more abstract
    34   \item[+]  intermediate values (appearing in recursive rules) need not be 
    35      stored explicitly, e.g. no call body construct or stack of invocation 
    36      frames containing local variables and return addresses for method calls 
    37      needed
    38   \item[+]  convenient rule induction for subject reduction theorem
    39   \item[-]  no interleaving (for parallelism) can be described
    40   \item[-]  stating a property of infinite executions requires the meta-level 
    41      argument that this property holds for any finite prefixes of it 
    42      (e.g. stopped using a counter that is decremented to zero and then 
    43      throwing an exception)
    44   \end{itemize}
    45 \item unified evaluation for variables, expressions, expression lists, 
    46       statements
    47 \item the value entry in statement rules is redundant 
    48 \item the value entry in rules is irrelevant in case of exceptions, but its full
    49   inclusion helps to make the rule structure independent of exception occurrence.
    50 \item as irrelevant value entries are ignored, it does not matter if they are 
    51       unique.
    52   For simplicity, (fixed) arbitrary values are preferred over "free" values.
    53 \item the rule format is such that the start state may contain an exception.
    54   \begin{itemize}
    55   \item[++] faciliates exception handling
    56   \item[+]  symmetry
    57   \end{itemize}
    58 \item the rules are defined carefully in order to be applicable even in not
    59   type-correct situations (yielding undefined values),
    60   e.g. \<open>the_Addr (Val (Bool b)) = undefined\<close>.
    61   \begin{itemize}
    62   \item[++] fewer rules 
    63   \item[-]  less readable because of auxiliary functions like \<open>the_Addr\<close>
    64   \end{itemize}
    65   Alternative: "defensive" evaluation throwing some InternalError exception
    66                in case of (impossible, for correct programs) type mismatches
    67 \item there is exactly one rule per syntactic construct
    68   \begin{itemize}
    69   \item[+] no redundancy in case distinctions
    70   \end{itemize}
    71 \item halloc fails iff there is no free heap address. When there is
    72   only one free heap address left, it returns an OutOfMemory exception.
    73   In this way it is guaranteed that when an OutOfMemory exception is thrown for
    74   the first time, there is a free location on the heap to allocate it.
    75 \item the allocation of objects that represent standard exceptions is deferred 
    76       until execution of any enclosing catch clause, which is transparent to 
    77       the program.
    78   \begin{itemize}
    79   \item[-]  requires an auxiliary execution relation
    80   \item[++] avoids copies of allocation code and awkward case distinctions 
    81            (whether there is enough memory to allocate the exception) in 
    82             evaluation rules
    83   \end{itemize}
    84 \item unfortunately \<open>new_Addr\<close> is not directly executable because of 
    85       Hilbert operator.
    86 \end{itemize}
    87 simplifications:
    88 \begin{itemize}
    89 \item local variables are initialized with default values 
    90       (no definite assignment)
    91 \item garbage collection not considered, therefore also no finalizers
    92 \item stack overflow and memory overflow during class initialization not 
    93       modelled
    94 \item exceptions in initializations not replaced by ExceptionInInitializerError
    95 \end{itemize}
    96 \<close>
    97 
    98 
    99 type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   100 type_synonym vals = "(val, vvar, val list) sum3"
   101 translations
   102   (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   103   (type) "vals" <= (type) "(val, vvar, val list) sum3" 
   104 
   105 text \<open>To avoid redundancy and to reduce the number of rules, there is only 
   106  one evaluation rule for each syntactic term. This is also true for variables
   107  (e.g. see the rules below for \<open>LVar\<close>, \<open>FVar\<close> and \<open>AVar\<close>). 
   108  So evaluation of a variable must capture both possible further uses: 
   109  read (rule \<open>Acc\<close>) or write (rule \<open>Ass\<close>) to the variable. 
   110  Therefor a variable evaluates to a special value @{term vvar}, which is 
   111  a pair, consisting of the current value (for later read access) and an update 
   112  function (for later write access). Because
   113  during assignment to an array variable an exception may occur if the types
   114  don't match, the update function is very generic: it transforms the 
   115  full state. This generic update function causes some technical trouble during
   116  some proofs (e.g. type safety, correctness of definite assignment). There we
   117  need to prove some additional invariant on this update function to prove the
   118  assignment correct, since the update function could potentially alter the whole
   119  state in an arbitrary manner. This invariant must be carried around through
   120  the whole induction.
   121  So for future approaches it may be better not to take
   122  such a generic update function, but only to store the address and the kind
   123  of variable (array (+ element type), local variable or field) for later 
   124  assignment. 
   125 \<close>
   126 
   127 abbreviation
   128   dummy_res :: "vals" ("\<diamondsuit>")
   129   where "\<diamondsuit> == In1 Unit"
   130 
   131 abbreviation (input)
   132   val_inj_vals ("\<lfloor>_\<rfloor>\<^sub>e" 1000)
   133   where "\<lfloor>e\<rfloor>\<^sub>e == In1 e"
   134 
   135 abbreviation (input)
   136   var_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>v" 1000)
   137   where "\<lfloor>v\<rfloor>\<^sub>v == In2 v"
   138 
   139 abbreviation (input)
   140   lst_inj_vals  ("\<lfloor>_\<rfloor>\<^sub>l" 1000)
   141   where "\<lfloor>es\<rfloor>\<^sub>l == In3 es"
   142 
   143 definition undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" where
   144  "undefined3 = case_sum3 (In1 \<circ> case_sum (\<lambda>x. undefined) (\<lambda>x. Unit))
   145                      (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
   146 
   147 lemma [simp]: "undefined3 (In1l x) = In1 undefined"
   148 by (simp add: undefined3_def)
   149 
   150 lemma [simp]: "undefined3 (In1r x) = \<diamondsuit>"
   151 by (simp add: undefined3_def)
   152 
   153 lemma [simp]: "undefined3 (In2  x) = In2 undefined"
   154 by (simp add: undefined3_def)
   155 
   156 lemma [simp]: "undefined3 (In3  x) = In3 undefined"
   157 by (simp add: undefined3_def)
   158 
   159 
   160 subsubsection "exception throwing and catching"
   161 
   162 definition
   163   throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" where
   164   "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   165 
   166 lemma throw_def2: 
   167  "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   168 apply (unfold throw_def)
   169 apply (simp (no_asm))
   170 done
   171 
   172 definition
   173   fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
   174   where "G,s\<turnstile>a' fits T = ((\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T)"
   175 
   176 lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
   177 by (simp add: fits_def)
   178 
   179 
   180 lemma fits_Addr_RefT [simp]:
   181   "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
   182 by (simp add: fits_def)
   183 
   184 lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>  
   185   (\<exists>t. T = RefT t) \<and> a' = Null \<or>  
   186   (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and>  G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
   187 apply (unfold fits_def)
   188 apply (case_tac "\<exists>pt. T = PrimT pt")
   189 apply  simp_all
   190 apply (case_tac "T")
   191 defer 
   192 apply (case_tac "a' = Null")
   193 apply  simp_all
   194 apply iprover
   195 done
   196 
   197 definition
   198   catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
   199   "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
   200                         G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
   201 
   202 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
   203 apply (unfold catch_def)
   204 apply (simp (no_asm))
   205 done
   206 
   207 lemma catch_XcptLoc [simp]: 
   208   "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
   209 apply (unfold catch_def)
   210 apply (simp (no_asm))
   211 done
   212 
   213 lemma catch_Jump [simp]: "\<not>G,(Some (Jump j),s)\<turnstile>catch tn"
   214 apply (unfold catch_def)
   215 apply (simp (no_asm))
   216 done
   217 
   218 lemma catch_Error [simp]: "\<not>G,(Some (Error e),s)\<turnstile>catch tn"
   219 apply (unfold catch_def)
   220 apply (simp (no_asm))
   221 done
   222 
   223 definition
   224   new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
   225   "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
   226 
   227 lemma new_xcpt_var_def2 [simp]: 
   228  "new_xcpt_var vn (x,s) = 
   229     Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
   230 apply (unfold new_xcpt_var_def)
   231 apply (simp (no_asm))
   232 done
   233 
   234 
   235 
   236 subsubsection "misc"
   237 
   238 definition
   239   assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
   240  "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
   241                         in  (x',if x' = None then s' else s))"
   242 
   243 (*
   244 lemma assign_Norm_Norm [simp]: 
   245 "f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 
   246  \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
   247 by (simp add: assign_def Let_def)
   248 *)
   249 
   250 lemma assign_Norm_Norm [simp]: 
   251 "f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
   252 by (simp add: assign_def Let_def)
   253 
   254 (*
   255 lemma assign_Norm_Some [simp]: 
   256   "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 
   257    \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
   258 by (simp add: assign_def Let_def split_beta)
   259 *)
   260 
   261 lemma assign_Norm_Some [simp]: 
   262   "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 
   263    \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
   264 by (simp add: assign_def Let_def split_beta)
   265 
   266 
   267 lemma assign_Some [simp]: 
   268 "assign f v (Some x,s) = (Some x,s)" 
   269 by (simp add: assign_def Let_def split_beta)
   270 
   271 lemma assign_Some1 [simp]:  "\<not> normal s \<Longrightarrow> assign f v s = s" 
   272 by (auto simp add: assign_def Let_def split_beta)
   273 
   274 lemma assign_supd [simp]: 
   275 "assign (\<lambda>v. supd (f v)) v (x,s)  
   276   = (x, if x = None then f v s else s)"
   277 apply auto
   278 done
   279 
   280 lemma assign_raise_if [simp]: 
   281   "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =  
   282   (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
   283 apply (case_tac "x = None")
   284 apply auto
   285 done
   286 
   287 
   288 (*
   289 lemma assign_raise_if [simp]: 
   290   "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
   291                   store = f v (store s)\<rparr>) v s =  
   292   \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
   293    store= if (abrupt s)=None \<and> \<not>b (store s) v 
   294              then f v (store s) else (store s)\<rparr>"
   295 apply (case_tac "abrupt s = None")
   296 apply auto
   297 done
   298 *)
   299 
   300 definition
   301   init_comp_ty :: "ty \<Rightarrow> stmt"
   302   where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
   303 
   304 lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
   305 apply (unfold init_comp_ty_def)
   306 apply (simp (no_asm))
   307 done
   308 
   309 definition
   310   invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
   311  "invocation_class m s a' statT =
   312     (case m of
   313        Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
   314                     then the_Class (RefT statT) 
   315                     else Object
   316      | SuperM \<Rightarrow> the_Class (RefT statT)
   317      | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
   318 
   319 definition
   320   invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
   321   "invocation_declclass G m s a' statT sig =
   322     declclass (the (dynlookup G statT
   323                                 (invocation_class m s a' statT)
   324                                 sig))" 
   325   
   326 lemma invocation_class_IntVir [simp]: 
   327 "invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
   328 by (simp add: invocation_class_def)
   329 
   330 lemma dynclass_SuperM [simp]: 
   331  "invocation_class SuperM s a' statT = the_Class (RefT statT)"
   332 by (simp add: invocation_class_def)
   333 
   334 lemma invocation_class_Static [simp]: 
   335   "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 
   336                                             then the_Class (RefT statT) 
   337                                             else Object)"
   338 by (simp add: invocation_class_def)
   339 
   340 definition
   341   init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
   342 where
   343   "init_lvars G C sig mode a' pvs =
   344     (\<lambda>(x,s). 
   345       let m = mthd (the (methd G C sig));
   346           l = \<lambda> k. 
   347               (case k of
   348                  EName e 
   349                    \<Rightarrow> (case e of 
   350                          VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v
   351                        | Res    \<Rightarrow> None)
   352                | This 
   353                    \<Rightarrow> (if mode=Static then None else Some a'))
   354       in set_lvars l (if mode = Static then x else np a' x,s))"
   355 
   356 
   357 
   358 lemma init_lvars_def2: \<comment>\<open>better suited for simplification\<close> 
   359 "init_lvars G C sig mode a' pvs (x,s) =  
   360   set_lvars 
   361     (\<lambda> k. 
   362        (case k of
   363           EName e 
   364             \<Rightarrow> (case e of 
   365                   VNam v 
   366                   \<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
   367                | Res \<Rightarrow> None)
   368         | This 
   369             \<Rightarrow> (if mode=Static then None else Some a')))
   370     (if mode = Static then x else np a' x,s)"
   371 apply (unfold init_lvars_def)
   372 apply (simp (no_asm) add: Let_def)
   373 done
   374 
   375 definition
   376   body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
   377  "body G C sig =
   378     (let m = the (methd G C sig) 
   379      in Body (declclass m) (stmt (mbody (mthd m))))"
   380 
   381 lemma body_def2: \<comment>\<open>better suited for simplification\<close> 
   382 "body G C sig = Body  (declclass (the (methd G C sig))) 
   383                       (stmt (mbody (mthd (the (methd G C sig)))))"
   384 apply (unfold body_def Let_def)
   385 apply auto
   386 done
   387 
   388 subsubsection "variables"
   389 
   390 definition
   391   lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
   392   where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
   393 
   394 definition
   395   fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
   396  "fvar C stat fn a' s =
   397    (let (oref,xf) = if stat then (Stat C,id)
   398                             else (Heap (the_Addr a'),np a');
   399                   n = Inl (fn,C); 
   400                   f = (\<lambda>v. supd (upd_gobj oref n v)) 
   401     in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
   402 
   403 definition
   404   avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
   405   "avar G i' a' s =
   406     (let   oref = Heap (the_Addr a'); 
   407               i = the_Intg i'; 
   408               n = Inr i;
   409        (T,k,cs) = the_Arr (globs (store s) oref); 
   410               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
   411                                            ArrStore x
   412                               ,upd_gobj oref n v s)) 
   413      in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
   414 
   415 lemma fvar_def2: \<comment>\<open>better suited for simplification\<close> 
   416 "fvar C stat fn a' s =  
   417   ((the 
   418      (values 
   419       (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
   420       (Inl (fn,C)))
   421    ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
   422                         (Inl (fn,C)) 
   423                         v)))
   424   ,abupd (if stat then id else np a') s)
   425   "
   426 apply (unfold fvar_def)
   427 apply (simp (no_asm) add: Let_def split_beta)
   428 done
   429 
   430 lemma avar_def2: \<comment>\<open>better suited for simplification\<close> 
   431 "avar G i' a' s =  
   432   ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
   433            (Inr (the_Intg i')))
   434    ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
   435                                                    (Heap (the_Addr a')))))) 
   436                             ArrStore x
   437                  ,upd_gobj  (Heap (the_Addr a')) 
   438                                (Inr (the_Intg i')) v s')))
   439   ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
   440                    (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
   441           s)"
   442 apply (unfold avar_def)
   443 apply (simp (no_asm) add: Let_def split_beta)
   444 done
   445 
   446 definition
   447   check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
   448   "check_field_access G accC statDeclC fn stat a' s =
   449     (let oref = if stat then Stat statDeclC
   450                 else Heap (the_Addr a');
   451          dynC = case oref of
   452                    Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
   453                  | Stat C \<Rightarrow> C;
   454          f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
   455      in abupd 
   456         (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
   457                   AccessViolation)
   458         s)"
   459 
   460 definition
   461   check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
   462   "check_method_access G accC statT mode sig  a' s =
   463     (let invC = invocation_class mode (store s) a' statT;
   464        dynM = the (dynlookup G statT invC sig)
   465      in abupd 
   466         (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
   467                   AccessViolation)
   468         s)"
   469        
   470 subsubsection "evaluation judgments"
   471 
   472 inductive
   473   halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
   474 where \<comment>\<open>allocating objects on the heap, cf. 12.5\<close>
   475 
   476   Abrupt: 
   477   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>undefined\<rightarrow> (Some x,s)"
   478 
   479 | New:    "\<lbrakk>new_Addr (heap s) = Some a; 
   480             (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   481                        else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   482             \<Longrightarrow>
   483             G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   484 
   485 inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
   486 where \<comment>\<open>allocating exception objects for
   487   standard exceptions (other than OutOfMemory)\<close>
   488 
   489   Norm:  "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   490 
   491 | Jmp:   "G\<turnstile>(Some (Jump j), s)  \<midarrow>sxalloc\<rightarrow> (Some (Jump j), s)"
   492 
   493 | Error: "G\<turnstile>(Some (Error e), s)  \<midarrow>sxalloc\<rightarrow> (Some (Error e), s)"
   494 
   495 | XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   496 
   497 | SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   498           G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   499 
   500 
   501 inductive
   502   eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')"  [61,61,80,0,0]60)
   503   and exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   504   and evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   505   and eval'::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   506   and evals::"[prog,state,expr list ,
   507                     val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   508   for G::prog
   509 where
   510 
   511   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,  s')"
   512 | "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v,  s')"
   513 | "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf, s')"
   514 | "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v,  s')"
   515 
   516 \<comment>\<open>propagation of abrupt completion\<close>
   517 
   518   \<comment>\<open>cf. 14.1, 15.5\<close>
   519 | Abrupt: 
   520    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t, (Some xc, s))"
   521 
   522 
   523 \<comment>\<open>execution of statements\<close>
   524 
   525   \<comment>\<open>cf. 14.5\<close>
   526 | Skip:                             "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   527 
   528   \<comment>\<open>cf. 14.7\<close>
   529 | Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   530                                   G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   531 
   532 | Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   533                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
   534   \<comment>\<open>cf. 14.2\<close>
   535 | Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   536           G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   537                                  G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   538 
   539   \<comment>\<open>cf. 14.8.2\<close>
   540 | If:   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   541           G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   542                        G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   543 
   544   \<comment>\<open>cf. 14.10, 14.10.1\<close>
   545   
   546   \<comment>\<open>A continue jump from the while body @{term c} is handled by 
   547      this rule. If a continue jump with the proper label was invoked inside 
   548      @{term c} this label (Cont l) is deleted out of the abrupt component of 
   549      the state before the iterative evaluation of the while statement.
   550      A break jump is handled by the Lab Statement \<open>Lab l (while\<dots>)\<close>.
   551 \<close>
   552 | Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   553           if the_Bool b 
   554              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   555                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   556              else s3 = s1\<rbrakk> \<Longrightarrow>
   557                               G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   558 
   559 | Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<rightarrow> (Some (Jump j), s)"
   560    
   561   \<comment>\<open>cf. 14.16\<close>
   562 | Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   563                                  G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   564 
   565   \<comment>\<open>cf. 14.18.1\<close>
   566 | Try:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   567           if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   568                   G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   569 
   570   \<comment>\<open>cf. 14.18.2\<close>
   571 | Fin:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   572           G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
   573           s3=(if (\<exists> err. x1=Some (Error err)) 
   574               then (x1,s1) 
   575               else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
   576           \<Longrightarrow>
   577           G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
   578   \<comment>\<open>cf. 12.4.2, 8.5\<close>
   579 | Init: "\<lbrakk>the (class G C) = c;
   580           if inited C (globs s0) then s3 = Norm s0
   581           else (G\<turnstile>Norm (init_class_obj G C s0) 
   582                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   583                G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   584               \<Longrightarrow>
   585                  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   586    \<comment>\<open>This class initialisation rule is a little bit inaccurate. Look at the
   587       exact sequence:
   588       (1) The current class object (the static fields) are initialised
   589            (\<open>init_class_obj\<close>),
   590       (2) the superclasses are initialised,
   591       (3) the static initialiser of the current class is invoked.
   592       More precisely we should expect another ordering, namely 2 1 3.
   593       But we can't just naively toggle 1 and 2. By calling 
   594       \<open>init_class_obj\<close> 
   595       before initialising the superclasses, we also implicitly record that
   596       we have started to initialise the current class (by setting an 
   597       value for the class object). This becomes 
   598       crucial for the completeness proof of the axiomatic semantics 
   599       \<open>AxCompl.thy\<close>. Static initialisation requires an induction on 
   600       the number of classes not yet initialised (or to be more precise, 
   601       classes were the initialisation has not yet begun). 
   602       So we could first assign a dummy value to the class before
   603       superclass initialisation and afterwards set the correct values.
   604       But as long as we don't take memory overflow into account 
   605       when allocating class objects, we can leave things as they are for 
   606       convenience. 
   607 \<close>
   608 \<comment>\<open>evaluation of expressions\<close>
   609 
   610   \<comment>\<open>cf. 15.8.1, 12.4.1\<close>
   611 | NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   612           G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   613                                   G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   614 
   615   \<comment>\<open>cf. 15.9.1, 12.4.1\<close>
   616 | NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   617           G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   618                                 G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   619 
   620   \<comment>\<open>cf. 15.15\<close>
   621 | Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   622           s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   623                                 G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   624 
   625   \<comment>\<open>cf. 15.19.2\<close>
   626 | Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   627           b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   628                               G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   629 
   630   \<comment>\<open>cf. 15.7.1\<close>
   631 | Lit:  "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   632 
   633 | UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
   634          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
   635  
   636 | BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
   637           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
   638                 \<succ>\<rightarrow> (In1 v2, s2)
   639           \<rbrakk> 
   640          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
   641    
   642   \<comment>\<open>cf. 15.10.2\<close>
   643 | Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   644 
   645   \<comment>\<open>cf. 15.2\<close>
   646 | Acc:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   647                                   G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   648 
   649   \<comment>\<open>cf. 15.25.1\<close>
   650 | Ass:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   651           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   652                                    G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   653 
   654   \<comment>\<open>cf. 15.24\<close>
   655 | Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   656           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   657                             G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   658 
   659 
   660 \<comment> \<open>The interplay of  @{term Call}, @{term Methd} and @{term Body}:
   661       Method invocation is split up into these three rules:
   662       \begin{itemize}
   663       \item [@{term Call}] Calculates the target address and evaluates the
   664                            arguments of the method, and then performs dynamic
   665                            or static lookup of the method, corresponding to the
   666                            call mode. Then the @{term Methd} rule is evaluated
   667                            on the calculated declaration class of the method
   668                            invocation.
   669       \item [@{term Methd}] A syntactic bridge for the folded method body.
   670                             It is used by the axiomatic semantics to add the
   671                             proper hypothesis for recursive calls of the method.
   672       \item [@{term Body}] An extra syntactic entity for the unfolded method
   673                            body was introduced to properly trigger class 
   674                            initialisation. Without class initialisation we 
   675                            could just evaluate the body statement. 
   676       \end{itemize}
   677 \<close>
   678   \<comment>\<open>cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5\<close>
   679 | Call: 
   680   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   681     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   682     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   683     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   684     G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
   685    \<Longrightarrow>
   686        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
   687 \<comment>\<open>The accessibility check is after @{term init_lvars}, to keep it simple. 
   688    @{term init_lvars} already tests for the absence of a null-pointer 
   689    reference in case of an instance method invocation.
   690 \<close>
   691 
   692 | Methd:        "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   693                                 G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   694   
   695 | Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; 
   696           s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
   697                          abrupt s2 = Some (Jump (Cont l)))
   698                   then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
   699                   else s2)\<rbrakk> \<Longrightarrow>
   700            G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
   701               \<rightarrow>abupd (absorb Ret) s3"
   702   \<comment>\<open>cf. 14.15, 12.4.1\<close>
   703   \<comment>\<open>We filter out a break/continue in @{term s2}, so that we can proof 
   704      definite assignment
   705      correct, without the need of conformance of the state. By this the
   706      different parts of the typesafety proof can be disentangled a little.\<close>
   707 
   708 \<comment>\<open>evaluation of variables\<close>
   709 
   710   \<comment>\<open>cf. 15.13.1, 15.7.2\<close>
   711 | LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   712 
   713   \<comment>\<open>cf. 15.10.1, 12.4.1\<close>
   714 | FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   715           (v,s2') = fvar statDeclC stat fn a s2;
   716           s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
   717           G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
   718  \<comment>\<open>The accessibility check is after @{term fvar}, to keep it simple. 
   719     @{term fvar} already tests for the absence of a null-pointer reference 
   720     in case of an instance field
   721 \<close>
   722 
   723   \<comment>\<open>cf. 15.12.1, 15.25.1\<close>
   724 | AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   725           (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   726                       G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   727 
   728 
   729 \<comment>\<open>evaluation of expression lists\<close>
   730 
   731   \<comment>\<open>cf. 15.11.4.2\<close>
   732 | Nil:
   733                                     "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   734 
   735   \<comment>\<open>cf. 15.6.4\<close>
   736 | Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   737           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   738                                    G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   739 
   740 (* Rearrangement of premisses:
   741 [0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
   742  17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
   743  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
   744  29(AVar),24(Call)]
   745 *)
   746 
   747 ML \<open>
   748 ML_Thms.bind_thm ("eval_induct", rearrange_prems 
   749 [0,1,2,8,4,30,31,27,15,16,
   750  17,18,19,20,21,3,5,25,26,23,6,
   751  7,11,9,13,14,12,22,10,28,
   752  29,24] @{thm eval.induct})
   753 \<close>
   754 
   755 
   756 declare split_if     [split del] split_if_asm     [split del] 
   757         option.split [split del] option.split_asm [split del]
   758 inductive_cases halloc_elim_cases: 
   759   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   760   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   761 
   762 inductive_cases sxalloc_elim_cases:
   763         "G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   764         "G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
   765         "G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
   766         "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   767         "G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   768 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   769 
   770 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   771        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   772        \<And>j s. \<lbrakk>s' = (Some (Jump j),s)\<rbrakk> \<Longrightarrow> P;
   773        \<And>e s. \<lbrakk>s' = (Some (Error e),s)\<rbrakk> \<Longrightarrow> P;
   774        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   775       \<rbrakk> \<Longrightarrow> P"
   776 apply cut_tac 
   777 apply (erule sxalloc_cases)
   778 apply blast+
   779 done
   780 
   781 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   782 declare split_paired_All [simp del] split_paired_Ex [simp del]
   783 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   784 
   785 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
   786 
   787 inductive_cases eval_elim_cases [cases set]:
   788         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> (v, s')"
   789         "G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> (x, s')"
   790         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                        \<succ>\<rightarrow> (x, s')"
   791         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> (x, s')"
   792         "G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> (v, s')"
   793         "G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> (v, s')"
   794         "G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> (v, s')"
   795         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> (v, s')"
   796         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> (v, s')"
   797         "G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> (v, s')"
   798         "G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> (v, s')"
   799         "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> (v, s')"
   800         "G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> (v, s')"
   801         "G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> (v, s')"
   802         "G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> (x, s')"
   803         "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> (x, s')"
   804         "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> (x, s')"
   805         "G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> (x, s')"
   806         "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> (v, s')"
   807         "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> (x, s')"
   808         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> (x, s')"
   809         "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> (x, s')"
   810         "G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> (x, s')"
   811         "G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> (v, s')"
   812         "G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> (v, s')"
   813         "G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> (v, s')"
   814         "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> (x, s')"
   815         "G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> (v, s')"
   816         "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> (v, s')"
   817         "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> (v, s')"
   818         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
   819 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   820 declare split_paired_All [simp] split_paired_Ex [simp]
   821 declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
   822 declare split_if     [split] split_if_asm     [split] 
   823         option.split [split] option.split_asm [split]
   824 
   825 lemma eval_Inj_elim: 
   826  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   827  \<Longrightarrow> case t of 
   828        In1 ec \<Rightarrow> (case ec of 
   829                     Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   830                   | Inr c \<Rightarrow> w = \<diamondsuit>)  
   831      | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   832      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   833 apply (erule eval_cases)
   834 apply auto
   835 apply (induct_tac "t")
   836 apply (rename_tac a, induct_tac "a")
   837 apply auto
   838 done
   839 
   840 text \<open>The following simplification procedures set up the proper injections of
   841  terms and their corresponding values in the evaluation relation:
   842  E.g. an expression 
   843  (injection @{term In1l} into terms) always evaluates to ordinary values 
   844  (injection @{term In1} into generalised values @{term vals}). 
   845 \<close>
   846 
   847 lemma eval_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s')"
   848   by (auto, frule eval_Inj_elim, auto)
   849 
   850 lemma eval_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s')"
   851   by (auto, frule eval_Inj_elim, auto)
   852 
   853 lemma eval_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s')"
   854   by (auto, frule eval_Inj_elim, auto)
   855 
   856 lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')"
   857   by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
   858 
   859 simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = \<open>
   860   fn _ => fn _ => fn ct =>
   861     (case Thm.term_of ct of
   862       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   863     | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\<close>
   864 
   865 simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = \<open>
   866   fn _ => fn _ => fn ct =>
   867     (case Thm.term_of ct of
   868       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   869     | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\<close>
   870 
   871 simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = \<open>
   872   fn _ => fn _ => fn ct =>
   873     (case Thm.term_of ct of
   874       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   875     | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\<close>
   876 
   877 simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = \<open>
   878   fn _ => fn _ => fn ct =>
   879     (case Thm.term_of ct of
   880       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   881     | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\<close>
   882 
   883 ML \<open>
   884 ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
   885 \<close>
   886 
   887 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
   888 
   889 text\<open>\<open>Callee\<close>,\<open>InsInitE\<close>, \<open>InsInitV\<close>, \<open>FinA\<close> are only
   890 used in smallstep semantics, not in the bigstep semantics. So their is no
   891 valid evaluation of these terms 
   892 \<close>
   893 
   894 
   895 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
   896 proof -
   897   { fix s t v s'
   898     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   899          normal: "normal s" and
   900          callee: "t=In1l (Callee l e)"
   901     then have "False" by induct auto
   902   }  
   903   then show ?thesis
   904     by (cases s') fastforce
   905 qed
   906 
   907 
   908 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
   909 proof -
   910   { fix s t v s'
   911     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   912          normal: "normal s" and
   913          callee: "t=In1l (InsInitE c e)"
   914     then have "False" by induct auto
   915   }
   916   then show ?thesis
   917     by (cases s') fastforce
   918 qed
   919 
   920 lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
   921 proof -
   922   { fix s t v s'
   923     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   924          normal: "normal s" and
   925          callee: "t=In2 (InsInitV c w)"
   926     then have "False" by induct auto
   927   }  
   928   then show ?thesis
   929     by (cases s') fastforce
   930 qed
   931 
   932 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
   933 proof -
   934   { fix s t v s'
   935     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   936          normal: "normal s" and
   937          callee: "t=In1r (FinA a c)"
   938     then have "False" by induct auto
   939   }  
   940   then show ?thesis
   941     by (cases s') fastforce 
   942 qed
   943 
   944 lemma eval_no_abrupt_lemma: 
   945    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   946 by (erule eval_cases, auto)
   947 
   948 lemma eval_no_abrupt: 
   949   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   950         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   951 apply auto
   952 apply (frule eval_no_abrupt_lemma, auto)+
   953 done
   954 
   955 simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = \<open>
   956   fn _ => fn _ => fn ct =>
   957     (case Thm.term_of ct of
   958       (_ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name None}, _)) $ _) $ _  $ _ $ _) => NONE
   959     | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
   960 \<close>
   961 
   962 
   963 lemma eval_abrupt_lemma: 
   964   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = undefined3 t"
   965 by (erule eval_cases, auto)
   966 
   967 lemma eval_abrupt: 
   968  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
   969      (s'=(Some xc,s) \<and> w=undefined3 t \<and> 
   970      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t,(Some xc,s)))"
   971 apply auto
   972 apply (frule eval_abrupt_lemma, auto)+
   973 done
   974 
   975 simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = \<open>
   976   fn _ => fn _ => fn ct =>
   977     (case Thm.term_of ct of
   978       (_ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some}, _) $ _)$ _)) => NONE
   979     | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
   980 \<close>
   981 
   982 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
   983 apply (case_tac "s", case_tac "a = None")
   984 by (auto intro!: eval.Lit)
   985 
   986 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
   987 apply (case_tac "s", case_tac "a = None")
   988 by (auto intro!: eval.Skip)
   989 
   990 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
   991 apply (case_tac "s", case_tac "a = None")
   992 by (auto intro!: eval.Expr)
   993 
   994 lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2"
   995 apply (case_tac "s", case_tac "a = None")
   996 by (auto intro!: eval.Comp)
   997 
   998 lemma CondI: 
   999   "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
  1000          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<rightarrow> s2"
  1001 apply (case_tac "s", case_tac "a = None")
  1002 by (auto intro!: eval.Cond)
  1003 
  1004 lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk>
  1005                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
  1006 apply (case_tac "s", case_tac "a = None")
  1007 by (auto intro!: eval.If)
  1008 
  1009 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
  1010                 \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
  1011 apply (case_tac "s", case_tac "a = None")
  1012 by (auto intro!: eval.Methd)
  1013 
  1014 lemma eval_Call: 
  1015    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
  1016      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
  1017      s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
  1018      s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
  1019      G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
  1020        s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
  1021        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
  1022 apply (drule eval.Call, assumption)
  1023 apply (rule HOL.refl)
  1024 apply simp+
  1025 done
  1026 
  1027 lemma eval_Init: 
  1028 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
  1029   else G\<turnstile>Norm (init_class_obj G C s0)  
  1030          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
  1031        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
  1032       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
  1033   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
  1034 apply (rule eval.Init)
  1035 apply auto
  1036 done
  1037 
  1038 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
  1039 apply (case_tac "s", simp)
  1040 apply (case_tac "a")
  1041 apply  safe
  1042 apply (rule eval_Init)
  1043 apply   auto
  1044 done
  1045 
  1046 lemma eval_StatRef: 
  1047 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else undefined)\<rightarrow> s"
  1048 apply (case_tac "s", simp)
  1049 apply (case_tac "a = None")
  1050 apply (auto del: eval.Abrupt intro!: eval.intros)
  1051 done
  1052 
  1053 
  1054 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
  1055 apply (erule eval_cases)
  1056 by auto
  1057 
  1058 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
  1059 by auto
  1060 
  1061 (*unused*)
  1062 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
  1063   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
  1064 apply (erule eval.induct)
  1065 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
  1066 apply auto
  1067 done
  1068 
  1069 lemma halloc_xcpt [dest!]: 
  1070   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
  1071 apply (erule_tac halloc_elim_cases)
  1072 by auto
  1073 
  1074 (*
  1075 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1076 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1077 *)
  1078 
  1079 lemma eval_Methd: 
  1080   "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
  1081    \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
  1082 apply (case_tac "s")
  1083 apply (case_tac "a")
  1084 apply clarsimp+
  1085 apply (erule eval.Methd)
  1086 apply (drule eval_abrupt_lemma)
  1087 apply force
  1088 done
  1089 
  1090 lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
  1091                    res=the (locals (store s2) Result);
  1092                    s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>
  1093                                   abrupt s2 = Some (Jump (Cont l))) 
  1094                    then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
  1095                    else s2);
  1096                    s4=abupd (absorb Ret) s3\<rbrakk> \<Longrightarrow>
  1097  G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s4"
  1098 by (auto elim: eval.Body)
  1099 
  1100 lemma eval_binop_arg2_indep:
  1101 "\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
  1102 by (cases binop)
  1103    (simp_all add: need_second_arg_def)
  1104 
  1105 
  1106 lemma eval_BinOp_arg2_indepI:
  1107   assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
  1108           no_need: "\<not> need_second_arg binop v1" 
  1109   shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
  1110          (is "?EvalBinOp v2")
  1111 proof -
  1112   from eval_e1 
  1113   have "?EvalBinOp Unit" 
  1114     by (rule eval.BinOp)
  1115        (simp add: no_need)
  1116   moreover
  1117   from no_need 
  1118   have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
  1119     by (simp add: eval_binop_arg2_indep)
  1120   ultimately
  1121   show ?thesis
  1122     by simp
  1123 qed
  1124 
  1125 
  1126 subsubsection "single valued"
  1127 
  1128 lemma unique_halloc [rule_format (no_asm)]: 
  1129   "G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>halloc oi\<succ>a' \<rightarrow> s'' \<longrightarrow> a' = a \<and> s'' = s'"
  1130 apply (erule halloc.induct)
  1131 apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
  1132 apply (drule trans [THEN sym], erule sym) 
  1133 defer
  1134 apply (drule trans [THEN sym], erule sym)
  1135 apply auto
  1136 done
  1137 
  1138 
  1139 lemma single_valued_halloc: 
  1140   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
  1141 apply (unfold single_valued_def)
  1142 by (clarsimp, drule (1) unique_halloc, auto)
  1143 
  1144 
  1145 lemma unique_sxalloc [rule_format (no_asm)]: 
  1146   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
  1147 apply (erule sxalloc.induct)
  1148 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
  1149               split del: split_if split_if_asm)
  1150 done
  1151 
  1152 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
  1153 apply (unfold single_valued_def)
  1154 apply (blast dest: unique_sxalloc)
  1155 done
  1156 
  1157 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
  1158 by auto
  1159 
  1160 
  1161 
  1162 lemma unique_eval [rule_format (no_asm)]: 
  1163   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w, s') \<Longrightarrow> (\<forall>w' s''. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w', s'') \<longrightarrow> w' = w \<and> s'' = s')"
  1164 apply (erule eval_induct)
  1165 apply (tactic \<open>ALLGOALS (EVERY'
  1166       [strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\<close>)
  1167 (* 31 subgoals *)
  1168 prefer 28 (* Try *) 
  1169 apply (simp (no_asm_use) only: split add: split_if_asm)
  1170 (* 34 subgoals *)
  1171 prefer 30 (* Init *)
  1172 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
  1173 prefer 26 (* While *)
  1174 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
  1175 (* 36 subgoals *)
  1176 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
  1177 done
  1178 
  1179 (* unused *)
  1180 lemma single_valued_eval: 
  1181  "single_valued {((s, t), (v, s')). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')}"
  1182 apply (unfold single_valued_def)
  1183 by (clarify, drule (1) unique_eval, auto)
  1184 
  1185 end