src/HOL/Bali/Eval.thy
author wenzelm
Mon Jan 28 18:50:23 2002 +0100 (2002-01-28)
changeset 12857 a4386cc9b1c3
parent 12854 00d4a435777f
child 12858 6214f03d6d27
permissions -rw-r--r--
tuned header;
     1 (*  Title:      HOL/Bali/Eval.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     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   avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
   375  "avar G i' a' s 
   376     \<equiv> let   oref = Heap (the_Addr a'); 
   377                i = the_Intg i'; 
   378                n = Inr i;
   379         (T,k,cs) = the_Arr (globs (store s) oref); 
   380                f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
   381                                            ArrStore x
   382                               ,upd_gobj oref n v s)) 
   383       in ((the (cs n),f)
   384          ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
   385 
   386 lemma fvar_def2: "fvar C stat fn a' s =  
   387   ((the 
   388      (values 
   389       (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
   390       (Inl (fn,C)))
   391    ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
   392                         (Inl (fn,C)) 
   393                         v)))
   394   ,abupd (if stat then id else np a') s)
   395   "
   396 apply (unfold fvar_def)
   397 apply (simp (no_asm) add: Let_def split_beta)
   398 done
   399 
   400 lemma avar_def2: "avar G i' a' s =  
   401   ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
   402            (Inr (the_Intg i')))
   403    ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
   404                                                    (Heap (the_Addr a')))))) 
   405                             ArrStore x
   406                  ,upd_gobj  (Heap (the_Addr a')) 
   407                                (Inr (the_Intg i')) v s')))
   408   ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
   409                    (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
   410           s)"
   411 apply (unfold avar_def)
   412 apply (simp (no_asm) add: Let_def split_beta)
   413 done
   414 
   415 
   416 section "evaluation judgments"
   417 
   418 consts
   419   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
   420   halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
   421   sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
   422 
   423 
   424 syntax
   425 eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
   426 exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
   427 evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
   428 eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
   429 evals::"[prog,state,expr list ,
   430 		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
   431 hallo::"[prog,state,obj_tag,
   432 	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
   433 sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
   434 
   435 syntax (xsymbols)
   436 eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
   437 exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   438 evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   439 eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   440 evals::"[prog,state,expr list ,
   441 		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   442 hallo::"[prog,state,obj_tag,
   443 	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   444 sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
   445 
   446 translations
   447   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
   448   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
   449   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
   450   "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
   451   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
   452   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
   453   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
   454   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
   455   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
   456   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
   457   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
   458   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
   459   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
   460   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
   461   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
   462 
   463 inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
   464 
   465   Abrupt: 
   466   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
   467 
   468   New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
   469 	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   470 		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   471             \<Longrightarrow>
   472 	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   473 
   474 inductive "sxalloc G" intros (* allocating exception objects for
   475 	 	 	      standard exceptions (other than OutOfMemory) *)
   476 
   477   Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   478 
   479   XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   480 
   481   SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   482 	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   483 
   484 
   485 inductive "eval G" intros
   486 
   487 (* propagation of abrupt completion *)
   488 
   489   (* cf. 14.1, 15.5 *)
   490   Abrupt: 
   491    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
   492 
   493 
   494 (* execution of statements *)
   495 
   496   (* cf. 14.5 *)
   497   Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   498 
   499   (* cf. 14.7 *)
   500   Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   501 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   502 
   503   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   504                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
   505   (* cf. 14.2 *)
   506   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   507 	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   508 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   509 
   510 
   511   (* cf. 14.8.2 *)
   512   If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   513 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   514 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   515 
   516   (* cf. 14.10, 14.10.1 *)
   517   (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
   518   (* A "continue jump" from the while body c is handled by 
   519      this rule. If a continue jump with the proper label was invoked inside c
   520      this label (Cont l) is deleted out of the abrupt component of the state 
   521      before the iterative evaluation of the while statement.
   522      A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
   523   *)
   524   Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   525 	  if normal s1 \<and> the_Bool b 
   526              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   527                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   528 	     else s3 = s1\<rbrakk> \<Longrightarrow>
   529 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   530 
   531   Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
   532    
   533   (* cf. 14.16 *)
   534   Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   535 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   536 
   537   (* cf. 14.18.1 *)
   538   Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   539 	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   540 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   541 
   542   (* cf. 14.18.2 *)
   543   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   544 	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   545                G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   546 
   547   (* cf. 12.4.2, 8.5 *)
   548   Init:	"\<lbrakk>the (class G C) = c;
   549 	  if inited C (globs s0) then s3 = Norm s0
   550 	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   551 		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   552 	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   553               \<Longrightarrow>
   554 		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   555 
   556 (* evaluation of expressions *)
   557 
   558   (* cf. 15.8.1, 12.4.1 *)
   559   NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   560 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   561 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   562 
   563   (* cf. 15.9.1, 12.4.1 *)
   564   NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   565 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   566 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   567 
   568   (* cf. 15.15 *)
   569   Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   570 	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   571 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   572 
   573   (* cf. 15.19.2 *)
   574   Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   575 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   576 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   577 
   578   (* cf. 15.7.1 *)
   579   Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   580 
   581 
   582 
   583   (* cf. 15.10.2 *)
   584   Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   585 
   586   (* cf. 15.2 *)
   587   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   588 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   589 
   590   (* cf. 15.25.1 *)
   591   Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   592           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   593 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   594 
   595   (* cf. 15.24 *)
   596   Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   597           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   598 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   599 
   600 
   601   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
   602   Call:	
   603   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   604     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   605     G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2 
   606          \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s3\<rbrakk>
   607    \<Longrightarrow>
   608        G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s3)"
   609 
   610   Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   611 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   612 
   613   (* cf. 14.15, 12.4.1 *)
   614   Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   615  G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   616 
   617 (* evaluation of variables *)
   618 
   619   (* cf. 15.13.1, 15.7.2 *)
   620   LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   621 
   622   (* cf. 15.10.1, 12.4.1 *)
   623   FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   624 	  (v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>
   625 	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"
   626 
   627   (* cf. 15.12.1, 15.25.1 *)
   628   AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   629 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   630 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   631 
   632 
   633 (* evaluation of expression lists *)
   634 
   635   (* cf. 15.11.4.2 *)
   636   Nil:
   637 				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   638 
   639   (* cf. 15.6.4 *)
   640   Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   641           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   642 				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   643 
   644 (* Rearrangement of premisses:
   645 [0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
   646  17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
   647  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
   648  27(AVar),22(Call)]
   649 *)
   650 ML {*
   651 bind_thm ("eval_induct_", rearrange_prems 
   652 [0,1,2,8,4,28,29,25,15,16,
   653  17,18,19,3,5,23,24,21,6,
   654  7,11,9,13,14,12,20,10,26,
   655  27,22] (thm "eval.induct"))
   656 *}
   657 
   658 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
   659    and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
   660    s2 (* Fin *) and and s2 (* NewC *)] 
   661 
   662 declare split_if     [split del] split_if_asm     [split del] 
   663         option.split [split del] option.split_asm [split del]
   664 inductive_cases halloc_elim_cases: 
   665   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   666   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   667 
   668 inductive_cases sxalloc_elim_cases:
   669  	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   670  	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   671  	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   672 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   673 
   674 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   675        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   676        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   677       \<rbrakk> \<Longrightarrow> P"
   678 apply cut_tac 
   679 apply (erule sxalloc_cases)
   680 apply blast+
   681 done
   682 
   683 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   684 declare split_paired_All [simp del] split_paired_Ex [simp del]
   685 ML_setup {*
   686 simpset_ref() := simpset() delloop "split_all_tac"
   687 *}
   688 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
   689 
   690 inductive_cases eval_elim_cases:
   691         "G\<turnstile>(Some xc,s) \<midarrow>t                         \<succ>\<rightarrow> vs'"
   692 	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<rightarrow> xs'"
   693         "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<rightarrow> xs'"
   694         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<rightarrow> xs'"
   695 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<rightarrow> vs'"
   696 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<rightarrow> vs'"
   697 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<rightarrow> vs'"
   698 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<rightarrow> vs'"
   699 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<rightarrow> vs'"
   700 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<rightarrow> vs'"
   701 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<rightarrow> vs'"
   702 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<rightarrow> vs'"
   703 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<rightarrow> xs'"
   704 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<rightarrow> xs'"
   705 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<rightarrow> xs'"
   706 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<rightarrow> xs'"
   707 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<rightarrow> vs'"
   708 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<rightarrow> xs'"
   709 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<rightarrow> xs'"
   710 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<rightarrow> xs'"
   711 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<rightarrow> xs'"
   712 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<rightarrow> vs'"
   713 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<rightarrow> vs'"
   714 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<rightarrow> vs'"
   715 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<rightarrow> xs'"
   716 	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<rightarrow> vs'"
   717 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<rightarrow> vs'"
   718 	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   719 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<rightarrow> xs'"
   720 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   721 declare split_paired_All [simp] split_paired_Ex [simp]
   722 ML_setup {*
   723 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   724 *}
   725 declare split_if     [split] split_if_asm     [split] 
   726         option.split [split] option.split_asm [split]
   727 
   728 lemma eval_Inj_elim: 
   729  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   730  \<Longrightarrow> case t of 
   731        In1 ec \<Rightarrow> (case ec of 
   732                     Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   733                   | Inr c \<Rightarrow> w = \<diamondsuit>)  
   734      | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   735      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   736 apply (erule eval_cases)
   737 apply auto
   738 apply (induct_tac "t")
   739 apply (induct_tac "a")
   740 apply auto
   741 done
   742 
   743 ML_setup {*
   744 fun eval_fun nam inj rhs =
   745 let
   746   val name = "eval_" ^ nam ^ "_eq"
   747   val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
   748   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   749 	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
   750   fun is_Inj (Const (inj,_) $ _) = true
   751     | is_Inj _                   = false
   752   fun pred (_ $ (Const ("Pair",_) $ _ $ 
   753       (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
   754 in
   755   make_simproc name lhs pred (thm name)
   756 end
   757 
   758 val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
   759 val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
   760 val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
   761 val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
   762 Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
   763 bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
   764 *}
   765 
   766 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
   767 
   768 
   769 lemma eval_no_abrupt_lemma: 
   770    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   771 by (erule eval_cases, auto)
   772 
   773 lemma eval_no_abrupt: 
   774   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   775         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   776 apply auto
   777 apply (frule eval_no_abrupt_lemma, auto)+
   778 done
   779 
   780 ML {*
   781 local
   782   fun is_None (Const ("Option.option.None",_)) = true
   783     | is_None _ = false
   784   fun pred (t as (_ $ (Const ("Pair",_) $
   785      (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
   786 in
   787   val eval_no_abrupt_proc = 
   788   make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
   789           (thm "eval_no_abrupt")
   790 end;
   791 Addsimprocs [eval_no_abrupt_proc]
   792 *}
   793 
   794 
   795 lemma eval_abrupt_lemma: 
   796   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
   797 by (erule eval_cases, auto)
   798 
   799 lemma eval_abrupt: 
   800  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
   801      (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
   802      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
   803 apply auto
   804 apply (frule eval_abrupt_lemma, auto)+
   805 done
   806 
   807 ML {*
   808 local
   809   fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
   810     | is_Some _ = false
   811   fun pred (_ $ (Const ("Pair",_) $
   812      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   813        x))) $ _ ) = is_Some x
   814 in
   815   val eval_abrupt_proc = 
   816   make_simproc "eval_abrupt" 
   817                "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
   818 end;
   819 Addsimprocs [eval_abrupt_proc]
   820 *}
   821 
   822 
   823 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
   824 apply (case_tac "s", case_tac "a = None")
   825 by (auto intro!: eval.Lit)
   826 
   827 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
   828 apply (case_tac "s", case_tac "a = None")
   829 by (auto intro!: eval.Skip)
   830 
   831 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
   832 apply (case_tac "s", case_tac "a = None")
   833 by (auto intro!: eval.Expr)
   834 
   835 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"
   836 apply (case_tac "s", case_tac "a = None")
   837 by (auto intro!: eval.Comp)
   838 
   839 lemma CondI: 
   840   "\<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> 
   841          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
   842 apply (case_tac "s", case_tac "a = None")
   843 by (auto intro!: eval.Cond)
   844 
   845 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>
   846                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
   847 apply (case_tac "s", case_tac "a = None")
   848 by (auto intro!: eval.If)
   849 
   850 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'"
   851 apply (case_tac "s", case_tac "a = None")
   852 by (auto intro!: eval.Methd)
   853 
   854 lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
   855        D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   856        G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2 
   857         \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s3; 
   858        s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>  
   859        G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s3'"
   860 apply (drule eval.Call, assumption)
   861 apply (rule HOL.refl)
   862 apply simp+
   863 done
   864 
   865 lemma eval_Init: 
   866 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
   867   else G\<turnstile>Norm (init_class_obj G C s0)  
   868          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
   869        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
   870       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
   871   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   872 apply (rule eval.Init)
   873 apply auto
   874 done
   875 
   876 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
   877 apply (case_tac "s", simp)
   878 apply (case_tac "a")
   879 apply  safe
   880 apply (rule eval_Init)
   881 apply   auto
   882 done
   883 
   884 lemma eval_StatRef: 
   885 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
   886 apply (case_tac "s", simp)
   887 apply (case_tac "a = None")
   888 apply (auto del: eval.Abrupt intro!: eval.intros)
   889 done
   890 
   891 
   892 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
   893 apply (erule eval_cases)
   894 by auto
   895 
   896 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
   897 by auto
   898 
   899 (*unused*)
   900 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
   901   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
   902 apply (erule eval.induct)
   903 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
   904 apply auto
   905 done
   906 
   907 lemma halloc_xcpt [dest!]: 
   908   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
   909 apply (erule_tac halloc_elim_cases)
   910 by auto
   911 
   912 (*
   913 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   914 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   915 *)
   916 
   917 lemma eval_Methd: 
   918   "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')"
   919 apply (case_tac "s")
   920 apply (case_tac "a")
   921 apply clarsimp+
   922 apply (erule eval.Methd)
   923 apply (drule eval_abrupt_lemma)
   924 apply force
   925 done
   926 
   927 
   928 section "single valued"
   929 
   930 lemma unique_halloc [rule_format (no_asm)]: 
   931   "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
   932 apply (simp (no_asm_simp) only: split_tupled_all)
   933 apply (erule halloc.induct)
   934 apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
   935 apply (drule trans [THEN sym], erule sym) 
   936 defer
   937 apply (drule trans [THEN sym], erule sym)
   938 apply auto
   939 done
   940 
   941 
   942 lemma single_valued_halloc: 
   943   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
   944 apply (unfold single_valued_def)
   945 by (clarsimp, drule (1) unique_halloc, auto)
   946 
   947 
   948 lemma unique_sxalloc [rule_format (no_asm)]: 
   949   "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
   950 apply (simp (no_asm_simp) only: split_tupled_all)
   951 apply (erule sxalloc.induct)
   952 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
   953               split del: split_if split_if_asm)
   954 done
   955 
   956 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
   957 apply (unfold single_valued_def)
   958 apply (blast dest: unique_sxalloc)
   959 done
   960 
   961 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
   962 by auto
   963 
   964 lemma unique_eval [rule_format (no_asm)]: 
   965   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
   966 apply (case_tac "ws")
   967 apply (simp only:)
   968 apply (erule thin_rl)
   969 apply (erule eval_induct)
   970 apply (tactic {* ALLGOALS (EVERY'
   971       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
   972 (* 29 subgoals *)
   973 prefer 26 (* Try *) 
   974 apply (simp (no_asm_use) only: split add: split_if_asm)
   975 (* 32 subgoals *)
   976 prefer 28 (* Init *)
   977 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
   978 prefer 24 (* While *)
   979 apply (simp (no_asm_use) only: split add: split_if_asm, blast)
   980 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   981 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   982 apply blast
   983 (* 31 subgoals *)
   984 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
   985 done
   986 
   987 (* unused *)
   988 lemma single_valued_eval: 
   989  "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
   990 apply (unfold single_valued_def)
   991 by (clarify, drule (1) unique_eval, auto)
   992 
   993 end