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