src/HOL/Bali/Eval.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 66110 d59f9f696110
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     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 done
   195 
   196 definition
   197   catch :: "prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) where
   198   "G,s\<turnstile>catch C = (\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
   199                         G,store s\<turnstile>Addr (the_Loc xc) fits Class C)"
   200 
   201 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
   202 apply (unfold catch_def)
   203 apply (simp (no_asm))
   204 done
   205 
   206 lemma catch_XcptLoc [simp]: 
   207   "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
   208 apply (unfold catch_def)
   209 apply (simp (no_asm))
   210 done
   211 
   212 lemma catch_Jump [simp]: "\<not>G,(Some (Jump j),s)\<turnstile>catch tn"
   213 apply (unfold catch_def)
   214 apply (simp (no_asm))
   215 done
   216 
   217 lemma catch_Error [simp]: "\<not>G,(Some (Error e),s)\<turnstile>catch tn"
   218 apply (unfold catch_def)
   219 apply (simp (no_asm))
   220 done
   221 
   222 definition
   223   new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" where
   224   "new_xcpt_var vn = (\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s))"
   225 
   226 lemma new_xcpt_var_def2 [simp]: 
   227  "new_xcpt_var vn (x,s) = 
   228     Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
   229 apply (unfold new_xcpt_var_def)
   230 apply (simp (no_asm))
   231 done
   232 
   233 
   234 
   235 subsubsection "misc"
   236 
   237 definition
   238   assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" where
   239  "assign f v = (\<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
   240                         in  (x',if x' = None then s' else s))"
   241 
   242 (*
   243 lemma assign_Norm_Norm [simp]: 
   244 "f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 
   245  \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
   246 by (simp add: assign_def Let_def)
   247 *)
   248 
   249 lemma assign_Norm_Norm [simp]: 
   250 "f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
   251 by (simp add: assign_def Let_def)
   252 
   253 (*
   254 lemma assign_Norm_Some [simp]: 
   255   "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 
   256    \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
   257 by (simp add: assign_def Let_def split_beta)
   258 *)
   259 
   260 lemma assign_Norm_Some [simp]: 
   261   "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 
   262    \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
   263 by (simp add: assign_def Let_def split_beta)
   264 
   265 
   266 lemma assign_Some [simp]: 
   267 "assign f v (Some x,s) = (Some x,s)" 
   268 by (simp add: assign_def Let_def split_beta)
   269 
   270 lemma assign_Some1 [simp]:  "\<not> normal s \<Longrightarrow> assign f v s = s" 
   271 by (auto simp add: assign_def Let_def split_beta)
   272 
   273 lemma assign_supd [simp]: 
   274 "assign (\<lambda>v. supd (f v)) v (x,s)  
   275   = (x, if x = None then f v s else s)"
   276 apply auto
   277 done
   278 
   279 lemma assign_raise_if [simp]: 
   280   "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =  
   281   (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
   282 apply (case_tac "x = None")
   283 apply auto
   284 done
   285 
   286 
   287 (*
   288 lemma assign_raise_if [simp]: 
   289   "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
   290                   store = f v (store s)\<rparr>) v s =  
   291   \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
   292    store= if (abrupt s)=None \<and> \<not>b (store s) v 
   293              then f v (store s) else (store s)\<rparr>"
   294 apply (case_tac "abrupt s = None")
   295 apply auto
   296 done
   297 *)
   298 
   299 definition
   300   init_comp_ty :: "ty \<Rightarrow> stmt"
   301   where "init_comp_ty T = (if (\<exists>C. T = Class C) then Init (the_Class T) else Skip)"
   302 
   303 lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
   304 apply (unfold init_comp_ty_def)
   305 apply (simp (no_asm))
   306 done
   307 
   308 definition
   309   invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" where
   310  "invocation_class m s a' statT =
   311     (case m of
   312        Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
   313                     then the_Class (RefT statT) 
   314                     else Object
   315      | SuperM \<Rightarrow> the_Class (RefT statT)
   316      | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
   317 
   318 definition
   319   invocation_declclass :: "prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" where
   320   "invocation_declclass G m s a' statT sig =
   321     declclass (the (dynlookup G statT
   322                                 (invocation_class m s a' statT)
   323                                 sig))" 
   324   
   325 lemma invocation_class_IntVir [simp]: 
   326 "invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
   327 by (simp add: invocation_class_def)
   328 
   329 lemma dynclass_SuperM [simp]: 
   330  "invocation_class SuperM s a' statT = the_Class (RefT statT)"
   331 by (simp add: invocation_class_def)
   332 
   333 lemma invocation_class_Static [simp]: 
   334   "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 
   335                                             then the_Class (RefT statT) 
   336                                             else Object)"
   337 by (simp add: invocation_class_def)
   338 
   339 definition
   340   init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> state \<Rightarrow> state"
   341 where
   342   "init_lvars G C sig mode a' pvs =
   343     (\<lambda>(x,s). 
   344       let m = mthd (the (methd G C sig));
   345           l = \<lambda> k. 
   346               (case k of
   347                  EName e 
   348                    \<Rightarrow> (case e of 
   349                          VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v
   350                        | Res    \<Rightarrow> None)
   351                | This 
   352                    \<Rightarrow> (if mode=Static then None else Some a'))
   353       in set_lvars l (if mode = Static then x else np a' x,s))"
   354 
   355 
   356 
   357 lemma init_lvars_def2: \<comment>\<open>better suited for simplification\<close> 
   358 "init_lvars G C sig mode a' pvs (x,s) =  
   359   set_lvars 
   360     (\<lambda> k. 
   361        (case k of
   362           EName e 
   363             \<Rightarrow> (case e of 
   364                   VNam v 
   365                   \<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
   366                | Res \<Rightarrow> None)
   367         | This 
   368             \<Rightarrow> (if mode=Static then None else Some a')))
   369     (if mode = Static then x else np a' x,s)"
   370 apply (unfold init_lvars_def)
   371 apply (simp (no_asm) add: Let_def)
   372 done
   373 
   374 definition
   375   body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" where
   376  "body G C sig =
   377     (let m = the (methd G C sig) 
   378      in Body (declclass m) (stmt (mbody (mthd m))))"
   379 
   380 lemma body_def2: \<comment>\<open>better suited for simplification\<close> 
   381 "body G C sig = Body  (declclass (the (methd G C sig))) 
   382                       (stmt (mbody (mthd (the (methd G C sig)))))"
   383 apply (unfold body_def Let_def)
   384 apply auto
   385 done
   386 
   387 subsubsection "variables"
   388 
   389 definition
   390   lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
   391   where "lvar vn s = (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
   392 
   393 definition
   394   fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
   395  "fvar C stat fn a' s =
   396    (let (oref,xf) = if stat then (Stat C,id)
   397                             else (Heap (the_Addr a'),np a');
   398                   n = Inl (fn,C); 
   399                   f = (\<lambda>v. supd (upd_gobj oref n v)) 
   400     in ((the (values (the (globs (store s) oref)) n),f),abupd xf s))"
   401 
   402 definition
   403   avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" where
   404   "avar G i' a' s =
   405     (let   oref = Heap (the_Addr a'); 
   406               i = the_Intg i'; 
   407               n = Inr i;
   408        (T,k,cs) = the_Arr (globs (store s) oref); 
   409               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
   410                                            ArrStore x
   411                               ,upd_gobj oref n v s)) 
   412      in ((the (cs n),f),abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s))"
   413 
   414 lemma fvar_def2: \<comment>\<open>better suited for simplification\<close> 
   415 "fvar C stat fn a' s =  
   416   ((the 
   417      (values 
   418       (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
   419       (Inl (fn,C)))
   420    ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
   421                         (Inl (fn,C)) 
   422                         v)))
   423   ,abupd (if stat then id else np a') s)
   424   "
   425 apply (unfold fvar_def)
   426 apply (simp (no_asm) add: Let_def split_beta)
   427 done
   428 
   429 lemma avar_def2: \<comment>\<open>better suited for simplification\<close> 
   430 "avar G i' a' s =  
   431   ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
   432            (Inr (the_Intg i')))
   433    ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
   434                                                    (Heap (the_Addr a')))))) 
   435                             ArrStore x
   436                  ,upd_gobj  (Heap (the_Addr a')) 
   437                                (Inr (the_Intg i')) v s')))
   438   ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
   439                    (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
   440           s)"
   441 apply (unfold avar_def)
   442 apply (simp (no_asm) add: Let_def split_beta)
   443 done
   444 
   445 definition
   446   check_field_access :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
   447   "check_field_access G accC statDeclC fn stat a' s =
   448     (let oref = if stat then Stat statDeclC
   449                 else Heap (the_Addr a');
   450          dynC = case oref of
   451                    Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
   452                  | Stat C \<Rightarrow> C;
   453          f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
   454      in abupd 
   455         (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
   456                   AccessViolation)
   457         s)"
   458 
   459 definition
   460   check_method_access :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" where
   461   "check_method_access G accC statT mode sig  a' s =
   462     (let invC = invocation_class mode (store s) a' statT;
   463        dynM = the (dynlookup G statT invC sig)
   464      in abupd 
   465         (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
   466                   AccessViolation)
   467         s)"
   468        
   469 subsubsection "evaluation judgments"
   470 
   471 inductive
   472   halloc :: "[prog,state,obj_tag,loc,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) for G::prog
   473 where \<comment>\<open>allocating objects on the heap, cf. 12.5\<close>
   474 
   475   Abrupt: 
   476   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>undefined\<rightarrow> (Some x,s)"
   477 
   478 | New:    "\<lbrakk>new_Addr (heap s) = Some a; 
   479             (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   480                        else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   481             \<Longrightarrow>
   482             G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   483 
   484 inductive sxalloc :: "[prog,state,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,61]60) for G::prog
   485 where \<comment>\<open>allocating exception objects for
   486   standard exceptions (other than OutOfMemory)\<close>
   487 
   488   Norm:  "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   489 
   490 | Jmp:   "G\<turnstile>(Some (Jump j), s)  \<midarrow>sxalloc\<rightarrow> (Some (Jump j), s)"
   491 
   492 | Error: "G\<turnstile>(Some (Error e), s)  \<midarrow>sxalloc\<rightarrow> (Some (Error e), s)"
   493 
   494 | XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   495 
   496 | SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   497           G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   498 
   499 
   500 inductive
   501   eval :: "[prog,state,term,vals,state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> '(_, _')"  [61,61,80,0,0]60)
   502   and exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   503   and evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   504   and eval'::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   505   and evals::"[prog,state,expr list ,
   506                     val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   507   for G::prog
   508 where
   509 
   510   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,  s')"
   511 | "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v,  s')"
   512 | "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf, s')"
   513 | "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v,  s')"
   514 
   515 \<comment>\<open>propagation of abrupt completion\<close>
   516 
   517   \<comment>\<open>cf. 14.1, 15.5\<close>
   518 | Abrupt: 
   519    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t, (Some xc, s))"
   520 
   521 
   522 \<comment>\<open>execution of statements\<close>
   523 
   524   \<comment>\<open>cf. 14.5\<close>
   525 | Skip:                             "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   526 
   527   \<comment>\<open>cf. 14.7\<close>
   528 | Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   529                                   G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   530 
   531 | Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   532                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
   533   \<comment>\<open>cf. 14.2\<close>
   534 | Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   535           G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   536                                  G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   537 
   538   \<comment>\<open>cf. 14.8.2\<close>
   539 | If:   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   540           G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   541                        G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   542 
   543   \<comment>\<open>cf. 14.10, 14.10.1\<close>
   544   
   545   \<comment>\<open>A continue jump from the while body @{term c} is handled by 
   546      this rule. If a continue jump with the proper label was invoked inside 
   547      @{term c} this label (Cont l) is deleted out of the abrupt component of 
   548      the state before the iterative evaluation of the while statement.
   549      A break jump is handled by the Lab Statement \<open>Lab l (while\<dots>)\<close>.
   550 \<close>
   551 | Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   552           if the_Bool b 
   553              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   554                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   555              else s3 = s1\<rbrakk> \<Longrightarrow>
   556                               G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   557 
   558 | Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<rightarrow> (Some (Jump j), s)"
   559    
   560   \<comment>\<open>cf. 14.16\<close>
   561 | Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   562                                  G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   563 
   564   \<comment>\<open>cf. 14.18.1\<close>
   565 | Try:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   566           if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   567                   G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   568 
   569   \<comment>\<open>cf. 14.18.2\<close>
   570 | Fin:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   571           G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
   572           s3=(if (\<exists> err. x1=Some (Error err)) 
   573               then (x1,s1) 
   574               else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
   575           \<Longrightarrow>
   576           G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
   577   \<comment>\<open>cf. 12.4.2, 8.5\<close>
   578 | Init: "\<lbrakk>the (class G C) = c;
   579           if inited C (globs s0) then s3 = Norm s0
   580           else (G\<turnstile>Norm (init_class_obj G C s0) 
   581                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   582                G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   583               \<Longrightarrow>
   584                  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   585    \<comment>\<open>This class initialisation rule is a little bit inaccurate. Look at the
   586       exact sequence:
   587       (1) The current class object (the static fields) are initialised
   588            (\<open>init_class_obj\<close>),
   589       (2) the superclasses are initialised,
   590       (3) the static initialiser of the current class is invoked.
   591       More precisely we should expect another ordering, namely 2 1 3.
   592       But we can't just naively toggle 1 and 2. By calling 
   593       \<open>init_class_obj\<close> 
   594       before initialising the superclasses, we also implicitly record that
   595       we have started to initialise the current class (by setting an 
   596       value for the class object). This becomes 
   597       crucial for the completeness proof of the axiomatic semantics 
   598       \<open>AxCompl.thy\<close>. Static initialisation requires an induction on 
   599       the number of classes not yet initialised (or to be more precise, 
   600       classes were the initialisation has not yet begun). 
   601       So we could first assign a dummy value to the class before
   602       superclass initialisation and afterwards set the correct values.
   603       But as long as we don't take memory overflow into account 
   604       when allocating class objects, we can leave things as they are for 
   605       convenience. 
   606 \<close>
   607 \<comment>\<open>evaluation of expressions\<close>
   608 
   609   \<comment>\<open>cf. 15.8.1, 12.4.1\<close>
   610 | NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   611           G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   612                                   G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   613 
   614   \<comment>\<open>cf. 15.9.1, 12.4.1\<close>
   615 | NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   616           G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   617                                 G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   618 
   619   \<comment>\<open>cf. 15.15\<close>
   620 | Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   621           s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   622                                 G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   623 
   624   \<comment>\<open>cf. 15.19.2\<close>
   625 | Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   626           b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   627                               G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   628 
   629   \<comment>\<open>cf. 15.7.1\<close>
   630 | Lit:  "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   631 
   632 | UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
   633          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
   634  
   635 | BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
   636           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
   637                 \<succ>\<rightarrow> (In1 v2, s2)
   638           \<rbrakk> 
   639          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
   640    
   641   \<comment>\<open>cf. 15.10.2\<close>
   642 | Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   643 
   644   \<comment>\<open>cf. 15.2\<close>
   645 | Acc:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   646                                   G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   647 
   648   \<comment>\<open>cf. 15.25.1\<close>
   649 | Ass:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   650           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   651                                    G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   652 
   653   \<comment>\<open>cf. 15.24\<close>
   654 | Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   655           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   656                             G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   657 
   658 
   659 \<comment> \<open>The interplay of  @{term Call}, @{term Methd} and @{term Body}:
   660       Method invocation is split up into these three rules:
   661       \begin{itemize}
   662       \item [@{term Call}] Calculates the target address and evaluates the
   663                            arguments of the method, and then performs dynamic
   664                            or static lookup of the method, corresponding to the
   665                            call mode. Then the @{term Methd} rule is evaluated
   666                            on the calculated declaration class of the method
   667                            invocation.
   668       \item [@{term Methd}] A syntactic bridge for the folded method body.
   669                             It is used by the axiomatic semantics to add the
   670                             proper hypothesis for recursive calls of the method.
   671       \item [@{term Body}] An extra syntactic entity for the unfolded method
   672                            body was introduced to properly trigger class 
   673                            initialisation. Without class initialisation we 
   674                            could just evaluate the body statement. 
   675       \end{itemize}
   676 \<close>
   677   \<comment>\<open>cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5\<close>
   678 | Call: 
   679   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   680     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   681     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   682     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   683     G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
   684    \<Longrightarrow>
   685        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
   686 \<comment>\<open>The accessibility check is after @{term init_lvars}, to keep it simple. 
   687    @{term init_lvars} already tests for the absence of a null-pointer 
   688    reference in case of an instance method invocation.
   689 \<close>
   690 
   691 | Methd:        "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   692                                 G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   693   
   694 | Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; 
   695           s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
   696                          abrupt s2 = Some (Jump (Cont l)))
   697                   then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
   698                   else s2)\<rbrakk> \<Longrightarrow>
   699            G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
   700               \<rightarrow>abupd (absorb Ret) s3"
   701   \<comment>\<open>cf. 14.15, 12.4.1\<close>
   702   \<comment>\<open>We filter out a break/continue in @{term s2}, so that we can proof 
   703      definite assignment
   704      correct, without the need of conformance of the state. By this the
   705      different parts of the typesafety proof can be disentangled a little.\<close>
   706 
   707 \<comment>\<open>evaluation of variables\<close>
   708 
   709   \<comment>\<open>cf. 15.13.1, 15.7.2\<close>
   710 | LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   711 
   712   \<comment>\<open>cf. 15.10.1, 12.4.1\<close>
   713 | FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   714           (v,s2') = fvar statDeclC stat fn a s2;
   715           s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
   716           G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
   717  \<comment>\<open>The accessibility check is after @{term fvar}, to keep it simple. 
   718     @{term fvar} already tests for the absence of a null-pointer reference 
   719     in case of an instance field
   720 \<close>
   721 
   722   \<comment>\<open>cf. 15.12.1, 15.25.1\<close>
   723 | AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   724           (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   725                       G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   726 
   727 
   728 \<comment>\<open>evaluation of expression lists\<close>
   729 
   730   \<comment>\<open>cf. 15.11.4.2\<close>
   731 | Nil:
   732                                     "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   733 
   734   \<comment>\<open>cf. 15.6.4\<close>
   735 | Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   736           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   737                                    G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   738 
   739 (* Rearrangement of premisses:
   740 [0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
   741  17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
   742  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
   743  29(AVar),24(Call)]
   744 *)
   745 
   746 ML \<open>
   747 ML_Thms.bind_thm ("eval_induct", rearrange_prems 
   748 [0,1,2,8,4,30,31,27,15,16,
   749  17,18,19,20,21,3,5,25,26,23,6,
   750  7,11,9,13,14,12,22,10,28,
   751  29,24] @{thm eval.induct})
   752 \<close>
   753 
   754 
   755 declare if_split     [split del] if_split_asm     [split del] 
   756         option.split [split del] option.split_asm [split del]
   757 inductive_cases halloc_elim_cases: 
   758   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   759   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   760 
   761 inductive_cases sxalloc_elim_cases:
   762         "G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   763         "G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
   764         "G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
   765         "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   766         "G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   767 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   768 
   769 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   770        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   771        \<And>j s. \<lbrakk>s' = (Some (Jump j),s)\<rbrakk> \<Longrightarrow> P;
   772        \<And>e s. \<lbrakk>s' = (Some (Error e),s)\<rbrakk> \<Longrightarrow> P;
   773        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   774       \<rbrakk> \<Longrightarrow> P"
   775 apply cut_tac 
   776 apply (erule sxalloc_cases)
   777 apply blast+
   778 done
   779 
   780 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   781 declare split_paired_All [simp del] split_paired_Ex [simp del]
   782 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   783 
   784 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
   785 
   786 inductive_cases eval_elim_cases [cases set]:
   787         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> (v, s')"
   788         "G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> (x, s')"
   789         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                        \<succ>\<rightarrow> (x, s')"
   790         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> (x, s')"
   791         "G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> (v, s')"
   792         "G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> (v, s')"
   793         "G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> (v, s')"
   794         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> (v, s')"
   795         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> (v, s')"
   796         "G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> (v, s')"
   797         "G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> (v, s')"
   798         "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> (v, s')"
   799         "G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> (v, s')"
   800         "G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> (v, s')"
   801         "G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> (x, s')"
   802         "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> (x, s')"
   803         "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> (x, s')"
   804         "G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> (x, s')"
   805         "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> (v, s')"
   806         "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> (x, s')"
   807         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> (x, s')"
   808         "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> (x, s')"
   809         "G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> (x, s')"
   810         "G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> (v, s')"
   811         "G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> (v, s')"
   812         "G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> (v, s')"
   813         "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> (x, s')"
   814         "G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> (v, s')"
   815         "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> (v, s')"
   816         "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> (v, s')"
   817         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
   818 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   819 declare split_paired_All [simp] split_paired_Ex [simp]
   820 declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
   821 declare if_split     [split] if_split_asm     [split] 
   822         option.split [split] option.split_asm [split]
   823 
   824 lemma eval_Inj_elim: 
   825  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   826  \<Longrightarrow> case t of 
   827        In1 ec \<Rightarrow> (case ec of 
   828                     Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   829                   | Inr c \<Rightarrow> w = \<diamondsuit>)  
   830      | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   831      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   832 apply (erule eval_cases)
   833 apply auto
   834 apply (induct_tac "t")
   835 apply (rename_tac a, induct_tac "a")
   836 apply auto
   837 done
   838 
   839 text \<open>The following simplification procedures set up the proper injections of
   840  terms and their corresponding values in the evaluation relation:
   841  E.g. an expression 
   842  (injection @{term In1l} into terms) always evaluates to ordinary values 
   843  (injection @{term In1} into generalised values @{term vals}). 
   844 \<close>
   845 
   846 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')"
   847   by (auto, frule eval_Inj_elim, auto)
   848 
   849 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')"
   850   by (auto, frule eval_Inj_elim, auto)
   851 
   852 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')"
   853   by (auto, frule eval_Inj_elim, auto)
   854 
   855 lemma eval_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s')"
   856   by (auto, frule eval_Inj_elim, auto, frule eval_Inj_elim, auto)
   857 
   858 simproc_setup eval_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<rightarrow> (w, s')") = \<open>
   859   fn _ => fn _ => fn ct =>
   860     (case Thm.term_of ct of
   861       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   862     | _ => SOME (mk_meta_eq @{thm eval_expr_eq}))\<close>
   863 
   864 simproc_setup eval_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<rightarrow> (w, s')") = \<open>
   865   fn _ => fn _ => fn ct =>
   866     (case Thm.term_of ct of
   867       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   868     | _ => SOME (mk_meta_eq @{thm eval_var_eq}))\<close>
   869 
   870 simproc_setup eval_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<rightarrow> (w, s')") = \<open>
   871   fn _ => fn _ => fn ct =>
   872     (case Thm.term_of ct of
   873       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   874     | _ => SOME (mk_meta_eq @{thm eval_exprs_eq}))\<close>
   875 
   876 simproc_setup eval_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<rightarrow> (w, s')") = \<open>
   877   fn _ => fn _ => fn ct =>
   878     (case Thm.term_of ct of
   879       (_ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   880     | _ => SOME (mk_meta_eq @{thm eval_stmt_eq}))\<close>
   881 
   882 ML \<open>
   883 ML_Thms.bind_thms ("AbruptIs", sum3_instantiate @{context} @{thm eval.Abrupt})
   884 \<close>
   885 
   886 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]
   887 
   888 text\<open>\<open>Callee\<close>,\<open>InsInitE\<close>, \<open>InsInitV\<close>, \<open>FinA\<close> are only
   889 used in smallstep semantics, not in the bigstep semantics. So their is no
   890 valid evaluation of these terms 
   891 \<close>
   892 
   893 
   894 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
   895 proof -
   896   { fix s t v s'
   897     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   898          normal: "normal s" and
   899          callee: "t=In1l (Callee l e)"
   900     then have "False" by induct auto
   901   }  
   902   then show ?thesis
   903     by (cases s') fastforce
   904 qed
   905 
   906 
   907 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
   908 proof -
   909   { fix s t v s'
   910     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   911          normal: "normal s" and
   912          callee: "t=In1l (InsInitE c e)"
   913     then have "False" by induct auto
   914   }
   915   then show ?thesis
   916     by (cases s') fastforce
   917 qed
   918 
   919 lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
   920 proof -
   921   { fix s t v s'
   922     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   923          normal: "normal s" and
   924          callee: "t=In2 (InsInitV c w)"
   925     then have "False" by induct auto
   926   }  
   927   then show ?thesis
   928     by (cases s') fastforce
   929 qed
   930 
   931 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
   932 proof -
   933   { fix s t v s'
   934     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   935          normal: "normal s" and
   936          callee: "t=In1r (FinA a c)"
   937     then have "False" by induct auto
   938   }  
   939   then show ?thesis
   940     by (cases s') fastforce 
   941 qed
   942 
   943 lemma eval_no_abrupt_lemma: 
   944    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   945 by (erule eval_cases, auto)
   946 
   947 lemma eval_no_abrupt: 
   948   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   949         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   950 apply auto
   951 apply (frule eval_no_abrupt_lemma, auto)+
   952 done
   953 
   954 simproc_setup eval_no_abrupt ("G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')") = \<open>
   955   fn _ => fn _ => fn ct =>
   956     (case Thm.term_of ct of
   957       (_ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name None}, _)) $ _) $ _  $ _ $ _) => NONE
   958     | _ => SOME (mk_meta_eq @{thm eval_no_abrupt}))
   959 \<close>
   960 
   961 
   962 lemma eval_abrupt_lemma: 
   963   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = undefined3 t"
   964 by (erule eval_cases, auto)
   965 
   966 lemma eval_abrupt: 
   967  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
   968      (s'=(Some xc,s) \<and> w=undefined3 t \<and> 
   969      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t,(Some xc,s)))"
   970 apply auto
   971 apply (frule eval_abrupt_lemma, auto)+
   972 done
   973 
   974 simproc_setup eval_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')") = \<open>
   975   fn _ => fn _ => fn ct =>
   976     (case Thm.term_of ct of
   977       (_ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some}, _) $ _)$ _)) => NONE
   978     | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
   979 \<close>
   980 
   981 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
   982 apply (case_tac "s", case_tac "a = None")
   983 by (auto intro!: eval.Lit)
   984 
   985 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
   986 apply (case_tac "s", case_tac "a = None")
   987 by (auto intro!: eval.Skip)
   988 
   989 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
   990 apply (case_tac "s", case_tac "a = None")
   991 by (auto intro!: eval.Expr)
   992 
   993 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"
   994 apply (case_tac "s", case_tac "a = None")
   995 by (auto intro!: eval.Comp)
   996 
   997 lemma CondI: 
   998   "\<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> 
   999          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<rightarrow> s2"
  1000 apply (case_tac "s", case_tac "a = None")
  1001 by (auto intro!: eval.Cond)
  1002 
  1003 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>
  1004                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
  1005 apply (case_tac "s", case_tac "a = None")
  1006 by (auto intro!: eval.If)
  1007 
  1008 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
  1009                 \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
  1010 apply (case_tac "s", case_tac "a = None")
  1011 by (auto intro!: eval.Methd)
  1012 
  1013 lemma eval_Call: 
  1014    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
  1015      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
  1016      s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
  1017      s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
  1018      G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
  1019        s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
  1020        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
  1021 apply (drule eval.Call, assumption)
  1022 apply (rule HOL.refl)
  1023 apply simp+
  1024 done
  1025 
  1026 lemma eval_Init: 
  1027 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
  1028   else G\<turnstile>Norm (init_class_obj G C s0)  
  1029          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
  1030        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
  1031       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
  1032   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
  1033 apply (rule eval.Init)
  1034 apply auto
  1035 done
  1036 
  1037 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
  1038 apply (case_tac "s", simp)
  1039 apply (case_tac "a")
  1040 apply  safe
  1041 apply (rule eval_Init)
  1042 apply   auto
  1043 done
  1044 
  1045 lemma eval_StatRef: 
  1046 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else undefined)\<rightarrow> s"
  1047 apply (case_tac "s", simp)
  1048 apply (case_tac "a = None")
  1049 apply (auto del: eval.Abrupt intro!: eval.intros)
  1050 done
  1051 
  1052 
  1053 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
  1054 apply (erule eval_cases)
  1055 by auto
  1056 
  1057 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
  1058 by auto
  1059 
  1060 (*unused*)
  1061 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
  1062   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
  1063 apply (erule eval.induct)
  1064 apply (simp (no_asm_use) split del: if_split_asm option.split_asm)+
  1065 apply auto
  1066 done
  1067 
  1068 lemma halloc_xcpt [dest!]: 
  1069   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
  1070 apply (erule_tac halloc_elim_cases)
  1071 by auto
  1072 
  1073 (*
  1074 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1075 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1076 *)
  1077 
  1078 lemma eval_Methd: 
  1079   "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
  1080    \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
  1081 apply (case_tac "s")
  1082 apply (case_tac "a")
  1083 apply clarsimp+
  1084 apply (erule eval.Methd)
  1085 apply (drule eval_abrupt_lemma)
  1086 apply force
  1087 done
  1088 
  1089 lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
  1090                    res=the (locals (store s2) Result);
  1091                    s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>
  1092                                   abrupt s2 = Some (Jump (Cont l))) 
  1093                    then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
  1094                    else s2);
  1095                    s4=abupd (absorb Ret) s3\<rbrakk> \<Longrightarrow>
  1096  G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s4"
  1097 by (auto elim: eval.Body)
  1098 
  1099 lemma eval_binop_arg2_indep:
  1100 "\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
  1101 by (cases binop)
  1102    (simp_all add: need_second_arg_def)
  1103 
  1104 
  1105 lemma eval_BinOp_arg2_indepI:
  1106   assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
  1107           no_need: "\<not> need_second_arg binop v1" 
  1108   shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
  1109          (is "?EvalBinOp v2")
  1110 proof -
  1111   from eval_e1 
  1112   have "?EvalBinOp Unit" 
  1113     by (rule eval.BinOp)
  1114        (simp add: no_need)
  1115   moreover
  1116   from no_need 
  1117   have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
  1118     by (simp add: eval_binop_arg2_indep)
  1119   ultimately
  1120   show ?thesis
  1121     by simp
  1122 qed
  1123 
  1124 
  1125 subsubsection "single valued"
  1126 
  1127 lemma unique_halloc [rule_format (no_asm)]: 
  1128   "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'"
  1129 apply (erule halloc.induct)
  1130 apply  (auto elim!: halloc_elim_cases split del: if_split if_split_asm)
  1131 apply (drule trans [THEN sym], erule sym) 
  1132 defer
  1133 apply (drule trans [THEN sym], erule sym)
  1134 apply auto
  1135 done
  1136 
  1137 
  1138 lemma single_valued_halloc: 
  1139   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
  1140 apply (unfold single_valued_def)
  1141 by (clarsimp, drule (1) unique_halloc, auto)
  1142 
  1143 
  1144 lemma unique_sxalloc [rule_format (no_asm)]: 
  1145   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
  1146 apply (erule sxalloc.induct)
  1147 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
  1148               split del: if_split if_split_asm)
  1149 done
  1150 
  1151 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
  1152 apply (unfold single_valued_def)
  1153 apply (blast dest: unique_sxalloc)
  1154 done
  1155 
  1156 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
  1157 by auto
  1158 
  1159 
  1160 
  1161 lemma unique_eval [rule_format (no_asm)]: 
  1162   "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')"
  1163 apply (erule eval_induct)
  1164 apply (tactic \<open>ALLGOALS (EVERY'
  1165       [strip_tac @{context}, rotate_tac ~1, eresolve_tac @{context} @{thms eval_elim_cases}])\<close>)
  1166 (* 31 subgoals *)
  1167 prefer 28 (* Try *) 
  1168 apply (simp (no_asm_use) only: split: if_split_asm)
  1169 (* 34 subgoals *)
  1170 prefer 30 (* Init *)
  1171 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False simp_thms)+)
  1172 prefer 26 (* While *)
  1173 apply (simp (no_asm_use) only: split: if_split_asm, blast)
  1174 (* 36 subgoals *)
  1175 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
  1176 done
  1177 
  1178 (* unused *)
  1179 lemma single_valued_eval: 
  1180  "single_valued {((s, t), (v, s')). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')}"
  1181 apply (unfold single_valued_def)
  1182 by (clarify, drule (1) unique_eval, auto)
  1183 
  1184 end