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