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