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