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