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