src/HOL/Bali/Eval.thy
author schirmer
Tue Jul 16 20:25:21 2002 +0200 (2002-07-16)
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13462 56610e2ba220
permissions -rw-r--r--
Added conditional and (&&) and or (||).
     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 primrec
   459 "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
   460 "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
   461 "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
   462 "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
   463 "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
   464 
   465 -- "Be aware of the explicit coercion of the shift distance to nat"
   466 "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
   467 "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
   468 "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
   469 
   470 "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
   471 "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
   472 "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
   473 "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
   474 
   475 "eval_binop Eq      v1 v2 = Bool (v1=v2)"
   476 "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
   477 "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   478 "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   479 "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   480 "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
   481 "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
   482 "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   483 "eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
   484 "eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
   485 
   486 constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
   487 "need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
   488                                (binop=CondOr  \<and> the_Bool v1))"
   489 text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
   490  if the value isn't already determined by the first argument*}
   491 
   492 lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
   493 by (simp add: need_second_arg_def)
   494 
   495 lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
   496 by (simp add: need_second_arg_def)
   497 
   498 lemma need_second_arg_strict[simp]: 
   499  "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
   500 by (cases binop) 
   501    (simp_all add: need_second_arg_def)
   502 
   503 consts
   504   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
   505   halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
   506   sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
   507 
   508 
   509 syntax
   510 eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
   511 exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
   512 evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
   513 eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
   514 evals::"[prog,state,expr list ,
   515 		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
   516 hallo::"[prog,state,obj_tag,
   517 	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
   518 sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
   519 
   520 syntax (xsymbols)
   521 eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
   522 exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   523 evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   524 eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   525 evals::"[prog,state,expr list ,
   526 		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   527 hallo::"[prog,state,obj_tag,
   528 	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   529 sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
   530 
   531 translations
   532   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
   533   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
   534   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
   535   "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
   536   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
   537   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
   538   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
   539   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
   540   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
   541   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
   542   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
   543   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
   544   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
   545   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
   546   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
   547 
   548 inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
   549 
   550   Abrupt: 
   551   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
   552 
   553   New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
   554 	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   555 		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   556             \<Longrightarrow>
   557 	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   558 
   559 inductive "sxalloc G" intros (* allocating exception objects for
   560 	 	 	      standard exceptions (other than OutOfMemory) *)
   561 
   562   Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   563 
   564   XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   565 
   566   SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   567 	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   568 
   569 text {* 
   570 \par
   571 *} (* dummy text command to break paragraph for latex;
   572               large paragraphs exhaust memory of debian pdflatex *)
   573 
   574 inductive "eval G" intros
   575 
   576 (* propagation of abrupt completion *)
   577 
   578   (* cf. 14.1, 15.5 *)
   579   Abrupt: 
   580    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
   581 
   582 
   583 (* execution of statements *)
   584 
   585   (* cf. 14.5 *)
   586   Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   587 
   588   (* cf. 14.7 *)
   589   Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   590 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   591 
   592   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   593                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
   594   (* cf. 14.2 *)
   595   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   596 	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   597 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   598 
   599 
   600   (* cf. 14.8.2 *)
   601   If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   602 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   603 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   604 
   605   (* cf. 14.10, 14.10.1 *)
   606   (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
   607   (* A "continue jump" from the while body c is handled by 
   608      this rule. If a continue jump with the proper label was invoked inside c
   609      this label (Cont l) is deleted out of the abrupt component of the state 
   610      before the iterative evaluation of the while statement.
   611      A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
   612   *)
   613   Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   614 	  if normal s1 \<and> the_Bool b 
   615              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   616                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   617 	     else s3 = s1\<rbrakk> \<Longrightarrow>
   618 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   619 
   620   Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
   621    
   622   (* cf. 14.16 *)
   623   Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   624 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   625 
   626   (* cf. 14.18.1 *)
   627   Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   628 	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   629 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   630 
   631   (* cf. 14.18.2 *)
   632   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   633 	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
   634           s3=(if (\<exists> err. x1=Some (Error err)) 
   635               then (x1,s1) 
   636               else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
   637           \<Longrightarrow>
   638           G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
   639   (* cf. 12.4.2, 8.5 *)
   640   Init:	"\<lbrakk>the (class G C) = c;
   641 	  if inited C (globs s0) then s3 = Norm s0
   642 	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   643 		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   644 	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   645               \<Longrightarrow>
   646 		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   647    (* This class initialisation rule is a little bit inaccurate. Look at the
   648       exact sequence:
   649       1. The current class object (the static fields) are initialised
   650          (init_class_obj)
   651       2. Then the superclasses are initialised
   652       3. The static initialiser of the current class is invoked
   653       More precisely we should expect another ordering, namely 2 1 3.
   654       But we can't just naively toggle 1 and 2. By calling init_class_obj 
   655       before initialising the superclasses we also implicitly record that
   656       we have started to initialise the current class (by setting an 
   657       value for the class object). This becomes 
   658       crucial for the completeness proof of the axiomatic semantics 
   659       (AxCompl.thy). Static initialisation requires an induction on the number 
   660       of classes not yet initialised (or to be more precise, classes where the
   661       initialisation has not yet begun). 
   662       So we could first assign a dummy value to the class before
   663       superclass initialisation and afterwards set the correct values.
   664       But as long as we don't take memory overflow into account 
   665       when allocating class objects, and don't model definite assignment in
   666       the static initialisers, we can leave things as they are for convenience. 
   667    *)
   668 (* evaluation of expressions *)
   669 
   670   (* cf. 15.8.1, 12.4.1 *)
   671   NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   672 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   673 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   674 
   675   (* cf. 15.9.1, 12.4.1 *)
   676   NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   677 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   678 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   679 
   680   (* cf. 15.15 *)
   681   Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   682 	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   683 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   684 
   685   (* cf. 15.19.2 *)
   686   Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   687 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   688 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   689 
   690   (* cf. 15.7.1 *)
   691   Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   692 
   693   UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
   694          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
   695  
   696   BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
   697           G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
   698                 \<succ>\<rightarrow> (In1 v2,s2)
   699           \<rbrakk> 
   700          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
   701    
   702   (* cf. 15.10.2 *)
   703   Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   704 
   705   (* cf. 15.2 *)
   706   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   707 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   708 
   709   (* cf. 15.25.1 *)
   710   Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   711           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   712 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   713 
   714   (* cf. 15.24 *)
   715   Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   716           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   717 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   718 
   719 
   720   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
   721   Call:	
   722   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   723     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   724     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   725     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   726     G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
   727    \<Longrightarrow>
   728        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
   729 (* The accessibility check is after init_lvars, to keep it simple. Init_lvars 
   730    already tests for the absence of a null-pointer reference in case of an
   731    instance method invocation
   732 *)
   733 
   734   Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   735 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   736   (* The local variables l are just a dummy here. The are only used by
   737      the smallstep semantics *)
   738   (* cf. 14.15, 12.4.1 *)
   739   Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   740            G\<turnstile>Norm s0 \<midarrow>Body D c
   741             -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   742   (* The local variables l are just a dummy here. The are only used by
   743      the smallstep semantics *)
   744 (* evaluation of variables *)
   745 
   746   (* cf. 15.13.1, 15.7.2 *)
   747   LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   748 
   749   (* cf. 15.10.1, 12.4.1 *)
   750   FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   751 	  (v,s2') = fvar statDeclC stat fn a s2;
   752           s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
   753 	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
   754  (* The accessibility check is after fvar, to keep it simple. Fvar already
   755     tests for the absence of a null-pointer reference in case of an instance
   756     field
   757   *)
   758 
   759   (* cf. 15.12.1, 15.25.1 *)
   760   AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   761 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   762 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   763 
   764 
   765 (* evaluation of expression lists *)
   766 
   767   (* cf. 15.11.4.2 *)
   768   Nil:
   769 				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   770 
   771   (* cf. 15.6.4 *)
   772   Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   773           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   774 				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   775 
   776 (* Rearrangement of premisses:
   777 [0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
   778  17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
   779  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
   780  29(AVar),24(Call)]
   781 *)
   782 ML {*
   783 bind_thm ("eval_induct_", rearrange_prems 
   784 [0,1,2,8,4,30,31,27,15,16,
   785  17,18,19,20,21,3,5,25,26,23,6,
   786  7,11,9,13,14,12,22,10,28,
   787  29,24] (thm "eval.induct"))
   788 *}
   789 
   790 
   791 text {* 
   792 \par
   793 *} (* dummy text command to break paragraph for latex;
   794               large paragraphs exhaust memory of debian pdflatex *)
   795 
   796 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
   797    and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
   798    and and 
   799    s2 (* Fin *) and and s2 (* NewC *)] 
   800 
   801 declare split_if     [split del] split_if_asm     [split del] 
   802         option.split [split del] option.split_asm [split del]
   803 inductive_cases halloc_elim_cases: 
   804   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   805   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   806 
   807 inductive_cases sxalloc_elim_cases:
   808  	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   809  	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   810  	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   811 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   812 
   813 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   814        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   815        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   816       \<rbrakk> \<Longrightarrow> P"
   817 apply cut_tac 
   818 apply (erule sxalloc_cases)
   819 apply blast+
   820 done
   821 
   822 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   823 declare split_paired_All [simp del] split_paired_Ex [simp del]
   824 ML_setup {*
   825 simpset_ref() := simpset() delloop "split_all_tac"
   826 *}
   827 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
   828 
   829 inductive_cases eval_elim_cases:
   830         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"
   831 	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"
   832         "G\<turnstile>Norm s \<midarrow>In1r (Do j)                         \<succ>\<rightarrow> xs'"
   833         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"
   834 	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
   835 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
   836 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
   837         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"
   838         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"
   839 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
   840 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
   841 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
   842 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"
   843 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"
   844 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"
   845 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"
   846 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"
   847 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"
   848 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"
   849 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"
   850 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"
   851 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"
   852 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"
   853 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"
   854 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"
   855 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"
   856 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"
   857 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"
   858 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"
   859 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   860 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"
   861 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   862 declare split_paired_All [simp] split_paired_Ex [simp]
   863 ML_setup {*
   864 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   865 *}
   866 declare split_if     [split] split_if_asm     [split] 
   867         option.split [split] option.split_asm [split]
   868 
   869 lemma eval_Inj_elim: 
   870  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   871  \<Longrightarrow> case t of 
   872        In1 ec \<Rightarrow> (case ec of 
   873                     Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   874                   | Inr c \<Rightarrow> w = \<diamondsuit>)  
   875      | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   876      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   877 apply (erule eval_cases)
   878 apply auto
   879 apply (induct_tac "t")
   880 apply (induct_tac "a")
   881 apply auto
   882 done
   883 
   884 
   885 ML_setup {*
   886 fun eval_fun nam inj rhs =
   887 let
   888   val name = "eval_" ^ nam ^ "_eq"
   889   val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
   890   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   891 	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
   892   fun is_Inj (Const (inj,_) $ _) = true
   893     | is_Inj _                   = false
   894   fun pred (_ $ (Const ("Pair",_) $ _ $ 
   895       (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
   896 in
   897   make_simproc name lhs pred (thm name)
   898 end
   899 
   900 val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
   901 val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
   902 val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
   903 val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
   904 Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
   905 bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
   906 *}
   907 
   908 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
   909 
   910 text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
   911 used in smallstep semantics, not in the bigstep semantics. So their is no
   912 valid evaluation of these terms 
   913 *}
   914 
   915 
   916 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
   917 proof -
   918   { fix s t v s'
   919     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   920          normal: "normal s" and
   921          callee: "t=In1l (Callee l e)"
   922     then have "False"
   923     proof (induct)
   924     qed (auto)
   925   }  
   926   then show ?thesis
   927     by (cases s') fastsimp
   928 qed
   929 
   930 
   931 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<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=In1l (InsInitE c e)"
   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_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
   946 proof -
   947   { fix s t v s'
   948     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   949          normal: "normal s" and
   950          callee: "t=In2 (InsInitV c w)"
   951     then have "False"
   952     proof (induct)
   953     qed (auto)
   954   }  
   955   then show ?thesis
   956     by (cases s') fastsimp
   957 qed
   958 
   959 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
   960 proof -
   961   { fix s t v s'
   962     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
   963          normal: "normal s" and
   964          callee: "t=In1r (FinA a c)"
   965     then have "False"
   966     proof (induct)
   967     qed (auto)
   968   }  
   969   then show ?thesis
   970     by (cases s') fastsimp 
   971 qed
   972 
   973 lemma eval_no_abrupt_lemma: 
   974    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   975 by (erule eval_cases, auto)
   976 
   977 lemma eval_no_abrupt: 
   978   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   979         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   980 apply auto
   981 apply (frule eval_no_abrupt_lemma, auto)+
   982 done
   983 
   984 ML {*
   985 local
   986   fun is_None (Const ("Datatype.option.None",_)) = true
   987     | is_None _ = false
   988   fun pred (t as (_ $ (Const ("Pair",_) $
   989      (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
   990 in
   991   val eval_no_abrupt_proc = 
   992   make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
   993           (thm "eval_no_abrupt")
   994 end;
   995 Addsimprocs [eval_no_abrupt_proc]
   996 *}
   997 
   998 
   999 lemma eval_abrupt_lemma: 
  1000   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
  1001 by (erule eval_cases, auto)
  1002 
  1003 lemma eval_abrupt: 
  1004  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
  1005      (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
  1006      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
  1007 apply auto
  1008 apply (frule eval_abrupt_lemma, auto)+
  1009 done
  1010 
  1011 ML {*
  1012 local
  1013   fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
  1014     | is_Some _ = false
  1015   fun pred (_ $ (Const ("Pair",_) $
  1016      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
  1017        x))) $ _ ) = is_Some x
  1018 in
  1019   val eval_abrupt_proc = 
  1020   make_simproc "eval_abrupt" 
  1021                "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
  1022 end;
  1023 Addsimprocs [eval_abrupt_proc]
  1024 *}
  1025 
  1026 
  1027 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
  1028 apply (case_tac "s", case_tac "a = None")
  1029 by (auto intro!: eval.Lit)
  1030 
  1031 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
  1032 apply (case_tac "s", case_tac "a = None")
  1033 by (auto intro!: eval.Skip)
  1034 
  1035 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
  1036 apply (case_tac "s", case_tac "a = None")
  1037 by (auto intro!: eval.Expr)
  1038 
  1039 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"
  1040 apply (case_tac "s", case_tac "a = None")
  1041 by (auto intro!: eval.Comp)
  1042 
  1043 lemma CondI: 
  1044   "\<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> 
  1045          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
  1046 apply (case_tac "s", case_tac "a = None")
  1047 by (auto intro!: eval.Cond)
  1048 
  1049 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>
  1050                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
  1051 apply (case_tac "s", case_tac "a = None")
  1052 by (auto intro!: eval.If)
  1053 
  1054 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
  1055                 \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
  1056 apply (case_tac "s", case_tac "a = None")
  1057 by (auto intro!: eval.Methd)
  1058 
  1059 lemma eval_Call: 
  1060    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
  1061      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
  1062      s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
  1063      s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
  1064      G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
  1065        s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
  1066        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
  1067 apply (drule eval.Call, assumption)
  1068 apply (rule HOL.refl)
  1069 apply simp+
  1070 done
  1071 
  1072 lemma eval_Init: 
  1073 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
  1074   else G\<turnstile>Norm (init_class_obj G C s0)  
  1075          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
  1076        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
  1077       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
  1078   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
  1079 apply (rule eval.Init)
  1080 apply auto
  1081 done
  1082 
  1083 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
  1084 apply (case_tac "s", simp)
  1085 apply (case_tac "a")
  1086 apply  safe
  1087 apply (rule eval_Init)
  1088 apply   auto
  1089 done
  1090 
  1091 lemma eval_StatRef: 
  1092 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
  1093 apply (case_tac "s", simp)
  1094 apply (case_tac "a = None")
  1095 apply (auto del: eval.Abrupt intro!: eval.intros)
  1096 done
  1097 
  1098 
  1099 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
  1100 apply (erule eval_cases)
  1101 by auto
  1102 
  1103 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
  1104 by auto
  1105 
  1106 (*unused*)
  1107 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
  1108   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
  1109 apply (erule eval.induct)
  1110 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
  1111 apply auto
  1112 done
  1113 
  1114 lemma halloc_xcpt [dest!]: 
  1115   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
  1116 apply (erule_tac halloc_elim_cases)
  1117 by auto
  1118 
  1119 (*
  1120 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1121 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
  1122 *)
  1123 
  1124 lemma eval_Methd: 
  1125   "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
  1126    \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
  1127 apply (case_tac "s")
  1128 apply (case_tac "a")
  1129 apply clarsimp+
  1130 apply (erule eval.Methd)
  1131 apply (drule eval_abrupt_lemma)
  1132 apply force
  1133 done
  1134 
  1135 lemma eval_binop_arg2_indep:
  1136 "\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
  1137 by (cases binop)
  1138    (simp_all add: need_second_arg_def)
  1139 
  1140 
  1141 lemma eval_BinOp_arg2_indepI:
  1142   assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
  1143           no_need: "\<not> need_second_arg binop v1" 
  1144   shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
  1145          (is "?EvalBinOp v2")
  1146 proof -
  1147   from eval_e1 
  1148   have "?EvalBinOp Unit" 
  1149     by (rule eval.BinOp)
  1150        (simp add: no_need)
  1151   moreover
  1152   from no_need 
  1153   have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
  1154     by (simp add: eval_binop_arg2_indep)
  1155   ultimately
  1156   show ?thesis
  1157     by simp
  1158 qed
  1159 
  1160 
  1161 section "single valued"
  1162 
  1163 lemma unique_halloc [rule_format (no_asm)]: 
  1164   "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
  1165 apply (simp (no_asm_simp) only: split_tupled_all)
  1166 apply (erule halloc.induct)
  1167 apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
  1168 apply (drule trans [THEN sym], erule sym) 
  1169 defer
  1170 apply (drule trans [THEN sym], erule sym)
  1171 apply auto
  1172 done
  1173 
  1174 
  1175 lemma single_valued_halloc: 
  1176   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
  1177 apply (unfold single_valued_def)
  1178 by (clarsimp, drule (1) unique_halloc, auto)
  1179 
  1180 
  1181 lemma unique_sxalloc [rule_format (no_asm)]: 
  1182   "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
  1183 apply (simp (no_asm_simp) only: split_tupled_all)
  1184 apply (erule sxalloc.induct)
  1185 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
  1186               split del: split_if split_if_asm)
  1187 done
  1188 
  1189 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
  1190 apply (unfold single_valued_def)
  1191 apply (blast dest: unique_sxalloc)
  1192 done
  1193 
  1194 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
  1195 by auto
  1196 
  1197 lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
  1198                    res=the (locals (store s2) Result);
  1199                    s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
  1200  G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
  1201 by (auto elim: eval.Body)
  1202 
  1203 lemma unique_eval [rule_format (no_asm)]: 
  1204   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
  1205 apply (case_tac "ws")
  1206 apply (simp only:)
  1207 apply (erule thin_rl)
  1208 apply (erule eval_induct)
  1209 apply (tactic {* ALLGOALS (EVERY'
  1210       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
  1211 (* 31 subgoals *)
  1212 prefer 28 (* Try *) 
  1213 apply (simp (no_asm_use) only: split add: split_if_asm)
  1214 (* 34 subgoals *)
  1215 prefer 30 (* Init *)
  1216 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
  1217 prefer 26 (* While *)
  1218 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
  1219 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
  1220 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
  1221 apply blast
  1222 (* 33 subgoals *)
  1223 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
  1224 done
  1225 
  1226 (* unused *)
  1227 lemma single_valued_eval: 
  1228  "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
  1229 apply (unfold single_valued_def)
  1230 by (clarify, drule (1) unique_eval, auto)
  1231 
  1232 end