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