src/HOL/Bali/Eval.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12919 d6a0d168291e
child 13337 f75dfc606ac7
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
     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
   451   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
   452   halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
   453   sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
   454 
   455 
   456 syntax
   457 eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
   458 exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
   459 evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
   460 eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
   461 evals::"[prog,state,expr list ,
   462 		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
   463 hallo::"[prog,state,obj_tag,
   464 	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
   465 sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
   466 
   467 syntax (xsymbols)
   468 eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
   469 exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   470 evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   471 eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   472 evals::"[prog,state,expr list ,
   473 		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   474 hallo::"[prog,state,obj_tag,
   475 	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   476 sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
   477 
   478 translations
   479   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
   480   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
   481   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
   482   "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
   483   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
   484   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
   485   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
   486   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
   487   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
   488   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
   489   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
   490   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
   491   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
   492   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
   493   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
   494 
   495 inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
   496 
   497   Abrupt: 
   498   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
   499 
   500   New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
   501 	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   502 		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   503             \<Longrightarrow>
   504 	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   505 
   506 inductive "sxalloc G" intros (* allocating exception objects for
   507 	 	 	      standard exceptions (other than OutOfMemory) *)
   508 
   509   Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   510 
   511   XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   512 
   513   SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   514 	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   515 
   516 
   517 inductive "eval G" intros
   518 
   519 (* propagation of abrupt completion *)
   520 
   521   (* cf. 14.1, 15.5 *)
   522   Abrupt: 
   523    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
   524 
   525 
   526 (* execution of statements *)
   527 
   528   (* cf. 14.5 *)
   529   Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   530 
   531   (* cf. 14.7 *)
   532   Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   533 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   534 
   535   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   536                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
   537   (* cf. 14.2 *)
   538   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   539 	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   540 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   541 
   542 
   543   (* cf. 14.8.2 *)
   544   If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   545 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   546 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   547 
   548   (* cf. 14.10, 14.10.1 *)
   549   (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
   550   (* A "continue jump" from the while body c is handled by 
   551      this rule. If a continue jump with the proper label was invoked inside c
   552      this label (Cont l) is deleted out of the abrupt component of the state 
   553      before the iterative evaluation of the while statement.
   554      A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
   555   *)
   556   Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   557 	  if normal s1 \<and> the_Bool b 
   558              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   559                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   560 	     else s3 = s1\<rbrakk> \<Longrightarrow>
   561 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   562 
   563   Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
   564    
   565   (* cf. 14.16 *)
   566   Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   567 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   568 
   569   (* cf. 14.18.1 *)
   570   Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   571 	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   572 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   573 
   574   (* cf. 14.18.2 *)
   575   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   576 	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   577                G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   578 
   579   (* cf. 12.4.2, 8.5 *)
   580   Init:	"\<lbrakk>the (class G C) = c;
   581 	  if inited C (globs s0) then s3 = Norm s0
   582 	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   583 		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   584 	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   585               \<Longrightarrow>
   586 		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   587    (* This class initialisation rule is a little bit inaccurate. Look at the
   588       exact sequence:
   589       1. The current class object (the static fields) are initialised
   590          (init_class_obj)
   591       2. Then the superclasses are initialised
   592       3. The static initialiser of the current class is invoked
   593       More precisely we should expect another ordering, namely 2 1 3.
   594       But we can't just naively toggle 1 and 2. By calling init_class_obj 
   595       before initialising the superclasses we also implicitly record that
   596       we have started to initialise the current class (by setting an 
   597       value for the class object). This becomes 
   598       crucial for the completeness proof of the axiomatic semantics 
   599       (AxCompl.thy). Static initialisation requires an induction on the number 
   600       of classes not yet initialised (or to be more precise, classes where the
   601       initialisation has not yet begun). 
   602       So we could first assign a dummy value to the class before
   603       superclass initialisation and afterwards set the correct values.
   604       But as long as we don't take memory overflow into account 
   605       when allocating class objects, and don't model definite assignment in
   606       the static initialisers, we can leave things as they are for convenience. 
   607    *)
   608 (* evaluation of expressions *)
   609 
   610   (* cf. 15.8.1, 12.4.1 *)
   611   NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   612 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   613 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   614 
   615   (* cf. 15.9.1, 12.4.1 *)
   616   NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   617 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   618 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   619 
   620   (* cf. 15.15 *)
   621   Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   622 	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   623 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   624 
   625   (* cf. 15.19.2 *)
   626   Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   627 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   628 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   629 
   630   (* cf. 15.7.1 *)
   631   Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   632 
   633 
   634 
   635   (* cf. 15.10.2 *)
   636   Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   637 
   638   (* cf. 15.2 *)
   639   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   640 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   641 
   642   (* cf. 15.25.1 *)
   643   Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   644           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   645 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   646 
   647   (* cf. 15.24 *)
   648   Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   649           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   650 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   651 
   652 
   653   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
   654   Call:	
   655   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   656     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   657     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   658     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   659     G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
   660    \<Longrightarrow>
   661        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
   662 (* The accessibility check is after init_lvars, to keep it simple. Init_lvars 
   663    already tests for the absence of a null-pointer reference in case of an
   664    instance method invocation
   665 *)
   666 
   667   Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   668 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   669 
   670   (* cf. 14.15, 12.4.1 *)
   671   Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   672  G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   673 
   674 (* evaluation of variables *)
   675 
   676   (* cf. 15.13.1, 15.7.2 *)
   677   LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   678 
   679   (* cf. 15.10.1, 12.4.1 *)
   680   FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   681 	  (v,s2') = fvar statDeclC stat fn a s2;
   682           s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
   683 	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
   684  (* The accessibility check is after fvar, to keep it simple. Fvar already
   685     tests for the absence of a null-pointer reference in case of an instance
   686     field
   687   *)
   688 
   689   (* cf. 15.12.1, 15.25.1 *)
   690   AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   691 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   692 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   693 
   694 
   695 (* evaluation of expression lists *)
   696 
   697   (* cf. 15.11.4.2 *)
   698   Nil:
   699 				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   700 
   701   (* cf. 15.6.4 *)
   702   Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   703           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   704 				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   705 
   706 (* Rearrangement of premisses:
   707 [0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
   708  17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
   709  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
   710  27(AVar),22(Call)]
   711 *)
   712 ML {*
   713 bind_thm ("eval_induct_", rearrange_prems 
   714 [0,1,2,8,4,28,29,25,15,16,
   715  17,18,19,3,5,23,24,21,6,
   716  7,11,9,13,14,12,20,10,26,
   717  27,22] (thm "eval.induct"))
   718 *}
   719 
   720 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
   721    and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
   722    s2 (* Fin *) and and s2 (* NewC *)] 
   723 
   724 declare split_if     [split del] split_if_asm     [split del] 
   725         option.split [split del] option.split_asm [split del]
   726 inductive_cases halloc_elim_cases: 
   727   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   728   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   729 
   730 inductive_cases sxalloc_elim_cases:
   731  	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   732  	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   733  	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   734 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   735 
   736 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   737        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   738        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   739       \<rbrakk> \<Longrightarrow> P"
   740 apply cut_tac 
   741 apply (erule sxalloc_cases)
   742 apply blast+
   743 done
   744 
   745 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   746 declare split_paired_All [simp del] split_paired_Ex [simp del]
   747 ML_setup {*
   748 simpset_ref() := simpset() delloop "split_all_tac"
   749 *}
   750 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
   751 
   752 inductive_cases eval_elim_cases:
   753         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"
   754 	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"
   755         "G\<turnstile>Norm s \<midarrow>In1r (Do j)                         \<succ>\<rightarrow> xs'"
   756         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"
   757 	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
   758 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
   759 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
   760 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
   761 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
   762 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
   763 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"
   764 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"
   765 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"
   766 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"
   767 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"
   768 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"
   769 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"
   770 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"
   771 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"
   772 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"
   773 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"
   774 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"
   775 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"
   776 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"
   777 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"
   778 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"
   779 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"
   780 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   781 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"
   782 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   783 declare split_paired_All [simp] split_paired_Ex [simp]
   784 ML_setup {*
   785 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   786 *}
   787 declare split_if     [split] split_if_asm     [split] 
   788         option.split [split] option.split_asm [split]
   789 
   790 lemma eval_Inj_elim: 
   791  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   792  \<Longrightarrow> case t of 
   793        In1 ec \<Rightarrow> (case ec of 
   794                     Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   795                   | Inr c \<Rightarrow> w = \<diamondsuit>)  
   796      | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   797      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   798 apply (erule eval_cases)
   799 apply auto
   800 apply (induct_tac "t")
   801 apply (induct_tac "a")
   802 apply auto
   803 done
   804 
   805 ML_setup {*
   806 fun eval_fun nam inj rhs =
   807 let
   808   val name = "eval_" ^ nam ^ "_eq"
   809   val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
   810   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   811 	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
   812   fun is_Inj (Const (inj,_) $ _) = true
   813     | is_Inj _                   = false
   814   fun pred (_ $ (Const ("Pair",_) $ _ $ 
   815       (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
   816 in
   817   make_simproc name lhs pred (thm name)
   818 end
   819 
   820 val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
   821 val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
   822 val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
   823 val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
   824 Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
   825 bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
   826 *}
   827 
   828 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
   829 
   830 
   831 lemma eval_no_abrupt_lemma: 
   832    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   833 by (erule eval_cases, auto)
   834 
   835 lemma eval_no_abrupt: 
   836   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   837         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   838 apply auto
   839 apply (frule eval_no_abrupt_lemma, auto)+
   840 done
   841 
   842 ML {*
   843 local
   844   fun is_None (Const ("Datatype.option.None",_)) = true
   845     | is_None _ = false
   846   fun pred (t as (_ $ (Const ("Pair",_) $
   847      (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
   848 in
   849   val eval_no_abrupt_proc = 
   850   make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
   851           (thm "eval_no_abrupt")
   852 end;
   853 Addsimprocs [eval_no_abrupt_proc]
   854 *}
   855 
   856 
   857 lemma eval_abrupt_lemma: 
   858   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
   859 by (erule eval_cases, auto)
   860 
   861 lemma eval_abrupt: 
   862  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
   863      (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
   864      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
   865 apply auto
   866 apply (frule eval_abrupt_lemma, auto)+
   867 done
   868 
   869 ML {*
   870 local
   871   fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
   872     | is_Some _ = false
   873   fun pred (_ $ (Const ("Pair",_) $
   874      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   875        x))) $ _ ) = is_Some x
   876 in
   877   val eval_abrupt_proc = 
   878   make_simproc "eval_abrupt" 
   879                "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
   880 end;
   881 Addsimprocs [eval_abrupt_proc]
   882 *}
   883 
   884 
   885 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
   886 apply (case_tac "s", case_tac "a = None")
   887 by (auto intro!: eval.Lit)
   888 
   889 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
   890 apply (case_tac "s", case_tac "a = None")
   891 by (auto intro!: eval.Skip)
   892 
   893 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
   894 apply (case_tac "s", case_tac "a = None")
   895 by (auto intro!: eval.Expr)
   896 
   897 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"
   898 apply (case_tac "s", case_tac "a = None")
   899 by (auto intro!: eval.Comp)
   900 
   901 lemma CondI: 
   902   "\<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> 
   903          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
   904 apply (case_tac "s", case_tac "a = None")
   905 by (auto intro!: eval.Cond)
   906 
   907 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>
   908                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
   909 apply (case_tac "s", case_tac "a = None")
   910 by (auto intro!: eval.If)
   911 
   912 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
   913 apply (case_tac "s", case_tac "a = None")
   914 by (auto intro!: eval.Methd)
   915 
   916 lemma eval_Call: 
   917    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
   918      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   919      s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
   920      s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   921      G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
   922        s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
   923        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
   924 apply (drule eval.Call, assumption)
   925 apply (rule HOL.refl)
   926 apply simp+
   927 done
   928 
   929 lemma eval_Init: 
   930 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
   931   else G\<turnstile>Norm (init_class_obj G C s0)  
   932          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
   933        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
   934       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
   935   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   936 apply (rule eval.Init)
   937 apply auto
   938 done
   939 
   940 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
   941 apply (case_tac "s", simp)
   942 apply (case_tac "a")
   943 apply  safe
   944 apply (rule eval_Init)
   945 apply   auto
   946 done
   947 
   948 lemma eval_StatRef: 
   949 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
   950 apply (case_tac "s", simp)
   951 apply (case_tac "a = None")
   952 apply (auto del: eval.Abrupt intro!: eval.intros)
   953 done
   954 
   955 
   956 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
   957 apply (erule eval_cases)
   958 by auto
   959 
   960 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
   961 by auto
   962 
   963 (*unused*)
   964 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
   965   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
   966 apply (erule eval.induct)
   967 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
   968 apply auto
   969 done
   970 
   971 lemma halloc_xcpt [dest!]: 
   972   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
   973 apply (erule_tac halloc_elim_cases)
   974 by auto
   975 
   976 (*
   977 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   978 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   979 *)
   980 
   981 lemma eval_Methd: 
   982   "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
   983 apply (case_tac "s")
   984 apply (case_tac "a")
   985 apply clarsimp+
   986 apply (erule eval.Methd)
   987 apply (drule eval_abrupt_lemma)
   988 apply force
   989 done
   990 
   991 
   992 section "single valued"
   993 
   994 lemma unique_halloc [rule_format (no_asm)]: 
   995   "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
   996 apply (simp (no_asm_simp) only: split_tupled_all)
   997 apply (erule halloc.induct)
   998 apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
   999 apply (drule trans [THEN sym], erule sym) 
  1000 defer
  1001 apply (drule trans [THEN sym], erule sym)
  1002 apply auto
  1003 done
  1004 
  1005 
  1006 lemma single_valued_halloc: 
  1007   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
  1008 apply (unfold single_valued_def)
  1009 by (clarsimp, drule (1) unique_halloc, auto)
  1010 
  1011 
  1012 lemma unique_sxalloc [rule_format (no_asm)]: 
  1013   "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
  1014 apply (simp (no_asm_simp) only: split_tupled_all)
  1015 apply (erule sxalloc.induct)
  1016 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
  1017               split del: split_if split_if_asm)
  1018 done
  1019 
  1020 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
  1021 apply (unfold single_valued_def)
  1022 apply (blast dest: unique_sxalloc)
  1023 done
  1024 
  1025 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
  1026 by auto
  1027 
  1028 lemma unique_eval [rule_format (no_asm)]: 
  1029   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
  1030 apply (case_tac "ws")
  1031 apply (simp only:)
  1032 apply (erule thin_rl)
  1033 apply (erule eval_induct)
  1034 apply (tactic {* ALLGOALS (EVERY'
  1035       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
  1036 (* 29 subgoals *)
  1037 prefer 26 (* Try *) 
  1038 apply (simp (no_asm_use) only: split add: split_if_asm)
  1039 (* 32 subgoals *)
  1040 prefer 28 (* Init *)
  1041 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
  1042 prefer 24 (* While *)
  1043 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
  1044 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
  1045 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
  1046 apply blast
  1047 (* 31 subgoals *)
  1048 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
  1049 done
  1050 
  1051 (* unused *)
  1052 lemma single_valued_eval: 
  1053  "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
  1054 apply (unfold single_valued_def)
  1055 by (clarify, drule (1) unique_eval, auto)
  1056 
  1057 end