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