src/HOL/Bali/AxSem.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62042 6c6ccf573479
child 62390 842917225d56
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Bali/AxSem.thy
     2     Author:     David von Oheimb
     3 *)
     4 
     5 subsection \<open>Axiomatic semantics of Java expressions and statements 
     6           (see also Eval.thy)
     7 \<close>
     8 theory AxSem imports Evaln TypeSafe begin
     9 
    10 text \<open>
    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 \<close>
    38 
    39 type_synonym  res = vals \<comment>\<open>result entry\<close>
    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   \<comment>\<open>relation on result values, state and auxiliary variables\<close>
    61 type_synonym '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 subsubsection "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 subsubsection "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_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
   384 type_synonym 'a triples = "'a triple set"
   385 
   386 abbreviation
   387   var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
   388                                          ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
   389   where "{P} e=\<succ> {Q} == {P} In2 e\<succ> {Q}"
   390 
   391 abbreviation
   392   expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
   393                                          ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
   394   where "{P} e-\<succ> {Q} == {P} In1l e\<succ> {Q}"
   395 
   396 abbreviation
   397   exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
   398                                          ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
   399   where "{P} e\<doteq>\<succ> {Q} == {P} In3 e\<succ> {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\<succ> {Q}"
   405 
   406 notation (ASCII)
   407   triple  ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75) and
   408   var_triple  ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75) and
   409   expr_triple  ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75) and
   410   exprs_triple  ("{(1_)}/ _#>/ {(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"  ("_|\<Turnstile>_:_" [61,0, 58] 57)
   435   where "G|\<Turnstile>n:ts == Ball ts (triple_valid G n)"
   436 
   437 notation (ASCII)
   438   triples_valid  (  "_||=_:_" [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"  ("_,_\<Turnstile>_" [61,58,58] 57)
   447   where "G,A \<Turnstile>t == G,A|\<Turnstile>{t}"
   448 
   449 notation (ASCII)
   450   ax_valid  ( "_,_|=_"   [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 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   468 setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
   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   \<comment>\<open>variables\<close>
   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   \<comment>\<open>expressions\<close>
   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   \<comment>\<open>expression lists\<close>
   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   \<comment>\<open>statements\<close>
   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 \<comment> \<open>Some dummy rules for the intermediate terms \<open>Callee\<close>,
   631 \<open>InsInitE\<close>, \<open>InsInitV\<close>, \<open>FinA\<close> only used by the smallstep 
   632 semantics.
   633 \<close>
   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 subsubsection "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 @{context}, REPEAT o smp_tac @{context} 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 @{context} 3 1",clarify,
   671   tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI) 
   672 (* 37 subgoals *)
   673 prefer 18 (* Methd *)
   674 apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
   675 apply (tactic \<open>TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros}))\<close>)
   676 apply auto
   677 done
   678 
   679 lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"
   680 apply (erule ax_thin)
   681 apply fast
   682 done
   683 
   684 lemma subset_mtriples_iff: 
   685   "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})"
   686 apply (unfold mtriples_def)
   687 apply (rule subset_image_iff)
   688 done
   689 
   690 lemma weaken: 
   691  "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
   692 apply (erule ax_derivs.induct)
   693 (*42 subgoals*)
   694 apply       (tactic "ALLGOALS (strip_tac @{context})")
   695 apply       (tactic \<open>ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD},
   696          eresolve_tac @{context} [disjE],
   697          fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))\<close>)
   698 apply       (tactic "TRYALL (hyp_subst_tac @{context})")
   699 apply       (simp, rule ax_derivs.empty)
   700 apply      (drule subset_insertD)
   701 apply      (blast intro: ax_derivs.insert)
   702 apply     (fast intro: ax_derivs.asm)
   703 (*apply  (blast intro: ax_derivs.cut) *)
   704 apply   (fast intro: ax_derivs.weaken)
   705 apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *))
   706 (*37 subgoals*)
   707 apply (tactic \<open>TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})
   708                    THEN_ALL_NEW fast_tac @{context})\<close>)
   709 (*1 subgoal*)
   710 apply (clarsimp simp add: subset_mtriples_iff)
   711 apply (rule ax_derivs.Methd)
   712 apply (drule spec)
   713 apply (erule impE)
   714 apply  (rule exI)
   715 apply  (erule conjI)
   716 apply  (rule HOL.refl)
   717 oops (* dead end, Methd is to blame *)
   718 
   719 
   720 subsubsection "rules derived from conseq"
   721 
   722 text \<open>In the following rules we often have to give some type annotations like:
   723  @{term "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}"}.
   724 Given only the term above without annotations, Isabelle would infer a more 
   725 general type were we could have 
   726 different types of auxiliary variables in the assumption set (@{term A}) and 
   727 in the triple itself (@{term P} and @{term Q}). But 
   728 \<open>ax_derivs.Methd\<close> enforces the same type in the inductive definition of
   729 the derivation. So we have to restrict the types to be able to apply the
   730 rules. 
   731 \<close>
   732 lemma conseq12: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
   733  \<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>  
   734   Q Y' s' Z)\<rbrakk>  
   735   \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"
   736 apply (rule ax_derivs.conseq)
   737 apply clarsimp
   738 apply blast
   739 done
   740 
   741 \<comment> \<open>Nice variant, since it is so symmetric we might be able to memorise it.\<close>
   742 lemma conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'}; \<forall>s Y' s'.  
   743        (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
   744        (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  Y' s' Z)\<rbrakk>  
   745   \<Longrightarrow>  G,A\<turnstile>{P::'a assn } t\<succ> {Q }"
   746 apply (erule conseq12)
   747 apply fast
   748 done
   749 
   750 lemma conseq12_from_conseq12': "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q'};  
   751  \<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>  
   752   Q Y' s' Z)\<rbrakk>  
   753   \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q }"
   754 apply (erule conseq12')
   755 apply blast
   756 done
   757 
   758 lemma conseq1: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P'::'a assn} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> 
   759  \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
   760 apply (erule conseq12)
   761 apply blast
   762 done
   763 
   764 lemma conseq2: "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> 
   765 \<Longrightarrow> G,A\<turnstile>{P::'a assn} t\<succ> {Q}"
   766 apply (erule conseq12)
   767 apply blast
   768 done
   769 
   770 lemma ax_escape: 
   771  "\<lbrakk>\<forall>Y s Z. P Y s Z 
   772    \<longrightarrow> G,(A::'a triple set)\<turnstile>{\<lambda>Y' s' (Z'::'a). (Y',s') = (Y,s)} 
   773                              t\<succ> 
   774                             {\<lambda>Y s Z'. Q Y s Z}
   775 \<rbrakk> \<Longrightarrow>  G,A\<turnstile>{P::'a assn} t\<succ> {Q::'a assn}"
   776 apply (rule ax_derivs.conseq)
   777 apply force
   778 done
   779 
   780 (* unused *)
   781 lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q}\<rbrakk> 
   782 \<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}"
   783 apply (rule ax_escape (* unused *))
   784 apply clarify
   785 apply (rule conseq12)
   786 apply  fast
   787 apply auto
   788 done
   789 (*alternative (more direct) proof:
   790 apply (rule ax_derivs.conseq) *)(* unused *)(*
   791 apply (fast)
   792 *)
   793 
   794 
   795 lemma ax_impossible [intro]: 
   796   "G,(A::'a triple set)\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q::'a assn}"
   797 apply (rule ax_escape)
   798 apply clarify
   799 done
   800 
   801 (* unused *)
   802 lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
   803 apply auto
   804 done
   805 
   806 lemma ax_nochange:
   807  "G,(A::(res \<times> state) triple set)\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} 
   808   \<Longrightarrow> G,A\<turnstile>{P::(res \<times> state) assn} t\<succ> {P}"
   809 apply (erule conseq12)
   810 apply auto
   811 apply (erule (1) ax_nochange_lemma)
   812 done
   813 
   814 (* unused *)
   815 lemma ax_trivial: "G,(A::'a triple set)\<turnstile>{P::'a assn}  t\<succ> {\<lambda>Y s Z. True}"
   816 apply (rule ax_derivs.conseq(* unused *))
   817 apply auto
   818 done
   819 
   820 (* unused *)
   821 lemma ax_disj: 
   822  "\<lbrakk>G,(A::'a triple set)\<turnstile>{P1::'a assn} t\<succ> {Q1}; G,A\<turnstile>{P2::'a assn} t\<succ> {Q2}\<rbrakk> 
   823   \<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}"
   824 apply (rule ax_escape (* unused *))
   825 apply safe
   826 apply  (erule conseq12, fast)+
   827 done
   828 
   829 (* unused *)
   830 lemma ax_supd_shuffle: 
   831  "(\<exists>Q. G,(A::'a triple set)\<turnstile>{P::'a assn} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =  
   832        (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
   833 apply (best elim!: conseq1 conseq2)
   834 done
   835 
   836 lemma ax_cases: "
   837  \<lbrakk>G,(A::'a triple set)\<turnstile>{P \<and>.       C} t\<succ> {Q::'a assn};  
   838                    G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   839 apply (unfold peek_and_def)
   840 apply (rule ax_escape)
   841 apply clarify
   842 apply (case_tac "C s")
   843 apply  (erule conseq12, force)+
   844 done
   845 (*alternative (more direct) proof:
   846 apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
   847 apply clarify
   848 apply (case_tac "C s")
   849 apply  force+
   850 *)
   851 
   852 lemma ax_adapt: "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
   853   \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   854 apply (unfold adapt_pre_def)
   855 apply (erule conseq12)
   856 apply fast
   857 done
   858 
   859 lemma adapt_pre_adapts: "G,(A::'a triple set)\<Turnstile>{P::'a assn} t\<succ> {Q} 
   860 \<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   861 apply (unfold adapt_pre_def)
   862 apply (simp add: ax_valids_def triple_valid_def2)
   863 apply fast
   864 done
   865 
   866 
   867 lemma adapt_pre_weakest: 
   868 "\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
   869   P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
   870 apply (unfold adapt_pre_def)
   871 apply (drule spec)
   872 apply (drule_tac x = "{}" in spec)
   873 apply (drule_tac x = "In1r Skip" in spec)
   874 apply (simp add: ax_valids_def triple_valid_def2)
   875 oops
   876 
   877 lemma peek_and_forget1_Normal: 
   878  "G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} 
   879  \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
   880 apply (erule conseq1)
   881 apply (simp (no_asm))
   882 done
   883 
   884 lemma peek_and_forget1: 
   885 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q} 
   886  \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
   887 apply (erule conseq1)
   888 apply (simp (no_asm))
   889 done
   890 
   891 lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
   892 
   893 lemma peek_and_forget2: 
   894 "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> {Q \<and>. p} 
   895 \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   896 apply (erule conseq2)
   897 apply (simp (no_asm))
   898 done
   899 
   900 lemma ax_subst_Val_allI: 
   901 "\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {(Q v)::'a assn}
   902  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"
   903 apply (force elim!: conseq1)
   904 done
   905 
   906 lemma ax_subst_Var_allI: 
   907 "\<forall>v. G,(A::'a triple set)\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {(Q v)::'a assn}
   908  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"
   909 apply (force elim!: conseq1)
   910 done
   911 
   912 lemma ax_subst_Vals_allI: 
   913 "(\<forall>v. G,(A::'a triple set)\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {(Q v)::'a assn})
   914  \<Longrightarrow>  \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"
   915 apply (force elim!: conseq1)
   916 done
   917 
   918 
   919 subsubsection "alternative axioms"
   920 
   921 lemma ax_Lit2: 
   922   "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
   923 apply (rule ax_derivs.Lit [THEN conseq1])
   924 apply force
   925 done
   926 lemma ax_Lit2_test_complete: 
   927   "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}"
   928 apply (rule ax_Lit2 [THEN conseq2])
   929 apply force
   930 done
   931 
   932 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))}"
   933 apply (rule ax_derivs.LVar [THEN conseq1])
   934 apply force
   935 done
   936 
   937 lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
   938   {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
   939 apply (rule ax_derivs.Super [THEN conseq1])
   940 apply force
   941 done
   942 
   943 lemma ax_Nil2: 
   944   "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
   945 apply (rule ax_derivs.Nil [THEN conseq1])
   946 apply force
   947 done
   948 
   949 
   950 subsubsection "misc derived structural rules"
   951 
   952 (* unused *)
   953 lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
   954     G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
   955        G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
   956 apply (frule (1) finite_subset)
   957 apply (erule rev_mp)
   958 apply (erule thin_rl)
   959 apply (erule finite_induct)
   960 apply  (unfold mtriples_def)
   961 apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
   962 apply force
   963 done
   964 lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
   965 
   966 lemma ax_derivs_insertD: 
   967  "G,(A::'a triple set)|\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts"
   968 apply (fast intro: ax_derivs.weaken)
   969 done
   970 
   971 lemma ax_methods_spec: 
   972 "\<lbrakk>G,(A::'a triple set)|\<turnstile>case_prod f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
   973 apply (erule ax_derivs.weaken)
   974 apply (force del: image_eqI intro: rev_image_eqI)
   975 done
   976 
   977 (* this version is used to avoid using the cut rule *)
   978 lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
   979   ((\<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>  
   980       G,A|\<turnstile>case_prod f ` F \<longrightarrow> G,A|\<turnstile>case_prod g ` F"
   981 apply (frule (1) finite_subset)
   982 apply (erule rev_mp)
   983 apply (erule thin_rl)
   984 apply (erule finite_induct)
   985 apply  clarsimp+
   986 apply (drule ax_derivs_insertD)
   987 apply (rule ax_derivs.insert)
   988 apply  (simp (no_asm_simp) only: split_tupled_all)
   989 apply  (auto elim: ax_methods_spec)
   990 done
   991 lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
   992  
   993 lemma ax_no_hazard: 
   994   "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}"
   995 apply (erule ax_cases)
   996 apply (rule ax_derivs.hazard [THEN conseq1])
   997 apply force
   998 done
   999 
  1000 lemma ax_free_wt: 
  1001  "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
  1002   \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
  1003   G,A\<turnstile>{Normal P} t\<succ> {Q}"
  1004 apply (rule ax_no_hazard)
  1005 apply (rule ax_escape)
  1006 apply clarify
  1007 apply (erule mp [THEN conseq12])
  1008 apply  (auto simp add: type_ok_def)
  1009 done
  1010 
  1011 ML \<open>ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt})\<close>
  1012 declare ax_Abrupts [intro!]
  1013 
  1014 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]
  1015 
  1016 lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
  1017 apply (rule ax_Normal_cases)
  1018 apply  (rule ax_derivs.Skip)
  1019 apply fast
  1020 done
  1021 lemmas ax_SkipI = ax_Skip [THEN conseq1]
  1022 
  1023 
  1024 subsubsection "derived rules for methd call"
  1025 
  1026 lemma ax_Call_known_DynT: 
  1027 "\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
  1028   \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.
  1029   init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
  1030     Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1031   \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
  1032        {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
  1033                      C = invocation_declclass 
  1034                             G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
  1035        G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
  1036    \<Longrightarrow> G,A\<turnstile>{Normal P} {accC,statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1037 apply (erule ax_derivs.Call)
  1038 apply  safe
  1039 apply  (erule spec)
  1040 apply (rule ax_escape, clarsimp)
  1041 apply (drule spec, drule spec, drule spec,erule conseq12)
  1042 apply force
  1043 done
  1044 
  1045 
  1046 lemma ax_Call_Static: 
  1047  "\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.  
  1048                init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
  1049               Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1050   G,A\<turnstile>{Normal P} e-\<succ> {Q};
  1051   \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
  1052   \<and>. (\<lambda> s. C=invocation_declclass 
  1053                 G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}
  1054 \<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {accC,statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1055 apply (erule ax_derivs.Call)
  1056 apply  safe
  1057 apply  (erule spec)
  1058 apply (rule ax_escape, clarsimp)
  1059 apply (erule_tac V = "P \<longrightarrow> Q" for P Q in thin_rl)
  1060 apply (drule spec,drule spec,drule spec, erule conseq12)
  1061 apply (force simp add: init_lvars_def Let_def)
  1062 done
  1063 
  1064 lemma ax_Methd1: 
  1065  "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 
  1066        G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
  1067 apply (drule ax_derivs.Methd)
  1068 apply (unfold mtriples_def)
  1069 apply (erule (1) ax_methods_spec)
  1070 done
  1071 
  1072 lemma ax_MethdN: 
  1073 "G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
  1074           {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
  1075       G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
  1076 apply (rule ax_Methd1)
  1077 apply  (rule_tac [2] singletonI)
  1078 apply (unfold mtriples_def)
  1079 apply clarsimp
  1080 done
  1081 
  1082 lemma ax_StatRef: 
  1083   "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}"
  1084 apply (rule ax_derivs.Cast)
  1085 apply (rule ax_Lit2 [THEN conseq2])
  1086 apply clarsimp
  1087 done
  1088 
  1089 subsubsection "rules derived from Init and Done"
  1090 
  1091   lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
  1092      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
  1093             .init c. {set_lvars l .; R};   
  1094          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
  1095   .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
  1096   G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"
  1097 apply (erule ax_derivs.Init)
  1098 apply  (simp (no_asm_simp))
  1099 apply assumption
  1100 done
  1101 
  1102 lemma ax_Init_Skip_lemma: 
  1103 "\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}
  1104   .Skip. {(set_lvars l .; P)::'a assn}"
  1105 apply (rule allI)
  1106 apply (rule ax_SkipI)
  1107 apply clarsimp
  1108 done
  1109 
  1110 lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
  1111        P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
  1112        G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>  
  1113        G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"
  1114 apply (rule_tac C = "initd C" in ax_cases)
  1115 apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1116 apply (simp (no_asm))
  1117 apply (erule (1) ax_InitS)
  1118 apply  simp
  1119 apply  (rule ax_Init_Skip_lemma)
  1120 apply (erule conseq1)
  1121 apply force
  1122 done
  1123 
  1124 lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
  1125   {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
  1126        .Init Object. {(P \<and>. initd Object)::'a assn}"
  1127 apply (rule ax_derivs.Init)
  1128 apply   (drule class_Object, force)
  1129 apply (simp_all (no_asm))
  1130 apply (rule_tac [2] ax_Init_Skip_lemma)
  1131 apply (rule ax_SkipI, force)
  1132 done
  1133 
  1134 lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
  1135        (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
  1136   G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
  1137 apply (rule_tac C = "initd Object" in ax_cases)
  1138 apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1139 apply (erule ax_Init_Object [THEN conseq1])
  1140 apply force
  1141 done
  1142 
  1143 
  1144 subsubsection "introduction rules for Alloc and SXAlloc"
  1145 
  1146 lemma ax_SXAlloc_Normal: 
  1147  "G,(A::'a triple set)\<turnstile>{P::'a assn} .c. {Normal Q} 
  1148  \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
  1149 apply (erule conseq2)
  1150 apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
  1151 done
  1152 
  1153 lemma ax_Alloc: 
  1154   "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1155      {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1156       Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
  1157       heap_free (Suc (Suc 0))}
  1158    \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
  1159 apply (erule conseq2)
  1160 apply (auto elim!: halloc_elim_cases)
  1161 done
  1162 
  1163 lemma ax_Alloc_Arr: 
  1164  "G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1165    {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>  
  1166     (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1167     Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.
  1168     heap_free (Suc (Suc 0))} 
  1169  \<Longrightarrow>  
  1170  G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"
  1171 apply (erule conseq2)
  1172 apply (auto elim!: halloc_elim_cases)
  1173 done
  1174 
  1175 lemma ax_SXAlloc_catch_SXcpt: 
  1176  "\<lbrakk>G,(A::'a triple set)\<turnstile>{P::'a assn} t\<succ> 
  1177      {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>  
  1178       (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1179       Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))  
  1180       \<and>. heap_free (Suc (Suc 0))}\<rbrakk> 
  1181  \<Longrightarrow>  
  1182  G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"
  1183 apply (erule conseq2)
  1184 apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
  1185 done
  1186 
  1187 end