src/HOL/Bali/AxSem.thy
author berghofe
Sat Jan 30 17:03:46 2010 +0100 (2010-01-30)
changeset 34990 81e8fdfeb849
parent 32960 69916a850301
child 35067 af4c18c30593
permissions -rw-r--r--
Adapted to changes in cases method.
     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 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   475 declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   476 
   477 inductive
   478   ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
   479   and ax_deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple  \<Rightarrow> bool" ("_,_\<turnstile>_" [61,58,58] 57)
   480   for G :: prog
   481 where
   482 
   483   "G,A \<turnstile>t \<equiv> G,A|\<turnstile>{t}"
   484 
   485 | empty: " G,A|\<turnstile>{}"
   486 | insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
   487           G,A|\<turnstile>insert t ts"
   488 
   489 | asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
   490 
   491 (* could be added for convenience and efficiency, but is not necessary
   492   cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
   493            G,A |\<turnstile>ts"
   494 *)
   495 | weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
   496 
   497 | conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
   498          (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
   499                                  Q  Y' s' Z ))
   500                                          \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
   501 
   502 | hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
   503 
   504 | Abrupt:  "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
   505 
   506   --{* variables *}
   507 | LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
   508 
   509 | FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
   510           G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
   511                                  G,A\<turnstile>{Normal P} {accC,C,stat}e..fn=\<succ> {R}"
   512 
   513 | AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
   514           \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
   515                                  G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
   516   --{* expressions *}
   517 
   518 | NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
   519                                  G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
   520 
   521 | NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
   522           {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
   523                                  G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
   524 
   525 | Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   526           abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   527                                  G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
   528 
   529 | Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   530                   Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
   531                                  G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
   532 
   533 | Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
   534 
   535 | UnOp: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. Q\<leftarrow>Val (eval_unop unop v)}\<rbrakk>
   536           \<Longrightarrow>
   537           G,A\<turnstile>{Normal P} UnOp unop e-\<succ> {Q}"
   538 
   539 | BinOp:
   540    "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
   541      \<forall>v1. G,A\<turnstile>{Q\<leftarrow>Val v1} 
   542                (if need_second_arg binop v1 then (In1l e2) else (In1r Skip))\<succ>
   543                {\<lambda>Val:v2:. R\<leftarrow>Val (eval_binop binop v1 v2)}\<rbrakk>
   544     \<Longrightarrow>
   545     G,A\<turnstile>{Normal P} BinOp binop e1 e2-\<succ> {R}" 
   546 
   547 | Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
   548 
   549 | Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   550                                  G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
   551 
   552 | Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
   553      \<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>
   554                                  G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
   555 
   556 | Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
   557           \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk> \<Longrightarrow>
   558                                  G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
   559 
   560 | Call: 
   561 "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
   562   \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
   563  (\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
   564       invC = invocation_class mode (store s) a statT \<and>
   565          l = locals (store s)) ;.
   566       init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
   567       (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
   568  Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
   569          G,A\<turnstile>{Normal P} {accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
   570 
   571 | Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
   572                                  G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
   573 
   574 | Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
   575   G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
   576     \<Longrightarrow>
   577                                  G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
   578   
   579   --{* expression lists *}
   580 
   581 | Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
   582 
   583 | Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
   584           \<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
   585                                  G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
   586 
   587   --{* statements *}
   588 
   589 | Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
   590 
   591 | Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   592                                  G,A\<turnstile>{Normal P} .Expr e. {Q}"
   593 
   594 | Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb l) .; Q}\<rbrakk> \<Longrightarrow>
   595                            G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
   596 
   597 | Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   598           G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
   599                                  G,A\<turnstile>{Normal P} .c1;;c2. {R}"
   600 
   601 | If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   602           \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
   603                                  G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
   604 (* unfolding variant of Loop, not needed here
   605   LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   606           \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
   607          \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
   608 *)
   609 | Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
   610           G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
   611                             G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
   612   
   613 | Jmp: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P}"
   614 
   615 | Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   616                                  G,A\<turnstile>{Normal P} .Throw e. {Q}"
   617 
   618 | Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
   619           G,A\<turnstile>{Q \<and>. (\<lambda>s.  G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
   620               (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
   621                                  G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
   622 
   623 | Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   624       \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
   625               .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
   626                                  G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
   627 
   628 | Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
   629 
   630 | Init: "\<lbrakk>the (class G C) = c;
   631           G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
   632               .(if C = Object then Skip else Init (super c)). {Q};
   633       \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
   634               .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
   635                                G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
   636 
   637 -- {* Some dummy rules for the intermediate terms @{text Callee},
   638 @{text InsInitE}, @{text InsInitV}, @{text FinA} only used by the smallstep 
   639 semantics.
   640 *}
   641 | InsInitV: " G,A\<turnstile>{Normal P} InsInitV c v=\<succ> {Q}"
   642 | InsInitE: " G,A\<turnstile>{Normal P} InsInitE c e-\<succ> {Q}"
   643 | Callee:    " G,A\<turnstile>{Normal P} Callee l e-\<succ> {Q}"
   644 | FinA:      " G,A\<turnstile>{Normal P} .FinA a c. {Q}"
   645 (*
   646 axioms 
   647 *)
   648 
   649 constdefs
   650  adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   651 "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)"
   652 
   653 
   654 section "rules derived by induction"
   655 
   656 lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
   657 apply (unfold ax_valids_def)
   658 apply fast
   659 done
   660 
   661 (*if cut is available
   662 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>  
   663        G,A|\<turnstile>ts"
   664 b y etac ax_derivs.cut 1;
   665 b y eatac ax_derivs.asm 1 1;
   666 qed "ax_thin";
   667 *)
   668 lemma ax_thin [rule_format (no_asm)]: 
   669   "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
   670 apply (erule ax_derivs.induct)
   671 apply                (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
   672 apply                (rule ax_derivs.empty)
   673 apply               (erule (1) ax_derivs.insert)
   674 apply              (fast intro: ax_derivs.asm)
   675 (*apply           (fast intro: ax_derivs.cut) *)
   676 apply            (fast intro: ax_derivs.weaken)
   677 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) 
   678 (* 37 subgoals *)
   679 prefer 18 (* Methd *)
   680 apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
   681 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
   682 apply auto
   683 done
   684 
   685 lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"
   686 apply (erule ax_thin)
   687 apply fast
   688 done
   689 
   690 lemma subset_mtriples_iff: 
   691   "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})"
   692 apply (unfold mtriples_def)
   693 apply (rule subset_image_iff)
   694 done
   695 
   696 lemma weaken: 
   697  "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
   698 apply (erule ax_derivs.induct)
   699 (*42 subgoals*)
   700 apply       (tactic "ALLGOALS strip_tac")
   701 apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
   702          etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
   703 apply       (tactic "TRYALL hyp_subst_tac")
   704 apply       (simp, rule ax_derivs.empty)
   705 apply      (drule subset_insertD)
   706 apply      (blast intro: ax_derivs.insert)
   707 apply     (fast intro: ax_derivs.asm)
   708 (*apply  (blast intro: ax_derivs.cut) *)
   709 apply   (fast intro: ax_derivs.weaken)
   710 apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
   711 (*37 subgoals*)
   712 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
   713                    THEN_ALL_NEW fast_tac @{claset}) *})
   714 (*1 subgoal*)
   715 apply (clarsimp simp add: subset_mtriples_iff)
   716 apply (rule ax_derivs.Methd)
   717 apply (drule spec)
   718 apply (erule impE)
   719 apply  (rule exI)
   720 apply  (erule conjI)
   721 apply  (rule HOL.refl)
   722 oops (* dead end, Methd is to blame *)
   723 
   724 
   725 section "rules derived from conseq"
   726 
   727 text {* In the following rules we often have to give some type annotations like:
   728  @{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
   729 Given only the term above without annotations, Isabelle would infer a more 
   730 general type were we could have 
   731 different types of auxiliary variables in the assumption set (@{term A}) and 
   732 in the triple itself (@{term P} and @{term Q}). But 
   733 @{text "ax_derivs.Methd"} enforces the same type in the inductive definition of
   734 the derivation. So we have to restrict the types to be able to apply the
   735 rules. 
   736 *}
   737 lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
   738  \<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>  
   739   Q Y' s' Z)\<rbrakk>  
   740   \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"
   741 apply (rule ax_derivs.conseq)
   742 apply clarsimp
   743 apply blast
   744 done
   745 
   746 -- {* Nice variant, since it is so symmetric we might be able to memorise it. *}
   747 lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'.  
   748        (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
   749        (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  Y' s' Z)\<rbrakk>  
   750   \<Longrightarrow>  G,A\<turnstile>{P::'a assn } t\<succ> {Q }"
   751 apply (erule conseq12)
   752 apply fast
   753 done
   754 
   755 lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
   756  \<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>  
   757   Q Y' s' Z)\<rbrakk>  
   758   \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q }"
   759 apply (erule conseq12')
   760 apply blast
   761 done
   762 
   763 lemma conseq1: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> 
   764  \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
   765 apply (erule conseq12)
   766 apply blast
   767 done
   768 
   769 lemma conseq2: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> 
   770 \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
   771 apply (erule conseq12)
   772 apply blast
   773 done
   774 
   775 lemma ax_escape: 
   776  "\<lbrakk>\<forall>Y s Z. P Y s Z 
   777    \<longrightarrow> G,(A::'a triple set)\<turnstile>{\<lambda>Y' s' (Z'::'a). (Y',s') = (Y,s)} 
   778                              t\<succ> 
   779                             {\<lambda>Y s Z'. Q Y s Z}
   780 \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q::'a assn}"
   781 apply (rule ax_derivs.conseq)
   782 apply force
   783 done
   784 
   785 (* unused *)
   786 lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}\<rbrakk> 
   787 \<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}"
   788 apply (rule ax_escape (* unused *))
   789 apply clarify
   790 apply (rule conseq12)
   791 apply  fast
   792 apply auto
   793 done
   794 (*alternative (more direct) proof:
   795 apply (rule ax_derivs.conseq) *)(* unused *)(*
   796 apply (fast)
   797 *)
   798 
   799 
   800 lemma ax_impossible [intro]: 
   801   "G,(A::'a triple set)\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q::'a assn}"
   802 apply (rule ax_escape)
   803 apply clarify
   804 done
   805 
   806 (* unused *)
   807 lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
   808 apply auto
   809 done
   810 
   811 lemma ax_nochange:
   812  "G,(A::(res \<times> state) triple set)\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} 
   813   \<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}"
   814 apply (erule conseq12)
   815 apply auto
   816 apply (erule (1) ax_nochange_lemma)
   817 done
   818 
   819 (* unused *)
   820 lemma ax_trivial: "G,(A::'a triple set)\<turnstile>{P::'a assn}  t\<succ> {\<lambda>Y s Z. True}"
   821 apply (rule ax_derivs.conseq(* unused *))
   822 apply auto
   823 done
   824 
   825 (* unused *)
   826 lemma ax_disj: 
   827  "\<lbrakk>G,(A::'a triple set)\<turnstile>{P1::'a assn} t\<succ> {Q1}; G,A\<turnstile>{P2::'a assn} t\<succ> {Q2}\<rbrakk> 
   828   \<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}"
   829 apply (rule ax_escape (* unused *))
   830 apply safe
   831 apply  (erule conseq12, fast)+
   832 done
   833 
   834 (* unused *)
   835 lemma ax_supd_shuffle: 
   836  "(\<exists>Q. G,(A::'a triple set)\<turnstile>{P::'a assn} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =  
   837        (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
   838 apply (best elim!: conseq1 conseq2)
   839 done
   840 
   841 lemma ax_cases: "
   842  \<lbrakk>G,(A::'a triple set)\<turnstile>{P \<and>.       C} t\<succ> {Q::'a assn};  
   843                    G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   844 apply (unfold peek_and_def)
   845 apply (rule ax_escape)
   846 apply clarify
   847 apply (case_tac "C s")
   848 apply  (erule conseq12, force)+
   849 done
   850 (*alternative (more direct) proof:
   851 apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
   852 apply clarify
   853 apply (case_tac "C s")
   854 apply  force+
   855 *)
   856 
   857 lemma ax_adapt: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
   858   \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   859 apply (unfold adapt_pre_def)
   860 apply (erule conseq12)
   861 apply fast
   862 done
   863 
   864 lemma adapt_pre_adapts: "G,(A::'a triple set)\<Turnstile>{P::'a assn} t\<succ> {Q} 
   865 \<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   866 apply (unfold adapt_pre_def)
   867 apply (simp add: ax_valids_def triple_valid_def2)
   868 apply fast
   869 done
   870 
   871 
   872 lemma adapt_pre_weakest: 
   873 "\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
   874   P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
   875 apply (unfold adapt_pre_def)
   876 apply (drule spec)
   877 apply (drule_tac x = "{}" in spec)
   878 apply (drule_tac x = "In1r Skip" in spec)
   879 apply (simp add: ax_valids_def triple_valid_def2)
   880 oops
   881 
   882 lemma peek_and_forget1_Normal: 
   883  "G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} 
   884  \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
   885 apply (erule conseq1)
   886 apply (simp (no_asm))
   887 done
   888 
   889 lemma peek_and_forget1: 
   890 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
   891  \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
   892 apply (erule conseq1)
   893 apply (simp (no_asm))
   894 done
   895 
   896 lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
   897 
   898 lemma peek_and_forget2: 
   899 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q \<and>. p} 
   900 \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   901 apply (erule conseq2)
   902 apply (simp (no_asm))
   903 done
   904 
   905 lemma ax_subst_Val_allI: 
   906 "\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {(Q v)::'a assn}
   907  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"
   908 apply (force elim!: conseq1)
   909 done
   910 
   911 lemma ax_subst_Var_allI: 
   912 "\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {(Q v)::'a assn}
   913  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"
   914 apply (force elim!: conseq1)
   915 done
   916 
   917 lemma ax_subst_Vals_allI: 
   918 "(\<forall>v. G,(A::'a triple set)\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {(Q v)::'a assn})
   919  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"
   920 apply (force elim!: conseq1)
   921 done
   922 
   923 
   924 section "alternative axioms"
   925 
   926 lemma ax_Lit2: 
   927   "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
   928 apply (rule ax_derivs.Lit [THEN conseq1])
   929 apply force
   930 done
   931 lemma ax_Lit2_test_complete: 
   932   "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}"
   933 apply (rule ax_Lit2 [THEN conseq2])
   934 apply force
   935 done
   936 
   937 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))}"
   938 apply (rule ax_derivs.LVar [THEN conseq1])
   939 apply force
   940 done
   941 
   942 lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
   943   {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
   944 apply (rule ax_derivs.Super [THEN conseq1])
   945 apply force
   946 done
   947 
   948 lemma ax_Nil2: 
   949   "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
   950 apply (rule ax_derivs.Nil [THEN conseq1])
   951 apply force
   952 done
   953 
   954 
   955 section "misc derived structural rules"
   956 
   957 (* unused *)
   958 lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
   959     G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
   960        G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
   961 apply (frule (1) finite_subset)
   962 apply (erule rev_mp)
   963 apply (erule thin_rl)
   964 apply (erule finite_induct)
   965 apply  (unfold mtriples_def)
   966 apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
   967 apply force
   968 done
   969 lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
   970 
   971 lemma ax_derivs_insertD: 
   972  "G,(A::'a triple set)|\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts"
   973 apply (fast intro: ax_derivs.weaken)
   974 done
   975 
   976 lemma ax_methods_spec: 
   977 "\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
   978 apply (erule ax_derivs.weaken)
   979 apply (force del: image_eqI intro: rev_image_eqI)
   980 done
   981 
   982 (* this version is used to avoid using the cut rule *)
   983 lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
   984   ((\<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>  
   985       G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
   986 apply (frule (1) finite_subset)
   987 apply (erule rev_mp)
   988 apply (erule thin_rl)
   989 apply (erule finite_induct)
   990 apply  clarsimp+
   991 apply (drule ax_derivs_insertD)
   992 apply (rule ax_derivs.insert)
   993 apply  (simp (no_asm_simp) only: split_tupled_all)
   994 apply  (auto elim: ax_methods_spec)
   995 done
   996 lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
   997  
   998 lemma ax_no_hazard: 
   999   "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}"
  1000 apply (erule ax_cases)
  1001 apply (rule ax_derivs.hazard [THEN conseq1])
  1002 apply force
  1003 done
  1004 
  1005 lemma ax_free_wt: 
  1006  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
  1007   \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
  1008   G,A\<turnstile>{Normal P} t\<succ> {Q}"
  1009 apply (rule ax_no_hazard)
  1010 apply (rule ax_escape)
  1011 apply clarify
  1012 apply (erule mp [THEN conseq12])
  1013 apply  (auto simp add: type_ok_def)
  1014 done
  1015 
  1016 ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *}
  1017 declare ax_Abrupts [intro!]
  1018 
  1019 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
  1020 
  1021 lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
  1022 apply (rule ax_Normal_cases)
  1023 apply  (rule ax_derivs.Skip)
  1024 apply fast
  1025 done
  1026 lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
  1027 
  1028 
  1029 section "derived rules for methd call"
  1030 
  1031 lemma ax_Call_known_DynT: 
  1032 "\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
  1033   \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.
  1034   init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
  1035     Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1036   \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
  1037        {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
  1038                      C = invocation_declclass 
  1039                             G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
  1040        G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
  1041    \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1042 apply (erule ax_derivs.Call)
  1043 apply  safe
  1044 apply  (erule spec)
  1045 apply (rule ax_escape, clarsimp)
  1046 apply (drule spec, drule spec, drule spec,erule conseq12)
  1047 apply force
  1048 done
  1049 
  1050 
  1051 lemma ax_Call_Static: 
  1052  "\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.  
  1053                init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
  1054               Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1055   G,A\<turnstile>{Normal P} e-\<succ> {Q};
  1056   \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
  1057   \<and>. (\<lambda> s. C=invocation_declclass 
  1058                 G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}
  1059 \<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1060 apply (erule ax_derivs.Call)
  1061 apply  safe
  1062 apply  (erule spec)
  1063 apply (rule ax_escape, clarsimp)
  1064 apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
  1065 apply (drule spec,drule spec,drule spec, erule conseq12)
  1066 apply (force simp add: init_lvars_def Let_def)
  1067 done
  1068 
  1069 lemma ax_Methd1: 
  1070  "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 
  1071        G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
  1072 apply (drule ax_derivs.Methd)
  1073 apply (unfold mtriples_def)
  1074 apply (erule (1) ax_methods_spec)
  1075 done
  1076 
  1077 lemma ax_MethdN: 
  1078 "G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
  1079           {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
  1080       G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
  1081 apply (rule ax_Methd1)
  1082 apply  (rule_tac [2] singletonI)
  1083 apply (unfold mtriples_def)
  1084 apply clarsimp
  1085 done
  1086 
  1087 lemma ax_StatRef: 
  1088   "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}"
  1089 apply (rule ax_derivs.Cast)
  1090 apply (rule ax_Lit2 [THEN conseq2])
  1091 apply clarsimp
  1092 done
  1093 
  1094 section "rules derived from Init and Done"
  1095 
  1096   lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
  1097      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
  1098             .init c. {set_lvars l .; R};   
  1099          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
  1100   .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
  1101   G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"
  1102 apply (erule ax_derivs.Init)
  1103 apply  (simp (no_asm_simp))
  1104 apply assumption
  1105 done
  1106 
  1107 lemma ax_Init_Skip_lemma: 
  1108 "\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}
  1109   .Skip. {(set_lvars l .; P)::'a assn}"
  1110 apply (rule allI)
  1111 apply (rule ax_SkipI)
  1112 apply clarsimp
  1113 done
  1114 
  1115 lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
  1116        P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
  1117        G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>  
  1118        G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"
  1119 apply (rule_tac C = "initd C" in ax_cases)
  1120 apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1121 apply (simp (no_asm))
  1122 apply (erule (1) ax_InitS)
  1123 apply  simp
  1124 apply  (rule ax_Init_Skip_lemma)
  1125 apply (erule conseq1)
  1126 apply force
  1127 done
  1128 
  1129 lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
  1130   {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
  1131        .Init Object. {(P \<and>. initd Object)::'a assn}"
  1132 apply (rule ax_derivs.Init)
  1133 apply   (drule class_Object, force)
  1134 apply (simp_all (no_asm))
  1135 apply (rule_tac [2] ax_Init_Skip_lemma)
  1136 apply (rule ax_SkipI, force)
  1137 done
  1138 
  1139 lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
  1140        (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
  1141   G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
  1142 apply (rule_tac C = "initd Object" in ax_cases)
  1143 apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1144 apply (erule ax_Init_Object [THEN conseq1])
  1145 apply force
  1146 done
  1147 
  1148 
  1149 section "introduction rules for Alloc and SXAlloc"
  1150 
  1151 lemma ax_SXAlloc_Normal: 
  1152  "G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
  1153  \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
  1154 apply (erule conseq2)
  1155 apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
  1156 done
  1157 
  1158 lemma ax_Alloc: 
  1159   "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1160      {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1161       Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
  1162       heap_free (Suc (Suc 0))}
  1163    \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
  1164 apply (erule conseq2)
  1165 apply (auto elim!: halloc_elim_cases)
  1166 done
  1167 
  1168 lemma ax_Alloc_Arr: 
  1169  "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1170    {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>  
  1171     (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1172     Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.
  1173     heap_free (Suc (Suc 0))} 
  1174  \<Longrightarrow>  
  1175  G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"
  1176 apply (erule conseq2)
  1177 apply (auto elim!: halloc_elim_cases)
  1178 done
  1179 
  1180 lemma ax_SXAlloc_catch_SXcpt: 
  1181  "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1182      {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>  
  1183       (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1184       Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))  
  1185       \<and>. heap_free (Suc (Suc 0))}\<rbrakk> 
  1186  \<Longrightarrow>  
  1187  G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"
  1188 apply (erule conseq2)
  1189 apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
  1190 done
  1191 
  1192 end