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