isabelle: src/HOL/Bali/Eval.thy@f75dfc606ac7

     1 (*  Title:      HOL/Bali/Eval.thy

     2     ID:         $Id$

     3     Author:     David von Oheimb

     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)

     5 *)

     6 header {* Operational evaluation (big-step) semantics of Java expressions and

     7           statements

     8 *}

    10 theory Eval = State + DeclConcepts:

    12 text {*

    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}

    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 *}

   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"

   106 syntax (xsymbols)

   107   dummy_res :: "vals" ("\<diamondsuit>")

   108 translations

   109   "\<diamondsuit>" == "In1 Unit"

   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)"

   116 lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"

   117 by (simp add: arbitrary3_def)

   119 lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"

   120 by (simp add: arbitrary3_def)

   122 lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"

   123 by (simp add: arbitrary3_def)

   125 lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"

   126 by (simp add: arbitrary3_def)

   129 section "exception throwing and catching"

   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)"

   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

   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"

   145 lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"

   146 by (simp add: fits_def)

   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)

   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

   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"

   170 lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"

   171 apply (unfold catch_def)

   172 apply (simp (no_asm))

   173 done

   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

   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)"

   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

   195 section "misc"

   197 constdefs

   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)"

   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 *)

   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)

   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 *)

   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)

   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)

   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

   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

   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 *)

   256 constdefs

   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"

   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

   266 constdefs

   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 *)

   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'))"

   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))"

   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)

   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 *)

   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)

   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)"

   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

   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)))"

   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

   359 section "variables"

   361 constdefs

   363   lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"

   364  "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"

   366   fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"

   367  "fvar C stat fn a' s

   368     \<equiv> let (oref,xf) = if stat then (Stat C,id)

   369                               else (Heap (the_Addr a'),np a');

   370 	          n = Inl (fn,C);

   371                   f = (\<lambda>v. supd (upd_gobj oref n v))

   372       in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"

   373 (*

   374  "fvar C stat fn a' s

   375     \<equiv> let (oref,xf) = if stat then (Stat C,id)

   376                               else (Heap (the_Addr a'),np a');

   377 	          n = Inl (fn,C);

   378                   f = (\<lambda>v. supd (upd_gobj oref n v))

   379       in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"

   380 *)

   381   avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"

   382  "avar G i' a' s

   383     \<equiv> let   oref = Heap (the_Addr a');

   384                i = the_Intg i';

   385                n = Inr i;

   386         (T,k,cs) = the_Arr (globs (store s) oref);

   387                f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T)

   388                                            ArrStore x

   389                               ,upd_gobj oref n v s))

   390       in ((the (cs n),f)

   391          ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"

   393 lemma fvar_def2: "fvar C stat fn a' s =

   394   ((the

   395      (values

   396       (the (globs (store s) (if stat then Stat C else Heap (the_Addr a'))))

   397       (Inl (fn,C)))

   398    ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a'))

   399                         (Inl (fn,C))

   400                         v)))

   401   ,abupd (if stat then id else np a') s)

   402   "

   403 apply (unfold fvar_def)

   404 apply (simp (no_asm) add: Let_def split_beta)

   405 done

   407 lemma avar_def2: "avar G i' a' s =

   408   ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a'))))))

   409            (Inr (the_Intg i')))

   410    ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)

   411                                                    (Heap (the_Addr a'))))))

   412                             ArrStore x

   413                  ,upd_gobj  (Heap (the_Addr a'))

   414                                (Inr (the_Intg i')) v s')))

   415   ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s)

   416                    (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')

   417           s)"

   418 apply (unfold avar_def)

   419 apply (simp (no_asm) add: Let_def split_beta)

   420 done

   422 constdefs

   423 check_field_access::

   424 "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"

   425 "check_field_access G accC statDeclC fn stat a' s

   426  \<equiv> let oref = if stat then Stat statDeclC

   427                       else Heap (the_Addr a');

   428        dynC = case oref of

   429                    Heap a \<Rightarrow> obj_class (the (globs (store s) oref))

   430                  | Stat C \<Rightarrow> C;

   431        f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))

   432    in abupd

   433         (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)

   434                   AccessViolation)

   435         s"

   437 constdefs

   438 check_method_access::

   439   "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"

   440 "check_method_access G accC statT mode sig  a' s

   441  \<equiv> let invC = invocation_class mode (store s) a' statT;

   442        dynM = the (dynlookup G statT invC sig)

   443    in abupd

   444         (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)

   445                   AccessViolation)

   446         s"

   448 section "evaluation judgments"

   450 consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"

   451 primrec

   452 "eval_unop UPlus   v = Intg (the_Intg v)"

   453 "eval_unop UMinus  v = Intg (- (the_Intg v))"

   454 "eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"

   455 "eval_unop UNot    v = Bool (\<not> the_Bool v)"

   457 consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"

   460 primrec

   461 "eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))"

   462 "eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"

   463 "eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"

   464 "eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"

   465 "eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"

   467 -- "Be aware of the explicit coercion of the shift distance to nat"

   468 "eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"

   469 "eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"

   470 "eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"

   472 "eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))"

   473 "eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"

   474 "eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"

   475 "eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"

   477 "eval_binop Eq      v1 v2 = Bool (v1=v2)"

   478 "eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"

   479 "eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"

   480 "eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"

   481 "eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"

   482 "eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"

   483 "eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"

   484 "eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"

   487 consts

   488   eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"

   489   halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"

   490   sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"

   493 syntax

   494 eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)

   495 exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)

   496 evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)

   497 eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)

   498 evals::"[prog,state,expr list ,

   499 		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)

   500 hallo::"[prog,state,obj_tag,

   501 	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)

   502 sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)

   504 syntax (xsymbols)

   505 eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)

   506 exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)

   507 evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)

   508 eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)

   509 evals::"[prog,state,expr list ,

   510 		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)

   511 hallo::"[prog,state,obj_tag,

   512 	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)

   513 sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)

   515 translations

   516   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"

   517   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"

   518   "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"

   519   "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"

   520   "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"

   521   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"

   522   "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"

   523   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"

   524   "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"

   525   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"

   526   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"

   527   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"

   528   "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"

   529   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"

   530   "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"

   532 inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)

   534   Abrupt:

   535   "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"

   537   New:	  "\<lbrakk>new_Addr (heap s) = Some a;

   538 	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)

   539 		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>

   540             \<Longrightarrow>

   541 	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"

   543 inductive "sxalloc G" intros (* allocating exception objects for

   544 	 	 	      standard exceptions (other than OutOfMemory) *)

   546   Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"

   548   XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"

   550   SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>

   551 	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"

   553 inductive "eval G" intros

   555 (* propagation of abrupt completion *)

   557   (* cf. 14.1, 15.5 *)

   558   Abrupt:

   559    "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"

   562 (* execution of statements *)

   564   (* cf. 14.5 *)

   565   Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"

   567   (* cf. 14.7 *)

   568   Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>

   569 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"

   571   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>

   572                                 G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"

   573   (* cf. 14.2 *)

   574   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;

   575 	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>

   576 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"

   579   (* cf. 14.8.2 *)

   580   If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;

   581 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>

   582 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"

   584   (* cf. 14.10, 14.10.1 *)

   585   (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)

   586   (* A "continue jump" from the while body c is handled by

   587      this rule. If a continue jump with the proper label was invoked inside c

   588      this label (Cont l) is deleted out of the abrupt component of the state

   589      before the iterative evaluation of the while statement.

   590      A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).

   591   *)

   592   Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;

   593 	  if normal s1 \<and> the_Bool b

   594              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and>

   595                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)

   596 	     else s3 = s1\<rbrakk> \<Longrightarrow>

   597 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"

   599   Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"

   601   (* cf. 14.16 *)

   602   Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>

   603 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"

   605   (* cf. 14.18.1 *)

   606   Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;

   607 	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>

   608 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"

   610   (* cf. 14.18.2 *)

   611   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);

   612 	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;

   613           s3=(if (\<exists> err. x1=Some (Error err))

   614               then (x1,s1)

   615               else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk>

   616           \<Longrightarrow>

   617           G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"

   618   (* cf. 12.4.2, 8.5 *)

   619   Init:	"\<lbrakk>the (class G C) = c;

   620 	  if inited C (globs s0) then s3 = Norm s0

   621 	  else (G\<turnstile>Norm (init_class_obj G C s0)

   622 		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>

   623 	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>

   624               \<Longrightarrow>

   625 		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"

   626    (* This class initialisation rule is a little bit inaccurate. Look at the

   627       exact sequence:

   628       1. The current class object (the static fields) are initialised

   629          (init_class_obj)

   630       2. Then the superclasses are initialised

   631       3. The static initialiser of the current class is invoked

   632       More precisely we should expect another ordering, namely 2 1 3.

   633       But we can't just naively toggle 1 and 2. By calling init_class_obj

   634       before initialising the superclasses we also implicitly record that

   635       we have started to initialise the current class (by setting an

   636       value for the class object). This becomes

   637       crucial for the completeness proof of the axiomatic semantics

   638       (AxCompl.thy). Static initialisation requires an induction on the number

   639       of classes not yet initialised (or to be more precise, classes where the

   640       initialisation has not yet begun).

   641       So we could first assign a dummy value to the class before

   642       superclass initialisation and afterwards set the correct values.

   643       But as long as we don't take memory overflow into account

   644       when allocating class objects, and don't model definite assignment in

   645       the static initialisers, we can leave things as they are for convenience.

   646    *)

   647 (* evaluation of expressions *)

   649   (* cf. 15.8.1, 12.4.1 *)

   650   NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;

   651 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>

   652 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"

   654   (* cf. 15.9.1, 12.4.1 *)

   655   NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2;

   656 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>

   657 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"

   659   (* cf. 15.15 *)

   660   Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;

   661 	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>

   662 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"

   664   (* cf. 15.19.2 *)

   665   Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;

   666 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>

   667 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"

   669   (* cf. 15.7.1 *)

   670   Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"

   672   UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk>

   673          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"

   675   BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<rightarrow> s2\<rbrakk>

   676          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"

   678   (* cf. 15.10.2 *)

   679   Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"

   681   (* cf. 15.2 *)

   682   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>

   683 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"

   685   (* cf. 15.25.1 *)

   686   Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;

   687           G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>

   688 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"

   690   (* cf. 15.24 *)

   691   Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;

   692           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>

   693 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"

   696   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)

   697   Call:

   698   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;

   699     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;

   700     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;

   701     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;

   702     G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>

   703    \<Longrightarrow>

   704        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"

   705 (* The accessibility check is after init_lvars, to keep it simple. Init_lvars

   706    already tests for the absence of a null-pointer reference in case of an

   707    instance method invocation

   708 *)

   710   Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>

   711 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"

   712   (* The local variables l are just a dummy here. The are only used by

   713      the smallstep semantics *)

   714   (* cf. 14.15, 12.4.1 *)

   715   Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>

   716            G\<turnstile>Norm s0 \<midarrow>Body D c

   717             -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"

   718   (* The local variables l are just a dummy here. The are only used by

   719      the smallstep semantics *)

   720 (* evaluation of variables *)

   722   (* cf. 15.13.1, 15.7.2 *)

   723   LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"

   725   (* cf. 15.10.1, 12.4.1 *)

   726   FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;

   727 	  (v,s2') = fvar statDeclC stat fn a s2;

   728           s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>

   729 	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"

   730  (* The accessibility check is after fvar, to keep it simple. Fvar already

   731     tests for the absence of a null-pointer reference in case of an instance

   732     field

   733   *)

   735   (* cf. 15.12.1, 15.25.1 *)

   736   AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;

   737 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>

   738 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"

   741 (* evaluation of expression lists *)

   743   (* cf. 15.11.4.2 *)

   744   Nil:

   745 				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"

   747   (* cf. 15.6.4 *)

   748   Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;

   749           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>

   750 				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"

   752 (* Rearrangement of premisses:

   753 [0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),

   754  17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),

   755  7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),

   756  29(AVar),24(Call)]

   757 *)

   758 ML {*

   759 bind_thm ("eval_induct_", rearrange_prems

   760 [0,1,2,8,4,30,31,27,15,16,

   761  17,18,19,20,21,3,5,25,26,23,6,

   762  7,11,9,13,14,12,22,10,28,

   763  29,24] (thm "eval.induct"))

   764 *}

   768 lemmas eval_induct = eval_induct_ [split_format and and and and and and and and

   769    and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and

   770    and and

   771    s2 (* Fin *) and and s2 (* NewC *)]

   773 declare split_if     [split del] split_if_asm     [split del]

   774         option.split [split del] option.split_asm [split del]

   775 inductive_cases halloc_elim_cases:

   776   "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"

   777   "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"

   779 inductive_cases sxalloc_elim_cases:

   780  	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"

   781  	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"

   782  	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"

   783 inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"

   785 lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';

   786        \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;

   787        \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P

   788       \<rbrakk> \<Longrightarrow> P"

   789 apply cut_tac

   790 apply (erule sxalloc_cases)

   791 apply blast+

   792 done

   794 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)

   795 declare split_paired_All [simp del] split_paired_Ex [simp del]

   796 ML_setup {*

   797 simpset_ref() := simpset() delloop "split_all_tac"

   798 *}

   799 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"

   801 inductive_cases eval_elim_cases:

   802         "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"

   803 	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"

   804         "G\<turnstile>Norm s \<midarrow>In1r (Do j)                         \<succ>\<rightarrow> xs'"

   805         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"

   806 	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"

   807 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"

   808 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"

   809         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"

   810         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"

   811 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"

   812 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"

   813 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"

   814 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"

   815 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"

   816 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"

   817 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"

   818 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"

   819 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"

   820 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"

   821 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"

   822 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"

   823 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"

   824 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"

   825 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"

   826 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"

   827 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"

   828 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"

   829 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"

   830 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"

   831 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"

   832 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"

   833 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)

   834 declare split_paired_All [simp] split_paired_Ex [simp]

   835 ML_setup {*

   836 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)

   837 *}

   838 declare split_if     [split] split_if_asm     [split]

   839         option.split [split] option.split_asm [split]

   841 lemma eval_Inj_elim:

   842  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s')

   843  \<Longrightarrow> case t of

   844        In1 ec \<Rightarrow> (case ec of

   845                     Inl e \<Rightarrow> (\<exists>v. w = In1 v)

   846                   | Inr c \<Rightarrow> w = \<diamondsuit>)

   847      | In2 e \<Rightarrow> (\<exists>v. w = In2 v)

   848      | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"

   849 apply (erule eval_cases)

   850 apply auto

   851 apply (induct_tac "t")

   852 apply (induct_tac "a")

   853 apply auto

   854 done

   857 ML_setup {*

   858 fun eval_fun nam inj rhs =

   859 let

   860   val name = "eval_" ^ nam ^ "_eq"

   861   val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"

   862   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")

   863 	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])

   864   fun is_Inj (Const (inj,_) $ _) = true

   865     | is_Inj _                   = false

   866   fun pred (_ $ (Const ("Pair",_) $ _ $

   867       (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x

   868 in

   869   make_simproc name lhs pred (thm name)

   870 end

   872 val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"

   873 val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"

   874 val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"

   875 val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";

   876 Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];

   877 bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))

   878 *}

   880 declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!]

   882 text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only

   883 used in smallstep semantics, not in the bigstep semantics. So their is no

   884 valid evaluation of these terms

   885 *}

   888 lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"

   889 proof -

   890   { fix s t v s'

   891     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and

   892          normal: "normal s" and

   893          callee: "t=In1l (Callee l e)"

   894     then have "False"

   895     proof (induct)

   896     qed (auto)

   897   }

   898   then show ?thesis

   899     by (cases s') fastsimp

   900 qed

   903 lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"

   904 proof -

   905   { fix s t v s'

   906     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and

   907          normal: "normal s" and

   908          callee: "t=In1l (InsInitE c e)"

   909     then have "False"

   910     proof (induct)

   911     qed (auto)

   912   }

   913   then show ?thesis

   914     by (cases s') fastsimp

   915 qed

   917 lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"

   918 proof -

   919   { fix s t v s'

   920     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and

   921          normal: "normal s" and

   922          callee: "t=In2 (InsInitV c w)"

   923     then have "False"

   924     proof (induct)

   925     qed (auto)

   926   }

   927   then show ?thesis

   928     by (cases s') fastsimp

   929 qed

   931 lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"

   932 proof -

   933   { fix s t v s'

   934     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and

   935          normal: "normal s" and

   936          callee: "t=In1r (FinA a c)"

   937     then have "False"

   938     proof (induct)

   939     qed (auto)

   940   }

   941   then show ?thesis

   942     by (cases s') fastsimp

   943 qed

   945 lemma eval_no_abrupt_lemma:

   946    "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"

   947 by (erule eval_cases, auto)

   949 lemma eval_no_abrupt:

   950   "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') =

   951         (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"

   952 apply auto

   953 apply (frule eval_no_abrupt_lemma, auto)+

   954 done

   956 ML {*

   957 local

   958   fun is_None (Const ("Datatype.option.None",_)) = true

   959     | is_None _ = false

   960   fun pred (t as (_ $ (Const ("Pair",_) $

   961      (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x

   962 in

   963   val eval_no_abrupt_proc =

   964   make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred

   965           (thm "eval_no_abrupt")

   966 end;

   967 Addsimprocs [eval_no_abrupt_proc]

   968 *}

   971 lemma eval_abrupt_lemma:

   972   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"

   973 by (erule eval_cases, auto)

   975 lemma eval_abrupt:

   976  " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =

   977      (s'=(Some xc,s) \<and> w=arbitrary3 t \<and>

   978      G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"

   979 apply auto

   980 apply (frule eval_abrupt_lemma, auto)+

   981 done

   983 ML {*

   984 local

   985   fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true

   986     | is_Some _ = false

   987   fun pred (_ $ (Const ("Pair",_) $

   988      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $

   989        x))) $ _ ) = is_Some x

   990 in

   991   val eval_abrupt_proc =

   992   make_simproc "eval_abrupt"

   993                "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")

   994 end;

   995 Addsimprocs [eval_abrupt_proc]

   996 *}

   999 lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"

  1000 apply (case_tac "s", case_tac "a = None")

  1001 by (auto intro!: eval.Lit)

  1003 lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"

  1004 apply (case_tac "s", case_tac "a = None")

  1005 by (auto intro!: eval.Skip)

  1007 lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"

  1008 apply (case_tac "s", case_tac "a = None")

  1009 by (auto intro!: eval.Expr)

  1011 lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2"

  1012 apply (case_tac "s", case_tac "a = None")

  1013 by (auto intro!: eval.Comp)

  1015 lemma CondI:

  1016   "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>

  1017          G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"

  1018 apply (case_tac "s", case_tac "a = None")

  1019 by (auto intro!: eval.Cond)

  1021 lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk>

  1022                  \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"

  1023 apply (case_tac "s", case_tac "a = None")

  1024 by (auto intro!: eval.If)

  1026 lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s'

  1027                 \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"

  1028 apply (case_tac "s", case_tac "a = None")

  1029 by (auto intro!: eval.Methd)

  1031 lemma eval_Call:

  1032    "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;

  1033      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;

  1034      s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;

  1035      s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;

  1036      G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4;

  1037        s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>

  1038        G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"

  1039 apply (drule eval.Call, assumption)

  1040 apply (rule HOL.refl)

  1041 apply simp+

  1042 done

  1044 lemma eval_Init:

  1045 "\<lbrakk>if inited C (globs s0) then s3 = Norm s0

  1046   else G\<turnstile>Norm (init_class_obj G C s0)

  1047          \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>

  1048        G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and>

  1049       s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>

  1050   G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"

  1051 apply (rule eval.Init)

  1052 apply auto

  1053 done

  1055 lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"

  1056 apply (case_tac "s", simp)

  1057 apply (case_tac "a")

  1058 apply  safe

  1059 apply (rule eval_Init)

  1060 apply   auto

  1061 done

  1063 lemma eval_StatRef:

  1064 "G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"

  1065 apply (case_tac "s", simp)

  1066 apply (case_tac "a = None")

  1067 apply (auto del: eval.Abrupt intro!: eval.intros)

  1068 done

  1071 lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s"

  1072 apply (erule eval_cases)

  1073 by auto

  1075 lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"

  1076 by auto

  1078 (*unused*)

  1079 lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>

  1080   (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"

  1081 apply (erule eval.induct)

  1082 apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+

  1083 apply auto

  1084 done

  1086 lemma halloc_xcpt [dest!]:

  1087   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"

  1088 apply (erule_tac halloc_elim_cases)

  1089 by auto

  1091 (*

  1092 G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"

  1093 G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"

  1094 *)

  1096 lemma eval_Methd:

  1097   "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s')

  1098    \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"

  1099 apply (case_tac "s")

  1100 apply (case_tac "a")

  1101 apply clarsimp+

  1102 apply (erule eval.Methd)

  1103 apply (drule eval_abrupt_lemma)

  1104 apply force

  1105 done

  1108 section "single valued"

  1110 lemma unique_halloc [rule_format (no_asm)]:

  1111   "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"

  1112 apply (simp (no_asm_simp) only: split_tupled_all)

  1113 apply (erule halloc.induct)

  1114 apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)

  1115 apply (drule trans [THEN sym], erule sym)

  1116 defer

  1117 apply (drule trans [THEN sym], erule sym)

  1118 apply auto

  1119 done

  1122 lemma single_valued_halloc:

  1123   "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"

  1124 apply (unfold single_valued_def)

  1125 by (clarsimp, drule (1) unique_halloc, auto)

  1128 lemma unique_sxalloc [rule_format (no_asm)]:

  1129   "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"

  1130 apply (simp (no_asm_simp) only: split_tupled_all)

  1131 apply (erule sxalloc.induct)

  1132 apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases

  1133               split del: split_if split_if_asm)

  1134 done

  1136 lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"

  1137 apply (unfold single_valued_def)

  1138 apply (blast dest: unique_sxalloc)

  1139 done

  1141 lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"

  1142 by auto

  1144 lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;

  1145                    res=the (locals (store s2) Result);

  1146                    s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>

  1147  G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"

  1148 by (auto elim: eval.Body)

  1150 lemma unique_eval [rule_format (no_asm)]:

  1151   "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"

  1152 apply (case_tac "ws")

  1153 apply (simp only:)

  1154 apply (erule thin_rl)

  1155 apply (erule eval_induct)

  1156 apply (tactic {* ALLGOALS (EVERY'

  1157       [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})

  1158 (* 31 subgoals *)

  1159 prefer 28 (* Try *)

  1160 apply (simp (no_asm_use) only: split add: split_if_asm)

  1161 (* 34 subgoals *)

  1162 prefer 30 (* Init *)

  1163 apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)

  1164 prefer 26 (* While *)

  1165 apply (simp (no_asm_use) only: split add: split_if_asm, blast)

  1166 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)

  1167 apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)

  1168 apply blast

  1169 (* 33 subgoals *)

  1170 apply (blast dest: unique_sxalloc unique_halloc split_pairD)+

  1171 done

  1173 (* unused *)

  1174 lemma single_valued_eval:

  1175  "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"

  1176 apply (unfold single_valued_def)

  1177 by (clarify, drule (1) unique_eval, auto)

  1179 end

author	schirmer
	Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337	f75dfc606ac7
parent 12925	99131847fb93
child 13384	a34e38154413
permissions	-rw-r--r--