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