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