src/HOL/Bali/AxSem.thy
author berghofe
Mon, 11 Dec 2006 16:06:14 +0100
changeset 21765 89275a3ed7be
parent 20014 729a45534001
child 23563 42f2f90b51a6
permissions -rw-r--r--
Adapted to new inductive definition package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/AxSem.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
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Axiomatic semantics of Java expressions and statements 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
          (see also Eval.thy)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
        *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
    10
theory AxSem imports Evaln TypeSafe begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
design issues:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\item a strong version of validity for triples with premises, namely one that 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
      takes the recursive depth needed to complete execution, enables 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
      correctness proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
\item auxiliary variables are handled first-class (-> Thomas Kleymann)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
\item expressions not flattened to elementary assignments (as usual for 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
      axiomatic semantics) but treated first-class => explicit result value 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
      handling
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\item intermediate values not on triple, but on assertion level 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
      (with result entry)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
\item multiple results with semantical substitution mechnism not requiring a 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
      stack 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
\item because of dynamic method binding, terms need to be dependent on state.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
  this is also useful for conditional expressions and statements
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
\item result values in triples exactly as in eval relation (also for xcpt 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
      states)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
\item validity: additional assumption of state conformance and well-typedness,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
  which is required for soundness and thus rule hazard required of completeness
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
restrictions:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
\item all triples in a derivation are of the same type (due to weak 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
      polymorphism)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
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: 13585
diff changeset
    41
types  res = vals --{* result entry *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
  Val  :: "val      \<Rightarrow> res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
  Var  :: "var      \<Rightarrow> res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
  Vals :: "val list \<Rightarrow> res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
  "Val  x"     => "(In1 x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
  "Var  x"     => "(In2 x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
  "Vals x"     => "(In3 x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
  "Val_"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
  "Var_"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
  "Vals_"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> the_In2"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> the_In3"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
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: 13585
diff changeset
    61
  --{* relation on result values, state and auxiliary variables *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
      "res"    <= (type) "AxSem.res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
  assn_imp   :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool"             (infixr "\<Rightarrow>" 25)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
 "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
apply (unfold assn_imp_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
apply (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
section "assertion transformers"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
subsection "peek-and"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
  peek_and   :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    83
 "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    84
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    85
lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    86
apply (unfold peek_and_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    87
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    88
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    89
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    90
lemma peek_and_Not [simp]: "(P \<and>. (\<lambda>s. \<not> f s)) = (P \<and>. Not \<circ> f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    91
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    92
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    93
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    94
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    95
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
lemma peek_and_and [simp]: "peek_and (peek_and P p) p = peek_and P p"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
apply (unfold peek_and_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
lemma peek_and_commut: "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   107
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   108
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   109
  Normal     :: "'a assn \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   110
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   111
  "Normal P" == "P \<and>. normal"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   112
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   113
lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   114
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   115
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   116
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   117
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   118
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   119
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   120
subsection "assn-supd"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   121
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   122
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   123
  assn_supd  :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   124
 "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   126
lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   127
apply (unfold assn_supd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   128
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   129
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   130
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
subsection "supd-assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
  supd_assn  :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
 "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
apply (unfold supd_assn_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
lemma supd_assn_supdD [elim]: "((f .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   147
lemma supd_assn_supdI [elim]: "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   148
apply (auto simp del: split_paired_Ex)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
subsection "subst-res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
  subst_res   :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"              ("_\<leftarrow>_"  [60,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
 "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   156
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   157
lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   158
apply (unfold subst_res_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   159
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   160
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   161
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   162
lemma subst_subst_res [simp]: "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   163
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   164
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   165
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   166
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   167
lemma peek_and_subst_res [simp]: "(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   168
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
apply (rule ext)
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
(*###Do not work for some strange (unification?) reason
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
lemma subst_res_Val_beta [simp]: "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
lemma subst_res_Var_beta [simp]: "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   182
lemma subst_res_Vals_beta [simp]: "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
subsection "subst-Bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
  subst_Bool  :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn"             ("_\<leftarrow>=_" [60,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
 "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemma subst_Bool_def2 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply (unfold subst_Bool_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
lemma subst_Bool_the_BoolI: "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
subsection "peek-res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
  peek_res    :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
 "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
"@peek_res"  :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
  "\<lambda>w:. P"   == "peek_res (\<lambda>w. P)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
apply (unfold peek_res_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
lemma peek_res_subst_res [simp]: "peek_res P\<leftarrow>w = P w\<leftarrow>w"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
lemma peek_subst_res_allI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
 "(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
subsection "ign-res"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
  ign_res    ::  "        'a assn \<Rightarrow> 'a assn"            ("_\<down>" [1000] 1000)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
apply (unfold ign_res_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
lemma ign_ign_res [simp]: "P\<down>\<down> = P\<down>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
lemma ign_subst_res [simp]: "P\<down>\<leftarrow>w = P\<down>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
lemma peek_and_ign_res [simp]: "(P \<and>. p)\<down> = (P\<down> \<and>. p)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
subsection "peek-st"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
  peek_st    :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
 "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
"@peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
  "\<lambda>s.. P"   == "peek_st (\<lambda>s. P)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
apply (unfold peek_st_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
lemma peek_st_triv [simp]: "(\<lambda>s.. P) = P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
lemma peek_st_st [simp]: "(\<lambda>s.. \<lambda>s'.. P s s') = (\<lambda>s.. P s s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
lemma peek_st_split [simp]: "(\<lambda>s.. \<lambda>Y s'. P s Y s') = (\<lambda>Y s. P (store s) Y s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
lemma peek_st_subst_res [simp]: "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
lemma peek_st_Normal [simp]: "(\<lambda>s..(Normal (P s))) = Normal (\<lambda>s.. P s)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
subsection "ign-res-eq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"               ("_\<down>=_"  [60,61] 60)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
 "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
apply (unfold ign_res_eq_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
lemma ign_ign_res_eq [simp]: "(P\<down>=w)\<down> = P\<down>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
lemma ign_res_eq_subst_res: "P\<down>=w\<leftarrow>w = P\<down>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
apply (rule ext)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
lemma subst_Bool_ign_res_eq: "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z  \<and> Y=x)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
subsection "RefVar"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
  RefVar    :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
 "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
  P (Var (fst (vf s))) (snd (vf s))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   348
apply (unfold RefVar_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   349
apply (simp (no_asm) add: split_beta)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   350
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
subsection "allocation"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
  Alloc      :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
 "Alloc G otag P \<equiv> \<lambda>Y s Z.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
  SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
 "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
       (\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
apply (unfold Alloc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
lemma SXAlloc_def2 [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
  "SXAlloc G P Y s Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
apply (unfold SXAlloc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
section "validity"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
  type_ok  :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool"
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: 13585
diff changeset
   379
 "type_ok G t s \<equiv> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   380
    \<exists>L T C A. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   381
                            \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A )
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   382
              \<and> s\<Colon>\<preceq>(G,L)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
                                        ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
types    'a triples = "'a triple set"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
                                         ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
                                         ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
                                         ("{(1_)}/ _#>/ {(1_)}"    [3,65,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   397
  stmt_triple  :: "['a assn, stmt,        'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   398
                                         ("{(1_)}/ ._./ {(1_)}"     [3,65,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   399
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   400
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   401
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   402
  triple       :: "['a assn, term        ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   403
                                         ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   404
  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   405
                                         ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   406
  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   407
                                         ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   408
  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   409
                                         ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   410
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   411
translations
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   412
  "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   413
  "{P} e=\<succ> {Q}" == "{P} In2  e\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   414
  "{P} e\<doteq>\<succ> {Q}" == "{P} In3  e\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   415
  "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   416
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   417
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
13585
db4005b40cc6 Converted Fun to Isar style.
paulson
parents: 13384
diff changeset
   418
apply (rule inj_onI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   419
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   420
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   421
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   422
lemma triple_inj_eq: "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   423
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   424
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
  mtriples  :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
                ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
                                     ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
 "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
 triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
                                                (  "_||=_:_" [61,0, 58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
                                                ( "_,_|=_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
 (\<forall>Y s Z. P Y s Z 
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: 13585
diff changeset
   462
  \<longrightarrow> (\<exists>L. (normal s \<longrightarrow> (\<exists> C T A. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   463
                   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>t\<guillemotright>A)) \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   464
           s\<Colon>\<preceq>(G,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: 13585
diff changeset
   465
  \<longrightarrow> (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
apply (unfold triple_valid_def type_ok_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
declare split_paired_All [simp del] split_paired_Ex [simp del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
declare split_if     [split del] split_if_asm     [split del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
        option.split [split del] option.split_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
ML_setup {*
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 16417
diff changeset
   475
change_simpset (fn ss => ss delloop "split_all_tac");
b9c92f384109 change_claset/simpset;
wenzelm
parents: 16417
diff changeset
   476
change_claset (fn cs => cs delSWrapper "split_all_tac");
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   479
inductive2
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   480
  ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   481
  and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   482
  for G :: prog
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   483
where
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   485
  "G,A \<turnstile>t \<equiv> G,A|\<turnstile>{t}"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   486
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   487
| empty: " G,A|\<turnstile>{}"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   488
| insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
          G,A|\<turnstile>insert t ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   491
| asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
(* could be added for convenience and efficiency, but is not necessary
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
  cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
           G,A |\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
*)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   497
| weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   499
| conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
         (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
                                 Q  Y' s' Z ))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
                                         \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   504
| hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   506
| Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
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: 13585
diff changeset
   508
  --{* variables *}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   509
| LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   511
| FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
          G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   513
                                 G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   515
| AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
          \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
                                 G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
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: 13585
diff changeset
   518
  --{* expressions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   520
| NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
                                 G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   523
| NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
	  {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
                                 G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   527
| Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
          abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
                                 G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   531
| Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
                  Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
                                 G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   535
| Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   537
| UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   538
          \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   539
          G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   540
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   541
| BinOp:
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   542
   "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   543
     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   544
               (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   545
               {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   546
    \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   547
    G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   548
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   549
| Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   551
| Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
                                 G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   554
| Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
     \<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
                                 G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   558
| Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
                                 G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   562
| Call: 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
  \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
 (\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
      invC = invocation_class mode (store s) a statT \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
         l = locals (store s)) ;.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
      init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
      (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
 Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
   571
         G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   573
| Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
                                 G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   576
| Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
  G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
    \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
                                 G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
  
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: 13585
diff changeset
   581
  --{* expression lists *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   583
| Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   585
| Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
          \<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
                                 G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
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: 13585
diff changeset
   589
  --{* statements *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   591
| Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   593
| Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
                                 G,A\<turnstile>{Normal P} .Expr e. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   596
| Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
                           G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   599
| Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
          G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
                                 G,A\<turnstile>{Normal P} .c1;;c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   603
| If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
                                 G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
(* unfolding variant of Loop, not needed here
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
  LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
         \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
*)
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   611
| Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
          G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
                            G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
  
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   615
| Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   617
| Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
                                 G,A\<turnstile>{Normal P} .Throw e. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   620
| Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
          G,A\<turnstile>{Q \<and>. (\<lambda>s.  G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
              (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
                                 G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   625
| Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
      \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
              .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
                                 G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   630
| Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   632
| Init: "\<lbrakk>the (class G C) = c;
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
              .(if C = Object then Skip else Init (super c)). {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
              .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
                               G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   639
-- {* Some dummy rules for the intermediate terms @{text Callee},
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   640
@{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   641
semantics.
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   642
*}
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   643
| InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   644
| InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   645
| Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
   646
| FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
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: 13585
diff changeset
   647
(*
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   648
axioms 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   649
*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
 adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
"adapt_pre P Q Q'\<equiv>\<lambda>Y s Z. \<forall>Y' s'. \<exists>Z'. P Y s Z' \<and> (Q Y' s' Z' \<longrightarrow> Q' Y' s' Z)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
section "rules derived by induction"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
apply (unfold ax_valids_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
(*if cut is available
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
Goal "\<lbrakk>G,A'|\<turnstile>ts; A' \<subseteq> A; \<forall>P Q t. {P} t\<succ> {Q} \<in> A' \<longrightarrow> (\<exists>T. (G,L)\<turnstile>t\<Colon>T) \<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
       G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
b y etac ax_derivs.cut 1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
b y eatac ax_derivs.asm 1 1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
qed "ax_thin";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
lemma ax_thin [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
  "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
apply (erule ax_derivs.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
apply                (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
apply                (rule ax_derivs.empty)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
apply               (erule (1) ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
apply              (fast intro: ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
(*apply           (fast intro: ax_derivs.cut) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
apply            (fast intro: ax_derivs.weaken)
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   679
apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   680
(* 37 subgoals *)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   681
prefer 18 (* Methd *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
                     THEN_ALL_NEW Blast_tac) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
apply   clarify 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
apply   blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
apply   (rule allI)+ 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
apply   (drule spec)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
apply   blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
apply (erule ax_thin)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
lemma subset_mtriples_iff: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
  "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
apply (rule subset_image_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
lemma weaken: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
 "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
apply (erule ax_derivs.induct)
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   708
(*42 subgoals*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
apply       (tactic "ALLGOALS strip_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
apply       (tactic "TRYALL hyp_subst_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
apply       (simp, rule ax_derivs.empty)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
apply      (drule subset_insertD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
apply      (blast intro: ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
apply     (fast intro: ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
(*apply  (blast intro: ax_derivs.cut) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
apply   (fast intro: ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   720
(*37 subgoals*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
                   THEN_ALL_NEW Fast_tac) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
(*1 subgoal*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
apply (clarsimp simp add: subset_mtriples_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
apply (rule ax_derivs.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
apply (erule impE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
apply  (rule exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
apply  (erule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
apply  (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
oops (* dead end, Methd is to blame *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
section "rules derived from conseq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
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: 13585
diff changeset
   736
text {* In the following rules we often have to give some type annotations like:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   737
 @{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   738
Given only the term above without annotations, Isabelle would infer a more 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   739
general type were we could have 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   740
different types of auxiliary variables in the assumption set (@{term A}) and 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   741
in the triple itself (@{term P} and @{term Q}). But 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   742
@{text "ax_derivs.Methd"} enforces the same type in the inductive definition 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: 13585
diff changeset
   743
the derivation. So we have to restrict the types to be able to apply 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: 13585
diff changeset
   744
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: 13585
diff changeset
   745
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   746
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
  Q Y' s' Z)\<rbrakk>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
  \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"
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: 13585
diff changeset
   750
apply (rule ax_derivs.conseq)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
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: 13585
diff changeset
   755
-- {* Nice variant, since it is so symmetric we might be able to memorise it. *}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   756
lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'.  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
       (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
       (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  Y' s' Z)\<rbrakk>  
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: 13585
diff changeset
   759
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn } t\<succ> {Q }"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
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: 13585
diff changeset
   764
lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
 \<forall>Y s Z. P Y s Z \<longrightarrow> (\<forall>Y' s'. (\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
  Q Y' s' Z)\<rbrakk>  
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: 13585
diff changeset
   767
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q }"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
apply (erule conseq12')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
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: 13585
diff changeset
   772
lemma conseq1: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   773
 \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
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: 13585
diff changeset
   778
lemma conseq2: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   779
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
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: 13585
diff changeset
   784
lemma ax_escape: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   785
 "\<lbrakk>\<forall>Y s Z. P Y s Z 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   786
   \<longrightarrow> G,(A::'a triple set)\<turnstile>{\<lambda>Y' s' (Z'::'a). (Y',s') = (Y,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: 13585
diff changeset
   787
                             t\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   788
                            {\<lambda>Y s Z'. Q Y s Z}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   789
\<rbrakk> \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q::'a assn}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   790
apply (rule ax_derivs.conseq)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
(* unused *)
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: 13585
diff changeset
   795
lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   796
\<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
apply (rule ax_escape (* unused *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
apply (rule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
apply  fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
(*alternative (more direct) proof:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
apply (rule ax_derivs.conseq) *)(* unused *)(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
apply (fast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
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: 13585
diff changeset
   809
lemma ax_impossible [intro]: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   810
  "G,(A::'a triple set)\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q::'a assn}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
done
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: 13585
diff changeset
   819
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   820
lemma ax_nochange:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   821
 "G,(A::(res \<times> state) triple set)\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   822
  \<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   824
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   825
apply (erule (1) ax_nochange_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
(* unused *)
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: 13585
diff changeset
   829
lemma ax_trivial: "G,(A::'a triple set)\<turnstile>{P::'a assn}  t\<succ> {\<lambda>Y s Z. True}"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   830
apply (rule ax_derivs.conseq(* unused *))
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
(* unused *)
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: 13585
diff changeset
   835
lemma ax_disj: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   836
 "\<lbrakk>G,(A::'a triple set)\<turnstile>{P1::'a assn} t\<succ> {Q1}; G,A\<turnstile>{P2::'a assn} t\<succ> {Q2}\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   837
  \<Longrightarrow>  G,A\<turnstile>{\<lambda>Y s Z. P1 Y s Z \<or> P2 Y s Z} t\<succ> {\<lambda>Y s Z. Q1 Y s Z \<or> Q2 Y s Z}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
apply (rule ax_escape (* unused *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
apply  (erule conseq12, fast)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
(* unused *)
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: 13585
diff changeset
   844
lemma ax_supd_shuffle: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   845
 "(\<exists>Q. G,(A::'a triple set)\<turnstile>{P::'a assn} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
       (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
apply (best elim!: conseq1 conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
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: 13585
diff changeset
   850
lemma ax_cases: "
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   851
 \<lbrakk>G,(A::'a triple set)\<turnstile>{P \<and>.       C} t\<succ> {Q::'a assn};  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   852
                   G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
apply (unfold peek_and_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   855
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   856
apply (case_tac "C s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   857
apply  (erule conseq12, force)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   858
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
(*alternative (more direct) proof:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
apply (case_tac "C s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
apply  force+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
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: 13585
diff changeset
   866
lemma ax_adapt: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   867
  \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
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: 13585
diff changeset
   873
lemma adapt_pre_adapts: "G,(A::'a triple set)\<Turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   874
\<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
apply (simp add: ax_valids_def triple_valid_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
lemma adapt_pre_weakest: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
"\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
  P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
apply (drule_tac x = "{}" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
apply (drule_tac x = "In1r Skip" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
apply (simp add: ax_valids_def triple_valid_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
oops
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
lemma peek_and_forget1_Normal: 
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: 13585
diff changeset
   892
 "G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   893
 \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   895
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   897
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: 13585
diff changeset
   898
lemma peek_and_forget1: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   899
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   900
 \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
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: 13585
diff changeset
   907
lemma peek_and_forget2: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   908
"G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q \<and>. 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: 13585
diff changeset
   909
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
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: 13585
diff changeset
   914
lemma ax_subst_Val_allI: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   915
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {(Q v)::'a assn}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   916
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
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: 13585
diff changeset
   920
lemma ax_subst_Var_allI: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   921
"\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {(Q v)::'a assn}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   922
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   925
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: 13585
diff changeset
   926
lemma ax_subst_Vals_allI: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   927
"(\<forall>v. G,(A::'a triple set)\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {(Q v)::'a assn})
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   928
 \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
section "alternative axioms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
lemma ax_Lit2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
apply (rule ax_derivs.Lit [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
lemma ax_Lit2_test_complete: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   942
apply (rule ax_Lit2 [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   943
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   944
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   945
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
lemma ax_LVar2: "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} LVar vn=\<succ> {Normal (\<lambda>s.. P\<down>=Var (lvar vn s))}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
apply (rule ax_derivs.LVar [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   948
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   949
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
  {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
apply (rule ax_derivs.Super [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
lemma ax_Nil2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   959
apply (rule ax_derivs.Nil [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   960
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   961
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   963
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   964
section "misc derived structural rules"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   967
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
    G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
       G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
apply (frule (1) finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
apply (erule finite_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   974
apply  (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
lemma ax_derivs_insertD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
 "G,(A::'a triple set)|\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
apply (fast intro: ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
lemma ax_methods_spec: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
apply (erule ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
apply (force del: image_eqI intro: rev_image_eqI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
(* this version is used to avoid using the cut rule *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
  ((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
apply (frule (1) finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
apply (erule finite_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   999
apply  clarsimp+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
apply (drule ax_derivs_insertD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
apply (rule ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
apply  (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
apply  (auto elim: ax_methods_spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1004
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
lemma ax_no_hazard: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
  "G,(A::'a triple set)\<turnstile>{P \<and>. type_ok G t} t\<succ> {Q::'a assn} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
apply (erule ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1010
apply (rule ax_derivs.hazard [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
apply force
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
lemma ax_free_wt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1015
 "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
  \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1017
  G,A\<turnstile>{Normal P} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
apply (rule ax_no_hazard)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1019
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1021
apply (erule mp [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1022
apply  (auto simp add: type_ok_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1023
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1024
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1025
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1026
bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1028
declare ax_Abrupts [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 20014
diff changeset
  1030
lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1031
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1032
lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1033
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1034
apply  (rule ax_derivs.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1035
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1036
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1037
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1038
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1039
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1040
section "derived rules for methd call"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1041
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1042
lemma ax_Call_known_DynT: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
  \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
  init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
    Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
  \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1048
       {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
                     C = invocation_declclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1050
                            G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
       G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12859
diff changeset
  1052
   \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1053
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1055
apply  (erule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1056
apply (rule ax_escape, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1057
apply (drule spec, drule spec, drule spec,erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1058
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1059
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1060
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1061
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1062
lemma ax_Call_Static: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
 "\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
               init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1065
              Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
  G,A\<turnstile>{Normal P} e-\<succ> {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
  \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
  \<and>. (\<lambda> s. C=invocation_declclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
                G Static (store s) 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: 12859
diff changeset
  1070
\<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1073
apply  (erule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1074
apply (rule ax_escape, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1075
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1076
apply (drule spec,drule spec,drule spec, erule conseq12)
20014
729a45534001 fixed let-simproc
schirmer
parents: 19685
diff changeset
  1077
apply (force simp add: init_lvars_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
lemma ax_Methd1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
 "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
       G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
apply (drule ax_derivs.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
apply (erule (1) ax_methods_spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
lemma ax_MethdN: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
"G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
          {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
      G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
apply (rule ax_Methd1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
apply  (rule_tac [2] singletonI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1096
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1097
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1098
lemma ax_StatRef: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1100
apply (rule ax_derivs.Cast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
apply (rule ax_Lit2 [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1102
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1105
section "rules derived from Init and Done"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1106
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
  lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
     \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
            .init c. {set_lvars l .; R};   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
         G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1111
  .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
  G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1113
apply (erule ax_derivs.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
apply assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1117
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1118
lemma ax_Init_Skip_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1119
"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1120
  .Skip. {(set_lvars l .; P)::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1121
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1122
apply (rule ax_SkipI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1123
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1124
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1125
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1126
lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1127
       P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1128
       G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
       G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1130
apply (rule_tac C = "initd C" in ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1132
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1133
apply (erule (1) ax_InitS)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1134
apply  simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1135
apply  (rule ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1136
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1137
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1138
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1139
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1140
lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1141
  {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1142
       .Init Object. {(P \<and>. initd Object)::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1143
apply (rule ax_derivs.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1144
apply   (drule class_Object, force)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1145
apply (simp_all (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1146
apply (rule_tac [2] ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1147
apply (rule ax_SkipI, force)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1148
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1149
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1150
lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1151
       (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1152
  G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
apply (rule_tac C = "initd Object" in ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1155
apply (erule ax_Init_Object [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1157
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
section "introduction rules for Alloc and SXAlloc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
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: 13585
diff changeset
  1162
lemma ax_SXAlloc_Normal: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1163
 "G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1164
 \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1165
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1167
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1168
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1169
lemma ax_Alloc: 
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: 13585
diff changeset
  1170
  "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1171
     {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<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: 13585
diff changeset
  1172
      Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1173
      heap_free (Suc (Suc 0))}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1174
   \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1175
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1176
apply (auto elim!: halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1177
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1179
lemma ax_Alloc_Arr: 
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: 13585
diff changeset
  1180
 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1181
   {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1182
    (\<forall>a. new_Addr (heap s) = Some a \<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: 13585
diff changeset
  1183
    Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1184
    heap_free (Suc (Suc 0))} 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1185
 \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1186
 G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1187
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1188
apply (auto elim!: halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1189
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1191
lemma ax_SXAlloc_catch_SXcpt: 
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: 13585
diff changeset
  1192
 "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1193
     {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1194
      (\<forall>a. new_Addr (heap s) = Some a \<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: 13585
diff changeset
  1195
      Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1196
      \<and>. heap_free (Suc (Suc 0))}\<rbrakk> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
  1197
 \<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: 13585
diff changeset
  1198
 G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1199
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1200
apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1201
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1202
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1203
end