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