src/HOL/Bali/Eval.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 18249 4398f0f12579
child 21765 89275a3ed7be
permissions -rw-r--r--
simplified code generator setup
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),
schirmer@12854
    61
  e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
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
schirmer@12854
   144
  arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
schirmer@12854
   145
 "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
schirmer@12854
   146
                     (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
schirmer@12854
   147
schirmer@12854
   148
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
schirmer@12854
   149
by (simp add: arbitrary3_def)
schirmer@12854
   150
schirmer@12854
   151
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
schirmer@12854
   152
by (simp add: arbitrary3_def)
schirmer@12854
   153
schirmer@12854
   154
lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"
schirmer@12854
   155
by (simp add: arbitrary3_def)
schirmer@12854
   156
schirmer@12854
   157
lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"
schirmer@12854
   158
by (simp add: arbitrary3_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)
schirmer@12854
   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>
schirmer@12854
   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');
schirmer@12854
   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
schirmer@12854
   477
consts
schirmer@12854
   478
  eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
schirmer@12854
   479
  halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
schirmer@12854
   480
  sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
schirmer@12854
   481
schirmer@12854
   482
schirmer@12854
   483
syntax
schirmer@12854
   484
eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
schirmer@12854
   485
exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
schirmer@12854
   486
evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
schirmer@12854
   487
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
schirmer@12854
   488
evals::"[prog,state,expr list ,
schirmer@12854
   489
		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
schirmer@12854
   490
hallo::"[prog,state,obj_tag,
schirmer@12854
   491
	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
schirmer@12854
   492
sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
schirmer@12854
   493
schirmer@12854
   494
syntax (xsymbols)
schirmer@12854
   495
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
schirmer@12854
   496
exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
schirmer@12854
   497
evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
schirmer@12854
   498
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
schirmer@12854
   499
evals::"[prog,state,expr list ,
schirmer@12854
   500
		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
schirmer@12854
   501
hallo::"[prog,state,obj_tag,
schirmer@12854
   502
	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
schirmer@12854
   503
sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
schirmer@12854
   504
schirmer@12854
   505
translations
schirmer@12854
   506
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
schirmer@12854
   507
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
schirmer@12854
   508
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
schirmer@12854
   509
  "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
schirmer@12854
   510
  "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
schirmer@12854
   511
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
schirmer@12854
   512
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
schirmer@12854
   513
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
schirmer@12854
   514
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
schirmer@12854
   515
  "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
   516
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
schirmer@12854
   517
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
schirmer@12854
   518
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
schirmer@12854
   519
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
schirmer@12854
   520
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
schirmer@12854
   521
schirmer@13688
   522
inductive "halloc G" intros --{* allocating objects on the heap, cf. 12.5 *}
schirmer@12854
   523
schirmer@12854
   524
  Abrupt: 
schirmer@12854
   525
  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
schirmer@12854
   526
schirmer@12854
   527
  New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
schirmer@12854
   528
	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
schirmer@12854
   529
		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
schirmer@12854
   530
            \<Longrightarrow>
schirmer@12854
   531
	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
schirmer@12854
   532
schirmer@13688
   533
inductive "sxalloc G" intros --{* allocating exception objects for
schirmer@13688
   534
	 	 	      standard exceptions (other than OutOfMemory) *}
schirmer@12854
   535
schirmer@12854
   536
  Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
schirmer@12854
   537
schirmer@13688
   538
  Jmp:   "G\<turnstile>(Some (Jump j), s)  \<midarrow>sxalloc\<rightarrow> (Some (Jump j), s)"
schirmer@13688
   539
schirmer@13688
   540
  Error: "G\<turnstile>(Some (Error e), s)  \<midarrow>sxalloc\<rightarrow> (Some (Error e), s)"
schirmer@13688
   541
schirmer@12854
   542
  XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
schirmer@12854
   543
schirmer@12854
   544
  SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
schirmer@12854
   545
	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
schirmer@12854
   546
schirmer@13688
   547
schirmer@12854
   548
inductive "eval G" intros
schirmer@12854
   549
schirmer@13688
   550
--{* propagation of abrupt completion *}
schirmer@12854
   551
schirmer@13688
   552
  --{* cf. 14.1, 15.5 *}
schirmer@12854
   553
  Abrupt: 
schirmer@12854
   554
   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
schirmer@12854
   555
schirmer@12854
   556
schirmer@13688
   557
--{* execution of statements *}
schirmer@12854
   558
schirmer@13688
   559
  --{* cf. 14.5 *}
schirmer@12854
   560
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
schirmer@12854
   561
schirmer@13688
   562
  --{* cf. 14.7 *}
schirmer@12854
   563
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   564
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
schirmer@12854
   565
schirmer@12854
   566
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@13337
   567
                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1"
schirmer@13688
   568
  --{* cf. 14.2 *}
schirmer@12854
   569
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
schirmer@12854
   570
	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   571
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
schirmer@12854
   572
schirmer@13688
   573
  --{* cf. 14.8.2 *}
schirmer@12854
   574
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
schirmer@12854
   575
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   576
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
schirmer@12854
   577
schirmer@13688
   578
  --{* cf. 14.10, 14.10.1 *}
schirmer@13688
   579
  
schirmer@13688
   580
  --{* A continue jump from the while body @{term c} is handled by 
schirmer@13688
   581
     this rule. If a continue jump with the proper label was invoked inside 
schirmer@13688
   582
     @{term c} this label (Cont l) is deleted out of the abrupt component of 
schirmer@13688
   583
     the state before the iterative evaluation of the while statement.
schirmer@13688
   584
     A break jump is handled by the Lab Statement @{text "Lab l (while\<dots>)"}.
schirmer@13688
   585
  *}
schirmer@12854
   586
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
schirmer@13688
   587
	  if the_Bool b 
schirmer@12854
   588
             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
schirmer@12854
   589
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
schirmer@12854
   590
	     else s3 = s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   591
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
schirmer@12854
   592
schirmer@13688
   593
  Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<rightarrow> (Some (Jump j), s)"
schirmer@12854
   594
   
schirmer@13688
   595
  --{* cf. 14.16 *}
schirmer@12854
   596
  Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   597
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
schirmer@12854
   598
schirmer@13688
   599
  --{* cf. 14.18.1 *}
schirmer@12854
   600
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
schirmer@12854
   601
	  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
   602
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
schirmer@12854
   603
schirmer@13688
   604
  --{* cf. 14.18.2 *}
schirmer@12854
   605
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
schirmer@13337
   606
	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2;
schirmer@13337
   607
          s3=(if (\<exists> err. x1=Some (Error err)) 
schirmer@13337
   608
              then (x1,s1) 
schirmer@13337
   609
              else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> 
schirmer@13337
   610
          \<Longrightarrow>
schirmer@13337
   611
          G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
schirmer@13688
   612
  --{* cf. 12.4.2, 8.5 *}
schirmer@12854
   613
  Init:	"\<lbrakk>the (class G C) = c;
schirmer@12854
   614
	  if inited C (globs s0) then s3 = Norm s0
schirmer@12854
   615
	  else (G\<turnstile>Norm (init_class_obj G C s0) 
schirmer@12854
   616
		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
schirmer@12854
   617
	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
schirmer@12854
   618
              \<Longrightarrow>
schirmer@12854
   619
		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
schirmer@13688
   620
   --{* This class initialisation rule is a little bit inaccurate. Look at the
schirmer@12925
   621
      exact sequence:
schirmer@13688
   622
      (1) The current class object (the static fields) are initialised
schirmer@13688
   623
           (@{text init_class_obj}),
schirmer@13688
   624
      (2) the superclasses are initialised,
schirmer@13688
   625
      (3) the static initialiser of the current class is invoked.
schirmer@12925
   626
      More precisely we should expect another ordering, namely 2 1 3.
schirmer@13688
   627
      But we can't just naively toggle 1 and 2. By calling 
schirmer@13688
   628
      @{text init_class_obj} 
schirmer@13688
   629
      before initialising the superclasses, we also implicitly record that
schirmer@12925
   630
      we have started to initialise the current class (by setting an 
schirmer@12925
   631
      value for the class object). This becomes 
schirmer@12925
   632
      crucial for the completeness proof of the axiomatic semantics 
schirmer@13688
   633
      @{text "AxCompl.thy"}. Static initialisation requires an induction on 
schirmer@13688
   634
      the number of classes not yet initialised (or to be more precise, 
schirmer@13688
   635
      classes were the initialisation has not yet begun). 
schirmer@12925
   636
      So we could first assign a dummy value to the class before
schirmer@12925
   637
      superclass initialisation and afterwards set the correct values.
schirmer@12925
   638
      But as long as we don't take memory overflow into account 
schirmer@13688
   639
      when allocating class objects, we can leave things as they are for 
schirmer@13688
   640
      convenience. 
schirmer@13688
   641
   *}
schirmer@13688
   642
--{* evaluation of expressions *}
schirmer@12854
   643
schirmer@13688
   644
  --{* cf. 15.8.1, 12.4.1 *}
schirmer@12854
   645
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
schirmer@12854
   646
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   647
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
schirmer@12854
   648
schirmer@13688
   649
  --{* cf. 15.9.1, 12.4.1 *}
schirmer@12854
   650
  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
schirmer@12854
   651
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
schirmer@12854
   652
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
schirmer@12854
   653
schirmer@13688
   654
  --{* cf. 15.15 *}
schirmer@12854
   655
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
schirmer@12854
   656
	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   657
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
schirmer@12854
   658
schirmer@13688
   659
  --{* cf. 15.19.2 *}
schirmer@12854
   660
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
schirmer@12854
   661
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
schirmer@12854
   662
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
schirmer@12854
   663
schirmer@13688
   664
  --{* cf. 15.7.1 *}
schirmer@12854
   665
  Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
schirmer@12854
   666
schirmer@13337
   667
  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> 
schirmer@13337
   668
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1"
schirmer@13384
   669
 
schirmer@13384
   670
  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; 
schirmer@13384
   671
          G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
schirmer@13384
   672
                \<succ>\<rightarrow> (In1 v2,s2)
schirmer@13384
   673
          \<rbrakk> 
schirmer@13337
   674
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2"
schirmer@13337
   675
   
schirmer@13688
   676
  --{* cf. 15.10.2 *}
schirmer@12854
   677
  Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
schirmer@12854
   678
schirmer@13688
   679
  --{* cf. 15.2 *}
schirmer@12854
   680
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   681
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
schirmer@12854
   682
schirmer@13688
   683
  --{* cf. 15.25.1 *}
schirmer@12854
   684
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
schirmer@12854
   685
          G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   686
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
schirmer@12854
   687
schirmer@13688
   688
  --{* cf. 15.24 *}
schirmer@12854
   689
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
schirmer@12854
   690
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   691
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
schirmer@12854
   692
schirmer@12854
   693
schirmer@13688
   694
-- {* The interplay of  @{term Call}, @{term Methd} and @{term Body}:
schirmer@13688
   695
      Method invocation is split up into these three rules:
schirmer@13688
   696
      \begin{itemize}
schirmer@13688
   697
      \item [@{term Call}] Calculates the target address and evaluates the
schirmer@13688
   698
                           arguments of the method, and then performs dynamic
schirmer@13688
   699
                           or static lookup of the method, corresponding to the
schirmer@13688
   700
                           call mode. Then the @{term Methd} rule is evaluated
schirmer@13688
   701
                           on the calculated declaration class of the method
schirmer@13688
   702
                           invocation.
schirmer@13688
   703
      \item [@{term Methd}] A syntactic bridge for the folded method body.
schirmer@13688
   704
                            It is used by the axiomatic semantics to add the
schirmer@13688
   705
                            proper hypothesis for recursive calls of the method.
schirmer@13688
   706
      \item [@{term Body}] An extra syntactic entity for the unfolded method
schirmer@13688
   707
                           body was introduced to properly trigger class 
schirmer@13688
   708
                           initialisation. Without class initialisation we 
schirmer@13688
   709
                           could just evaluate the body statement. 
schirmer@13688
   710
      \end{itemize}
schirmer@13688
   711
   *}
schirmer@13688
   712
  --{* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *}
schirmer@12854
   713
  Call:	
schirmer@12854
   714
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
schirmer@12854
   715
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
schirmer@12925
   716
    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
schirmer@12925
   717
    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
schirmer@12925
   718
    G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk>
schirmer@12854
   719
   \<Longrightarrow>
schirmer@12925
   720
       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)"
schirmer@13688
   721
--{* The accessibility check is after @{term init_lvars}, to keep it simple. 
schirmer@13688
   722
   @{term init_lvars} already tests for the absence of a null-pointer 
schirmer@13688
   723
   reference in case of an instance method invocation.
schirmer@13688
   724
*}
schirmer@12854
   725
schirmer@12854
   726
  Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   727
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
schirmer@13688
   728
  
schirmer@13688
   729
  Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; 
schirmer@13688
   730
          s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
schirmer@13688
   731
                         abrupt s2 = Some (Jump (Cont l)))
schirmer@13688
   732
                  then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
schirmer@13688
   733
                  else s2)\<rbrakk> \<Longrightarrow>
schirmer@13688
   734
           G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)
schirmer@13688
   735
              \<rightarrow>abupd (absorb Ret) s3"
schirmer@13688
   736
  --{* cf. 14.15, 12.4.1 *}
schirmer@13688
   737
  --{* We filter out a break/continue in @{term s2}, so that we can proof 
schirmer@13688
   738
     definite assignment
schirmer@13688
   739
     correct, without the need of conformance of the state. By this the
schirmer@13688
   740
     different parts of the typesafety proof can be disentangled a little. *}
schirmer@12854
   741
schirmer@13688
   742
--{* evaluation of variables *}
schirmer@13688
   743
schirmer@13688
   744
  --{* cf. 15.13.1, 15.7.2 *}
schirmer@12854
   745
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
schirmer@12854
   746
schirmer@13688
   747
  --{* cf. 15.10.1, 12.4.1 *}
schirmer@12925
   748
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
schirmer@12925
   749
	  (v,s2') = fvar statDeclC stat fn a s2;
schirmer@12925
   750
          s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow>
schirmer@12925
   751
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3"
schirmer@13688
   752
 --{* The accessibility check is after @{term fvar}, to keep it simple. 
schirmer@13688
   753
    @{term fvar} already tests for the absence of a null-pointer reference 
schirmer@13688
   754
    in case of an instance field
schirmer@13688
   755
  *}
schirmer@12854
   756
schirmer@13688
   757
  --{* cf. 15.12.1, 15.25.1 *}
schirmer@12854
   758
  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
schirmer@12854
   759
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   760
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
schirmer@12854
   761
schirmer@12854
   762
schirmer@13688
   763
--{* evaluation of expression lists *}
schirmer@12854
   764
schirmer@13688
   765
  --{* cf. 15.11.4.2 *}
schirmer@12854
   766
  Nil:
schirmer@12854
   767
				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
schirmer@12854
   768
schirmer@13688
   769
  --{* cf. 15.6.4 *}
schirmer@12854
   770
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
schirmer@12854
   771
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   772
				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
schirmer@12854
   773
schirmer@12854
   774
(* Rearrangement of premisses:
schirmer@13688
   775
[0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst),
schirmer@13337
   776
 17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If),
schirmer@13337
   777
 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar),
schirmer@13337
   778
 29(AVar),24(Call)]
schirmer@12854
   779
*)
schirmer@13688
   780
schirmer@12854
   781
ML {*
schirmer@12854
   782
bind_thm ("eval_induct_", rearrange_prems 
schirmer@13337
   783
[0,1,2,8,4,30,31,27,15,16,
schirmer@13337
   784
 17,18,19,20,21,3,5,25,26,23,6,
schirmer@13337
   785
 7,11,9,13,14,12,22,10,28,
schirmer@13337
   786
 29,24] (thm "eval.induct"))
schirmer@12854
   787
*}
schirmer@12854
   788
schirmer@13337
   789
schirmer@12854
   790
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
schirmer@13337
   791
   and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and 
schirmer@13337
   792
   and and 
schirmer@12854
   793
   s2 (* Fin *) and and s2 (* NewC *)] 
schirmer@12854
   794
schirmer@12854
   795
declare split_if     [split del] split_if_asm     [split del] 
schirmer@12854
   796
        option.split [split del] option.split_asm [split del]
schirmer@12854
   797
inductive_cases halloc_elim_cases: 
schirmer@12854
   798
  "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
schirmer@12854
   799
  "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
schirmer@12854
   800
schirmer@12854
   801
inductive_cases sxalloc_elim_cases:
schirmer@12854
   802
 	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
schirmer@13688
   803
        "G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@13688
   804
 	"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@13688
   805
        "G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   806
 	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   807
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
schirmer@12854
   808
schirmer@12854
   809
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
schirmer@12854
   810
       \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
schirmer@13688
   811
       \<And>j s. \<lbrakk>s' = (Some (Jump j),s)\<rbrakk> \<Longrightarrow> P;
schirmer@13688
   812
       \<And>e s. \<lbrakk>s' = (Some (Error e),s)\<rbrakk> \<Longrightarrow> P;
schirmer@12854
   813
       \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
schirmer@12854
   814
      \<rbrakk> \<Longrightarrow> P"
schirmer@12854
   815
apply cut_tac 
schirmer@12854
   816
apply (erule sxalloc_cases)
schirmer@12854
   817
apply blast+
schirmer@12854
   818
done
schirmer@12854
   819
schirmer@12854
   820
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
schirmer@12854
   821
declare split_paired_All [simp del] split_paired_Ex [simp del]
schirmer@12854
   822
ML_setup {*
wenzelm@17876
   823
change_simpset (fn ss => ss delloop "split_all_tac");
schirmer@12854
   824
*}
schirmer@12854
   825
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
schirmer@12854
   826
schirmer@13688
   827
inductive_cases eval_elim_cases [cases set]:
schirmer@12925
   828
        "G\<turnstile>(Some xc,s) \<midarrow>t                              \<succ>\<rightarrow> vs'"
schirmer@12925
   829
	"G\<turnstile>Norm s \<midarrow>In1r Skip                           \<succ>\<rightarrow> xs'"
schirmer@13688
   830
        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                        \<succ>\<rightarrow> xs'"
schirmer@12925
   831
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                         \<succ>\<rightarrow> xs'"
schirmer@12925
   832
	"G\<turnstile>Norm s \<midarrow>In3  ([])                           \<succ>\<rightarrow> vs'"
schirmer@12925
   833
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                         \<succ>\<rightarrow> vs'"
schirmer@12925
   834
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                        \<succ>\<rightarrow> vs'"
schirmer@13337
   835
        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)                  \<succ>\<rightarrow> vs'"
schirmer@13337
   836
        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)            \<succ>\<rightarrow> vs'"
schirmer@12925
   837
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                      \<succ>\<rightarrow> vs'"
schirmer@12925
   838
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                     \<succ>\<rightarrow> vs'"
schirmer@12925
   839
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)                   \<succ>\<rightarrow> vs'"
schirmer@12925
   840
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                        \<succ>\<rightarrow> vs'"
schirmer@12925
   841
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                       \<succ>\<rightarrow> vs'"
schirmer@12925
   842
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                       \<succ>\<rightarrow> xs'"
schirmer@12925
   843
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                      \<succ>\<rightarrow> xs'"
schirmer@12925
   844
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)                  \<succ>\<rightarrow> xs'"
schirmer@12925
   845
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                     \<succ>\<rightarrow> xs'"
schirmer@12925
   846
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)                 \<succ>\<rightarrow> vs'"
schirmer@12925
   847
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)             \<succ>\<rightarrow> xs'"
schirmer@12925
   848
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)                \<succ>\<rightarrow> xs'"
schirmer@12925
   849
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)                \<succ>\<rightarrow> xs'"
schirmer@12925
   850
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                      \<succ>\<rightarrow> xs'"
schirmer@12925
   851
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                       \<succ>\<rightarrow> vs'"
schirmer@12925
   852
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                     \<succ>\<rightarrow> vs'"
schirmer@12925
   853
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                     \<succ>\<rightarrow> vs'"
schirmer@12925
   854
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)       \<succ>\<rightarrow> xs'"
schirmer@12925
   855
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn)   \<succ>\<rightarrow> vs'"
schirmer@12925
   856
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                      \<succ>\<rightarrow> vs'"
schirmer@12925
   857
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
schirmer@12925
   858
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> xs'"
schirmer@12854
   859
declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
schirmer@12854
   860
declare split_paired_All [simp] split_paired_Ex [simp]
schirmer@12854
   861
ML_setup {*
wenzelm@17876
   862
change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
schirmer@12854
   863
*}
schirmer@12854
   864
declare split_if     [split] split_if_asm     [split] 
schirmer@12854
   865
        option.split [split] option.split_asm [split]
schirmer@12854
   866
schirmer@12854
   867
lemma eval_Inj_elim: 
schirmer@12854
   868
 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
schirmer@12854
   869
 \<Longrightarrow> case t of 
schirmer@12854
   870
       In1 ec \<Rightarrow> (case ec of 
schirmer@12854
   871
                    Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
schirmer@12854
   872
                  | Inr c \<Rightarrow> w = \<diamondsuit>)  
schirmer@12854
   873
     | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
schirmer@12854
   874
     | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
schirmer@12854
   875
apply (erule eval_cases)
schirmer@12854
   876
apply auto
schirmer@12854
   877
apply (induct_tac "t")
schirmer@12854
   878
apply (induct_tac "a")
schirmer@12854
   879
apply auto
schirmer@12854
   880
done
schirmer@12854
   881
schirmer@13688
   882
text {* The following simplification procedures set up the proper injections of
schirmer@13688
   883
 terms and their corresponding values in the evaluation relation:
schirmer@13688
   884
 E.g. an expression 
schirmer@13688
   885
 (injection @{term In1l} into terms) always evaluates to ordinary values 
schirmer@13688
   886
 (injection @{term In1} into generalised values @{term vals}). 
schirmer@13688
   887
*}
schirmer@12854
   888
ML_setup {*
schirmer@12854
   889
fun eval_fun nam inj rhs =
schirmer@12854
   890
let
schirmer@12854
   891
  val name = "eval_" ^ nam ^ "_eq"
schirmer@12854
   892
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
schirmer@12854
   893
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
schirmer@12854
   894
	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
schirmer@12854
   895
  fun is_Inj (Const (inj,_) $ _) = true
schirmer@12854
   896
    | is_Inj _                   = false
schirmer@12854
   897
  fun pred (_ $ (Const ("Pair",_) $ _ $ 
schirmer@12854
   898
      (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
schirmer@12854
   899
in
wenzelm@13462
   900
  cond_simproc name lhs pred (thm name)
schirmer@12854
   901
end
schirmer@12854
   902
schirmer@12854
   903
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
   904
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
   905
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
   906
val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
schirmer@12854
   907
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
schirmer@12854
   908
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
schirmer@12854
   909
*}
schirmer@12854
   910
schirmer@12854
   911
declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
schirmer@12854
   912
schirmer@13337
   913
text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only
schirmer@13337
   914
used in smallstep semantics, not in the bigstep semantics. So their is no
schirmer@13337
   915
valid evaluation of these terms 
schirmer@13337
   916
*}
schirmer@13337
   917
schirmer@13337
   918
schirmer@13337
   919
lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False"
schirmer@13337
   920
proof -
schirmer@13337
   921
  { fix s t v s'
schirmer@13337
   922
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   923
         normal: "normal s" and
schirmer@13337
   924
         callee: "t=In1l (Callee l e)"
schirmer@13337
   925
    then have "False"
schirmer@13337
   926
    proof (induct)
schirmer@13337
   927
    qed (auto)
schirmer@13337
   928
  }  
schirmer@13337
   929
  then show ?thesis
schirmer@13337
   930
    by (cases s') fastsimp
schirmer@13337
   931
qed
schirmer@13337
   932
schirmer@13337
   933
schirmer@13337
   934
lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False"
schirmer@13337
   935
proof -
schirmer@13337
   936
  { fix s t v s'
schirmer@13337
   937
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   938
         normal: "normal s" and
schirmer@13337
   939
         callee: "t=In1l (InsInitE c e)"
schirmer@13337
   940
    then have "False"
schirmer@13337
   941
    proof (induct)
schirmer@13337
   942
    qed (auto)
schirmer@13337
   943
  }
schirmer@13337
   944
  then show ?thesis
schirmer@13337
   945
    by (cases s') fastsimp
schirmer@13337
   946
qed
schirmer@13337
   947
schirmer@13337
   948
lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False"
schirmer@13337
   949
proof -
schirmer@13337
   950
  { fix s t v s'
schirmer@13337
   951
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   952
         normal: "normal s" and
schirmer@13337
   953
         callee: "t=In2 (InsInitV c w)"
schirmer@13337
   954
    then have "False"
schirmer@13337
   955
    proof (induct)
schirmer@13337
   956
    qed (auto)
schirmer@13337
   957
  }  
schirmer@13337
   958
  then show ?thesis
schirmer@13337
   959
    by (cases s') fastsimp
schirmer@13337
   960
qed
schirmer@13337
   961
schirmer@13337
   962
lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False"
schirmer@13337
   963
proof -
schirmer@13337
   964
  { fix s t v s'
schirmer@13337
   965
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and
schirmer@13337
   966
         normal: "normal s" and
schirmer@13337
   967
         callee: "t=In1r (FinA a c)"
schirmer@13337
   968
    then have "False"
schirmer@13337
   969
    proof (induct)
schirmer@13337
   970
    qed (auto)
schirmer@13337
   971
  }  
schirmer@13337
   972
  then show ?thesis
schirmer@13337
   973
    by (cases s') fastsimp 
schirmer@13337
   974
qed
schirmer@12854
   975
schirmer@12854
   976
lemma eval_no_abrupt_lemma: 
schirmer@12854
   977
   "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
schirmer@12854
   978
by (erule eval_cases, auto)
schirmer@12854
   979
schirmer@12854
   980
lemma eval_no_abrupt: 
schirmer@12854
   981
  "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
schirmer@12854
   982
        (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
schirmer@12854
   983
apply auto
schirmer@12854
   984
apply (frule eval_no_abrupt_lemma, auto)+
schirmer@12854
   985
done
schirmer@12854
   986
schirmer@12854
   987
ML {*
schirmer@12854
   988
local
wenzelm@12919
   989
  fun is_None (Const ("Datatype.option.None",_)) = true
schirmer@12854
   990
    | is_None _ = false
schirmer@12854
   991
  fun pred (t as (_ $ (Const ("Pair",_) $
schirmer@12854
   992
     (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
schirmer@12854
   993
in
schirmer@12854
   994
  val eval_no_abrupt_proc = 
wenzelm@13462
   995
  cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
schirmer@12854
   996
          (thm "eval_no_abrupt")
schirmer@12854
   997
end;
schirmer@12854
   998
Addsimprocs [eval_no_abrupt_proc]
schirmer@12854
   999
*}
schirmer@12854
  1000
schirmer@12854
  1001
schirmer@12854
  1002
lemma eval_abrupt_lemma: 
schirmer@12854
  1003
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
schirmer@12854
  1004
by (erule eval_cases, auto)
schirmer@12854
  1005
schirmer@12854
  1006
lemma eval_abrupt: 
schirmer@12854
  1007
 " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
schirmer@12854
  1008
     (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
schirmer@12854
  1009
     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
schirmer@12854
  1010
apply auto
schirmer@12854
  1011
apply (frule eval_abrupt_lemma, auto)+
schirmer@12854
  1012
done
schirmer@12854
  1013
schirmer@12854
  1014
ML {*
schirmer@12854
  1015
local
wenzelm@12919
  1016
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
schirmer@12854
  1017
    | is_Some _ = false
schirmer@12854
  1018
  fun pred (_ $ (Const ("Pair",_) $
schirmer@12854
  1019
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
schirmer@12854
  1020
       x))) $ _ ) = is_Some x
schirmer@12854
  1021
in
schirmer@12854
  1022
  val eval_abrupt_proc = 
wenzelm@13462
  1023
  cond_simproc "eval_abrupt" 
schirmer@12854
  1024
               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
schirmer@12854
  1025
end;
schirmer@12854
  1026
Addsimprocs [eval_abrupt_proc]
schirmer@12854
  1027
*}
schirmer@12854
  1028
schirmer@12854
  1029
schirmer@12854
  1030
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
schirmer@12854
  1031
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1032
by (auto intro!: eval.Lit)
schirmer@12854
  1033
schirmer@12854
  1034
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
schirmer@12854
  1035
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1036
by (auto intro!: eval.Skip)
schirmer@12854
  1037
schirmer@12854
  1038
lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
schirmer@12854
  1039
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1040
by (auto intro!: eval.Expr)
schirmer@12854
  1041
schirmer@12854
  1042
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
  1043
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1044
by (auto intro!: eval.Comp)
schirmer@12854
  1045
schirmer@12854
  1046
lemma CondI: 
schirmer@12854
  1047
  "\<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
  1048
         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
schirmer@12854
  1049
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1050
by (auto intro!: eval.Cond)
schirmer@12854
  1051
schirmer@12854
  1052
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
  1053
                 \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
schirmer@12854
  1054
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1055
by (auto intro!: eval.If)
schirmer@12854
  1056
schirmer@13337
  1057
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' 
schirmer@13337
  1058
                \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
schirmer@12854
  1059
apply (case_tac "s", case_tac "a = None")
schirmer@12854
  1060
by (auto intro!: eval.Methd)
schirmer@12854
  1061
schirmer@12925
  1062
lemma eval_Call: 
schirmer@12925
  1063
   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
schirmer@12925
  1064
     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
schirmer@12925
  1065
     s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2;
schirmer@12925
  1066
     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
schirmer@12925
  1067
     G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; 
schirmer@12925
  1068
       s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow>  
schirmer@12925
  1069
       G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'"
schirmer@12854
  1070
apply (drule eval.Call, assumption)
schirmer@12854
  1071
apply (rule HOL.refl)
schirmer@12854
  1072
apply simp+
schirmer@12854
  1073
done
schirmer@12854
  1074
schirmer@12854
  1075
lemma eval_Init: 
schirmer@12854
  1076
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
schirmer@12854
  1077
  else G\<turnstile>Norm (init_class_obj G C s0)  
schirmer@12854
  1078
         \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
schirmer@12854
  1079
       G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
schirmer@12854
  1080
      s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1081
  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
schirmer@12854
  1082
apply (rule eval.Init)
schirmer@12854
  1083
apply auto
schirmer@12854
  1084
done
schirmer@12854
  1085
schirmer@12854
  1086
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
schirmer@12854
  1087
apply (case_tac "s", simp)
schirmer@12854
  1088
apply (case_tac "a")
schirmer@12854
  1089
apply  safe
schirmer@12854
  1090
apply (rule eval_Init)
schirmer@12854
  1091
apply   auto
schirmer@12854
  1092
done
schirmer@12854
  1093
schirmer@12854
  1094
lemma eval_StatRef: 
schirmer@12854
  1095
"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
schirmer@12854
  1096
apply (case_tac "s", simp)
schirmer@12854
  1097
apply (case_tac "a = None")
schirmer@12854
  1098
apply (auto del: eval.Abrupt intro!: eval.intros)
schirmer@12854
  1099
done
schirmer@12854
  1100
schirmer@12854
  1101
schirmer@12854
  1102
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
schirmer@12854
  1103
apply (erule eval_cases)
schirmer@12854
  1104
by auto
schirmer@12854
  1105
schirmer@12854
  1106
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
schirmer@12854
  1107
by auto
schirmer@12854
  1108
schirmer@12854
  1109
(*unused*)
schirmer@12854
  1110
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
schirmer@12854
  1111
  (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
schirmer@12854
  1112
apply (erule eval.induct)
schirmer@12854
  1113
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
schirmer@12854
  1114
apply auto
schirmer@12854
  1115
done
schirmer@12854
  1116
schirmer@12854
  1117
lemma halloc_xcpt [dest!]: 
schirmer@12854
  1118
  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
schirmer@12854
  1119
apply (erule_tac halloc_elim_cases)
schirmer@12854
  1120
by auto
schirmer@12854
  1121
schirmer@12854
  1122
(*
schirmer@12854
  1123
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
schirmer@12854
  1124
G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
schirmer@12854
  1125
*)
schirmer@12854
  1126
schirmer@12854
  1127
lemma eval_Methd: 
schirmer@13337
  1128
  "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') 
schirmer@13337
  1129
   \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
schirmer@12854
  1130
apply (case_tac "s")
schirmer@12854
  1131
apply (case_tac "a")
schirmer@12854
  1132
apply clarsimp+
schirmer@12854
  1133
apply (erule eval.Methd)
schirmer@12854
  1134
apply (drule eval_abrupt_lemma)
schirmer@12854
  1135
apply force
schirmer@12854
  1136
done
schirmer@12854
  1137
schirmer@13688
  1138
lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2;
schirmer@13688
  1139
                   res=the (locals (store s2) Result);
schirmer@13688
  1140
                   s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>
schirmer@13688
  1141
                                  abrupt s2 = Some (Jump (Cont l))) 
schirmer@13688
  1142
                   then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
schirmer@13688
  1143
                   else s2);
schirmer@13688
  1144
                   s4=abupd (absorb Ret) s3\<rbrakk> \<Longrightarrow>
schirmer@13688
  1145
 G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s4"
schirmer@13688
  1146
by (auto elim: eval.Body)
schirmer@13688
  1147
schirmer@13384
  1148
lemma eval_binop_arg2_indep:
schirmer@13384
  1149
"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y"
schirmer@13384
  1150
by (cases binop)
schirmer@13384
  1151
   (simp_all add: need_second_arg_def)
schirmer@13384
  1152
schirmer@13384
  1153
schirmer@13384
  1154
lemma eval_BinOp_arg2_indepI:
schirmer@13384
  1155
  assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and
schirmer@13384
  1156
          no_need: "\<not> need_second_arg binop v1" 
schirmer@13384
  1157
  shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1"
schirmer@13384
  1158
         (is "?EvalBinOp v2")
schirmer@13384
  1159
proof -
schirmer@13384
  1160
  from eval_e1 
schirmer@13384
  1161
  have "?EvalBinOp Unit" 
schirmer@13384
  1162
    by (rule eval.BinOp)
schirmer@13384
  1163
       (simp add: no_need)
schirmer@13384
  1164
  moreover
schirmer@13384
  1165
  from no_need 
schirmer@13384
  1166
  have "eval_binop binop v1 Unit = eval_binop binop v1 v2"
schirmer@13384
  1167
    by (simp add: eval_binop_arg2_indep)
schirmer@13384
  1168
  ultimately
schirmer@13384
  1169
  show ?thesis
schirmer@13384
  1170
    by simp
schirmer@13384
  1171
qed
schirmer@13384
  1172
schirmer@12854
  1173
schirmer@12854
  1174
section "single valued"
schirmer@12854
  1175
schirmer@12854
  1176
lemma unique_halloc [rule_format (no_asm)]: 
schirmer@12854
  1177
  "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
schirmer@12854
  1178
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
  1179
apply (erule halloc.induct)
schirmer@12854
  1180
apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
schirmer@12854
  1181
apply (drule trans [THEN sym], erule sym) 
schirmer@12854
  1182
defer
schirmer@12854
  1183
apply (drule trans [THEN sym], erule sym)
schirmer@12854
  1184
apply auto
schirmer@12854
  1185
done
schirmer@12854
  1186
schirmer@12854
  1187
schirmer@12854
  1188
lemma single_valued_halloc: 
schirmer@12854
  1189
  "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
schirmer@12854
  1190
apply (unfold single_valued_def)
schirmer@12854
  1191
by (clarsimp, drule (1) unique_halloc, auto)
schirmer@12854
  1192
schirmer@12854
  1193
schirmer@12854
  1194
lemma unique_sxalloc [rule_format (no_asm)]: 
schirmer@12854
  1195
  "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
schirmer@12854
  1196
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12854
  1197
apply (erule sxalloc.induct)
schirmer@12854
  1198
apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
schirmer@12854
  1199
              split del: split_if split_if_asm)
schirmer@12854
  1200
done
schirmer@12854
  1201
schirmer@12854
  1202
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
schirmer@12854
  1203
apply (unfold single_valued_def)
schirmer@12854
  1204
apply (blast dest: unique_sxalloc)
schirmer@12854
  1205
done
schirmer@12854
  1206
schirmer@12854
  1207
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
schirmer@12854
  1208
by auto
schirmer@12854
  1209
schirmer@13688
  1210
schirmer@13337
  1211
schirmer@12854
  1212
lemma unique_eval [rule_format (no_asm)]: 
schirmer@12854
  1213
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
schirmer@12854
  1214
apply (case_tac "ws")
berghofe@13601
  1215
apply hypsubst
schirmer@12854
  1216
apply (erule eval_induct)
schirmer@12854
  1217
apply (tactic {* ALLGOALS (EVERY'
schirmer@12854
  1218
      [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
schirmer@13337
  1219
(* 31 subgoals *)
schirmer@13337
  1220
prefer 28 (* Try *) 
schirmer@12854
  1221
apply (simp (no_asm_use) only: split add: split_if_asm)
schirmer@13337
  1222
(* 34 subgoals *)
schirmer@13337
  1223
prefer 30 (* Init *)
schirmer@12854
  1224
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
schirmer@13337
  1225
prefer 26 (* While *)
schirmer@12854
  1226
apply (simp (no_asm_use) only: split add: split_if_asm, blast)
schirmer@12854
  1227
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
schirmer@12854
  1228
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
schirmer@12854
  1229
apply blast
schirmer@13337
  1230
(* 33 subgoals *)
schirmer@12854
  1231
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
schirmer@12854
  1232
done
schirmer@12854
  1233
schirmer@12854
  1234
(* unused *)
schirmer@12854
  1235
lemma single_valued_eval: 
schirmer@12854
  1236
 "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
schirmer@12854
  1237
apply (unfold single_valued_def)
schirmer@12854
  1238
by (clarify, drule (1) unique_eval, auto)
schirmer@12854
  1239
schirmer@12854
  1240
end