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