src/HOL/Bali/AxSem.thy
author schirmer
Wed, 05 Jul 2006 11:32:38 +0200
changeset 20014 729a45534001
parent 19685 4477003648cc
child 21765 89275a3ed7be
permissions -rw-r--r--
fixed let-simproc ----------------------------------------------------------------------
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)
19685
4477003648cc ax_derivs: precise typing;
wenzelm
parents: 17876
diff changeset
   438
    ax_derivs :: "prog \<Rightarrow> ('a triples \<times> 'a triples) set"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
syntax
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
                                                (  "_||=_:_" [61,0, 58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
                                                ( "_,_|=_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
                                                ("_,_||-_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
                                                ( "_,_|-_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
syntax (xsymbols)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
 triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
                                                ("_,_|\<turnstile>_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
                                                ( "_,_\<turnstile>_"   [61,58,58] 57)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
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
   463
                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
                          (\<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
   465
translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
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
   467
translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
                     "G,A|\<turnstile>ts" == "(A,ts) \<in> ax_derivs G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
                     "G,A \<turnstile>t"  == "G,A|\<turnstile>{t}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
 (\<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
   473
  \<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
   474
                   \<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
   475
           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
   476
  \<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
   477
apply (unfold triple_valid_def type_ok_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
declare split_paired_All [simp del] split_paired_Ex [simp del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
declare split_if     [split del] split_if_asm     [split del] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
        option.split [split del] option.split_asm [split del]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
ML_setup {*
17876
b9c92f384109 change_claset/simpset;
wenzelm
parents: 16417
diff changeset
   486
change_simpset (fn ss => ss delloop "split_all_tac");
b9c92f384109 change_claset/simpset;
wenzelm
parents: 16417
diff changeset
   487
change_claset (fn cs => cs delSWrapper "split_all_tac");
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
inductive "ax_derivs G" intros
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
  empty: " G,A|\<turnstile>{}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
  insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
          G,A|\<turnstile>insert t ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
  asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
(* could be added for convenience and efficiency, but is not necessary
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
  cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
           G,A |\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
  weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
  conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
         (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
                                 Q  Y' s' Z ))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
                                         \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
  hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
  Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
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
   513
  --{* variables *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
  LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
  FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
          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
   518
                                 G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
  AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
          \<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
   522
                                 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
   523
  --{* expressions *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
  NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
                                 G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
  NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
	  {\<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
   530
                                 G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
  Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
          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
   534
                                 G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
  Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
                  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
   538
                                 G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
  Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   542
  UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   543
          \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   544
          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
   545
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   546
  BinOp:
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   547
   "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
13384
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   548
     \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   549
               (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
a34e38154413 Added conditional and (&&) and or (||).
schirmer
parents: 13337
diff changeset
   550
               {\<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
   551
    \<Longrightarrow>
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   552
    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
   553
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
  Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
  Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
                                 G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
  Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
     \<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
   561
                                 G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
  Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
          \<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
   565
                                 G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
  Call: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
"\<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
   569
  \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
 (\<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
   571
      invC = invocation_class mode (store s) a statT \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
         l = locals (store s)) ;.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
      init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
      (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
 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
   576
         G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
  Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
                                 G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
  Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
  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
   583
    \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
                                 G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
  
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
   586
  --{* expression lists *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
  Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
  Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
          \<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
   592
                                 G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
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
   594
  --{* statements *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
  Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
  Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   599
                                 G,A\<turnstile>{Normal P} .Expr e. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   601
  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
                           G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
  Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
          G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
                                 G,A\<turnstile>{Normal P} .c1;;c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
  If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
          \<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
   610
                                 G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
(* unfolding variant of Loop, not needed here
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
  LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
          \<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
   614
         \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
  Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
          G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
                            G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
  
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   620
  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
   621
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
  Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
                                 G,A\<turnstile>{Normal P} .Throw e. {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
  Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
          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
   627
              (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
                                 G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
  Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
      \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
              .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
                                 G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
  Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
  Init: "\<lbrakk>the (class G C) = c;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
              .(if C = Object then Skip else Init (super c)). {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
              .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
                               G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   644
-- {* 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
   645
@{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
   646
semantics.
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   647
*}
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
   648
  InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<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
   649
  InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
13337
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   650
  Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   651
  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
   652
(*
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   653
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
   654
*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
 adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
"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
   659
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
section "rules derived by induction"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
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
   664
apply (unfold ax_valids_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
(*if cut is available
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
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
   670
       G,A|\<turnstile>ts"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
b y etac ax_derivs.cut 1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
b y eatac ax_derivs.asm 1 1;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
qed "ax_thin";
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
lemma ax_thin [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
  "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
   677
apply (erule ax_derivs.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
apply                (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
apply                (rule ax_derivs.empty)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
apply               (erule (1) ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
apply              (fast intro: ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
(*apply           (fast intro: ax_derivs.cut) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
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
   684
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
   685
(* 37 subgoals *)
f75dfc606ac7 Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents: 12925
diff changeset
   686
prefer 18 (* Methd *)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
                     THEN_ALL_NEW Blast_tac) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
apply   clarify 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
apply   blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
apply   (rule allI)+ 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
apply   (drule spec)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
apply   blast
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 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
   700
apply (erule ax_thin)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
lemma subset_mtriples_iff: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
  "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
   706
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
apply (rule subset_image_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
lemma weaken: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
 "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
   712
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
   713
(*42 subgoals*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
apply       (tactic "ALLGOALS strip_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
apply       (tactic "TRYALL hyp_subst_tac")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
apply       (simp, rule ax_derivs.empty)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
apply      (drule subset_insertD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
apply      (blast intro: ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
apply     (fast intro: ax_derivs.asm)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
(*apply  (blast intro: ax_derivs.cut) *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
apply   (fast intro: ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
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
   725
(*37 subgoals*)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
                   THEN_ALL_NEW Fast_tac) *})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
(*1 subgoal*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
apply (clarsimp simp add: subset_mtriples_iff)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
apply (rule ax_derivs.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
apply (erule impE)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
apply  (rule exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
apply  (erule conjI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
apply  (rule HOL.refl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
oops (* dead end, Methd is to blame *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
section "rules derived from conseq"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
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
   741
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
   742
 @{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
   743
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
   744
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
   745
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
   746
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
   747
@{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
   748
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
   749
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
   750
*}
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   751
lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
 \<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
   753
  Q Y' s' Z)\<rbrakk>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
  \<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
   755
apply (rule ax_derivs.conseq)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
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
   760
-- {* 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
   761
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
   762
       (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
       (\<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
   764
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn } t\<succ> {Q }"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13585
diff changeset
   769
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
   770
 \<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
   771
  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
   772
  \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q }"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
apply (erule conseq12')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
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
   777
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
   778
 \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
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
   783
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
   784
\<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
apply blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
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
   789
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
   790
 "\<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
   791
   \<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
   792
                             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
   793
                            {\<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
   794
\<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
   795
apply (rule ax_derivs.conseq)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
(* 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
   800
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
   801
\<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
   802
apply (rule ax_escape (* unused *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
apply (rule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
apply  fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
(*alternative (more direct) proof:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
apply (rule ax_derivs.conseq) *)(* unused *)(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
apply (fast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
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
   814
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
   815
  "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
   816
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   821
lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
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
   824
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness 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
   825
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
   826
 "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
   827
  \<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
apply (erule (1) ax_nochange_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
(* 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
   834
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
   835
apply (rule ax_derivs.conseq(* unused *))
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   836
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
(* 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
   840
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
   841
 "\<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
   842
  \<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
   843
apply (rule ax_escape (* unused *))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
apply safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
apply  (erule conseq12, fast)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
(* 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
   849
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
   850
 "(\<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
   851
       (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   852
apply (best elim!: conseq1 conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
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
   855
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
   856
 \<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
   857
                   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
   858
apply (unfold peek_and_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
apply (case_tac "C s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
apply  (erule conseq12, force)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
(*alternative (more direct) proof:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
apply (case_tac "C s")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
apply  force+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
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
   871
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
   872
  \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
apply (erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
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
   878
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
   879
\<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
apply (simp add: ax_valids_def triple_valid_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
lemma adapt_pre_weakest: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
"\<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
   888
  P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
apply (unfold adapt_pre_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
apply (drule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
apply (drule_tac x = "{}" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
apply (drule_tac x = "In1r Skip" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
apply (simp add: ax_valids_def triple_valid_def2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
oops
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   895
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   896
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
   897
 "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
   898
 \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   899
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   900
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
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
   903
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
   904
"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
   905
 \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
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
   912
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
   913
"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
   914
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
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
   919
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
   920
"\<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
   921
 \<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
   922
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
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
   925
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
   926
"\<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
   927
 \<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
   928
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
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
   931
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
   932
"(\<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
   933
 \<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
   934
apply (force elim!: conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
section "alternative axioms"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
lemma ax_Lit2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
  "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
   942
apply (rule ax_derivs.Lit [THEN conseq1])
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
lemma ax_Lit2_test_complete: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
  "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
   947
apply (rule ax_Lit2 [THEN conseq2])
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_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
   952
apply (rule ax_derivs.LVar [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
  {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
apply (rule ax_derivs.Super [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   959
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   960
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   961
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
lemma ax_Nil2: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   963
  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   964
apply (rule ax_derivs.Nil [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   967
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
section "misc derived structural rules"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
(* unused *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
    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
   974
       G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
apply (frule (1) finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
apply (erule finite_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
apply  (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
lemma ax_derivs_insertD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
 "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
   987
apply (fast intro: ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
lemma ax_methods_spec: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
"\<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
   992
apply (erule ax_derivs.weaken)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
apply (force del: image_eqI intro: rev_image_eqI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
(* this version is used to avoid using the cut rule *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
  ((\<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
   999
      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
apply (frule (1) finite_subset)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
apply (erule make_imp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
apply (erule thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
apply (erule finite_induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1004
apply  clarsimp+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
apply (drule ax_derivs_insertD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
apply (rule ax_derivs.insert)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
apply  (simp (no_asm_simp) only: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
apply  (auto elim: ax_methods_spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1010
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1012
lemma ax_no_hazard: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1013
  "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
  1014
apply (erule ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1015
apply (rule ax_derivs.hazard [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1017
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1019
lemma ax_free_wt: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
 "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1021
  \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1022
  G,A\<turnstile>{Normal P} t\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1023
apply (rule ax_no_hazard)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1024
apply (rule ax_escape)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1025
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1026
apply (erule mp [THEN conseq12])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
apply  (auto simp add: type_ok_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1028
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1030
ML {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1031
bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1032
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1033
declare ax_Abrupts [intro!]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1034
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1035
lemmas ax_Normal_cases = ax_cases [of _ _ normal]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1036
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1037
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
  1038
apply (rule ax_Normal_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1039
apply  (rule ax_derivs.Skip)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1040
apply fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1041
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1042
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
section "derived rules for methd call"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
lemma ax_Call_known_DynT: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1048
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
  \<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
  1050
  init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
    Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1052
  \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1053
       {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
                     C = invocation_declclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1055
                            G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1056
       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
  1057
   \<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
  1058
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1059
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1060
apply  (erule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1061
apply (rule ax_escape, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1062
apply (drule spec, drule spec, drule spec,erule conseq12)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1065
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
lemma ax_Call_Static: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
 "\<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
  1069
               init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
              Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
  G,A\<turnstile>{Normal P} e-\<succ> {Q};
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
  \<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
  1073
  \<and>. (\<lambda> s. C=invocation_declclass 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1074
                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
  1075
\<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
  1076
apply (erule ax_derivs.Call)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1077
apply  safe
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
apply  (erule spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
apply (rule ax_escape, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
apply (drule spec,drule spec,drule spec, erule conseq12)
20014
729a45534001 fixed let-simproc
schirmer
parents: 19685
diff changeset
  1082
apply (force simp add: init_lvars_def Let_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
lemma ax_Methd1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
 "\<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
  1087
       G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
apply (drule ax_derivs.Methd)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
apply (erule (1) ax_methods_spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
lemma ax_MethdN: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
"G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
          {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1096
      G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1097
apply (rule ax_Methd1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1098
apply  (rule_tac [2] singletonI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
apply (unfold mtriples_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1100
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1102
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
lemma ax_StatRef: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
  "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
  1105
apply (rule ax_derivs.Cast)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1106
apply (rule ax_Lit2 [THEN conseq2])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
section "rules derived from Init and Done"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1111
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
  lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1113
     \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
            .init c. {set_lvars l .; R};   
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
         G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
  .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1117
  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
  1118
apply (erule ax_derivs.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1119
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1120
apply assumption
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1121
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1122
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1123
lemma ax_Init_Skip_lemma: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1124
"\<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
  1125
  .Skip. {(set_lvars l .; P)::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1126
apply (rule allI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1127
apply (rule ax_SkipI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1128
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1130
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1132
       P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1133
       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
  1134
       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
  1135
apply (rule_tac C = "initd C" in ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1136
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1137
apply (simp (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1138
apply (erule (1) ax_InitS)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1139
apply  simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1140
apply  (rule ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1141
apply (erule conseq1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1142
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1143
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1144
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1145
lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1146
  {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1147
       .Init Object. {(P \<and>. initd Object)::'a assn}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1148
apply (rule ax_derivs.Init)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1149
apply   (drule class_Object, force)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1150
apply (simp_all (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1151
apply (rule_tac [2] ax_Init_Skip_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1152
apply (rule ax_SkipI, force)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1155
lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
       (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1157
  G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
apply (rule_tac C = "initd Object" in ax_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
apply (erule ax_Init_Object [THEN conseq1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
apply force
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1162
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1163
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1164
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1165
section "introduction rules for Alloc and SXAlloc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
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
  1167
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
  1168
 "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
  1169
 \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1170
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1171
apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1172
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1173
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1174
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
  1175
  "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
  1176
     {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
  1177
      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
  1178
      heap_free (Suc (Suc 0))}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1179
   \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1180
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1181
apply (auto elim!: halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1182
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1183
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1184
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
  1185
 "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
  1186
   {\<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
  1187
    (\<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
  1188
    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
  1189
    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
  1190
 \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1191
 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
  1192
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1193
apply (auto elim!: halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1194
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1195
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1196
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
  1197
 "\<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
  1198
     {(\<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
  1199
      (\<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
  1200
      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
  1201
      \<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
  1202
 \<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
  1203
 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
  1204
apply (erule conseq2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1205
apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1206
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1207
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1208
end