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