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