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