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