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