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