src/HOL/Bali/Eval.thy
author schirmer
Mon, 28 Jan 2002 17:00:19 +0100
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     1
(*  Title:      isabelle/Bali/Eval.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
    Copyright   1997 Technische Universitaet Muenchen
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Operational evaluation (big-step) semantics of Java expressions and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
          statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
theory Eval = State + DeclConcepts:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
improvements over Java Specification 1.0:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
\item dynamic method lookup does not need to consider the return type 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
      (cf.15.11.4.4)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
\item throw raises a NullPointer exception if a null reference is given, and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
      each throw of a standard exception yield a fresh exception object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
      (was not specified)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\item if there is not enough memory even to allocate an OutOfMemory exception,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
  evaluation/execution fails, i.e. simply stops (was not specified)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
\item array assignment checks lhs (and may throw exceptions) before evaluating 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
      rhs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
\item fixed exact positions of class initializations 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
      (immediate at first active use)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
\item evaluation vs. (single-step) transition semantics
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
  evaluation semantics chosen, because:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
  \begin{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
  \item[++] less verbose and therefore easier to read (and to handle in proofs)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
  \item[+]  more abstract
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  \item[+]  intermediate values (appearing in recursive rules) need not be 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
     stored explicitly, e.g. no call body construct or stack of invocation 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
     frames containing local variables and return addresses for method calls 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
     needed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
  \item[+]  convenient rule induction for subject reduction theorem
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
  \item[-]  no interleaving (for parallelism) can be described
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
  \item[-]  stating a property of infinite executions requires the meta-level 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
     argument that this property holds for any finite prefixes of it 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
     (e.g. stopped using a counter that is decremented to zero and then 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
     throwing an exception)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
\item unified evaluation for variables, expressions, expression lists, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
      statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
\item the value entry in statement rules is redundant 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
\item the value entry in rules is irrelevant in case of exceptions, but its full
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
  inclusion helps to make the rule structure independent of exception occurence.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
\item as irrelevant value entries are ignored, it does not matter if they are 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
      unique.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
  For simplicity, (fixed) arbitrary values are preferred over "free" values.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
\item the rule format is such that the start state may contain an exception.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
  \item[++] faciliates exception handling
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
  \item[+]  symmetry
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
\item the rules are defined carefully in order to be applicable even in not
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
  type-correct situations (yielding undefined values),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
  e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
  \item[++] fewer rules 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
  \item[-]  less readable because of auxiliary functions like @{text the_Addr}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
  Alternative: "defensive" evaluation throwing some InternalError exception
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
               in case of (impossible, for correct programs) type mismatches
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
\item there is exactly one rule per syntactic construct
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
  \item[+] no redundancy in case distinctions
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
\item halloc fails iff there is no free heap address. When there is
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
  only one free heap address left, it returns an OutOfMemory exception.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
  In this way it is guaranteed that when an OutOfMemory exception is thrown for
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
  the first time, there is a free location on the heap to allocate it.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
\item the allocation of objects that represent standard exceptions is deferred 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
      until execution of any enclosing catch clause, which is transparent to 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
      the program.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
  \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
  \item[-]  requires an auxiliary execution relation
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  \item[++] avoids copies of allocation code and awkward case distinctions 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
           (whether there is enough memory to allocate the exception) in 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
            evaluation rules
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
  \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
\item unfortunately @{text new_Addr} is not directly executable because of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
      Hilbert operator.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
\item local variables are initialized with default values 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
      (no definite assignment)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
\item garbage collection not considered, therefore also no finalizers
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
\item stack overflow and memory overflow during class initialization not 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
      modelled
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
\item exceptions in initializations not replaced by ExceptionInInitializerError
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
types vvar  =         "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
      vals  =        "(val, vvar, val list) sum3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
     "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
     "vals" <= (type)"(val, vvar, val list) sum3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
  dummy_res :: "vals" ("\<diamondsuit>")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
  "\<diamondsuit>" == "In1 Unit"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
  arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
 "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
                     (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
by (simp add: arbitrary3_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
by (simp add: arbitrary3_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
by (simp add: arbitrary3_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
by (simp add: arbitrary3_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
section "exception throwing and catching"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
  throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
 "throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
lemma throw_def2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
 "throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
apply (unfold throw_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  fits    :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
 "G,s\<turnstile>a' fits T  \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
by (simp add: fits_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
lemma fits_Addr_RefT [simp]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  "G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
by (simp add: fits_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
  (\<exists>t. T = RefT t) \<and> a' = Null \<or>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
  (\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and>  G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
apply (unfold fits_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
apply (case_tac "\<exists>pt. T = PrimT pt")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
apply  simp_all
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
apply (case_tac "T")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
defer 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
apply (case_tac "a' = Null")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
apply  simp_all
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
  catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool"      ("_,_\<turnstile>catch _"[61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
 "G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
                    G,store s\<turnstile>Addr (the_Loc xc) fits Class C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
apply (unfold catch_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
lemma catch_XcptLoc [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
  "G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
apply (unfold catch_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
  new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
 "new_xcpt_var vn \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
     \<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
lemma new_xcpt_var_def2 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
 "new_xcpt_var vn (x,s) = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
    Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
apply (unfold new_xcpt_var_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
section "misc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
  assign     :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
 "assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
		   in  (x',if x' = None then s' else s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
lemma assign_Norm_Norm [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
 \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
by (simp add: assign_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
lemma assign_Norm_Norm [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
by (simp add: assign_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
lemma assign_Norm_Some [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
  "\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
   \<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
by (simp add: assign_def Let_def split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
lemma assign_Norm_Some [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
  "\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
   \<Longrightarrow> assign f v (Norm s) = (Some y,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
by (simp add: assign_def Let_def split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
lemma assign_Some [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
"assign f v (Some x,s) = (Some x,s)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
by (simp add: assign_def Let_def split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
lemma assign_supd [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
"assign (\<lambda>v. supd (f v)) v (x,s)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
  = (x, if x = None then f v s else s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
lemma assign_raise_if [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
  "assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
  (raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
apply (case_tac "x = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
lemma assign_raise_if [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
  "assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
                  store = f v (store s)\<rparr>) v s =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
  \<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
   store= if (abrupt s)=None \<and> \<not>b (store s) v 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
             then f v (store s) else (store s)\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
apply (case_tac "abrupt s = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
  init_comp_ty :: "ty \<Rightarrow> stmt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
 "init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
apply (unfold init_comp_ty_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
  target  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
 "target m s a' t 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
    \<equiv> if m = IntVir
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
	 then obj_class (lookup_obj s a') 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
         else the_Class (RefT t)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
 invocation_class  :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
 "invocation_class m s a' statT 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
    \<equiv> (case m of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
         Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
                      then the_Class (RefT statT) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
                      else Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
       | SuperM \<Rightarrow> the_Class (RefT statT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
       | IntVir \<Rightarrow> obj_class (lookup_obj s a'))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
"invocation_declclass G m s a' statT sig 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
   \<equiv> declclass (the (dynlookup G statT 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
                                (invocation_class m s a' statT)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
                                sig))" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
lemma invocation_class_IntVir [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
by (simp add: invocation_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
lemma dynclass_SuperM [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
 "invocation_class SuperM s a' statT = the_Class (RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
by (simp add: invocation_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
lemma invocation_class_notIntVir [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
 "m \<noteq> IntVir \<Longrightarrow> invocation_class m s a' statT = the_Class (RefT statT)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
by (simp add: invocation_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
lemma invocation_class_Static [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
  "invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
                                            then the_Class (RefT statT) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
                                            else Object)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
by (simp add: invocation_class_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
  init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
		   state \<Rightarrow> state"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
 "init_lvars G C sig mode a' pvs 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
   \<equiv> \<lambda> (x,s). 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
      let m = mthd (the (methd G C sig));
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
          l = \<lambda> k. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
              (case k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
                 EName e 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
                   \<Rightarrow> (case e of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
                         VNam v \<Rightarrow> (init_vals (table_of (lcls (mbody m)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
                                                     ((pars m)[\<mapsto>]pvs)) v
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
                       | Res    \<Rightarrow> Some (default_val (resTy m)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
               | This 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
                   \<Rightarrow> (if mode=Static then None else Some a'))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
      in set_lvars l (if mode = Static then x else np a' x,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
  set_lvars 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
    (\<lambda> k. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
       (case k of
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
          EName e 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
            \<Rightarrow> (case e of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
                  VNam v 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
                  \<Rightarrow> (init_vals 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
                       (table_of (lcls (mbody (mthd (the (methd G C sig))))))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
                                 ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
               | Res \<Rightarrow> Some (default_val (resTy (mthd (the (methd G C sig))))))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
        | This 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
            \<Rightarrow> (if mode=Static then None else Some a')))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
    (if mode = Static then x else np a' x,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
apply (unfold init_lvars_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
apply (simp (no_asm) add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
  body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
 "body G C sig \<equiv> let m = the (methd G C sig) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
                 in Body (declclass m) (stmt (mbody (mthd m)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
lemma body_def2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
"body G C sig = Body  (declclass (the (methd G C sig))) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
                      (stmt (mbody (mthd (the (methd G C sig)))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
apply (unfold body_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
section "variables"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
  lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
 "lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
  fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
 "fvar C stat fn a' s 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
    \<equiv> let (oref,xf) = if stat then (Stat C,id)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
                              else (Heap (the_Addr a'),np a');
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
	          n = Inl (fn,C); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
                  f = (\<lambda>v. supd (upd_gobj oref n v)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
      in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
  avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
 "avar G i' a' s 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
    \<equiv> let   oref = Heap (the_Addr a'); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
               i = the_Intg i'; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
               n = Inr i;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
        (T,k,cs) = the_Arr (globs (store s) oref); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
               f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
                                           ArrStore x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
                              ,upd_gobj oref n v s)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
      in ((the (cs n),f)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
         ,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
lemma fvar_def2: "fvar C stat fn a' s =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
  ((the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
     (values 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
      (the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
      (Inl (fn,C)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
   ,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
                        (Inl (fn,C)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
                        v)))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
  ,abupd (if stat then id else np a') s)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
  "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
apply (unfold fvar_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
apply (simp (no_asm) add: Let_def split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
lemma avar_def2: "avar G i' a' s =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
  ((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
           (Inr (the_Intg i')))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
   ,(\<lambda>v (x,s').  (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
                                                   (Heap (the_Addr a')))))) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
                            ArrStore x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
                 ,upd_gobj  (Heap (the_Addr a')) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
                               (Inr (the_Intg i')) v s')))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
  ,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
                   (Heap (the_Addr a'))))))) IndOutBound \<circ> np a')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
          s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
apply (unfold avar_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
apply (simp (no_asm) add: Let_def split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
section "evaluation judgments"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   418
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
  eval   :: "prog \<Rightarrow> (state \<times> term    \<times> vals \<times> state) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
  halloc::  "prog \<Rightarrow> (state \<times> obj_tag \<times> loc  \<times> state) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
  sxalloc:: "prog \<Rightarrow> (state                  \<times> state) set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _"  [61,61,80,   61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
exec ::"[prog,state,stmt      ,state]=>bool"("_|-_ -_-> _"   [61,61,65,   61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
evar ::"[prog,state,var  ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
evals::"[prog,state,expr list ,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
		    val  list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
hallo::"[prog,state,obj_tag,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
	             loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
sallo::"[prog,state        ,state]=>bool"("_|-_ -sxalloc-> _"[61,61,      61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _"  [61,61,80,   61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
exec ::"[prog,state,stmt      ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _"   [61,61,65,   61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
evar ::"[prog,state,var  ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
evals::"[prog,state,expr list ,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
		    val  list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
hallo::"[prog,state,obj_tag,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
	             loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
sallo::"[prog,state,        state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61,      61]60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow>  w___s' " == "(s,t,w___s') \<in> eval G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,  s')" <= "(s,t,w,  s') \<in> eval G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
  "G\<turnstile>s \<midarrow>t   \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
  "G\<turnstile>s \<midarrow>c    \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
  "G\<turnstile>s \<midarrow>c    \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>  ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
  "G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
  "G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<rightarrow> (In2 vf,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>  (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,x,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
  "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow>     s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<rightarrow> (In3 v ,  s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
  "G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow>    s' " == "(s,oi,a,  s') \<in> halloc G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>     (x,s')" <= "(s     ,x,s') \<in> sxalloc G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
  "G\<turnstile>s \<midarrow>sxalloc\<rightarrow>        s' " == "(s     ,  s') \<in> sxalloc G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
  Abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
  New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
		       else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
            \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
	    G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
inductive "sxalloc G" intros (* allocating exception objects for
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
	 	 	      standard exceptions (other than OutOfMemory) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
  Norm:	 "G\<turnstile> Norm              s   \<midarrow>sxalloc\<rightarrow>  Norm             s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
  XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s)  \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
  SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
	  G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
inductive "eval G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
(* propagation of abrupt completion *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
  (* cf. 14.1, 15.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
  Abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
(* execution of statements *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
  (* cf. 14.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
  (* cf. 14.7 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
                                G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
  (* cf. 14.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
	  G\<turnstile>     s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
  (* cf. 14.8.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
  (* cf. 14.10, 14.10.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
  (*      G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
  (* A "continue jump" from the while body c is handled by 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
     this rule. If a continue jump with the proper label was invoked inside c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
     this label (Cont l) is deleted out of the abrupt component of the state 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
     before the iterative evaluation of the while statement.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
     A "break jump" is handled by the Lab Statement (Lab l (while\<dots>).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
  *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
	  if normal s1 \<and> the_Bool b 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
	     else s3 = s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
  Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
  (* cf. 14.16 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
  Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
  (* cf. 14.18.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
	  if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
  (* cf. 14.18.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
	  G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
  (* cf. 12.4.2, 8.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
  Init:	"\<lbrakk>the (class G C) = c;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
	  if inited C (globs s0) then s3 = Norm s0
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
	  else (G\<turnstile>Norm (init_class_obj G C s0) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
              \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
		 G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
(* evaluation of expressions *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
  (* cf. 15.8.1, 12.4.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
  (* cf. 15.9.1, 12.4.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
  NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
  (* cf. 15.15 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
	  s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
  (* cf. 15.19.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
  (* cf. 15.7.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
  Lit:	"G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
  (* cf. 15.10.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
  Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
  (* cf. 15.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
  (* cf. 15.25.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
          G\<turnstile>     s1 \<midarrow>e-\<succ>v  \<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
  (* cf. 15.24 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
  (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
  Call:	
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
         \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s3\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
   \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s3)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
  Methd:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
  (* cf. 14.15, 12.4.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
  Body:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
 G\<turnstile>Norm s0 \<midarrow>Body D c -\<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
(* evaluation of variables *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
  (* cf. 15.13.1, 15.7.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
  (* cf. 15.10.1, 12.4.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
	  (v,s2') = fvar C stat fn a s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
	  G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<rightarrow> s2'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
  (* cf. 15.12.1, 15.25.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
  AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
(* evaluation of expression lists *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
  (* cf. 15.11.4.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
  Nil:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
				    "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
  (* cf. 15.6.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
				   G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
(* Rearrangement of premisses:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
 17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
 7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
 27(AVar),22(Call)]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
bind_thm ("eval_induct_", rearrange_prems 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
[0,1,2,8,4,28,29,25,15,16,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
 17,18,19,3,5,23,24,21,6,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
 7,11,9,13,14,12,20,10,26,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
 27,22] (thm "eval.induct"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
   and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
   s2 (* Fin *) and and s2 (* NewC *)] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
declare split_if     [split del] split_if_asm     [split del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
        option.split [split del] option.split_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
inductive_cases halloc_elim_cases: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
  "G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
  "G\<turnstile>(Norm    s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
inductive_cases sxalloc_elim_cases:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
 	"G\<turnstile> Norm                 s  \<midarrow>sxalloc\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
 	"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
 	"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s';  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
       \<And>s.   \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
       \<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
      \<rbrakk> \<Longrightarrow> P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
apply cut_tac 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
apply (erule sxalloc_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
apply blast+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
declare split_paired_All [simp del] split_paired_Ex [simp del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
simpset_ref() := simpset() delloop "split_all_tac"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
inductive_cases eval_elim_cases:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
        "G\<turnstile>(Some xc,s) \<midarrow>t                         \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
	"G\<turnstile>Norm s \<midarrow>In1l ({statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<rightarrow> xs'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
declare split_paired_All [simp] split_paired_Ex [simp]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
declare split_if     [split] split_if_asm     [split] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
        option.split [split] option.split_asm [split]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
lemma eval_Inj_elim: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
 "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
 \<Longrightarrow> case t of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
       In1 ec \<Rightarrow> (case ec of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
                    Inl e \<Rightarrow> (\<exists>v. w = In1 v) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
                  | Inr c \<Rightarrow> w = \<diamondsuit>)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
     | In2 e \<Rightarrow> (\<exists>v. w = In2 v) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
     | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
apply (erule eval_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
apply (induct_tac "t")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
apply (induct_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
ML_setup {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
fun eval_fun nam inj rhs =
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
let
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
  val name = "eval_" ^ nam ^ "_eq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
	(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
  fun is_Inj (Const (inj,_) $ _) = true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
    | is_Inj _                   = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
  fun pred (_ $ (Const ("Pair",_) $ _ $ 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
      (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
  make_simproc name lhs pred (thm name)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
end
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
val eval_var_proc  =eval_fun "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
val eval_exprs_proc=eval_fun "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
val eval_stmt_proc =eval_fun "stmt" "In1r" "     w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t    \<rightarrow> s'";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc];
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
declare halloc.Abrupt [intro!] eval.Abrupt [intro!]  AbruptIs [intro!] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
lemma eval_no_abrupt_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
   "\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
by (erule eval_cases, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
lemma eval_no_abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
  "G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
        (x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
apply (frule eval_no_abrupt_lemma, auto)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
local
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
  fun is_None (Const ("Option.option.None",_)) = true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
    | is_None _ = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
  fun pred (t as (_ $ (Const ("Pair",_) $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
     (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
  val eval_no_abrupt_proc = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
  make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
          (thm "eval_no_abrupt")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
Addsimprocs [eval_no_abrupt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
lemma eval_abrupt_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
by (erule eval_cases, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
lemma eval_abrupt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
 " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
     (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
apply (frule eval_abrupt_lemma, auto)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
local
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
    | is_Some _ = false
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
  fun pred (_ $ (Const ("Pair",_) $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
       x))) $ _ ) = is_Some x
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
  val eval_abrupt_proc = 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
  make_simproc "eval_abrupt" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
               "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
end;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
Addsimprocs [eval_abrupt_proc]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   821
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   824
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   825
by (auto intro!: eval.Lit)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
by (auto intro!: eval.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
by (auto intro!: eval.Expr)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
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"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   836
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
by (auto intro!: eval.Comp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
lemma CondI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
  "\<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> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
by (auto intro!: eval.Cond)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
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>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
                 \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
by (auto intro!: eval.If)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   850
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   851
apply (case_tac "s", case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   852
by (auto intro!: eval.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
lemma eval_Call: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   855
       D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   856
       G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   857
        \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s3; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   858
       s3' = restore_lvars s2 s3\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
       G\<turnstile>Norm s0 \<midarrow>{statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s3'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
apply (drule eval.Call, assumption)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
apply (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
apply simp+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
lemma eval_Init: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
  else G\<turnstile>Norm (init_class_obj G C s0)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
         \<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
       G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
      s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
  G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
apply (rule eval.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
apply (case_tac "s", simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
apply (case_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
apply (rule eval_Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
apply   auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
lemma eval_StatRef: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
apply (case_tac "s", simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
apply (case_tac "a = None")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
apply (auto del: eval.Abrupt intro!: eval.intros)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
apply (erule eval_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   895
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   897
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   898
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   899
(*unused*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   900
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
  (\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
apply (erule eval.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
lemma halloc_xcpt [dest!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
apply (erule_tac halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   914
G\<turnstile>(x,(h,l)) \<midarrow>s  \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
lemma eval_Methd: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
  "G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
apply (case_tac "s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   920
apply (case_tac "a")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   921
apply clarsimp+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   922
apply (erule eval.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
apply (drule eval_abrupt_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   925
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   926
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   927
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   928
section "single valued"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
lemma unique_halloc [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
  "\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
apply (erule halloc.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
apply  (auto elim!: halloc_elim_cases split del: split_if split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
apply (drule trans [THEN sym], erule sym) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
defer
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
apply (drule trans [THEN sym], erule sym)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   942
lemma single_valued_halloc: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   943
  "single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   944
apply (unfold single_valued_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   945
by (clarsimp, drule (1) unique_halloc, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   948
lemma unique_sxalloc [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   949
  "\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
apply (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
apply (erule sxalloc.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
apply   (auto dest: unique_halloc elim!: sxalloc_elim_cases 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
              split del: split_if split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
apply (unfold single_valued_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
apply (blast dest: unique_sxalloc)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   959
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   960
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   961
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   963
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   964
lemma unique_eval [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
apply (case_tac "ws")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   967
apply (simp only:)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
apply (erule eval_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
apply (tactic {* ALLGOALS (EVERY'
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
      [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
(* 29 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
prefer 26 (* Try *) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   974
apply (simp (no_asm_use) only: split add: split_if_asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
(* 32 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
prefer 28 (* Init *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
prefer 24 (* While *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
apply (simp (no_asm_use) only: split add: split_if_asm, blast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
(* 31 subgoals *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
lemma single_valued_eval: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
 "single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
apply (unfold single_valued_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
by (clarify, drule (1) unique_eval, auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
end