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