src/HOL/Bali/Eval.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Eval.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,993 @@
     1.4 +(*  Title:      isabelle/Bali/Eval.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* Operational evaluation (big-step) semantics of Java expressions and 
    1.10 +          statements
    1.11 +*}
    1.12 +
    1.13 +theory Eval = State + DeclConcepts:
    1.14 +
    1.15 +text {*
    1.16 +
    1.17 +improvements over Java Specification 1.0:
    1.18 +\begin{itemize}
    1.19 +\item dynamic method lookup does not need to consider the return type 
    1.20 +      (cf.15.11.4.4)
    1.21 +\item throw raises a NullPointer exception if a null reference is given, and 
    1.22 +      each throw of a standard exception yield a fresh exception object 
    1.23 +      (was not specified)
    1.24 +\item if there is not enough memory even to allocate an OutOfMemory exception,
    1.25 +  evaluation/execution fails, i.e. simply stops (was not specified)
    1.26 +\item array assignment checks lhs (and may throw exceptions) before evaluating 
    1.27 +      rhs
    1.28 +\item fixed exact positions of class initializations 
    1.29 +      (immediate at first active use)
    1.30 +\end{itemize}
    1.31 +
    1.32 +design issues:
    1.33 +\begin{itemize}
    1.34 +\item evaluation vs. (single-step) transition semantics
    1.35 +  evaluation semantics chosen, because:
    1.36 +  \begin{itemize} 
    1.37 +  \item[++] less verbose and therefore easier to read (and to handle in proofs)
    1.38 +  \item[+]  more abstract
    1.39 +  \item[+]  intermediate values (appearing in recursive rules) need not be 
    1.40 +     stored explicitly, e.g. no call body construct or stack of invocation 
    1.41 +     frames containing local variables and return addresses for method calls 
    1.42 +     needed
    1.43 +  \item[+]  convenient rule induction for subject reduction theorem
    1.44 +  \item[-]  no interleaving (for parallelism) can be described
    1.45 +  \item[-]  stating a property of infinite executions requires the meta-level 
    1.46 +     argument that this property holds for any finite prefixes of it 
    1.47 +     (e.g. stopped using a counter that is decremented to zero and then 
    1.48 +     throwing an exception)
    1.49 +  \end{itemize}
    1.50 +\item unified evaluation for variables, expressions, expression lists, 
    1.51 +      statements
    1.52 +\item the value entry in statement rules is redundant 
    1.53 +\item the value entry in rules is irrelevant in case of exceptions, but its full
    1.54 +  inclusion helps to make the rule structure independent of exception occurence.
    1.55 +\item as irrelevant value entries are ignored, it does not matter if they are 
    1.56 +      unique.
    1.57 +  For simplicity, (fixed) arbitrary values are preferred over "free" values.
    1.58 +\item the rule format is such that the start state may contain an exception.
    1.59 +  \begin{itemize}
    1.60 +  \item[++] faciliates exception handling
    1.61 +  \item[+]  symmetry
    1.62 +  \end{itemize}
    1.63 +\item the rules are defined carefully in order to be applicable even in not
    1.64 +  type-correct situations (yielding undefined values),
    1.65 +  e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
    1.66 +  \begin{itemize}
    1.67 +  \item[++] fewer rules 
    1.68 +  \item[-]  less readable because of auxiliary functions like @{text the_Addr}
    1.69 +  \end{itemize}
    1.70 +  Alternative: "defensive" evaluation throwing some InternalError exception
    1.71 +               in case of (impossible, for correct programs) type mismatches
    1.72 +\item there is exactly one rule per syntactic construct
    1.73 +  \begin{itemize}
    1.74 +  \item[+] no redundancy in case distinctions
    1.75 +  \end{itemize}
    1.76 +\item halloc fails iff there is no free heap address. When there is
    1.77 +  only one free heap address left, it returns an OutOfMemory exception.
    1.78 +  In this way it is guaranteed that when an OutOfMemory exception is thrown for
    1.79 +  the first time, there is a free location on the heap to allocate it.
    1.80 +\item the allocation of objects that represent standard exceptions is deferred 
    1.81 +      until execution of any enclosing catch clause, which is transparent to 
    1.82 +      the program.
    1.83 +  \begin{itemize}
    1.84 +  \item[-]  requires an auxiliary execution relation
    1.85 +  \item[++] avoids copies of allocation code and awkward case distinctions 
    1.86 +           (whether there is enough memory to allocate the exception) in 
    1.87 +            evaluation rules
    1.88 +  \end{itemize}
    1.89 +\item unfortunately @{text new_Addr} is not directly executable because of 
    1.90 +      Hilbert operator.
    1.91 +\end{itemize}
    1.92 +simplifications:
    1.93 +\begin{itemize}
    1.94 +\item local variables are initialized with default values 
    1.95 +      (no definite assignment)
    1.96 +\item garbage collection not considered, therefore also no finalizers
    1.97 +\item stack overflow and memory overflow during class initialization not 
    1.98 +      modelled
    1.99 +\item exceptions in initializations not replaced by ExceptionInInitializerError
   1.100 +\end{itemize}
   1.101 +*}
   1.102 +
   1.103 +types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   1.104 +      vals  =        "(val, vvar, val list) sum3"
   1.105 +translations
   1.106 +     "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
   1.107 +     "vals" <= (type)"(val, vvar, val list) sum3"
   1.108 +
   1.109 +syntax (xsymbols)
   1.110 +  dummy_res :: "vals" ("\<diamondsuit>")
   1.111 +translations
   1.112 +  "\<diamondsuit>" == "In1 Unit"
   1.113 +
   1.114 +constdefs
   1.115 +  arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
   1.116 + "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
   1.117 +                     (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
   1.118 +
   1.119 +lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
   1.120 +by (simp add: arbitrary3_def)
   1.121 +
   1.122 +lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
   1.123 +by (simp add: arbitrary3_def)
   1.124 +
   1.125 +lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"
   1.126 +by (simp add: arbitrary3_def)
   1.127 +
   1.128 +lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"
   1.129 +by (simp add: arbitrary3_def)
   1.130 +
   1.131 +
   1.132 +section "exception throwing and catching"
   1.133 +
   1.134 +constdefs
   1.135 +  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
   1.136 + "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   1.137 +
   1.138 +lemma throw_def2: 
   1.139 + "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
   1.140 +apply (unfold throw_def)
   1.141 +apply (simp (no_asm))
   1.142 +done
   1.143 +
   1.144 +constdefs
   1.145 +  fits    :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
   1.146 + "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"
   1.147 +
   1.148 +lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
   1.149 +by (simp add: fits_def)
   1.150 +
   1.151 +
   1.152 +lemma fits_Addr_RefT [simp]:
   1.153 +  "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
   1.154 +by (simp add: fits_def)
   1.155 +
   1.156 +lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>  
   1.157 +  (\<exists>t. T = RefT t) \<and> a' = Null \<or>  
   1.158 +  (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and>  G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
   1.159 +apply (unfold fits_def)
   1.160 +apply (case_tac "\<exists>pt. T = PrimT pt")
   1.161 +apply  simp_all
   1.162 +apply (case_tac "T")
   1.163 +defer 
   1.164 +apply (case_tac "a' = Null")
   1.165 +apply  simp_all
   1.166 +done
   1.167 +
   1.168 +constdefs
   1.169 +  catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool"      ("_,_\<turnstile>catch _"[61,61,61]60)
   1.170 + "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
   1.171 +                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
   1.172 +
   1.173 +lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
   1.174 +apply (unfold catch_def)
   1.175 +apply (simp (no_asm))
   1.176 +done
   1.177 +
   1.178 +lemma catch_XcptLoc [simp]: 
   1.179 +  "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
   1.180 +apply (unfold catch_def)
   1.181 +apply (simp (no_asm))
   1.182 +done
   1.183 +
   1.184 +constdefs
   1.185 +  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state"
   1.186 + "new_xcpt_var vn \<equiv> 
   1.187 +     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
   1.188 +
   1.189 +lemma new_xcpt_var_def2 [simp]: 
   1.190 + "new_xcpt_var vn (x,s) = 
   1.191 +    Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
   1.192 +apply (unfold new_xcpt_var_def)
   1.193 +apply (simp (no_asm))
   1.194 +done
   1.195 +
   1.196 +
   1.197 +
   1.198 +section "misc"
   1.199 +
   1.200 +constdefs
   1.201 +
   1.202 +  assign     :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state"
   1.203 + "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
   1.204 +		   in  (x',if x' = None then s' else s)"
   1.205 +
   1.206 +(*
   1.207 +lemma assign_Norm_Norm [simp]: 
   1.208 +"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 
   1.209 + \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
   1.210 +by (simp add: assign_def Let_def)
   1.211 +*)
   1.212 +
   1.213 +lemma assign_Norm_Norm [simp]: 
   1.214 +"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
   1.215 +by (simp add: assign_def Let_def)
   1.216 +
   1.217 +(*
   1.218 +lemma assign_Norm_Some [simp]: 
   1.219 +  "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 
   1.220 +   \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
   1.221 +by (simp add: assign_def Let_def split_beta)
   1.222 +*)
   1.223 +
   1.224 +lemma assign_Norm_Some [simp]: 
   1.225 +  "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 
   1.226 +   \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
   1.227 +by (simp add: assign_def Let_def split_beta)
   1.228 +
   1.229 +
   1.230 +lemma assign_Some [simp]: 
   1.231 +"assign f v (Some x,s) = (Some x,s)" 
   1.232 +by (simp add: assign_def Let_def split_beta)
   1.233 +
   1.234 +lemma assign_supd [simp]: 
   1.235 +"assign (\<lambda>v. supd (f v)) v (x,s)  
   1.236 +  = (x, if x = None then f v s else s)"
   1.237 +apply auto
   1.238 +done
   1.239 +
   1.240 +lemma assign_raise_if [simp]: 
   1.241 +  "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =  
   1.242 +  (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
   1.243 +apply (case_tac "x = None")
   1.244 +apply auto
   1.245 +done
   1.246 +
   1.247 +(*
   1.248 +lemma assign_raise_if [simp]: 
   1.249 +  "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
   1.250 +                  store = f v (store s)\<rparr>) v s =  
   1.251 +  \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
   1.252 +   store= if (abrupt s)=None \<and> \<not>b (store s) v 
   1.253 +             then f v (store s) else (store s)\<rparr>"
   1.254 +apply (case_tac "abrupt s = None")
   1.255 +apply auto
   1.256 +done
   1.257 +*)
   1.258 +
   1.259 +constdefs
   1.260 +
   1.261 +  init_comp_ty :: "ty \<Rightarrow> stmt"
   1.262 + "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
   1.263 +
   1.264 +lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
   1.265 +apply (unfold init_comp_ty_def)
   1.266 +apply (simp (no_asm))
   1.267 +done
   1.268 +
   1.269 +constdefs
   1.270 +
   1.271 +(*
   1.272 +  target  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
   1.273 + "target m s a' t 
   1.274 +    \<equiv> if m = IntVir
   1.275 +	 then obj_class (lookup_obj s a') 
   1.276 +         else the_Class (RefT t)"
   1.277 +*)
   1.278 +
   1.279 + invocation_class  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
   1.280 + "invocation_class m s a' statT 
   1.281 +    \<equiv> (case m of
   1.282 +         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
   1.283 +                      then the_Class (RefT statT) 
   1.284 +                      else Object
   1.285 +       | SuperM \<Rightarrow> the_Class (RefT statT)
   1.286 +       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
   1.287 +
   1.288 +invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname"
   1.289 +"invocation_declclass G m s a' statT sig 
   1.290 +   \<equiv> declclass (the (dynlookup G statT 
   1.291 +                                (invocation_class m s a' statT)
   1.292 +                                sig))" 
   1.293 +  
   1.294 +lemma invocation_class_IntVir [simp]: 
   1.295 +"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
   1.296 +by (simp add: invocation_class_def)
   1.297 +
   1.298 +lemma dynclass_SuperM [simp]: 
   1.299 + "invocation_class SuperM s a' statT = the_Class (RefT statT)"
   1.300 +by (simp add: invocation_class_def)
   1.301 +(*
   1.302 +lemma invocation_class_notIntVir [simp]: 
   1.303 + "m \<noteq> IntVir \<Longrightarrow> invocation_class m s a' statT = the_Class (RefT statT)"
   1.304 +by (simp add: invocation_class_def)
   1.305 +*)
   1.306 +
   1.307 +lemma invocation_class_Static [simp]: 
   1.308 +  "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 
   1.309 +                                            then the_Class (RefT statT) 
   1.310 +                                            else Object)"
   1.311 +by (simp add: invocation_class_def)
   1.312 +
   1.313 +constdefs
   1.314 +  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
   1.315 +		   state \<Rightarrow> state"
   1.316 + "init_lvars G C sig mode a' pvs 
   1.317 +   \<equiv> \<lambda> (x,s). 
   1.318 +      let m = mthd (the (methd G C sig));
   1.319 +          l = \<lambda> k. 
   1.320 +              (case k of
   1.321 +                 EName e 
   1.322 +                   \<Rightarrow> (case e of 
   1.323 +                         VNam v \<Rightarrow> (init_vals (table_of (lcls (mbody m)))
   1.324 +                                                     ((pars m)[\<mapsto>]pvs)) v
   1.325 +                       | Res    \<Rightarrow> Some (default_val (resTy m)))
   1.326 +               | This 
   1.327 +                   \<Rightarrow> (if mode=Static then None else Some a'))
   1.328 +      in set_lvars l (if mode = Static then x else np a' x,s)"
   1.329 +
   1.330 +
   1.331 +
   1.332 +lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =  
   1.333 +  set_lvars 
   1.334 +    (\<lambda> k. 
   1.335 +       (case k of
   1.336 +          EName e 
   1.337 +            \<Rightarrow> (case e of 
   1.338 +                  VNam v 
   1.339 +                  \<Rightarrow> (init_vals 
   1.340 +                       (table_of (lcls (mbody (mthd (the (methd G C sig))))))
   1.341 +                                 ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
   1.342 +               | Res \<Rightarrow> Some (default_val (resTy (mthd (the (methd G C sig))))))
   1.343 +        | This 
   1.344 +            \<Rightarrow> (if mode=Static then None else Some a')))
   1.345 +    (if mode = Static then x else np a' x,s)"
   1.346 +apply (unfold init_lvars_def)
   1.347 +apply (simp (no_asm) add: Let_def)
   1.348 +done
   1.349 +
   1.350 +constdefs
   1.351 +  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr"
   1.352 + "body G C sig \<equiv> let m = the (methd G C sig) 
   1.353 +                 in Body (declclass m) (stmt (mbody (mthd m)))"
   1.354 +
   1.355 +lemma body_def2: 
   1.356 +"body G C sig = Body  (declclass (the (methd G C sig))) 
   1.357 +                      (stmt (mbody (mthd (the (methd G C sig)))))"
   1.358 +apply (unfold body_def Let_def)
   1.359 +apply auto
   1.360 +done
   1.361 +
   1.362 +section "variables"
   1.363 +
   1.364 +constdefs
   1.365 +
   1.366 +  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
   1.367 + "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
   1.368 +
   1.369 +  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
   1.370 + "fvar C stat fn a' s 
   1.371 +    \<equiv> let (oref,xf) = if stat then (Stat C,id)
   1.372 +                              else (Heap (the_Addr a'),np a');
   1.373 +	          n = Inl (fn,C); 
   1.374 +                  f = (\<lambda>v. supd (upd_gobj oref n v)) 
   1.375 +      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
   1.376 +
   1.377 +  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
   1.378 + "avar G i' a' s 
   1.379 +    \<equiv> let   oref = Heap (the_Addr a'); 
   1.380 +               i = the_Intg i'; 
   1.381 +               n = Inr i;
   1.382 +        (T,k,cs) = the_Arr (globs (store s) oref); 
   1.383 +               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
   1.384 +                                           ArrStore x
   1.385 +                              ,upd_gobj oref n v s)) 
   1.386 +      in ((the (cs n),f)
   1.387 +         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
   1.388 +
   1.389 +lemma fvar_def2: "fvar C stat fn a' s =  
   1.390 +  ((the 
   1.391 +     (values 
   1.392 +      (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
   1.393 +      (Inl (fn,C)))
   1.394 +   ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
   1.395 +                        (Inl (fn,C)) 
   1.396 +                        v)))
   1.397 +  ,abupd (if stat then id else np a') s)
   1.398 +  "
   1.399 +apply (unfold fvar_def)
   1.400 +apply (simp (no_asm) add: Let_def split_beta)
   1.401 +done
   1.402 +
   1.403 +lemma avar_def2: "avar G i' a' s =  
   1.404 +  ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
   1.405 +           (Inr (the_Intg i')))
   1.406 +   ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
   1.407 +                                                   (Heap (the_Addr a')))))) 
   1.408 +                            ArrStore x
   1.409 +                 ,upd_gobj  (Heap (the_Addr a')) 
   1.410 +                               (Inr (the_Intg i')) v s')))
   1.411 +  ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
   1.412 +                   (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
   1.413 +          s)"
   1.414 +apply (unfold avar_def)
   1.415 +apply (simp (no_asm) add: Let_def split_beta)
   1.416 +done
   1.417 +
   1.418 +
   1.419 +section "evaluation judgments"
   1.420 +
   1.421 +consts
   1.422 +  eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
   1.423 +  halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
   1.424 +  sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
   1.425 +
   1.426 +
   1.427 +syntax
   1.428 +eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
   1.429 +exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
   1.430 +evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
   1.431 +eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
   1.432 +evals::"[prog,state,expr list ,
   1.433 +		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
   1.434 +hallo::"[prog,state,obj_tag,
   1.435 +	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
   1.436 +sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
   1.437 +
   1.438 +syntax (xsymbols)
   1.439 +eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
   1.440 +exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
   1.441 +evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
   1.442 +eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
   1.443 +evals::"[prog,state,expr list ,
   1.444 +		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   1.445 +hallo::"[prog,state,obj_tag,
   1.446 +	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
   1.447 +sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
   1.448 +
   1.449 +translations
   1.450 +  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
   1.451 +  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
   1.452 +  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
   1.453 +  "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
   1.454 +  "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
   1.455 +  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
   1.456 +  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
   1.457 +  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
   1.458 +  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
   1.459 +  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
   1.460 +  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
   1.461 +  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
   1.462 +  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
   1.463 +  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
   1.464 +  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
   1.465 +
   1.466 +inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
   1.467 +
   1.468 +  Abrupt: 
   1.469 +  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
   1.470 +
   1.471 +  New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
   1.472 +	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
   1.473 +		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
   1.474 +            \<Longrightarrow>
   1.475 +	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
   1.476 +
   1.477 +inductive "sxalloc G" intros (* allocating exception objects for
   1.478 +	 	 	      standard exceptions (other than OutOfMemory) *)
   1.479 +
   1.480 +  Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
   1.481 +
   1.482 +  XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
   1.483 +
   1.484 +  SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
   1.485 +	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
   1.486 +
   1.487 +
   1.488 +inductive "eval G" intros
   1.489 +
   1.490 +(* propagation of abrupt completion *)
   1.491 +
   1.492 +  (* cf. 14.1, 15.5 *)
   1.493 +  Abrupt: 
   1.494 +   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
   1.495 +
   1.496 +
   1.497 +(* execution of statements *)
   1.498 +
   1.499 +  (* cf. 14.5 *)
   1.500 +  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
   1.501 +
   1.502 +  (* cf. 14.7 *)
   1.503 +  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.504 +				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
   1.505 +
   1.506 +  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.507 +                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
   1.508 +  (* cf. 14.2 *)
   1.509 +  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
   1.510 +	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.511 +				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
   1.512 +
   1.513 +
   1.514 +  (* cf. 14.8.2 *)
   1.515 +  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   1.516 +	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.517 +		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
   1.518 +
   1.519 +  (* cf. 14.10, 14.10.1 *)
   1.520 +  (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
   1.521 +  (* A "continue jump" from the while body c is handled by 
   1.522 +     this rule. If a continue jump with the proper label was invoked inside c
   1.523 +     this label (Cont l) is deleted out of the abrupt component of the state 
   1.524 +     before the iterative evaluation of the while statement.
   1.525 +     A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
   1.526 +  *)
   1.527 +  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
   1.528 +	  if normal s1 \<and> the_Bool b 
   1.529 +             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   1.530 +                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   1.531 +	     else s3 = s1\<rbrakk> \<Longrightarrow>
   1.532 +			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   1.533 +
   1.534 +  Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
   1.535 +   
   1.536 +  (* cf. 14.16 *)
   1.537 +  Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.538 +				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
   1.539 +
   1.540 +  (* cf. 14.18.1 *)
   1.541 +  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
   1.542 +	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
   1.543 +		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
   1.544 +
   1.545 +  (* cf. 14.18.2 *)
   1.546 +  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
   1.547 +	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.548 +               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   1.549 +
   1.550 +  (* cf. 12.4.2, 8.5 *)
   1.551 +  Init:	"\<lbrakk>the (class G C) = c;
   1.552 +	  if inited C (globs s0) then s3 = Norm s0
   1.553 +	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   1.554 +		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   1.555 +	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
   1.556 +              \<Longrightarrow>
   1.557 +		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   1.558 +
   1.559 +(* evaluation of expressions *)
   1.560 +
   1.561 +  (* cf. 15.8.1, 12.4.1 *)
   1.562 +  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
   1.563 +	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.564 +	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
   1.565 +
   1.566 +  (* cf. 15.9.1, 12.4.1 *)
   1.567 +  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
   1.568 +	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   1.569 +	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
   1.570 +
   1.571 +  (* cf. 15.15 *)
   1.572 +  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   1.573 +	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   1.574 +			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
   1.575 +
   1.576 +  (* cf. 15.19.2 *)
   1.577 +  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
   1.578 +	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   1.579 +			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
   1.580 +
   1.581 +  (* cf. 15.7.1 *)
   1.582 +  Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
   1.583 +
   1.584 +
   1.585 +
   1.586 +  (* cf. 15.10.2 *)
   1.587 +  Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
   1.588 +
   1.589 +  (* cf. 15.2 *)
   1.590 +  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.591 +	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
   1.592 +
   1.593 +  (* cf. 15.25.1 *)
   1.594 +  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
   1.595 +          G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.596 +				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
   1.597 +
   1.598 +  (* cf. 15.24 *)
   1.599 +  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
   1.600 +          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.601 +			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
   1.602 +
   1.603 +
   1.604 +  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
   1.605 +  Call:	
   1.606 +  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
   1.607 +    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
   1.608 +    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2 
   1.609 +         \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s3\<rbrakk>
   1.610 +   \<Longrightarrow>
   1.611 +       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s3)"
   1.612 +
   1.613 +  Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.614 +				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
   1.615 +
   1.616 +  (* cf. 14.15, 12.4.1 *)
   1.617 +  Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.618 + G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
   1.619 +
   1.620 +(* evaluation of variables *)
   1.621 +
   1.622 +  (* cf. 15.13.1, 15.7.2 *)
   1.623 +  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
   1.624 +
   1.625 +  (* cf. 15.10.1, 12.4.1 *)
   1.626 +  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
   1.627 +	  (v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>
   1.628 +	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"
   1.629 +
   1.630 +  (* cf. 15.12.1, 15.25.1 *)
   1.631 +  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
   1.632 +	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
   1.633 +	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
   1.634 +
   1.635 +
   1.636 +(* evaluation of expression lists *)
   1.637 +
   1.638 +  (* cf. 15.11.4.2 *)
   1.639 +  Nil:
   1.640 +				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
   1.641 +
   1.642 +  (* cf. 15.6.4 *)
   1.643 +  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
   1.644 +          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.645 +				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
   1.646 +
   1.647 +(* Rearrangement of premisses:
   1.648 +[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
   1.649 + 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
   1.650 + 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
   1.651 + 27(AVar),22(Call)]
   1.652 +*)
   1.653 +ML {*
   1.654 +bind_thm ("eval_induct_", rearrange_prems 
   1.655 +[0,1,2,8,4,28,29,25,15,16,
   1.656 + 17,18,19,3,5,23,24,21,6,
   1.657 + 7,11,9,13,14,12,20,10,26,
   1.658 + 27,22] (thm "eval.induct"))
   1.659 +*}
   1.660 +
   1.661 +lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
   1.662 +   and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
   1.663 +   s2 (* Fin *) and and s2 (* NewC *)] 
   1.664 +
   1.665 +declare split_if     [split del] split_if_asm     [split del] 
   1.666 +        option.split [split del] option.split_asm [split del]
   1.667 +inductive_cases halloc_elim_cases: 
   1.668 +  "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   1.669 +  "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
   1.670 +
   1.671 +inductive_cases sxalloc_elim_cases:
   1.672 + 	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
   1.673 + 	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
   1.674 + 	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
   1.675 +inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
   1.676 +
   1.677 +lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
   1.678 +       \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
   1.679 +       \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
   1.680 +      \<rbrakk> \<Longrightarrow> P"
   1.681 +apply cut_tac 
   1.682 +apply (erule sxalloc_cases)
   1.683 +apply blast+
   1.684 +done
   1.685 +
   1.686 +declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
   1.687 +declare split_paired_All [simp del] split_paired_Ex [simp del]
   1.688 +ML_setup {*
   1.689 +simpset_ref() := simpset() delloop "split_all_tac"
   1.690 +*}
   1.691 +inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
   1.692 +
   1.693 +inductive_cases eval_elim_cases:
   1.694 +        "G\<turnstile>(Some xc,s) \<midarrow>t                         \<succ>\<rightarrow> vs'"
   1.695 +	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<rightarrow> xs'"
   1.696 +        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<rightarrow> xs'"
   1.697 +        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<rightarrow> xs'"
   1.698 +	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<rightarrow> vs'"
   1.699 +	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<rightarrow> vs'"
   1.700 +	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<rightarrow> vs'"
   1.701 +	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<rightarrow> vs'"
   1.702 +	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<rightarrow> vs'"
   1.703 +	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<rightarrow> vs'"
   1.704 +	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<rightarrow> vs'"
   1.705 +	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<rightarrow> vs'"
   1.706 +	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<rightarrow> xs'"
   1.707 +	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<rightarrow> xs'"
   1.708 +	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<rightarrow> xs'"
   1.709 +	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<rightarrow> xs'"
   1.710 +	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<rightarrow> vs'"
   1.711 +	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<rightarrow> xs'"
   1.712 +	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<rightarrow> xs'"
   1.713 +	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<rightarrow> xs'"
   1.714 +	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<rightarrow> xs'"
   1.715 +	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<rightarrow> vs'"
   1.716 +	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<rightarrow> vs'"
   1.717 +	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<rightarrow> vs'"
   1.718 +	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<rightarrow> xs'"
   1.719 +	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<rightarrow> vs'"
   1.720 +	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<rightarrow> vs'"
   1.721 +	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
   1.722 +	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<rightarrow> xs'"
   1.723 +declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
   1.724 +declare split_paired_All [simp] split_paired_Ex [simp]
   1.725 +ML_setup {*
   1.726 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   1.727 +*}
   1.728 +declare split_if     [split] split_if_asm     [split] 
   1.729 +        option.split [split] option.split_asm [split]
   1.730 +
   1.731 +lemma eval_Inj_elim: 
   1.732 + "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
   1.733 + \<Longrightarrow> case t of 
   1.734 +       In1 ec \<Rightarrow> (case ec of 
   1.735 +                    Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
   1.736 +                  | Inr c \<Rightarrow> w = \<diamondsuit>)  
   1.737 +     | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
   1.738 +     | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   1.739 +apply (erule eval_cases)
   1.740 +apply auto
   1.741 +apply (induct_tac "t")
   1.742 +apply (induct_tac "a")
   1.743 +apply auto
   1.744 +done
   1.745 +
   1.746 +ML_setup {*
   1.747 +fun eval_fun nam inj rhs =
   1.748 +let
   1.749 +  val name = "eval_" ^ nam ^ "_eq"
   1.750 +  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
   1.751 +  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   1.752 +	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
   1.753 +  fun is_Inj (Const (inj,_) $ _) = true
   1.754 +    | is_Inj _                   = false
   1.755 +  fun pred (_ $ (Const ("Pair",_) $ _ $ 
   1.756 +      (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
   1.757 +in
   1.758 +  make_simproc name lhs pred (thm name)
   1.759 +end
   1.760 +
   1.761 +val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
   1.762 +val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
   1.763 +val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
   1.764 +val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
   1.765 +Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
   1.766 +bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
   1.767 +*}
   1.768 +
   1.769 +declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
   1.770 +
   1.771 +
   1.772 +lemma eval_no_abrupt_lemma: 
   1.773 +   "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
   1.774 +by (erule eval_cases, auto)
   1.775 +
   1.776 +lemma eval_no_abrupt: 
   1.777 +  "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
   1.778 +        (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
   1.779 +apply auto
   1.780 +apply (frule eval_no_abrupt_lemma, auto)+
   1.781 +done
   1.782 +
   1.783 +ML {*
   1.784 +local
   1.785 +  fun is_None (Const ("Option.option.None",_)) = true
   1.786 +    | is_None _ = false
   1.787 +  fun pred (t as (_ $ (Const ("Pair",_) $
   1.788 +     (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
   1.789 +in
   1.790 +  val eval_no_abrupt_proc = 
   1.791 +  make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
   1.792 +          (thm "eval_no_abrupt")
   1.793 +end;
   1.794 +Addsimprocs [eval_no_abrupt_proc]
   1.795 +*}
   1.796 +
   1.797 +
   1.798 +lemma eval_abrupt_lemma: 
   1.799 +  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
   1.800 +by (erule eval_cases, auto)
   1.801 +
   1.802 +lemma eval_abrupt: 
   1.803 + " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
   1.804 +     (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
   1.805 +     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
   1.806 +apply auto
   1.807 +apply (frule eval_abrupt_lemma, auto)+
   1.808 +done
   1.809 +
   1.810 +ML {*
   1.811 +local
   1.812 +  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
   1.813 +    | is_Some _ = false
   1.814 +  fun pred (_ $ (Const ("Pair",_) $
   1.815 +     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   1.816 +       x))) $ _ ) = is_Some x
   1.817 +in
   1.818 +  val eval_abrupt_proc = 
   1.819 +  make_simproc "eval_abrupt" 
   1.820 +               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
   1.821 +end;
   1.822 +Addsimprocs [eval_abrupt_proc]
   1.823 +*}
   1.824 +
   1.825 +
   1.826 +lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
   1.827 +apply (case_tac "s", case_tac "a = None")
   1.828 +by (auto intro!: eval.Lit)
   1.829 +
   1.830 +lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
   1.831 +apply (case_tac "s", case_tac "a = None")
   1.832 +by (auto intro!: eval.Skip)
   1.833 +
   1.834 +lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
   1.835 +apply (case_tac "s", case_tac "a = None")
   1.836 +by (auto intro!: eval.Expr)
   1.837 +
   1.838 +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"
   1.839 +apply (case_tac "s", case_tac "a = None")
   1.840 +by (auto intro!: eval.Comp)
   1.841 +
   1.842 +lemma CondI: 
   1.843 +  "\<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> 
   1.844 +         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
   1.845 +apply (case_tac "s", case_tac "a = None")
   1.846 +by (auto intro!: eval.Cond)
   1.847 +
   1.848 +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>
   1.849 +                 \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
   1.850 +apply (case_tac "s", case_tac "a = None")
   1.851 +by (auto intro!: eval.If)
   1.852 +
   1.853 +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'"
   1.854 +apply (case_tac "s", case_tac "a = None")
   1.855 +by (auto intro!: eval.Methd)
   1.856 +
   1.857 +lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
   1.858 +       D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   1.859 +       G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2 
   1.860 +        \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s3; 
   1.861 +       s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>  
   1.862 +       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s3'"
   1.863 +apply (drule eval.Call, assumption)
   1.864 +apply (rule HOL.refl)
   1.865 +apply simp+
   1.866 +done
   1.867 +
   1.868 +lemma eval_Init: 
   1.869 +"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
   1.870 +  else G\<turnstile>Norm (init_class_obj G C s0)  
   1.871 +         \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
   1.872 +       G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
   1.873 +      s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
   1.874 +  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
   1.875 +apply (rule eval.Init)
   1.876 +apply auto
   1.877 +done
   1.878 +
   1.879 +lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
   1.880 +apply (case_tac "s", simp)
   1.881 +apply (case_tac "a")
   1.882 +apply  safe
   1.883 +apply (rule eval_Init)
   1.884 +apply   auto
   1.885 +done
   1.886 +
   1.887 +lemma eval_StatRef: 
   1.888 +"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
   1.889 +apply (case_tac "s", simp)
   1.890 +apply (case_tac "a = None")
   1.891 +apply (auto del: eval.Abrupt intro!: eval.intros)
   1.892 +done
   1.893 +
   1.894 +
   1.895 +lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
   1.896 +apply (erule eval_cases)
   1.897 +by auto
   1.898 +
   1.899 +lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
   1.900 +by auto
   1.901 +
   1.902 +(*unused*)
   1.903 +lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
   1.904 +  (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
   1.905 +apply (erule eval.induct)
   1.906 +apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
   1.907 +apply auto
   1.908 +done
   1.909 +
   1.910 +lemma halloc_xcpt [dest!]: 
   1.911 +  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
   1.912 +apply (erule_tac halloc_elim_cases)
   1.913 +by auto
   1.914 +
   1.915 +(*
   1.916 +G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   1.917 +G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
   1.918 +*)
   1.919 +
   1.920 +lemma eval_Methd: 
   1.921 +  "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')"
   1.922 +apply (case_tac "s")
   1.923 +apply (case_tac "a")
   1.924 +apply clarsimp+
   1.925 +apply (erule eval.Methd)
   1.926 +apply (drule eval_abrupt_lemma)
   1.927 +apply force
   1.928 +done
   1.929 +
   1.930 +
   1.931 +section "single valued"
   1.932 +
   1.933 +lemma unique_halloc [rule_format (no_asm)]: 
   1.934 +  "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
   1.935 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.936 +apply (erule halloc.induct)
   1.937 +apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
   1.938 +apply (drule trans [THEN sym], erule sym) 
   1.939 +defer
   1.940 +apply (drule trans [THEN sym], erule sym)
   1.941 +apply auto
   1.942 +done
   1.943 +
   1.944 +
   1.945 +lemma single_valued_halloc: 
   1.946 +  "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
   1.947 +apply (unfold single_valued_def)
   1.948 +by (clarsimp, drule (1) unique_halloc, auto)
   1.949 +
   1.950 +
   1.951 +lemma unique_sxalloc [rule_format (no_asm)]: 
   1.952 +  "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
   1.953 +apply (simp (no_asm_simp) only: split_tupled_all)
   1.954 +apply (erule sxalloc.induct)
   1.955 +apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
   1.956 +              split del: split_if split_if_asm)
   1.957 +done
   1.958 +
   1.959 +lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
   1.960 +apply (unfold single_valued_def)
   1.961 +apply (blast dest: unique_sxalloc)
   1.962 +done
   1.963 +
   1.964 +lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
   1.965 +by auto
   1.966 +
   1.967 +lemma unique_eval [rule_format (no_asm)]: 
   1.968 +  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
   1.969 +apply (case_tac "ws")
   1.970 +apply (simp only:)
   1.971 +apply (erule thin_rl)
   1.972 +apply (erule eval_induct)
   1.973 +apply (tactic {* ALLGOALS (EVERY'
   1.974 +      [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
   1.975 +(* 29 subgoals *)
   1.976 +prefer 26 (* Try *) 
   1.977 +apply (simp (no_asm_use) only: split add: split_if_asm)
   1.978 +(* 32 subgoals *)
   1.979 +prefer 28 (* Init *)
   1.980 +apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
   1.981 +prefer 24 (* While *)
   1.982 +apply (simp (no_asm_use) only: split add: split_if_asm, blast)
   1.983 +apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   1.984 +apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
   1.985 +apply blast
   1.986 +(* 31 subgoals *)
   1.987 +apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
   1.988 +done
   1.989 +
   1.990 +(* unused *)
   1.991 +lemma single_valued_eval: 
   1.992 + "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
   1.993 +apply (unfold single_valued_def)
   1.994 +by (clarify, drule (1) unique_eval, auto)
   1.995 +
   1.996 +end