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