src/HOL/Bali/Eval.thy
author wenzelm
Tue Aug 06 11:22:05 2002 +0200 (2002-08-06)
changeset 13462 56610e2ba220
parent 13384 a34e38154413
child 13601 fd3e3d6b37b2
permissions -rw-r--r--
sane interface for simprocs;
wenzelm@12857
     1
(*  Title:      HOL/Bali/Eval.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
wenzelm@12858
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Operational evaluation (big-step) semantics of Java expressions and 
schirmer@12854
     7
          statements
schirmer@12854
     8
*}
schirmer@12854
     9
schirmer@12854
    10
theory Eval = State + DeclConcepts:
schirmer@12854
    11
schirmer@12854
    12
text {*
schirmer@12854
    13
schirmer@12854
    14
improvements over Java Specification 1.0:
schirmer@12854
    15
\begin{itemize}
schirmer@12854
    16
\item dynamic method lookup does not need to consider the return type 
schirmer@12854
    17
      (cf.15.11.4.4)
schirmer@12854
    18
\item throw raises a NullPointer exception if a null reference is given, and 
schirmer@12854
    19
      each throw of a standard exception yield a fresh exception object 
schirmer@12854
    20
      (was not specified)
schirmer@12854
    21
\item if there is not enough memory even to allocate an OutOfMemory exception,
schirmer@12854
    22
  evaluation/execution fails, i.e. simply stops (was not specified)
schirmer@12854
    23
\item array assignment checks lhs (and may throw exceptions) before evaluating 
schirmer@12854
    24
      rhs
schirmer@12854
    25
\item fixed exact positions of class initializations 
schirmer@12854
    26
      (immediate at first active use)
schirmer@12854
    27
\end{itemize}
schirmer@12854
    28
schirmer@12854
    29
design issues:
schirmer@12854
    30
\begin{itemize}
schirmer@12854
    31
\item evaluation vs. (single-step) transition semantics
schirmer@12854
    32
  evaluation semantics chosen, because:
schirmer@12854
    33
  \begin{itemize} 
schirmer@12854
    34
  \item[++] less verbose and therefore easier to read (and to handle in proofs)
schirmer@12854
    35
  \item[+]  more abstract
schirmer@12854
    36
  \item[+]  intermediate values (appearing in recursive rules) need not be 
schirmer@12854
    37
     stored explicitly, e.g. no call body construct or stack of invocation 
schirmer@12854
    38
     frames containing local variables and return addresses for method calls 
schirmer@12854
    39
     needed
schirmer@12854
    40
  \item[+]  convenient rule induction for subject reduction theorem
schirmer@12854
    41
  \item[-]  no interleaving (for parallelism) can be described
schirmer@12854
    42
  \item[-]  stating a property of infinite executions requires the meta-level 
schirmer@12854
    43
     argument that this property holds for any finite prefixes of it 
schirmer@12854
    44
     (e.g. stopped using a counter that is decremented to zero and then 
schirmer@12854
    45
     throwing an exception)
schirmer@12854
    46
  \end{itemize}
schirmer@12854
    47
\item unified evaluation for variables, expressions, expression lists, 
schirmer@12854
    48
      statements
schirmer@12854
    49
\item the value entry in statement rules is redundant 
schirmer@12854
    50
\item the value entry in rules is irrelevant in case of exceptions, but its full
schirmer@12854
    51
  inclusion helps to make the rule structure independent of exception occurence.
schirmer@12854
    52
\item as irrelevant value entries are ignored, it does not matter if they are 
schirmer@12854
    53
      unique.
schirmer@12854
    54
  For simplicity, (fixed) arbitrary values are preferred over "free" values.
schirmer@12854
    55
\item the rule format is such that the start state may contain an exception.
schirmer@12854
    56
  \begin{itemize}
schirmer@12854
    57
  \item[++] faciliates exception handling
schirmer@12854
    58
  \item[+]  symmetry
schirmer@12854
    59
  \end{itemize}
schirmer@12854
    60
\item the rules are defined carefully in order to be applicable even in not
schirmer@12854
    61
  type-correct situations (yielding undefined values),
schirmer@12854
    62
  e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
schirmer@12854
    63
  \begin{itemize}
schirmer@12854
    64
  \item[++] fewer rules 
schirmer@12854
    65
  \item[-]  less readable because of auxiliary functions like @{text the_Addr}
schirmer@12854
    66
  \end{itemize}
schirmer@12854
    67
  Alternative: "defensive" evaluation throwing some InternalError exception
schirmer@12854
    68
               in case of (impossible, for correct programs) type mismatches
schirmer@12854
    69
\item there is exactly one rule per syntactic construct
schirmer@12854
    70
  \begin{itemize}
schirmer@12854
    71
  \item[+] no redundancy in case distinctions
schirmer@12854
    72
  \end{itemize}
schirmer@12854
    73
\item halloc fails iff there is no free heap address. When there is
schirmer@12854
    74
  only one free heap address left, it returns an OutOfMemory exception.
schirmer@12854
    75
  In this way it is guaranteed that when an OutOfMemory exception is thrown for
schirmer@12854
    76
  the first time, there is a free location on the heap to allocate it.
schirmer@12854
    77
\item the allocation of objects that represent standard exceptions is deferred 
schirmer@12854
    78
      until execution of any enclosing catch clause, which is transparent to 
schirmer@12854
    79
      the program.
schirmer@12854
    80
  \begin{itemize}
schirmer@12854
    81
  \item[-]  requires an auxiliary execution relation
schirmer@12854
    82
  \item[++] avoids copies of allocation code and awkward case distinctions 
schirmer@12854
    83
           (whether there is enough memory to allocate the exception) in 
schirmer@12854
    84
            evaluation rules
schirmer@12854
    85
  \end{itemize}
schirmer@12854
    86
\item unfortunately @{text new_Addr} is not directly executable because of 
schirmer@12854
    87
      Hilbert operator.
schirmer@12854
    88
\end{itemize}
schirmer@12854
    89
simplifications:
schirmer@12854
    90
\begin{itemize}
schirmer@12854
    91
\item local variables are initialized with default values 
schirmer@12854
    92
      (no definite assignment)
schirmer@12854
    93
\item garbage collection not considered, therefore also no finalizers
schirmer@12854
    94
\item stack overflow and memory overflow during class initialization not 
schirmer@12854
    95
      modelled
schirmer@12854
    96
\item exceptions in initializations not replaced by ExceptionInInitializerError
schirmer@12854
    97
\end{itemize}
schirmer@12854
    98
*}
schirmer@12854
    99
schirmer@12854
   100
types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
schirmer@12854
   101
      vals  =        "(val, vvar, val list) sum3"
schirmer@12854
   102
translations
schirmer@12854
   103
     "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
schirmer@12854
   104
     "vals" <= (type)"(val, vvar, val list) sum3"
schirmer@12854
   105
schirmer@12854
   106
syntax (xsymbols)
schirmer@12854
   107
  dummy_res :: "vals" ("\<diamondsuit>")
schirmer@12854
   108
translations
schirmer@12854
   109
  "\<diamondsuit>" == "In1 Unit"
schirmer@12854
   110
schirmer@12854
   111
constdefs
schirmer@12854
   112
  arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
schirmer@12854
   113
 "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
schirmer@12854
   114
                     (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
schirmer@12854
   115
schirmer@12854
   116
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
schirmer@12854
   117
by (simp add: arbitrary3_def)
schirmer@12854
   118
schirmer@12854
   119
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
schirmer@12854
   120
by (simp add: arbitrary3_def)
schirmer@12854
   121
schirmer@12854
   122
lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"
schirmer@12854
   123
by (simp add: arbitrary3_def)
schirmer@12854
   124
schirmer@12854
   125
lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"
schirmer@12854
   126
by (simp add: arbitrary3_def)
schirmer@12854
   127
schirmer@12854
   128
schirmer@12854
   129
section "exception throwing and catching"
schirmer@12854
   130
schirmer@12854
   131
constdefs
schirmer@12854
   132
  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
schirmer@12854
   133
 "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
schirmer@12854
   134
schirmer@12854
   135
lemma throw_def2: 
schirmer@12854
   136
 "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
schirmer@12854
   137
apply (unfold throw_def)
schirmer@12854
   138
apply (simp (no_asm))
schirmer@12854
   139
done
schirmer@12854
   140
schirmer@12854
   141
constdefs
schirmer@12854
   142
  fits    :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
schirmer@12854
   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"
schirmer@12854
   144
schirmer@12854
   145
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
schirmer@12854
   146
by (simp add: fits_def)
schirmer@12854
   147
schirmer@12854
   148
schirmer@12854
   149
lemma fits_Addr_RefT [simp]:
schirmer@12854
   150
  "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
schirmer@12854
   151
by (simp add: fits_def)
schirmer@12854
   152
schirmer@12854
   153
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>  
schirmer@12854
   154
  (\<exists>t. T = RefT t) \<and> a' = Null \<or>  
schirmer@12854
   155
  (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and>  G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
schirmer@12854
   156
apply (unfold fits_def)
schirmer@12854
   157
apply (case_tac "\<exists>pt. T = PrimT pt")
schirmer@12854
   158
apply  simp_all
schirmer@12854
   159
apply (case_tac "T")
schirmer@12854
   160
defer 
schirmer@12854
   161
apply (case_tac "a' = Null")
schirmer@12854
   162
apply  simp_all
schirmer@12854
   163
done
schirmer@12854
   164
schirmer@12854
   165
constdefs
schirmer@12854
   166
  catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool"      ("_,_\<turnstile>catch _"[61,61,61]60)
schirmer@12854
   167
 "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
schirmer@12854
   168
                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
schirmer@12854
   169
schirmer@12854
   170
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
schirmer@12854
   171
apply (unfold catch_def)
schirmer@12854
   172
apply (simp (no_asm))
schirmer@12854
   173
done
schirmer@12854
   174
schirmer@12854
   175
lemma catch_XcptLoc [simp]: 
schirmer@12854
   176
  "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
schirmer@12854
   177
apply (unfold catch_def)
schirmer@12854
   178
apply (simp (no_asm))
schirmer@12854
   179
done
schirmer@12854
   180
schirmer@12854
   181
constdefs
schirmer@12854
   182
  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state"
schirmer@12854
   183
 "new_xcpt_var vn \<equiv> 
schirmer@12854
   184
     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
schirmer@12854
   185
schirmer@12854
   186
lemma new_xcpt_var_def2 [simp]: 
schirmer@12854
   187
 "new_xcpt_var vn (x,s) = 
schirmer@12854
   188
    Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
schirmer@12854
   189
apply (unfold new_xcpt_var_def)
schirmer@12854
   190
apply (simp (no_asm))
schirmer@12854
   191
done
schirmer@12854
   192
schirmer@12854
   193
schirmer@12854
   194
schirmer@12854
   195
section "misc"
schirmer@12854
   196
schirmer@12854
   197
constdefs
schirmer@12854
   198
schirmer@12854
   199
  assign     :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state"
schirmer@12854
   200
 "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
schirmer@12854
   201
		   in  (x',if x' = None then s' else s)"
schirmer@12854
   202
schirmer@12854
   203
(*
schirmer@12854
   204
lemma assign_Norm_Norm [simp]: 
schirmer@12854
   205
"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 
schirmer@12854
   206
 \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
schirmer@12854
   207
by (simp add: assign_def Let_def)
schirmer@12854
   208
*)
schirmer@12854
   209
schirmer@12854
   210
lemma assign_Norm_Norm [simp]: 
schirmer@12854
   211
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
schirmer@12854
   212
by (simp add: assign_def Let_def)
schirmer@12854
   213
schirmer@12854
   214
(*
schirmer@12854
   215
lemma assign_Norm_Some [simp]: 
schirmer@12854
   216
  "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 
schirmer@12854
   217
   \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
schirmer@12854
   218
by (simp add: assign_def Let_def split_beta)
schirmer@12854
   219
*)
schirmer@12854
   220
schirmer@12854
   221
lemma assign_Norm_Some [simp]: 
schirmer@12854
   222
  "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 
schirmer@12854
   223
   \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
schirmer@12854
   224
by (simp add: assign_def Let_def split_beta)
schirmer@12854
   225
schirmer@12854
   226
schirmer@12854
   227
lemma assign_Some [simp]: 
schirmer@12854
   228
"assign f v (Some x,s) = (Some x,s)" 
schirmer@12854
   229
by (simp add: assign_def Let_def split_beta)
schirmer@12854
   230
schirmer@12854
   231
lemma assign_supd [simp]: 
schirmer@12854
   232
"assign (\<lambda>v. supd (f v)) v (x,s)  
schirmer@12854
   233
  = (x, if x = None then f v s else s)"
schirmer@12854
   234
apply auto
schirmer@12854
   235
done
schirmer@12854
   236
schirmer@12854
   237
lemma assign_raise_if [simp]: 
schirmer@12854
   238
  "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =  
schirmer@12854
   239
  (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
schirmer@12854
   240
apply (case_tac "x = None")
schirmer@12854
   241
apply auto
schirmer@12854
   242
done
schirmer@12854
   243
schirmer@12854
   244
(*
schirmer@12854
   245
lemma assign_raise_if [simp]: 
schirmer@12854
   246
  "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
schirmer@12854
   247
                  store = f v (store s)\<rparr>) v s =  
schirmer@12854
   248
  \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
schirmer@12854
   249
   store= if (abrupt s)=None \<and> \<not>b (store s) v 
schirmer@12854
   250
             then f v (store s) else (store s)\<rparr>"
schirmer@12854
   251
apply (case_tac "abrupt s = None")
schirmer@12854
   252
apply auto
schirmer@12854
   253
done
schirmer@12854
   254
*)
schirmer@12854
   255
schirmer@12854
   256
constdefs
schirmer@12854
   257
schirmer@12854
   258
  init_comp_ty :: "ty \<Rightarrow> stmt"
schirmer@12854
   259
 "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
schirmer@12854
   260
schirmer@12854
   261
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
schirmer@12854
   262
apply (unfold init_comp_ty_def)
schirmer@12854
   263
apply (simp (no_asm))
schirmer@12854
   264
done
schirmer@12854
   265
schirmer@12854
   266
constdefs
schirmer@12854
   267
schirmer@12854
   268
(*
schirmer@12854
   269
  target  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
schirmer@12854
   270
 "target m s a' t 
schirmer@12854
   271
    \<equiv> if m = IntVir
schirmer@12854
   272
	 then obj_class (lookup_obj s a') 
schirmer@12854
   273
         else the_Class (RefT t)"
schirmer@12854
   274
*)
schirmer@12854
   275
schirmer@12854
   276
 invocation_class  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
schirmer@12854
   277
 "invocation_class m s a' statT 
schirmer@12854
   278
    \<equiv> (case m of
schirmer@12854
   279
         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
schirmer@12854
   280
                      then the_Class (RefT statT) 
schirmer@12854
   281
                      else Object
schirmer@12854
   282
       | SuperM \<Rightarrow> the_Class (RefT statT)
schirmer@12854
   283
       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
schirmer@12854
   284
schirmer@12854
   285
invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname"
schirmer@12854
   286
"invocation_declclass G m s a' statT sig 
schirmer@12854
   287
   \<equiv> declclass (the (dynlookup G statT 
schirmer@12854
   288
                                (invocation_class m s a' statT)
schirmer@12854
   289
                                sig))" 
schirmer@12854
   290
  
schirmer@12854
   291
lemma invocation_class_IntVir [simp]: 
schirmer@12854
   292
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
schirmer@12854
   293
by (simp add: invocation_class_def)
schirmer@12854
   294
schirmer@12854
   295
lemma dynclass_SuperM [simp]: 
schirmer@12854
   296
 "invocation_class SuperM s a' statT = the_Class (RefT statT)"
schirmer@12854
   297
by (simp add: invocation_class_def)
schirmer@12854
   298
(*
schirmer@12854
   299
lemma invocation_class_notIntVir [simp]: 
schirmer@12854
   300
 "m \<noteq> IntVir \<Longrightarrow> invocation_class m s a' statT = the_Class (RefT statT)"
schirmer@12854
   301
by (simp add: invocation_class_def)
schirmer@12854
   302
*)
schirmer@12854
   303
schirmer@12854
   304
lemma invocation_class_Static [simp]: 
schirmer@12854
   305
  "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 
schirmer@12854
   306
                                            then the_Class (RefT statT) 
schirmer@12854
   307
                                            else Object)"
schirmer@12854
   308
by (simp add: invocation_class_def)
schirmer@12854
   309
schirmer@12854
   310
constdefs
schirmer@12854
   311
  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
schirmer@12854
   312
		   state \<Rightarrow> state"
schirmer@12854
   313
 "init_lvars G C sig mode a' pvs 
schirmer@12854
   314
   \<equiv> \<lambda> (x,s). 
schirmer@12854
   315
      let m = mthd (the (methd G C sig));
schirmer@12854
   316
          l = \<lambda> k. 
schirmer@12854
   317
              (case k of
schirmer@12854
   318
                 EName e 
schirmer@12854
   319
                   \<Rightarrow> (case e of 
schirmer@12854
   320
                         VNam v \<Rightarrow> (init_vals (table_of (lcls (mbody m)))
schirmer@12854
   321
                                                     ((pars m)[\<mapsto>]pvs)) v
schirmer@12854
   322
                       | Res    \<Rightarrow> Some (default_val (resTy m)))
schirmer@12854
   323
               | This 
schirmer@12854
   324
                   \<Rightarrow> (if mode=Static then None else Some a'))
schirmer@12854
   325
      in set_lvars l (if mode = Static then x else np a' x,s)"
schirmer@12854
   326
schirmer@12854
   327
schirmer@12854
   328
schirmer@12854
   329
lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =  
schirmer@12854
   330
  set_lvars 
schirmer@12854
   331
    (\<lambda> k. 
schirmer@12854
   332
       (case k of
schirmer@12854
   333
          EName e 
schirmer@12854
   334
            \<Rightarrow> (case e of 
schirmer@12854
   335
                  VNam v 
schirmer@12854
   336
                  \<Rightarrow> (init_vals 
schirmer@12854
   337
                       (table_of (lcls (mbody (mthd (the (methd G C sig))))))
schirmer@12854
   338
                                 ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
schirmer@12854
   339
               | Res \<Rightarrow> Some (default_val (resTy (mthd (the (methd G C sig))))))
schirmer@12854
   340
        | This 
schirmer@12854
   341
            \<Rightarrow> (if mode=Static then None else Some a')))
schirmer@12854
   342
    (if mode = Static then x else np a' x,s)"
schirmer@12854
   343
apply (unfold init_lvars_def)
schirmer@12854
   344
apply (simp (no_asm) add: Let_def)
schirmer@12854
   345
done
schirmer@12854
   346
schirmer@12854
   347
constdefs
schirmer@12854
   348
  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr"
schirmer@12854
   349
 "body G C sig \<equiv> let m = the (methd G C sig) 
schirmer@12854
   350
                 in Body (declclass m) (stmt (mbody (mthd m)))"
schirmer@12854
   351
schirmer@12854
   352
lemma body_def2: 
schirmer@12854
   353
"body G C sig = Body  (declclass (the (methd G C sig))) 
schirmer@12854
   354
                      (stmt (mbody (mthd (the (methd G C sig)))))"
schirmer@12854
   355
apply (unfold body_def Let_def)
schirmer@12854
   356
apply auto
schirmer@12854
   357
done
schirmer@12854
   358
schirmer@12854
   359
section "variables"
schirmer@12854
   360
schirmer@12854
   361
constdefs
schirmer@12854
   362
schirmer@12854
   363
  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
schirmer@12854
   364
 "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
schirmer@12854
   365
schirmer@12854
   366
  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
schirmer@12854
   367
 "fvar C stat fn a' s 
schirmer@12854
   368
    \<equiv> let (oref,xf) = if stat then (Stat C,id)
schirmer@12854
   369
                              else (Heap (the_Addr a'),np a');
schirmer@12854
   370
	          n = Inl (fn,C); 
schirmer@12854
   371
                  f = (\<lambda>v. supd (upd_gobj oref n v)) 
schirmer@12854
   372
      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
schirmer@12925
   373
(*
schirmer@12925
   374
 "fvar C stat fn a' s 
schirmer@12925
   375
    \<equiv> let (oref,xf) = if stat then (Stat C,id)
schirmer@12925
   376
                              else (Heap (the_Addr a'),np a');
schirmer@12925
   377
	          n = Inl (fn,C); 
schirmer@12925
   378
                  f = (\<lambda>v. supd (upd_gobj oref n v)) 
schirmer@12925
   379
      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
schirmer@12925
   380
*)
schirmer@12854
   381
  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
schirmer@12854
   382
 "avar G i' a' s 
schirmer@12854
   383
    \<equiv> let   oref = Heap (the_Addr a'); 
schirmer@12854
   384
               i = the_Intg i'; 
schirmer@12854
   385
               n = Inr i;
schirmer@12854
   386
        (T,k,cs) = the_Arr (globs (store s) oref); 
schirmer@12854
   387
               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
schirmer@12854
   388
                                           ArrStore x
schirmer@12854
   389
                              ,upd_gobj oref n v s)) 
schirmer@12854
   390
      in ((the (cs n),f)
schirmer@12854
   391
         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
schirmer@12854
   392
schirmer@12854
   393
lemma fvar_def2: "fvar C stat fn a' s =  
schirmer@12854
   394
  ((the 
schirmer@12854
   395
     (values 
schirmer@12854
   396
      (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
schirmer@12854
   397
      (Inl (fn,C)))
schirmer@12854
   398
   ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
schirmer@12854
   399
                        (Inl (fn,C)) 
schirmer@12854
   400
                        v)))
schirmer@12854
   401
  ,abupd (if stat then id else np a') s)
schirmer@12854
   402
  "
schirmer@12854
   403
apply (unfold fvar_def)
schirmer@12854
   404
apply (simp (no_asm) add: Let_def split_beta)
schirmer@12854
   405
done
schirmer@12854
   406
schirmer@12854
   407
lemma avar_def2: "avar G i' a' s =  
schirmer@12854
   408
  ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
schirmer@12854
   409
           (Inr (the_Intg i')))
schirmer@12854
   410
   ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
schirmer@12854
   411
                                                   (Heap (the_Addr a')))))) 
schirmer@12854
   412
                            ArrStore x
schirmer@12854
   413
                 ,upd_gobj  (Heap (the_Addr a')) 
schirmer@12854
   414
                               (Inr (the_Intg i')) v s')))
schirmer@12854
   415
  ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
schirmer@12854
   416
                   (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
schirmer@12854
   417
          s)"
schirmer@12854
   418
apply (unfold avar_def)
schirmer@12854
   419
apply (simp (no_asm) add: Let_def split_beta)
schirmer@12854
   420
done
schirmer@12854
   421
schirmer@12925
   422
constdefs
schirmer@12925
   423
check_field_access::
schirmer@12925
   424
"prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
schirmer@12925
   425
"check_field_access G accC statDeclC fn stat a' s
schirmer@12925
   426
 \<equiv> let oref = if stat then Stat statDeclC
schirmer@12925
   427
                      else Heap (the_Addr a');
schirmer@12925
   428
       dynC = case oref of
schirmer@12925
   429
                   Heap a \<Rightarrow> obj_class (the (globs (store s) oref))
schirmer@12925
   430
                 | Stat C \<Rightarrow> C;
schirmer@12925
   431
       f    = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC)))
schirmer@12925
   432
   in abupd 
schirmer@12925
   433
        (error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC)
schirmer@12925
   434
                  AccessViolation)
schirmer@12925
   435
        s"
schirmer@12854
   436
schirmer@12925
   437
constdefs
schirmer@12925
   438
check_method_access:: 
schirmer@12925
   439
  "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow>  sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
schirmer@12925
   440
"check_method_access G accC statT mode sig  a' s
schirmer@12925
   441
 \<equiv> let invC = invocation_class mode (store s) a' statT;
schirmer@12925
   442
       dynM = the (dynlookup G statT invC sig)
schirmer@12925
   443
   in abupd 
schirmer@12925
   444
        (error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC)
schirmer@12925
   445
                  AccessViolation)
schirmer@12925
   446
        s"
schirmer@12925
   447
       
schirmer@12854
   448
section "evaluation judgments"
schirmer@12854
   449
schirmer@13337
   450
consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
schirmer@13337
   451
primrec
schirmer@13337
   452
"eval_unop UPlus   v = Intg (the_Intg v)"
schirmer@13337
   453
"eval_unop UMinus  v = Intg (- (the_Intg v))"
schirmer@13337
   454
"eval_unop UBitNot v = Intg 42"                -- "FIXME: Not yet implemented"
schirmer@13337
   455
"eval_unop UNot    v = Bool (\<not> the_Bool v)"
schirmer@13337
   456
schirmer@13337
   457
consts eval_binop :: "binop \<Rightarrow> val \<Rightarrow> val \<Rightarrow> val"
schirmer@13337
   458
primrec
schirmer@13337
   459
"eval_binop Mul     v1 v2 = Intg ((the_Intg v1) * (the_Intg v2))" 
schirmer@13337
   460
"eval_binop Div     v1 v2 = Intg ((the_Intg v1) div (the_Intg v2))"
schirmer@13337
   461
"eval_binop Mod     v1 v2 = Intg ((the_Intg v1) mod (the_Intg v2))"
schirmer@13337
   462
"eval_binop Plus    v1 v2 = Intg ((the_Intg v1) + (the_Intg v2))"
schirmer@13337
   463
"eval_binop Minus   v1 v2 = Intg ((the_Intg v1) - (the_Intg v2))"
schirmer@13337
   464
schirmer@13337
   465
-- "Be aware of the explicit coercion of the shift distance to nat"
schirmer@13337
   466
"eval_binop LShift  v1 v2 = Intg ((the_Intg v1) *   (2^(nat (the_Intg v2))))"
schirmer@13337
   467
"eval_binop RShift  v1 v2 = Intg ((the_Intg v1) div (2^(nat (the_Intg v2))))"
schirmer@13337
   468
"eval_binop RShiftU v1 v2 = Intg 42" --"FIXME: Not yet implemented"
schirmer@13337
   469
schirmer@13337
   470
"eval_binop Less    v1 v2 = Bool ((the_Intg v1) < (the_Intg v2))" 
schirmer@13337
   471
"eval_binop Le      v1 v2 = Bool ((the_Intg v1) \<le> (the_Intg v2))"
schirmer@13337
   472
"eval_binop Greater v1 v2 = Bool ((the_Intg v2) < (the_Intg v1))"
schirmer@13337
   473
"eval_binop Ge      v1 v2 = Bool ((the_Intg v2) \<le> (the_Intg v1))"
schirmer@13337
   474
schirmer@13337
   475
"eval_binop Eq      v1 v2 = Bool (v1=v2)"
schirmer@13337
   476
"eval_binop Neq     v1 v2 = Bool (v1\<noteq>v2)"
schirmer@13337
   477
"eval_binop BitAnd  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
schirmer@13337
   478
"eval_binop And     v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
schirmer@13337
   479
"eval_binop BitXor  v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
schirmer@13337
   480
"eval_binop Xor     v1 v2 = Bool ((the_Bool v1) \<noteq> (the_Bool v2))"
schirmer@13337
   481
"eval_binop BitOr   v1 v2 = Intg 42" -- "FIXME: Not yet implemented"
schirmer@13337
   482
"eval_binop Or      v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
schirmer@13384
   483
"eval_binop CondAnd v1 v2 = Bool ((the_Bool v1) \<and> (the_Bool v2))"
schirmer@13384
   484
"eval_binop CondOr  v1 v2 = Bool ((the_Bool v1) \<or> (the_Bool v2))"
schirmer@13337
   485
schirmer@13384
   486
constdefs need_second_arg :: "binop \<Rightarrow> val \<Rightarrow> bool"
schirmer@13384
   487
"need_second_arg binop v1 \<equiv> \<not> ((binop=CondAnd \<and>  \<not> the_Bool v1) \<or>
schirmer@13384
   488
                               (binop=CondOr  \<and> the_Bool v1))"
schirmer@13384
   489
text {* @{term CondAnd} and @{term CondOr} only evalulate the second argument
schirmer@13384
   490
 if the value isn't already determined by the first argument*}
schirmer@13384
   491
schirmer@13384
   492
lemma need_second_arg_CondAnd [simp]: "need_second_arg CondAnd (Bool b) = b" 
schirmer@13384
   493
by (simp add: need_second_arg_def)
schirmer@13384
   494
schirmer@13384
   495
lemma need_second_arg_CondOr [simp]: "need_second_arg CondOr (Bool b) = (\<not> b)" 
schirmer@13384
   496
by (simp add: need_second_arg_def)
schirmer@13384
   497
schirmer@13384
   498
lemma need_second_arg_strict[simp]: 
schirmer@13384
   499
 "\<lbrakk>binop\<noteq>CondAnd; binop\<noteq>CondOr\<rbrakk> \<Longrightarrow> need_second_arg binop b"
schirmer@13384
   500
by (cases binop) 
schirmer@13384
   501
   (simp_all add: need_second_arg_def)
schirmer@13337
   502
schirmer@12854
   503
consts
schirmer@12854
   504
  eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
schirmer@12854
   505
  halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
schirmer@12854
   506
  sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
schirmer@12854
   507
schirmer@12854
   508
schirmer@12854
   509
syntax
schirmer@12854
   510
eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
schirmer@12854
   511
exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
schirmer@12854
   512
evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
schirmer@12854
   513
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
schirmer@12854
   514
evals::"[prog,state,expr list ,
schirmer@12854
   515
		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
schirmer@12854
   516
hallo::"[prog,state,obj_tag,
schirmer@12854
   517
	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
schirmer@12854
   518
sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
schirmer@12854
   519
schirmer@12854
   520
syntax (xsymbols)
schirmer@12854
   521
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
schirmer@12854
   522
exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
schirmer@12854
   523
evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
schirmer@12854
   524
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
schirmer@12854
   525
evals::"[prog,state,expr list ,
schirmer@12854
   526
		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
schirmer@12854
   527
hallo::"[prog,state,obj_tag,
schirmer@12854
   528
	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
schirmer@12854
   529
sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
schirmer@12854
   530
schirmer@12854
   531
translations
schirmer@12854
   532
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
schirmer@12854
   533
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
schirmer@12854
   534
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
schirmer@12854
   535
  "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
schirmer@12854
   536
  "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
schirmer@12854
   537
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
schirmer@12854
   538
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
schirmer@12854
   539
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
schirmer@12854
   540
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
schirmer@12854
   541
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
schirmer@12854
   542
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
schirmer@12854
   543
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
schirmer@12854
   544
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
schirmer@12854
   545
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
schirmer@12854
   546
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
schirmer@12854
   547
schirmer@12854
   548
inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
schirmer@12854
   549
schirmer@12854
   550
  Abrupt: 
schirmer@12854
   551
  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
schirmer@12854
   552
schirmer@12854
   553
  New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
schirmer@12854
   554
	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
schirmer@12854
   555
		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
schirmer@12854
   556
            \<Longrightarrow>
schirmer@12854
   557
	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
schirmer@12854
   558
schirmer@12854
   559
inductive "sxalloc G" intros (* allocating exception objects for
schirmer@12854
   560
	 	 	      standard exceptions (other than OutOfMemory) *)
schirmer@12854
   561
schirmer@12854
   562
  Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
schirmer@12854
   563
schirmer@12854
   564
  XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
schirmer@12854
   565
schirmer@12854
   566
  SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
schirmer@12854
   567
	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
schirmer@12854
   568
schirmer@13384
   569
text {* 
schirmer@13384
   570
\par
schirmer@13384
   571
*} (* dummy text command to break paragraph for latex;
schirmer@13384
   572
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@13384
   573
schirmer@12854
   574
inductive "eval G" intros
schirmer@12854
   575
schirmer@12854
   576
(* propagation of abrupt completion *)
schirmer@12854
   577
schirmer@12854
   578
  (* cf. 14.1, 15.5 *)
schirmer@12854
   579
  Abrupt: 
schirmer@12854
   580
   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
schirmer@12854
   581
schirmer@12854
   582
schirmer@12854
   583
(* execution of statements *)
schirmer@12854
   584
schirmer@12854
   585
  (* cf. 14.5 *)
schirmer@12854
   586
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
schirmer@12854
   587
schirmer@12854
   588
  (* cf. 14.7 *)
schirmer@12854
   589
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   590
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
schirmer@12854
   591
schirmer@12854
   592
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@13337
   593
                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
schirmer@12854
   594
  (* cf. 14.2 *)
schirmer@12854
   595
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
schirmer@12854
   596
	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   597
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
schirmer@12854
   598
schirmer@12854
   599
schirmer@12854
   600
  (* cf. 14.8.2 *)
schirmer@12854
   601
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
schirmer@12854
   602
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   603
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
schirmer@12854
   604
schirmer@12854
   605
  (* cf. 14.10, 14.10.1 *)
schirmer@12854
   606
  (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
schirmer@12854
   607
  (* A "continue jump" from the while body c is handled by 
schirmer@12854
   608
     this rule. If a continue jump with the proper label was invoked inside c
schirmer@12854
   609
     this label (Cont l) is deleted out of the abrupt component of the state 
schirmer@12854
   610
     before the iterative evaluation of the while statement.
schirmer@12854
   611
     A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
schirmer@12854
   612
  *)
schirmer@12854
   613
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
schirmer@12854
   614
	  if normal s1 \<and> the_Bool b 
schirmer@12854
   615
             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
schirmer@12854
   616
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
schirmer@12854
   617
	     else s3 = s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   618
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
schirmer@12854
   619
schirmer@12854
   620
  Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
schirmer@12854
   621
   
schirmer@12854
   622
  (* cf. 14.16 *)
schirmer@12854
   623
  Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   624
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
schirmer@12854
   625
schirmer@12854
   626
  (* cf. 14.18.1 *)
schirmer@12854
   627
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
schirmer@12854
   628
	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   629
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
schirmer@12854
   630
schirmer@12854
   631
  (* cf. 14.18.2 *)
schirmer@12854
   632
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
schirmer@13337
   633
	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
schirmer@13337
   634
          s3=(if (\<exists> err. x1=Some (Error err)) 
schirmer@13337
   635
              then (x1,s1) 
schirmer@13337
   636
              else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
schirmer@13337
   637
          \<Longrightarrow>
schirmer@13337
   638
          G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
schirmer@12854
   639
  (* cf. 12.4.2, 8.5 *)
schirmer@12854
   640
  Init:	"\<lbrakk>the (class G C) = c;
schirmer@12854
   641
	  if inited C (globs s0) then s3 = Norm s0
schirmer@12854
   642
	  else (G\<turnstile>Norm (init_class_obj G C s0) 
schirmer@12854
   643
		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
schirmer@12854
   644
	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
schirmer@12854
   645
              \<Longrightarrow>
schirmer@12854
   646
		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
schirmer@12925
   647
   (* This class initialisation rule is a little bit inaccurate. Look at the
schirmer@12925
   648
      exact sequence:
schirmer@12925
   649
      1. The current class object (the static fields) are initialised
schirmer@12925
   650
         (init_class_obj)
schirmer@12925
   651
      2. Then the superclasses are initialised
schirmer@12925
   652
      3. The static initialiser of the current class is invoked
schirmer@12925
   653
      More precisely we should expect another ordering, namely 2 1 3.
schirmer@12925
   654
      But we can't just naively toggle 1 and 2. By calling init_class_obj 
schirmer@12925
   655
      before initialising the superclasses we also implicitly record that
schirmer@12925
   656
      we have started to initialise the current class (by setting an 
schirmer@12925
   657
      value for the class object). This becomes 
schirmer@12925
   658
      crucial for the completeness proof of the axiomatic semantics 
schirmer@12925
   659
      (AxCompl.thy). Static initialisation requires an induction on the number 
schirmer@12925
   660
      of classes not yet initialised (or to be more precise, classes where the
schirmer@12925
   661
      initialisation has not yet begun). 
schirmer@12925
   662
      So we could first assign a dummy value to the class before
schirmer@12925
   663
      superclass initialisation and afterwards set the correct values.
schirmer@12925
   664
      But as long as we don't take memory overflow into account 
schirmer@12925
   665
      when allocating class objects, and don't model definite assignment in
schirmer@12925
   666
      the static initialisers, we can leave things as they are for convenience. 
schirmer@12925
   667
   *)
schirmer@12854
   668
(* evaluation of expressions *)
schirmer@12854
   669
schirmer@12854
   670
  (* cf. 15.8.1, 12.4.1 *)
schirmer@12854
   671
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
schirmer@12854
   672
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   673
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
schirmer@12854
   674
schirmer@12854
   675
  (* cf. 15.9.1, 12.4.1 *)
schirmer@12854
   676
  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
schirmer@12854
   677
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
schirmer@12854
   678
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
schirmer@12854
   679
schirmer@12854
   680
  (* cf. 15.15 *)
schirmer@12854
   681
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
schirmer@12854
   682
	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   683
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
schirmer@12854
   684
schirmer@12854
   685
  (* cf. 15.19.2 *)
schirmer@12854
   686
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
schirmer@12854
   687
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
schirmer@12854
   688
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
schirmer@12854
   689
schirmer@12854
   690
  (* cf. 15.7.1 *)
schirmer@12854
   691
  Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
schirmer@12854
   692
schirmer@13337
   693
  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
schirmer@13337
   694
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
schirmer@13384
   695
 
schirmer@13384
   696
  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
schirmer@13384
   697
          G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
schirmer@13384
   698
                \<succ>\<rightarrow> (In1 v2,s2)
schirmer@13384
   699
          \<rbrakk> 
schirmer@13337
   700
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
schirmer@13337
   701
   
schirmer@12854
   702
  (* cf. 15.10.2 *)
schirmer@12854
   703
  Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
schirmer@12854
   704
schirmer@12854
   705
  (* cf. 15.2 *)
schirmer@12854
   706
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   707
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
schirmer@12854
   708
schirmer@12854
   709
  (* cf. 15.25.1 *)
schirmer@12854
   710
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
schirmer@12854
   711
          G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   712
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
schirmer@12854
   713
schirmer@12854
   714
  (* cf. 15.24 *)
schirmer@12854
   715
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
schirmer@12854
   716
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   717
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
schirmer@12854
   718
schirmer@12854
   719
schirmer@12854
   720
  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
schirmer@12854
   721
  Call:	
schirmer@12854
   722
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
schirmer@12854
   723
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
schirmer@12925
   724
    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
schirmer@12925
   725
    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
schirmer@12925
   726
    G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
schirmer@12854
   727
   \<Longrightarrow>
schirmer@12925
   728
       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
schirmer@12925
   729
(* The accessibility check is after init_lvars, to keep it simple. Init_lvars 
schirmer@12925
   730
   already tests for the absence of a null-pointer reference in case of an
schirmer@12925
   731
   instance method invocation
schirmer@12925
   732
*)
schirmer@12854
   733
schirmer@12854
   734
  Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   735
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
schirmer@13337
   736
  (* The local variables l are just a dummy here. The are only used by
schirmer@13337
   737
     the smallstep semantics *)
schirmer@12854
   738
  (* cf. 14.15, 12.4.1 *)
schirmer@12854
   739
  Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@13337
   740
           G\<turnstile>Norm s0 \<midarrow>Body D c
schirmer@13337
   741
            -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
schirmer@13337
   742
  (* The local variables l are just a dummy here. The are only used by
schirmer@13337
   743
     the smallstep semantics *)
schirmer@12854
   744
(* evaluation of variables *)
schirmer@12854
   745
schirmer@12854
   746
  (* cf. 15.13.1, 15.7.2 *)
schirmer@12854
   747
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
schirmer@12854
   748
schirmer@12854
   749
  (* cf. 15.10.1, 12.4.1 *)
schirmer@12925
   750
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
schirmer@12925
   751
	  (v,s2') = fvar statDeclC stat fn a s2;
schirmer@12925
   752
          s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
schirmer@12925
   753
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
schirmer@12925
   754
 (* The accessibility check is after fvar, to keep it simple. Fvar already
schirmer@12925
   755
    tests for the absence of a null-pointer reference in case of an instance
schirmer@12925
   756
    field
schirmer@12925
   757
  *)
schirmer@12854
   758
schirmer@12854
   759
  (* cf. 15.12.1, 15.25.1 *)
schirmer@12854
   760
  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
schirmer@12854
   761
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   762
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
schirmer@12854
   763
schirmer@12854
   764
schirmer@12854
   765
(* evaluation of expression lists *)
schirmer@12854
   766
schirmer@12854
   767
  (* cf. 15.11.4.2 *)
schirmer@12854
   768
  Nil:
schirmer@12854
   769
				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
schirmer@12854
   770
schirmer@12854
   771
  (* cf. 15.6.4 *)
schirmer@12854
   772
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
schirmer@12854
   773
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   774
				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
schirmer@12854
   775
schirmer@12854
   776
(* Rearrangement of premisses:
schirmer@13337
   777
[0,1(Abrupt),2(Skip),8(Do),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
schirmer@13337
   778
 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
schirmer@13337
   779
 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
schirmer@13337
   780
 29(AVar),24(Call)]
schirmer@12854
   781
*)
schirmer@12854
   782
ML {*
schirmer@12854
   783
bind_thm ("eval_induct_", rearrange_prems 
schirmer@13337
   784
[0,1,2,8,4,30,31,27,15,16,
schirmer@13337
   785
 17,18,19,20,21,3,5,25,26,23,6,
schirmer@13337
   786
 7,11,9,13,14,12,22,10,28,
schirmer@13337
   787
 29,24] (thm "eval.induct"))
schirmer@12854
   788
*}
schirmer@12854
   789
schirmer@13337
   790
schirmer@13384
   791
text {* 
schirmer@13384
   792
\par
schirmer@13384
   793
*} (* dummy text command to break paragraph for latex;
schirmer@13384
   794
              large paragraphs exhaust memory of debian pdflatex *)
schirmer@13337
   795
schirmer@12854
   796
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
schirmer@13337
   797
   and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
schirmer@13337
   798
   and and 
schirmer@12854
   799
   s2 (* Fin *) and and s2 (* NewC *)] 
schirmer@12854
   800
schirmer@12854
   801
declare split_if     [split del] split_if_asm     [split del] 
schirmer@12854
   802
        option.split [split del] option.split_asm [split del]
schirmer@12854
   803
inductive_cases halloc_elim_cases: 
schirmer@12854
   804
  "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
schirmer@12854
   805
  "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
schirmer@12854
   806
schirmer@12854
   807
inductive_cases sxalloc_elim_cases:
schirmer@12854
   808
 	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   809
 	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   810
 	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   811
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   812
schirmer@12854
   813
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
schirmer@12854
   814
       \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
schirmer@12854
   815
       \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
schirmer@12854
   816
      \<rbrakk> \<Longrightarrow> P"
schirmer@12854
   817
apply cut_tac 
schirmer@12854
   818
apply (erule sxalloc_cases)
schirmer@12854
   819
apply blast+
schirmer@12854
   820
done
schirmer@12854
   821
schirmer@12854
   822
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
schirmer@12854
   823
declare split_paired_All [simp del] split_paired_Ex [simp del]
schirmer@12854
   824
ML_setup {*
schirmer@12854
   825
simpset_ref() := simpset() delloop "split_all_tac"
schirmer@12854
   826
*}
schirmer@12854
   827
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
schirmer@12854
   828
schirmer@12854
   829
inductive_cases eval_elim_cases:
schirmer@12925
   830
        "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"
schirmer@12925
   831
	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"
schirmer@12925
   832
        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                         \<succ>\<rightarrow> xs'"
schirmer@12925
   833
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"
schirmer@12925
   834
	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
schirmer@12925
   835
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
schirmer@12925
   836
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
schirmer@13337
   837
        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"
schirmer@13337
   838
        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"
schirmer@12925
   839
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
schirmer@12925
   840
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
schirmer@12925
   841
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
schirmer@12925
   842
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"
schirmer@12925
   843
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"
schirmer@12925
   844
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"
schirmer@12925
   845
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"
schirmer@12925
   846
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"
schirmer@12925
   847
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"
schirmer@12925
   848
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"
schirmer@12925
   849
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"
schirmer@12925
   850
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"
schirmer@12925
   851
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"
schirmer@12925
   852
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"
schirmer@12925
   853
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"
schirmer@12925
   854
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"
schirmer@12925
   855
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"
schirmer@12925
   856
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"
schirmer@12925
   857
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"
schirmer@12925
   858
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"
schirmer@12925
   859
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
schirmer@12925
   860
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"
schirmer@12854
   861
declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
schirmer@12854
   862
declare split_paired_All [simp] split_paired_Ex [simp]
schirmer@12854
   863
ML_setup {*
schirmer@12854
   864
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
schirmer@12854
   865
*}
schirmer@12854
   866
declare split_if     [split] split_if_asm     [split] 
schirmer@12854
   867
        option.split [split] option.split_asm [split]
schirmer@12854
   868
schirmer@12854
   869
lemma eval_Inj_elim: 
schirmer@12854
   870
 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
schirmer@12854
   871
 \<Longrightarrow> case t of 
schirmer@12854
   872
       In1 ec \<Rightarrow> (case ec of 
schirmer@12854
   873
                    Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
schirmer@12854
   874
                  | Inr c \<Rightarrow> w = \<diamondsuit>)  
schirmer@12854
   875
     | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
schirmer@12854
   876
     | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
schirmer@12854
   877
apply (erule eval_cases)
schirmer@12854
   878
apply auto
schirmer@12854
   879
apply (induct_tac "t")
schirmer@12854
   880
apply (induct_tac "a")
schirmer@12854
   881
apply auto
schirmer@12854
   882
done
schirmer@12854
   883
schirmer@13337
   884
schirmer@12854
   885
ML_setup {*
schirmer@12854
   886
fun eval_fun nam inj rhs =
schirmer@12854
   887
let
schirmer@12854
   888
  val name = "eval_" ^ nam ^ "_eq"
schirmer@12854
   889
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
schirmer@12854
   890
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
schirmer@12854
   891
	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
schirmer@12854
   892
  fun is_Inj (Const (inj,_) $ _) = true
schirmer@12854
   893
    | is_Inj _                   = false
schirmer@12854
   894
  fun pred (_ $ (Const ("Pair",_) $ _ $ 
schirmer@12854
   895
      (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
schirmer@12854
   896
in
wenzelm@13462
   897
  cond_simproc name lhs pred (thm name)
schirmer@12854
   898
end
schirmer@12854
   899
schirmer@12854
   900
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
schirmer@12854
   901
val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
schirmer@12854
   902
val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
schirmer@12854
   903
val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
schirmer@12854
   904
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
schirmer@12854
   905
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
schirmer@12854
   906
*}
schirmer@12854
   907
schirmer@12854
   908
declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
schirmer@12854
   909
schirmer@13337
   910
text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
schirmer@13337
   911
used in smallstep semantics, not in the bigstep semantics. So their is no
schirmer@13337
   912
valid evaluation of these terms 
schirmer@13337
   913
*}
schirmer@13337
   914
schirmer@13337
   915
schirmer@13337
   916
lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
schirmer@13337
   917
proof -
schirmer@13337
   918
  { fix s t v s'
schirmer@13337
   919
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   920
         normal: "normal s" and
schirmer@13337
   921
         callee: "t=In1l (Callee l e)"
schirmer@13337
   922
    then have "False"
schirmer@13337
   923
    proof (induct)
schirmer@13337
   924
    qed (auto)
schirmer@13337
   925
  }  
schirmer@13337
   926
  then show ?thesis
schirmer@13337
   927
    by (cases s') fastsimp
schirmer@13337
   928
qed
schirmer@13337
   929
schirmer@13337
   930
schirmer@13337
   931
lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
schirmer@13337
   932
proof -
schirmer@13337
   933
  { fix s t v s'
schirmer@13337
   934
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   935
         normal: "normal s" and
schirmer@13337
   936
         callee: "t=In1l (InsInitE c e)"
schirmer@13337
   937
    then have "False"
schirmer@13337
   938
    proof (induct)
schirmer@13337
   939
    qed (auto)
schirmer@13337
   940
  }
schirmer@13337
   941
  then show ?thesis
schirmer@13337
   942
    by (cases s') fastsimp
schirmer@13337
   943
qed
schirmer@13337
   944
schirmer@13337
   945
lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
schirmer@13337
   946
proof -
schirmer@13337
   947
  { fix s t v s'
schirmer@13337
   948
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   949
         normal: "normal s" and
schirmer@13337
   950
         callee: "t=In2 (InsInitV c w)"
schirmer@13337
   951
    then have "False"
schirmer@13337
   952
    proof (induct)
schirmer@13337
   953
    qed (auto)
schirmer@13337
   954
  }  
schirmer@13337
   955
  then show ?thesis
schirmer@13337
   956
    by (cases s') fastsimp
schirmer@13337
   957
qed
schirmer@13337
   958
schirmer@13337
   959
lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
schirmer@13337
   960
proof -
schirmer@13337
   961
  { fix s t v s'
schirmer@13337
   962
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   963
         normal: "normal s" and
schirmer@13337
   964
         callee: "t=In1r (FinA a c)"
schirmer@13337
   965
    then have "False"
schirmer@13337
   966
    proof (induct)
schirmer@13337
   967
    qed (auto)
schirmer@13337
   968
  }  
schirmer@13337
   969
  then show ?thesis
schirmer@13337
   970
    by (cases s') fastsimp 
schirmer@13337
   971
qed
schirmer@12854
   972
schirmer@12854
   973
lemma eval_no_abrupt_lemma: 
schirmer@12854
   974
   "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
schirmer@12854
   975
by (erule eval_cases, auto)
schirmer@12854
   976
schirmer@12854
   977
lemma eval_no_abrupt: 
schirmer@12854
   978
  "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
schirmer@12854
   979
        (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
schirmer@12854
   980
apply auto
schirmer@12854
   981
apply (frule eval_no_abrupt_lemma, auto)+
schirmer@12854
   982
done
schirmer@12854
   983
schirmer@12854
   984
ML {*
schirmer@12854
   985
local
wenzelm@12919
   986
  fun is_None (Const ("Datatype.option.None",_)) = true
schirmer@12854
   987
    | is_None _ = false
schirmer@12854
   988
  fun pred (t as (_ $ (Const ("Pair",_) $
schirmer@12854
   989
     (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
schirmer@12854
   990
in
schirmer@12854
   991
  val eval_no_abrupt_proc = 
wenzelm@13462
   992
  cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
schirmer@12854
   993
          (thm "eval_no_abrupt")
schirmer@12854
   994
end;
schirmer@12854
   995
Addsimprocs [eval_no_abrupt_proc]
schirmer@12854
   996
*}
schirmer@12854
   997
schirmer@12854
   998
schirmer@12854
   999
lemma eval_abrupt_lemma: 
schirmer@12854
  1000
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
schirmer@12854
  1001
by (erule eval_cases, auto)
schirmer@12854
  1002
schirmer@12854
  1003
lemma eval_abrupt: 
schirmer@12854
  1004
 " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
schirmer@12854
  1005
     (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
schirmer@12854
  1006
     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
schirmer@12854
  1007
apply auto
schirmer@12854
  1008
apply (frule eval_abrupt_lemma, auto)+
schirmer@12854
  1009
done
schirmer@12854
  1010
schirmer@12854
  1011
ML {*
schirmer@12854
  1012
local
wenzelm@12919
  1013
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
schirmer@12854
  1014
    | is_Some _ = false
schirmer@12854
  1015
  fun pred (_ $ (Const ("Pair",_) $
schirmer@12854
  1016
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
schirmer@12854
  1017
       x))) $ _ ) = is_Some x
schirmer@12854
  1018
in
schirmer@12854
  1019
  val eval_abrupt_proc = 
wenzelm@13462
  1020
  cond_simproc "eval_abrupt" 
schirmer@12854
  1021
               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
schirmer@12854
  1022
end;
schirmer@12854
  1023
Addsimprocs [eval_abrupt_proc]
schirmer@12854
  1024
*}
schirmer@12854
  1025
schirmer@12854
  1026
schirmer@12854
  1027
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
schirmer@12854
  1028
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1029
by (auto intro!: eval.Lit)
schirmer@12854
  1030
schirmer@12854
  1031
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
schirmer@12854
  1032
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1033
by (auto intro!: eval.Skip)
schirmer@12854
  1034
schirmer@12854
  1035
lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
schirmer@12854
  1036
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1037
by (auto intro!: eval.Expr)
schirmer@12854
  1038
schirmer@12854
  1039
lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2"
schirmer@12854
  1040
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1041
by (auto intro!: eval.Comp)
schirmer@12854
  1042
schirmer@12854
  1043
lemma CondI: 
schirmer@12854
  1044
  "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
schirmer@12854
  1045
         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
schirmer@12854
  1046
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1047
by (auto intro!: eval.Cond)
schirmer@12854
  1048
schirmer@12854
  1049
lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk>
schirmer@12854
  1050
                 \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
schirmer@12854
  1051
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1052
by (auto intro!: eval.If)
schirmer@12854
  1053
schirmer@13337
  1054
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
schirmer@13337
  1055
                \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
schirmer@12854
  1056
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1057
by (auto intro!: eval.Methd)
schirmer@12854
  1058
schirmer@12925
  1059
lemma eval_Call: 
schirmer@12925
  1060
   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
schirmer@12925
  1061
     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
schirmer@12925
  1062
     s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
schirmer@12925
  1063
     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
schirmer@12925
  1064
     G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
schirmer@12925
  1065
       s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
schirmer@12925
  1066
       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
schirmer@12854
  1067
apply (drule eval.Call, assumption)
schirmer@12854
  1068
apply (rule HOL.refl)
schirmer@12854
  1069
apply simp+
schirmer@12854
  1070
done
schirmer@12854
  1071
schirmer@12854
  1072
lemma eval_Init: 
schirmer@12854
  1073
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
schirmer@12854
  1074
  else G\<turnstile>Norm (init_class_obj G C s0)  
schirmer@12854
  1075
         \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
schirmer@12854
  1076
       G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
schirmer@12854
  1077
      s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1078
  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
schirmer@12854
  1079
apply (rule eval.Init)
schirmer@12854
  1080
apply auto
schirmer@12854
  1081
done
schirmer@12854
  1082
schirmer@12854
  1083
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
schirmer@12854
  1084
apply (case_tac "s", simp)
schirmer@12854
  1085
apply (case_tac "a")
schirmer@12854
  1086
apply  safe
schirmer@12854
  1087
apply (rule eval_Init)
schirmer@12854
  1088
apply   auto
schirmer@12854
  1089
done
schirmer@12854
  1090
schirmer@12854
  1091
lemma eval_StatRef: 
schirmer@12854
  1092
"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
schirmer@12854
  1093
apply (case_tac "s", simp)
schirmer@12854
  1094
apply (case_tac "a = None")
schirmer@12854
  1095
apply (auto del: eval.Abrupt intro!: eval.intros)
schirmer@12854
  1096
done
schirmer@12854
  1097
schirmer@12854
  1098
schirmer@12854
  1099
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
schirmer@12854
  1100
apply (erule eval_cases)
schirmer@12854
  1101
by auto
schirmer@12854
  1102
schirmer@12854
  1103
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
schirmer@12854
  1104
by auto
schirmer@12854
  1105
schirmer@12854
  1106
(*unused*)
schirmer@12854
  1107
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
schirmer@12854
  1108
  (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
schirmer@12854
  1109
apply (erule eval.induct)
schirmer@12854
  1110
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
schirmer@12854
  1111
apply auto
schirmer@12854
  1112
done
schirmer@12854
  1113
schirmer@12854
  1114
lemma halloc_xcpt [dest!]: 
schirmer@12854
  1115
  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
schirmer@12854
  1116
apply (erule_tac halloc_elim_cases)
schirmer@12854
  1117
by auto
schirmer@12854
  1118
schirmer@12854
  1119
(*
schirmer@12854
  1120
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
schirmer@12854
  1121
G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
schirmer@12854
  1122
*)
schirmer@12854
  1123
schirmer@12854
  1124
lemma eval_Methd: 
schirmer@13337
  1125
  "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
schirmer@13337
  1126
   \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
schirmer@12854
  1127
apply (case_tac "s")
schirmer@12854
  1128
apply (case_tac "a")
schirmer@12854
  1129
apply clarsimp+
schirmer@12854
  1130
apply (erule eval.Methd)
schirmer@12854
  1131
apply (drule eval_abrupt_lemma)
schirmer@12854
  1132
apply force
schirmer@12854
  1133
done
schirmer@12854
  1134
schirmer@13384
  1135
lemma eval_binop_arg2_indep:
schirmer@13384
  1136
"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
schirmer@13384
  1137
by (cases binop)
schirmer@13384
  1138
   (simp_all add: need_second_arg_def)
schirmer@13384
  1139
schirmer@13384
  1140
schirmer@13384
  1141
lemma eval_BinOp_arg2_indepI:
schirmer@13384
  1142
  assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
schirmer@13384
  1143
          no_need: "\<not> need_second_arg binop v1" 
schirmer@13384
  1144
  shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
schirmer@13384
  1145
         (is "?EvalBinOp v2")
schirmer@13384
  1146
proof -
schirmer@13384
  1147
  from eval_e1 
schirmer@13384
  1148
  have "?EvalBinOp Unit" 
schirmer@13384
  1149
    by (rule eval.BinOp)
schirmer@13384
  1150
       (simp add: no_need)
schirmer@13384
  1151
  moreover
schirmer@13384
  1152
  from no_need 
schirmer@13384
  1153
  have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
schirmer@13384
  1154
    by (simp add: eval_binop_arg2_indep)
schirmer@13384
  1155
  ultimately
schirmer@13384
  1156
  show ?thesis
schirmer@13384
  1157
    by simp
schirmer@13384
  1158
qed
schirmer@13384
  1159
schirmer@12854
  1160
schirmer@12854
  1161
section "single valued"
schirmer@12854
  1162
schirmer@12854
  1163
lemma unique_halloc [rule_format (no_asm)]: 
schirmer@12854
  1164
  "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
schirmer@12854
  1165
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
  1166
apply (erule halloc.induct)
schirmer@12854
  1167
apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
schirmer@12854
  1168
apply (drule trans [THEN sym], erule sym) 
schirmer@12854
  1169
defer
schirmer@12854
  1170
apply (drule trans [THEN sym], erule sym)
schirmer@12854
  1171
apply auto
schirmer@12854
  1172
done
schirmer@12854
  1173
schirmer@12854
  1174
schirmer@12854
  1175
lemma single_valued_halloc: 
schirmer@12854
  1176
  "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
schirmer@12854
  1177
apply (unfold single_valued_def)
schirmer@12854
  1178
by (clarsimp, drule (1) unique_halloc, auto)
schirmer@12854
  1179
schirmer@12854
  1180
schirmer@12854
  1181
lemma unique_sxalloc [rule_format (no_asm)]: 
schirmer@12854
  1182
  "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
schirmer@12854
  1183
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
  1184
apply (erule sxalloc.induct)
schirmer@12854
  1185
apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
schirmer@12854
  1186
              split del: split_if split_if_asm)
schirmer@12854
  1187
done
schirmer@12854
  1188
schirmer@12854
  1189
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
schirmer@12854
  1190
apply (unfold single_valued_def)
schirmer@12854
  1191
apply (blast dest: unique_sxalloc)
schirmer@12854
  1192
done
schirmer@12854
  1193
schirmer@12854
  1194
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
schirmer@12854
  1195
by auto
schirmer@12854
  1196
schirmer@13337
  1197
lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
schirmer@13337
  1198
                   res=the (locals (store s2) Result);
schirmer@13337
  1199
                   s3=abupd (absorb Ret) s2\<rbrakk> \<Longrightarrow>
schirmer@13337
  1200
 G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s3"
schirmer@13337
  1201
by (auto elim: eval.Body)
schirmer@13337
  1202
schirmer@12854
  1203
lemma unique_eval [rule_format (no_asm)]: 
schirmer@12854
  1204
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
schirmer@12854
  1205
apply (case_tac "ws")
schirmer@12854
  1206
apply (simp only:)
schirmer@12854
  1207
apply (erule thin_rl)
schirmer@12854
  1208
apply (erule eval_induct)
schirmer@12854
  1209
apply (tactic {* ALLGOALS (EVERY'
schirmer@12854
  1210
      [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
schirmer@13337
  1211
(* 31 subgoals *)
schirmer@13337
  1212
prefer 28 (* Try *) 
schirmer@12854
  1213
apply (simp (no_asm_use) only: split add: split_if_asm)
schirmer@13337
  1214
(* 34 subgoals *)
schirmer@13337
  1215
prefer 30 (* Init *)
schirmer@12854
  1216
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
schirmer@13337
  1217
prefer 26 (* While *)
schirmer@12854
  1218
apply (simp (no_asm_use) only: split add: split_if_asm, blast)
schirmer@12854
  1219
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
schirmer@12854
  1220
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
schirmer@12854
  1221
apply blast
schirmer@13337
  1222
(* 33 subgoals *)
schirmer@12854
  1223
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
schirmer@12854
  1224
done
schirmer@12854
  1225
schirmer@12854
  1226
(* unused *)
schirmer@12854
  1227
lemma single_valued_eval: 
schirmer@12854
  1228
 "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
schirmer@12854
  1229
apply (unfold single_valued_def)
schirmer@12854
  1230
by (clarify, drule (1) unique_eval, auto)
schirmer@12854
  1231
schirmer@12854
  1232
end