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