src/HOL/Bali/AxSem.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,1191 @@
     1.4 +(*  Title:      isabelle/Bali/AxSem.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1998 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +header {* Axiomatic semantics of Java expressions and statements 
    1.11 +          (see also Eval.thy)
    1.12 +        *}
    1.13 +
    1.14 +theory AxSem = Evaln + TypeSafe:
    1.15 +
    1.16 +text {*
    1.17 +design issues:
    1.18 +\begin{itemize}
    1.19 +\item a strong version of validity for triples with premises, namely one that 
    1.20 +      takes the recursive depth needed to complete execution, enables 
    1.21 +      correctness proof
    1.22 +\item auxiliary variables are handled first-class (-> Thomas Kleymann)
    1.23 +\item expressions not flattened to elementary assignments (as usual for 
    1.24 +      axiomatic semantics) but treated first-class => explicit result value 
    1.25 +      handling
    1.26 +\item intermediate values not on triple, but on assertion level 
    1.27 +      (with result entry)
    1.28 +\item multiple results with semantical substitution mechnism not requiring a 
    1.29 +      stack 
    1.30 +\item because of dynamic method binding, terms need to be dependent on state.
    1.31 +  this is also useful for conditional expressions and statements
    1.32 +\item result values in triples exactly as in eval relation (also for xcpt 
    1.33 +      states)
    1.34 +\item validity: additional assumption of state conformance and well-typedness,
    1.35 +  which is required for soundness and thus rule hazard required of completeness
    1.36 +\end{itemize}
    1.37 +
    1.38 +restrictions:
    1.39 +\begin{itemize}
    1.40 +\item all triples in a derivation are of the same type (due to weak 
    1.41 +      polymorphism)
    1.42 +\end{itemize}
    1.43 +*}
    1.44 +
    1.45 +
    1.46 +
    1.47 +types  res = vals (* result entry *)
    1.48 +syntax
    1.49 +  Val  :: "val      \<Rightarrow> res"
    1.50 +  Var  :: "var      \<Rightarrow> res"
    1.51 +  Vals :: "val list \<Rightarrow> res"
    1.52 +translations
    1.53 +  "Val  x"     => "(In1 x)"
    1.54 +  "Var  x"     => "(In2 x)"
    1.55 +  "Vals x"     => "(In3 x)"
    1.56 +
    1.57 +syntax
    1.58 +  "Val_"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
    1.59 +  "Var_"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
    1.60 +  "Vals_"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
    1.61 +
    1.62 +translations
    1.63 +  "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
    1.64 +  "\<lambda>Var:v . b"  == "(\<lambda>v. b) \<circ> the_In2"
    1.65 +  "\<lambda>Vals:v. b"  == "(\<lambda>v. b) \<circ> the_In3"
    1.66 +
    1.67 +  (* relation on result values, state and auxiliary variables *)
    1.68 +types 'a assn   =        "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
    1.69 +translations
    1.70 +      "res"    <= (type) "AxSem.res"
    1.71 +      "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
    1.72 +
    1.73 +constdefs
    1.74 +  assn_imp   :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool"             (infixr "\<Rightarrow>" 25)
    1.75 + "P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
    1.76 +  
    1.77 +lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"
    1.78 +apply (unfold assn_imp_def)
    1.79 +apply (rule HOL.refl)
    1.80 +done
    1.81 +
    1.82 +
    1.83 +section "assertion transformers"
    1.84 +
    1.85 +subsection "peek-and"
    1.86 +
    1.87 +constdefs
    1.88 +  peek_and   :: "'a assn \<Rightarrow> (state \<Rightarrow>  bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
    1.89 + "P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"
    1.90 +
    1.91 +lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"
    1.92 +apply (unfold peek_and_def)
    1.93 +apply (simp (no_asm))
    1.94 +done
    1.95 +
    1.96 +lemma peek_and_Not [simp]: "(P \<and>. (\<lambda>s. \<not> f s)) = (P \<and>. Not \<circ> f)"
    1.97 +apply (rule ext)
    1.98 +apply (rule ext)
    1.99 +apply (simp (no_asm))
   1.100 +done
   1.101 +
   1.102 +lemma peek_and_and [simp]: "peek_and (peek_and P p) p = peek_and P p"
   1.103 +apply (unfold peek_and_def)
   1.104 +apply (simp (no_asm))
   1.105 +done
   1.106 +
   1.107 +lemma peek_and_commut: "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)"
   1.108 +apply (rule ext)
   1.109 +apply (rule ext)
   1.110 +apply (rule ext)
   1.111 +apply auto
   1.112 +done
   1.113 +
   1.114 +syntax
   1.115 +  Normal     :: "'a assn \<Rightarrow> 'a assn"
   1.116 +translations
   1.117 +  "Normal P" == "P \<and>. normal"
   1.118 +
   1.119 +lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"
   1.120 +apply (rule ext)
   1.121 +apply (rule ext)
   1.122 +apply (rule ext)
   1.123 +apply auto
   1.124 +done
   1.125 +
   1.126 +subsection "assn-supd"
   1.127 +
   1.128 +constdefs
   1.129 +  assn_supd  :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
   1.130 + "P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"
   1.131 +
   1.132 +lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"
   1.133 +apply (unfold assn_supd_def)
   1.134 +apply (simp (no_asm))
   1.135 +done
   1.136 +
   1.137 +subsection "supd-assn"
   1.138 +
   1.139 +constdefs
   1.140 +  supd_assn  :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
   1.141 + "f .; P \<equiv> \<lambda>Y s. P Y (f s)"
   1.142 +
   1.143 +
   1.144 +lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"
   1.145 +apply (unfold supd_assn_def)
   1.146 +apply (simp (no_asm))
   1.147 +done
   1.148 +
   1.149 +lemma supd_assn_supdD [elim]: "((f .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z"
   1.150 +apply auto
   1.151 +done
   1.152 +
   1.153 +lemma supd_assn_supdI [elim]: "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z"
   1.154 +apply (auto simp del: split_paired_Ex)
   1.155 +done
   1.156 +
   1.157 +subsection "subst-res"
   1.158 +
   1.159 +constdefs
   1.160 +  subst_res   :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"              ("_\<leftarrow>_"  [60,61] 60)
   1.161 + "P\<leftarrow>w \<equiv> \<lambda>Y. P w"
   1.162 +
   1.163 +lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"
   1.164 +apply (unfold subst_res_def)
   1.165 +apply (simp (no_asm))
   1.166 +done
   1.167 +
   1.168 +lemma subst_subst_res [simp]: "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w"
   1.169 +apply (rule ext)
   1.170 +apply (simp (no_asm))
   1.171 +done
   1.172 +
   1.173 +lemma peek_and_subst_res [simp]: "(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)"
   1.174 +apply (rule ext)
   1.175 +apply (rule ext)
   1.176 +apply (simp (no_asm))
   1.177 +done
   1.178 +
   1.179 +(*###Do not work for some strange (unification?) reason
   1.180 +lemma subst_res_Val_beta [simp]: "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)"
   1.181 +apply (rule ext)
   1.182 +by simp
   1.183 +
   1.184 +lemma subst_res_Var_beta [simp]: "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)";
   1.185 +apply (rule ext)
   1.186 +by simp
   1.187 +
   1.188 +lemma subst_res_Vals_beta [simp]: "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)";
   1.189 +apply (rule ext)
   1.190 +by simp
   1.191 +*)
   1.192 +
   1.193 +subsection "subst-Bool"
   1.194 +
   1.195 +constdefs
   1.196 +  subst_Bool  :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn"             ("_\<leftarrow>=_" [60,61] 60)
   1.197 + "P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
   1.198 +
   1.199 +lemma subst_Bool_def2 [simp]: 
   1.200 +"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"
   1.201 +apply (unfold subst_Bool_def)
   1.202 +apply (simp (no_asm))
   1.203 +done
   1.204 +
   1.205 +lemma subst_Bool_the_BoolI: "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z"
   1.206 +apply auto
   1.207 +done
   1.208 +
   1.209 +subsection "peek-res"
   1.210 +
   1.211 +constdefs
   1.212 +  peek_res    :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
   1.213 + "peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
   1.214 +
   1.215 +syntax
   1.216 +"@peek_res"  :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_:. _" [0,3] 3)
   1.217 +translations
   1.218 +  "\<lambda>w:. P"   == "peek_res (\<lambda>w. P)"
   1.219 +
   1.220 +lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"
   1.221 +apply (unfold peek_res_def)
   1.222 +apply (simp (no_asm))
   1.223 +done
   1.224 +
   1.225 +lemma peek_res_subst_res [simp]: "peek_res P\<leftarrow>w = P w\<leftarrow>w"
   1.226 +apply (rule ext)
   1.227 +apply (simp (no_asm))
   1.228 +done
   1.229 +
   1.230 +(* unused *)
   1.231 +lemma peek_subst_res_allI: 
   1.232 + "(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)"
   1.233 +apply (rule allI)
   1.234 +apply (simp (no_asm))
   1.235 +apply fast
   1.236 +done
   1.237 +
   1.238 +subsection "ign-res"
   1.239 +
   1.240 +constdefs
   1.241 +  ign_res    ::  "        'a assn \<Rightarrow> 'a assn"            ("_\<down>" [1000] 1000)
   1.242 +  "P\<down>        \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
   1.243 +
   1.244 +lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"
   1.245 +apply (unfold ign_res_def)
   1.246 +apply (simp (no_asm))
   1.247 +done
   1.248 +
   1.249 +lemma ign_ign_res [simp]: "P\<down>\<down> = P\<down>"
   1.250 +apply (rule ext)
   1.251 +apply (rule ext)
   1.252 +apply (rule ext)
   1.253 +apply (simp (no_asm))
   1.254 +done
   1.255 +
   1.256 +lemma ign_subst_res [simp]: "P\<down>\<leftarrow>w = P\<down>"
   1.257 +apply (rule ext)
   1.258 +apply (rule ext)
   1.259 +apply (rule ext)
   1.260 +apply (simp (no_asm))
   1.261 +done
   1.262 +
   1.263 +lemma peek_and_ign_res [simp]: "(P \<and>. p)\<down> = (P\<down> \<and>. p)"
   1.264 +apply (rule ext)
   1.265 +apply (rule ext)
   1.266 +apply (rule ext)
   1.267 +apply (simp (no_asm))
   1.268 +done
   1.269 +
   1.270 +subsection "peek-st"
   1.271 +
   1.272 +constdefs
   1.273 +  peek_st    :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
   1.274 + "peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"
   1.275 +
   1.276 +syntax
   1.277 +"@peek_st"   :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"            ("\<lambda>_.. _" [0,3] 3)
   1.278 +translations
   1.279 +  "\<lambda>s.. P"   == "peek_st (\<lambda>s. P)"
   1.280 +
   1.281 +lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"
   1.282 +apply (unfold peek_st_def)
   1.283 +apply (simp (no_asm))
   1.284 +done
   1.285 +
   1.286 +lemma peek_st_triv [simp]: "(\<lambda>s.. P) = P"
   1.287 +apply (rule ext)
   1.288 +apply (rule ext)
   1.289 +apply (simp (no_asm))
   1.290 +done
   1.291 +
   1.292 +lemma peek_st_st [simp]: "(\<lambda>s.. \<lambda>s'.. P s s') = (\<lambda>s.. P s s)"
   1.293 +apply (rule ext)
   1.294 +apply (rule ext)
   1.295 +apply (simp (no_asm))
   1.296 +done
   1.297 +
   1.298 +lemma peek_st_split [simp]: "(\<lambda>s.. \<lambda>Y s'. P s Y s') = (\<lambda>Y s. P (store s) Y s)"
   1.299 +apply (rule ext)
   1.300 +apply (rule ext)
   1.301 +apply (simp (no_asm))
   1.302 +done
   1.303 +
   1.304 +lemma peek_st_subst_res [simp]: "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)"
   1.305 +apply (rule ext)
   1.306 +apply (simp (no_asm))
   1.307 +done
   1.308 +
   1.309 +lemma peek_st_Normal [simp]: "(\<lambda>s..(Normal (P s))) = Normal (\<lambda>s.. P s)"
   1.310 +apply (rule ext)
   1.311 +apply (rule ext)
   1.312 +apply (simp (no_asm))
   1.313 +done
   1.314 +
   1.315 +subsection "ign-res-eq"
   1.316 +
   1.317 +constdefs
   1.318 +  ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn"               ("_\<down>=_"  [60,61] 60)
   1.319 + "P\<down>=w       \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
   1.320 +
   1.321 +lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"
   1.322 +apply (unfold ign_res_eq_def)
   1.323 +apply auto
   1.324 +done
   1.325 +
   1.326 +lemma ign_ign_res_eq [simp]: "(P\<down>=w)\<down> = P\<down>"
   1.327 +apply (rule ext)
   1.328 +apply (rule ext)
   1.329 +apply (rule ext)
   1.330 +apply (simp (no_asm))
   1.331 +done
   1.332 +
   1.333 +(* unused *)
   1.334 +lemma ign_res_eq_subst_res: "P\<down>=w\<leftarrow>w = P\<down>"
   1.335 +apply (rule ext)
   1.336 +apply (rule ext)
   1.337 +apply (rule ext)
   1.338 +apply (simp (no_asm))
   1.339 +done
   1.340 +
   1.341 +(* unused *)
   1.342 +lemma subst_Bool_ign_res_eq: "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z  \<and> Y=x)"
   1.343 +apply (simp (no_asm))
   1.344 +done
   1.345 +
   1.346 +subsection "RefVar"
   1.347 +
   1.348 +constdefs
   1.349 +  RefVar    :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13)
   1.350 + "vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"
   1.351 + 
   1.352 +lemma RefVar_def2 [simp]: "(vf ..; P) Y s =  
   1.353 +  P (Var (fst (vf s))) (snd (vf s))"
   1.354 +apply (unfold RefVar_def Let_def)
   1.355 +apply (simp (no_asm) add: split_beta)
   1.356 +done
   1.357 +
   1.358 +subsection "allocation"
   1.359 +
   1.360 +constdefs
   1.361 +  Alloc      :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.362 + "Alloc G otag P \<equiv> \<lambda>Y s Z.
   1.363 +                   \<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"
   1.364 +
   1.365 +  SXAlloc     :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.366 + "SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"
   1.367 +
   1.368 +
   1.369 +lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =  
   1.370 +       (\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"
   1.371 +apply (unfold Alloc_def)
   1.372 +apply (simp (no_asm))
   1.373 +done
   1.374 +
   1.375 +lemma SXAlloc_def2 [simp]: 
   1.376 +  "SXAlloc G P Y s Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"
   1.377 +apply (unfold SXAlloc_def)
   1.378 +apply (simp (no_asm))
   1.379 +done
   1.380 +
   1.381 +section "validity"
   1.382 +
   1.383 +constdefs
   1.384 +  type_ok  :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool"
   1.385 + "type_ok G t s \<equiv> \<exists>L T C. (normal s \<longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) \<and> s\<Colon>\<preceq>(G,L)"
   1.386 +
   1.387 +datatype    'a triple = triple "('a assn)" "term" "('a assn)" (** should be
   1.388 +something like triple = \<forall>'a. triple ('a assn) term ('a assn)   **)
   1.389 +                                        ("{(1_)}/ _>/ {(1_)}"      [3,65,3]75)
   1.390 +types    'a triples = "'a triple set"
   1.391 +
   1.392 +syntax
   1.393 +
   1.394 +  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
   1.395 +                                         ("{(1_)}/ _=>/ {(1_)}"    [3,80,3] 75)
   1.396 +  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
   1.397 +                                         ("{(1_)}/ _->/ {(1_)}"    [3,80,3] 75)
   1.398 +  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
   1.399 +                                         ("{(1_)}/ _#>/ {(1_)}"    [3,65,3] 75)
   1.400 +  stmt_triple  :: "['a assn, stmt,        'a assn] \<Rightarrow> 'a triple"
   1.401 +                                         ("{(1_)}/ ._./ {(1_)}"     [3,65,3] 75)
   1.402 +
   1.403 +syntax (xsymbols)
   1.404 +
   1.405 +  triple       :: "['a assn, term        ,'a assn] \<Rightarrow> 'a triple"
   1.406 +                                         ("{(1_)}/ _\<succ>/ {(1_)}"     [3,65,3] 75)
   1.407 +  var_triple   :: "['a assn, var         ,'a assn] \<Rightarrow> 'a triple"
   1.408 +                                         ("{(1_)}/ _=\<succ>/ {(1_)}"    [3,80,3] 75)
   1.409 +  expr_triple  :: "['a assn, expr        ,'a assn] \<Rightarrow> 'a triple"
   1.410 +                                         ("{(1_)}/ _-\<succ>/ {(1_)}"    [3,80,3] 75)
   1.411 +  exprs_triple :: "['a assn, expr list   ,'a assn] \<Rightarrow> 'a triple"
   1.412 +                                         ("{(1_)}/ _\<doteq>\<succ>/ {(1_)}"    [3,65,3] 75)
   1.413 +
   1.414 +translations
   1.415 +  "{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
   1.416 +  "{P} e=\<succ> {Q}" == "{P} In2  e\<succ> {Q}"
   1.417 +  "{P} e\<doteq>\<succ> {Q}" == "{P} In3  e\<succ> {Q}"
   1.418 +  "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
   1.419 +
   1.420 +lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
   1.421 +apply (rule injI)
   1.422 +apply auto
   1.423 +done
   1.424 +
   1.425 +lemma triple_inj_eq: "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')"
   1.426 +apply auto
   1.427 +done
   1.428 +
   1.429 +constdefs
   1.430 +  mtriples  :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow> 
   1.431 +                ('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times>  'sig) set \<Rightarrow> 'a triples"
   1.432 +                                     ("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75)
   1.433 + "{{P} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig-\<succ> {Q C sig})`ms"
   1.434 +  
   1.435 +consts
   1.436 +
   1.437 + triple_valid :: "prog \<Rightarrow> nat \<Rightarrow>        'a triple  \<Rightarrow> bool"
   1.438 +                                                (   "_\<Turnstile>_:_" [61,0, 58] 57)
   1.439 +    ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   1.440 +                                                ("_,_|\<Turnstile>_"   [61,58,58] 57)
   1.441 +    ax_derivs :: "prog \<Rightarrow> ('b triples \<times> 'a triples) set"
   1.442 +
   1.443 +syntax
   1.444 +
   1.445 + triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   1.446 +                                                (  "_||=_:_" [61,0, 58] 57)
   1.447 +     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   1.448 +                                                ( "_,_|=_"   [61,58,58] 57)
   1.449 +     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   1.450 +                                                ("_,_||-_"   [61,58,58] 57)
   1.451 +     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   1.452 +                                                ( "_,_|-_"   [61,58,58] 57)
   1.453 +
   1.454 +syntax (xsymbols)
   1.455 +
   1.456 + triples_valid:: "prog \<Rightarrow> nat \<Rightarrow>         'a triples \<Rightarrow> bool"
   1.457 +                                                (  "_|\<Turnstile>_:_" [61,0, 58] 57)
   1.458 +     ax_valid :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   1.459 +                                                ( "_,_\<Turnstile>_"   [61,58,58] 57)
   1.460 +     ax_Derivs:: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
   1.461 +                                                ("_,_|\<turnstile>_"   [61,58,58] 57)
   1.462 +     ax_Deriv :: "prog \<Rightarrow>  'b triples \<Rightarrow> 'a triple  \<Rightarrow> bool"
   1.463 +                                                ( "_,_\<turnstile>_"   [61,58,58] 57)
   1.464 +
   1.465 +defs  triple_valid_def:  "G\<Turnstile>n:t  \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
   1.466 +                          \<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>
   1.467 +                          (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"
   1.468 +translations         "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
   1.469 +defs   ax_valids_def:"G,A|\<Turnstile>ts  \<equiv>  \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
   1.470 +translations         "G,A \<Turnstile>t"  == "G,A|\<Turnstile>{t}"
   1.471 +                     "G,A|\<turnstile>ts" == "(A,ts) \<in> ax_derivs G"
   1.472 +                     "G,A \<turnstile>t"  == "G,A|\<turnstile>{t}"
   1.473 +
   1.474 +lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =  
   1.475 + (\<forall>Y s Z. P Y s Z 
   1.476 +  \<longrightarrow> (\<exists>L. (normal s \<longrightarrow> (\<exists>T C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T)) \<and> s\<Colon>\<preceq>(G,L)) \<longrightarrow> 
   1.477 +  (\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))"
   1.478 +apply (unfold triple_valid_def type_ok_def)
   1.479 +apply (simp (no_asm))
   1.480 +done
   1.481 +
   1.482 +
   1.483 +declare split_paired_All [simp del] split_paired_Ex [simp del] 
   1.484 +declare split_if     [split del] split_if_asm     [split del] 
   1.485 +        option.split [split del] option.split_asm [split del]
   1.486 +ML_setup {*
   1.487 +simpset_ref() := simpset() delloop "split_all_tac";
   1.488 +claset_ref () := claset () delSWrapper "split_all_tac"
   1.489 +*}
   1.490 +
   1.491 +
   1.492 +inductive "ax_derivs G" intros
   1.493 +
   1.494 +  empty: " G,A|\<turnstile>{}"
   1.495 +  insert:"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
   1.496 +          G,A|\<turnstile>insert t ts"
   1.497 +
   1.498 +  asm:   "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
   1.499 +
   1.500 +(* could be added for convenience and efficiency, but is not necessary
   1.501 +  cut:   "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
   1.502 +           G,A |\<turnstile>ts"
   1.503 +*)
   1.504 +  weaken:"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
   1.505 +
   1.506 +  conseq:"\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
   1.507 +         (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
   1.508 +                                 Q  Y' s' Z ))
   1.509 +                                         \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
   1.510 +
   1.511 +  hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
   1.512 +
   1.513 +  Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
   1.514 +
   1.515 +  (* variables *)
   1.516 +  LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
   1.517 +
   1.518 +  FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};
   1.519 +          G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
   1.520 +                                 G,A\<turnstile>{Normal P} {C,stat}e..fn=\<succ> {R}"
   1.521 +
   1.522 +  AVar:  "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
   1.523 +          \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>
   1.524 +                                 G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
   1.525 +  (* expressions *)
   1.526 +
   1.527 +  NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
   1.528 +                                 G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
   1.529 +
   1.530 +  NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};  G,A\<turnstile>{Q} e-\<succ>
   1.531 +	  {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>
   1.532 +                                 G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
   1.533 +
   1.534 +  Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.535 +          abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   1.536 +                                 G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
   1.537 +
   1.538 +  Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v:. \<lambda>s..
   1.539 +                  Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
   1.540 +                                 G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
   1.541 +
   1.542 +  Lit:                          "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v-\<succ> {P}"
   1.543 +
   1.544 +  Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
   1.545 +
   1.546 +  Acc:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
   1.547 +                                 G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
   1.548 +
   1.549 +  Ass:  "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
   1.550 +     \<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>
   1.551 +                                 G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
   1.552 +
   1.553 +  Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
   1.554 +          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk> \<Longrightarrow>
   1.555 +                                 G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
   1.556 +
   1.557 +  Call: 
   1.558 +"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
   1.559 +  \<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
   1.560 + (\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>
   1.561 +      invC = invocation_class mode (store s) a statT \<and>
   1.562 +         l = locals (store s)) ;.
   1.563 +      init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.
   1.564 +      (\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}
   1.565 + Methd declC \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>
   1.566 +         G,A\<turnstile>{Normal P} {statT,mode}e\<cdot>mn({pTs}args)-\<succ> {S}"
   1.567 +
   1.568 +  Methd:"\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
   1.569 +                                 G,A|\<turnstile>{{P} Methd-\<succ>  {Q} | ms}"
   1.570 +
   1.571 +  Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q}; 
   1.572 +  G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk> 
   1.573 +    \<Longrightarrow>
   1.574 +                                 G,A\<turnstile>{Normal P} Body D c-\<succ> {R}"
   1.575 +  
   1.576 +  (* expression lists *)
   1.577 +
   1.578 +  Nil:                          "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
   1.579 +
   1.580 +  Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
   1.581 +          \<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
   1.582 +                                 G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
   1.583 +
   1.584 +  (* statements *)
   1.585 +
   1.586 +  Skip:                         "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"
   1.587 +
   1.588 +  Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.589 +                                 G,A\<turnstile>{Normal P} .Expr e. {Q}"
   1.590 +
   1.591 +  Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb (Break l)) .; Q}\<rbrakk> \<Longrightarrow>
   1.592 +                           G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"
   1.593 +
   1.594 +  Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.595 +          G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
   1.596 +                                 G,A\<turnstile>{Normal P} .c1;;c2. {R}"
   1.597 +
   1.598 +  If:   "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   1.599 +          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
   1.600 +                                 G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
   1.601 +(* unfolding variant of Loop, not needed here
   1.602 +  LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
   1.603 +          \<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
   1.604 +         \<Longrightarrow>              G,A\<turnstile>{Normal P} .While(e) c. {Q}"
   1.605 +*)
   1.606 +  Loop: "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
   1.607 +          G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
   1.608 +                            G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
   1.609 +(** Beware of polymorphic_Loop below: should be identical terms **)
   1.610 +  
   1.611 +  Do: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Do j. {P}"
   1.612 +
   1.613 +  Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>
   1.614 +                                 G,A\<turnstile>{Normal P} .Throw e. {Q}"
   1.615 +
   1.616 +  Try:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
   1.617 +          G,A\<turnstile>{Q \<and>. (\<lambda>s.  G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
   1.618 +              (Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
   1.619 +                                 G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
   1.620 +
   1.621 +  Fin:  "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
   1.622 +      \<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}
   1.623 +              .c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>
   1.624 +                                 G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
   1.625 +
   1.626 +  Done:                       "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"
   1.627 +
   1.628 +  Init: "\<lbrakk>the (class G C) = c;
   1.629 +          G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
   1.630 +              .(if C = Object then Skip else Init (super c)). {Q};
   1.631 +      \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}
   1.632 +              .init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
   1.633 +                               G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"
   1.634 +
   1.635 +axioms (** these terms are the same as above, but with generalized typing **)
   1.636 +  polymorphic_conseq:
   1.637 +        "\<forall>Y s Z . P  Y s Z  \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'. 
   1.638 +        (\<forall>Y   Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
   1.639 +                                Q  Y' s' Z ))
   1.640 +                                         \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
   1.641 +
   1.642 +  polymorphic_Loop:
   1.643 +        "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; 
   1.644 +          G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>
   1.645 +                            G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"
   1.646 +
   1.647 +constdefs
   1.648 + adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
   1.649 +"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)"
   1.650 +
   1.651 +
   1.652 +section "rules derived by induction"
   1.653 +
   1.654 +lemma cut_valid: "\<lbrakk>G,A'|\<Turnstile>ts; G,A|\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A|\<Turnstile>ts"
   1.655 +apply (unfold ax_valids_def)
   1.656 +apply fast
   1.657 +done
   1.658 +
   1.659 +(*if cut is available
   1.660 +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>  
   1.661 +       G,A|\<turnstile>ts"
   1.662 +b y etac ax_derivs.cut 1;
   1.663 +b y eatac ax_derivs.asm 1 1;
   1.664 +qed "ax_thin";
   1.665 +*)
   1.666 +lemma ax_thin [rule_format (no_asm)]: 
   1.667 +  "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
   1.668 +apply (erule ax_derivs.induct)
   1.669 +apply                (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
   1.670 +apply                (rule ax_derivs.empty)
   1.671 +apply               (erule (1) ax_derivs.insert)
   1.672 +apply              (fast intro: ax_derivs.asm)
   1.673 +(*apply           (fast intro: ax_derivs.cut) *)
   1.674 +apply            (fast intro: ax_derivs.weaken)
   1.675 +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)
   1.676 +(* 31 subgoals *)
   1.677 +prefer 16 (* Methd *)
   1.678 +apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
   1.679 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
   1.680 +                     THEN_ALL_NEW Blast_tac) *})
   1.681 +apply (erule ax_derivs.Call)
   1.682 +apply   clarify 
   1.683 +apply   blast
   1.684 +
   1.685 +apply   (rule allI)+ 
   1.686 +apply   (drule spec)+
   1.687 +apply   blast
   1.688 +done
   1.689 +
   1.690 +lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"
   1.691 +apply (erule ax_thin)
   1.692 +apply fast
   1.693 +done
   1.694 +
   1.695 +lemma subset_mtriples_iff: 
   1.696 +  "ts \<subseteq> {{P} mb-\<succ> {Q} | ms} = (\<exists>ms'. ms'\<subseteq>ms \<and>  ts = {{P} mb-\<succ> {Q} | ms'})"
   1.697 +apply (unfold mtriples_def)
   1.698 +apply (rule subset_image_iff)
   1.699 +done
   1.700 +
   1.701 +lemma weaken: 
   1.702 + "G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
   1.703 +apply (erule ax_derivs.induct)
   1.704 +(*36 subgoals*)
   1.705 +apply       (tactic "ALLGOALS strip_tac")
   1.706 +apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
   1.707 +         etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})
   1.708 +apply       (tactic "TRYALL hyp_subst_tac")
   1.709 +apply       (simp, rule ax_derivs.empty)
   1.710 +apply      (drule subset_insertD)
   1.711 +apply      (blast intro: ax_derivs.insert)
   1.712 +apply     (fast intro: ax_derivs.asm)
   1.713 +(*apply  (blast intro: ax_derivs.cut) *)
   1.714 +apply   (fast intro: ax_derivs.weaken)
   1.715 +apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
   1.716 +(*31 subgoals*)
   1.717 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
   1.718 +                   THEN_ALL_NEW Fast_tac) *})
   1.719 +(*1 subgoal*)
   1.720 +apply (clarsimp simp add: subset_mtriples_iff)
   1.721 +apply (rule ax_derivs.Methd)
   1.722 +apply (drule spec)
   1.723 +apply (erule impE)
   1.724 +apply  (rule exI)
   1.725 +apply  (erule conjI)
   1.726 +apply  (rule HOL.refl)
   1.727 +oops (* dead end, Methd is to blame *)
   1.728 +
   1.729 +
   1.730 +section "rules derived from conseq"
   1.731 +
   1.732 +lemma conseq12: "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'};  
   1.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>  
   1.734 +  Q Y' s' Z)\<rbrakk>  
   1.735 +  \<Longrightarrow>  G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"
   1.736 +apply (rule polymorphic_conseq)
   1.737 +apply clarsimp
   1.738 +apply blast
   1.739 +done
   1.740 +
   1.741 +(*unused, but nice variant*)
   1.742 +lemma conseq12': "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'}; \<forall>s Y' s'.  
   1.743 +       (\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>  
   1.744 +       (\<forall>Y Z. P  Y s Z \<longrightarrow> Q  Y' s' Z)\<rbrakk>  
   1.745 +  \<Longrightarrow>  G,A\<turnstile>{P } t\<succ> {Q }"
   1.746 +apply (erule conseq12)
   1.747 +apply fast
   1.748 +done
   1.749 +
   1.750 +lemma conseq12_from_conseq12': "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'};  
   1.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>  
   1.752 +  Q Y' s' Z)\<rbrakk>  
   1.753 +  \<Longrightarrow>  G,A\<turnstile>{P } t\<succ> {Q }"
   1.754 +apply (erule conseq12')
   1.755 +apply blast
   1.756 +done
   1.757 +
   1.758 +lemma conseq1: "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q}"
   1.759 +apply (erule conseq12)
   1.760 +apply blast
   1.761 +done
   1.762 +
   1.763 +lemma conseq2: "\<lbrakk>G,A\<turnstile>{P} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   1.764 +apply (erule conseq12)
   1.765 +apply blast
   1.766 +done
   1.767 +
   1.768 +lemma ax_escape: "\<lbrakk>\<forall>Y s Z. P Y s Z \<longrightarrow> G,A\<turnstile>{\<lambda>Y' s' Z'. (Y',s') = (Y,s)} t\<succ> {\<lambda>Y s Z'. Q Y s Z}\<rbrakk> \<Longrightarrow>  
   1.769 +  G,A\<turnstile>{P} t\<succ> {Q}"
   1.770 +apply (rule polymorphic_conseq)
   1.771 +apply force
   1.772 +done
   1.773 +
   1.774 +(* unused *)
   1.775 +lemma ax_constant: "\<lbrakk> C \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{\<lambda>Y s Z. C \<and> P Y s Z} t\<succ> {Q}"
   1.776 +apply (rule ax_escape (* unused *))
   1.777 +apply clarify
   1.778 +apply (rule conseq12)
   1.779 +apply  fast
   1.780 +apply auto
   1.781 +done
   1.782 +(*alternative (more direct) proof:
   1.783 +apply (rule ax_derivs.conseq) *)(* unused *)(*
   1.784 +apply (fast)
   1.785 +*)
   1.786 +
   1.787 +
   1.788 +lemma ax_impossible [intro]: "G,A\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q}"
   1.789 +apply (rule ax_escape)
   1.790 +apply clarify
   1.791 +done
   1.792 +
   1.793 +(* unused *)
   1.794 +lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"
   1.795 +apply auto
   1.796 +done
   1.797 +lemma ax_nochange:"G,A\<turnstile>{\<lambda>Y s Z. (Y,s)=Z} t\<succ> {\<lambda>Y s Z. (Y,s)=Z} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {P}"
   1.798 +apply (erule conseq12)
   1.799 +apply auto
   1.800 +apply (erule (1) ax_nochange_lemma)
   1.801 +done
   1.802 +
   1.803 +(* unused *)
   1.804 +lemma ax_trivial: "G,A\<turnstile>{P}  t\<succ> {\<lambda>Y s Z. True}"
   1.805 +apply (rule polymorphic_conseq(* unused *))
   1.806 +apply auto
   1.807 +done
   1.808 +
   1.809 +(* unused *)
   1.810 +lemma ax_disj: "\<lbrakk>G,A\<turnstile>{P1} t\<succ> {Q1}; G,A\<turnstile>{P2} t\<succ> {Q2}\<rbrakk> \<Longrightarrow>  
   1.811 +  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}"
   1.812 +apply (rule ax_escape (* unused *))
   1.813 +apply safe
   1.814 +apply  (erule conseq12, fast)+
   1.815 +done
   1.816 +
   1.817 +(* unused *)
   1.818 +lemma ax_supd_shuffle: "(\<exists>Q. G,A\<turnstile>{P} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =  
   1.819 +       (\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"
   1.820 +apply (best elim!: conseq1 conseq2)
   1.821 +done
   1.822 +
   1.823 +lemma ax_cases: "\<lbrakk>G,A\<turnstile>{P \<and>.       C} t\<succ> {Q};  
   1.824 +                       G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   1.825 +apply (unfold peek_and_def)
   1.826 +apply (rule ax_escape)
   1.827 +apply clarify
   1.828 +apply (case_tac "C s")
   1.829 +apply  (erule conseq12, force)+
   1.830 +done
   1.831 +(*alternative (more direct) proof:
   1.832 +apply (rule rtac ax_derivs.conseq) *)(* unused *)(*
   1.833 +apply clarify
   1.834 +apply (case_tac "C s")
   1.835 +apply  force+
   1.836 +*)
   1.837 +
   1.838 +lemma ax_adapt: "G,A\<turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   1.839 +apply (unfold adapt_pre_def)
   1.840 +apply (erule conseq12)
   1.841 +apply fast
   1.842 +done
   1.843 +
   1.844 +lemma adapt_pre_adapts: "G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"
   1.845 +apply (unfold adapt_pre_def)
   1.846 +apply (simp add: ax_valids_def triple_valid_def2)
   1.847 +apply fast
   1.848 +done
   1.849 +
   1.850 +
   1.851 +lemma adapt_pre_weakest: 
   1.852 +"\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
   1.853 +  P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"
   1.854 +apply (unfold adapt_pre_def)
   1.855 +apply (drule spec)
   1.856 +apply (drule_tac x = "{}" in spec)
   1.857 +apply (drule_tac x = "In1r Skip" in spec)
   1.858 +apply (simp add: ax_valids_def triple_valid_def2)
   1.859 +oops
   1.860 +
   1.861 +(*
   1.862 +Goal "\<forall>(A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>  
   1.863 +  wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>{P} t\<succ> {Q::'a assn} \<Longrightarrow> G,A\<turnstile>{P'} t\<succ> {Q'::'a assn}"
   1.864 +b y fatac ax_sound 1 1;
   1.865 +b y asm_full_simp_tac (simpset() addsimps [ax_valids_def,triple_valid_def2]) 1;
   1.866 +b y rtac ax_no_hazard 1; 
   1.867 +b y etac conseq12 1;
   1.868 +b y Clarify_tac 1;
   1.869 +b y case_tac "\<forall>Z. \<not>P Y s Z" 1;
   1.870 +b y smp_tac 2 1;
   1.871 +b y etac thin_rl 1;
   1.872 +b y etac thin_rl 1;
   1.873 +b y clarsimp_tac (claset(), simpset() addsimps [type_ok_def]) 1;
   1.874 +b y subgoal_tac "G|\<Turnstile>n:A" 1;
   1.875 +b y smp_tac 1 1;
   1.876 +b y smp_tac 3 1;
   1.877 +b y etac impE 1;
   1.878 + back();
   1.879 + b y Fast_tac 1;
   1.880 +b y 
   1.881 +b y rotate_tac 2 1;
   1.882 +b y etac thin_rl 1;
   1.883 +b y  etac thin_rl 2;
   1.884 +b y  etac thin_rl 2;
   1.885 +b y  Clarify_tac 2;
   1.886 +b y  dtac spec 2;
   1.887 +b y  EVERY'[dtac spec, mp_tac] 2;
   1.888 +b y  thin_tac "\<forall>n Y s Z. ?PP n Y s Z" 2;
   1.889 +b y  thin_tac "P' Y s Z" 2;
   1.890 +b y  Blast_tac 2;
   1.891 +b y smp_tac 3 1;
   1.892 +b y case_tac "\<forall>Z. \<not>P Y s Z" 1;
   1.893 +b y dres_inst_tac [("x","In1r Skip")] spec 1;
   1.894 +b y Full_simp_tac 1;
   1.895 +*)
   1.896 +
   1.897 +lemma peek_and_forget1_Normal: 
   1.898 + "G,A\<turnstile>{Normal P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"
   1.899 +apply (erule conseq1)
   1.900 +apply (simp (no_asm))
   1.901 +done
   1.902 +
   1.903 +lemma peek_and_forget1: "G,A\<turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"
   1.904 +apply (erule conseq1)
   1.905 +apply (simp (no_asm))
   1.906 +done
   1.907 +
   1.908 +lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal] 
   1.909 +
   1.910 +lemma peek_and_forget2: "G,A\<turnstile>{P} t\<succ> {Q \<and>. p} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"
   1.911 +apply (erule conseq2)
   1.912 +apply (simp (no_asm))
   1.913 +done
   1.914 +
   1.915 +lemma ax_subst_Val_allI: "\<forall>v. G,A\<turnstile>{(P'               v )\<leftarrow>Val v} t\<succ> {Q v} \<Longrightarrow>  
   1.916 +      \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"
   1.917 +apply (force elim!: conseq1)
   1.918 +done
   1.919 +
   1.920 +lemma ax_subst_Var_allI: "\<forall>v. G,A\<turnstile>{(P'               v )\<leftarrow>Var v} t\<succ> {Q v} \<Longrightarrow>  
   1.921 +      \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"
   1.922 +apply (force elim!: conseq1)
   1.923 +done
   1.924 +
   1.925 +lemma ax_subst_Vals_allI: "(\<forall>v. G,A\<turnstile>{(     P'          v )\<leftarrow>Vals v} t\<succ> {Q v}) \<Longrightarrow>  
   1.926 +       \<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"
   1.927 +apply (force elim!: conseq1)
   1.928 +done
   1.929 +
   1.930 +
   1.931 +section "alternative axioms"
   1.932 +
   1.933 +lemma ax_Lit2: 
   1.934 +  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v-\<succ> {Normal (P\<down>=Val v)}"
   1.935 +apply (rule ax_derivs.Lit [THEN conseq1])
   1.936 +apply force
   1.937 +done
   1.938 +lemma ax_Lit2_test_complete: 
   1.939 +  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v-\<succ> {P}"
   1.940 +apply (rule ax_Lit2 [THEN conseq2])
   1.941 +apply force
   1.942 +done
   1.943 +
   1.944 +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))}"
   1.945 +apply (rule ax_derivs.LVar [THEN conseq1])
   1.946 +apply force
   1.947 +done
   1.948 +
   1.949 +lemma ax_Super2: "G,(A::'a triple set)\<turnstile>
   1.950 +  {Normal P::'a assn} Super-\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"
   1.951 +apply (rule ax_derivs.Super [THEN conseq1])
   1.952 +apply force
   1.953 +done
   1.954 +
   1.955 +lemma ax_Nil2: 
   1.956 +  "G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"
   1.957 +apply (rule ax_derivs.Nil [THEN conseq1])
   1.958 +apply force
   1.959 +done
   1.960 +
   1.961 +
   1.962 +section "misc derived structural rules"
   1.963 +
   1.964 +(* unused *)
   1.965 +lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms. 
   1.966 +    G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
   1.967 +       G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
   1.968 +apply (frule (1) finite_subset)
   1.969 +apply (erule make_imp)
   1.970 +apply (erule thin_rl)
   1.971 +apply (erule finite_induct)
   1.972 +apply  (unfold mtriples_def)
   1.973 +apply  (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+
   1.974 +apply force
   1.975 +done
   1.976 +lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]
   1.977 +
   1.978 +lemma ax_derivs_insertD: 
   1.979 + "G,(A::'a triple set)|\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A|\<turnstile>ts"
   1.980 +apply (fast intro: ax_derivs.weaken)
   1.981 +done
   1.982 +
   1.983 +lemma ax_methods_spec: 
   1.984 +"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
   1.985 +apply (erule ax_derivs.weaken)
   1.986 +apply (force del: image_eqI intro: rev_image_eqI)
   1.987 +done
   1.988 +
   1.989 +(* this version is used to avoid using the cut rule *)
   1.990 +lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
   1.991 +  ((\<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>  
   1.992 +      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
   1.993 +apply (frule (1) finite_subset)
   1.994 +apply (erule make_imp)
   1.995 +apply (erule thin_rl)
   1.996 +apply (erule finite_induct)
   1.997 +apply  clarsimp+
   1.998 +apply (drule ax_derivs_insertD)
   1.999 +apply (rule ax_derivs.insert)
  1.1000 +apply  (simp (no_asm_simp) only: split_tupled_all)
  1.1001 +apply  (auto elim: ax_methods_spec)
  1.1002 +done
  1.1003 +lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]
  1.1004 + 
  1.1005 +lemma ax_no_hazard: 
  1.1006 +  "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}"
  1.1007 +apply (erule ax_cases)
  1.1008 +apply (rule ax_derivs.hazard [THEN conseq1])
  1.1009 +apply force
  1.1010 +done
  1.1011 +
  1.1012 +lemma ax_free_wt: 
  1.1013 + "(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T) 
  1.1014 +  \<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow> 
  1.1015 +  G,A\<turnstile>{Normal P} t\<succ> {Q}"
  1.1016 +apply (rule ax_no_hazard)
  1.1017 +apply (rule ax_escape)
  1.1018 +apply clarify
  1.1019 +apply (erule mp [THEN conseq12])
  1.1020 +apply  (auto simp add: type_ok_def)
  1.1021 +done
  1.1022 +
  1.1023 +ML {*
  1.1024 +bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
  1.1025 +*}
  1.1026 +declare ax_Abrupts [intro!]
  1.1027 +
  1.1028 +lemmas ax_Normal_cases = ax_cases [of _ _ normal]
  1.1029 +
  1.1030 +lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"
  1.1031 +apply (rule ax_Normal_cases)
  1.1032 +apply  (rule ax_derivs.Skip)
  1.1033 +apply fast
  1.1034 +done
  1.1035 +lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
  1.1036 +
  1.1037 +
  1.1038 +section "derived rules for methd call"
  1.1039 +
  1.1040 +lemma ax_Call_known_DynT: 
  1.1041 +"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT; 
  1.1042 +  \<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.
  1.1043 +  init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)} 
  1.1044 +    Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1.1045 +  \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>  
  1.1046 +       {R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>
  1.1047 +                     C = invocation_declclass 
  1.1048 +                            G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};  
  1.1049 +       G,(A::'a triple set)\<turnstile>{Normal P} e-\<succ> {Q::'a assn}\<rbrakk>  
  1.1050 +   \<Longrightarrow> G,A\<turnstile>{Normal P} {statT,IntVir}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1.1051 +apply (erule ax_derivs.Call)
  1.1052 +apply  safe
  1.1053 +apply  (erule spec)
  1.1054 +apply (rule ax_escape, clarsimp)
  1.1055 +apply (drule spec, drule spec, drule spec,erule conseq12)
  1.1056 +apply force
  1.1057 +done
  1.1058 +
  1.1059 +
  1.1060 +lemma ax_Call_Static: 
  1.1061 + "\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.  
  1.1062 +               init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}  
  1.1063 +              Methd C \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> {set_lvars l .; S}; 
  1.1064 +  G,A\<turnstile>{Normal P} e-\<succ> {Q};
  1.1065 +  \<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn)  a 
  1.1066 +  \<and>. (\<lambda> s. C=invocation_declclass 
  1.1067 +                G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}
  1.1068 +\<rbrakk>  \<Longrightarrow>  G,A\<turnstile>{Normal P} {statT,Static}e\<cdot>mn({pTs}args)-\<succ> {S}"
  1.1069 +apply (erule ax_derivs.Call)
  1.1070 +apply  safe
  1.1071 +apply  (erule spec)
  1.1072 +apply (rule ax_escape, clarsimp)
  1.1073 +apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)
  1.1074 +apply (drule spec,drule spec,drule spec, erule conseq12)
  1.1075 +apply (force simp add: init_lvars_def)
  1.1076 +done
  1.1077 +
  1.1078 +lemma ax_Methd1: 
  1.1079 + "\<lbrakk>G,A\<union>{{P} Methd-\<succ> {Q} | ms}|\<turnstile> {{P} body G-\<succ> {Q} | ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow> 
  1.1080 +       G,A\<turnstile>{Normal (P C sig)} Methd C sig-\<succ> {Q C sig}"
  1.1081 +apply (drule ax_derivs.Methd)
  1.1082 +apply (unfold mtriples_def)
  1.1083 +apply (erule (1) ax_methods_spec)
  1.1084 +done
  1.1085 +
  1.1086 +lemma ax_MethdN: 
  1.1087 +"G,insert({Normal P} Methd  C sig-\<succ> {Q}) A\<turnstile> 
  1.1088 +          {Normal P} body G C sig-\<succ> {Q} \<Longrightarrow>  
  1.1089 +      G,A\<turnstile>{Normal P} Methd   C sig-\<succ> {Q}"
  1.1090 +apply (rule ax_Methd1)
  1.1091 +apply  (rule_tac [2] singletonI)
  1.1092 +apply (unfold mtriples_def)
  1.1093 +apply clarsimp
  1.1094 +done
  1.1095 +
  1.1096 +lemma ax_StatRef: 
  1.1097 +  "G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt-\<succ> {P::'a assn}"
  1.1098 +apply (rule ax_derivs.Cast)
  1.1099 +apply (rule ax_Lit2 [THEN conseq2])
  1.1100 +apply clarsimp
  1.1101 +done
  1.1102 +
  1.1103 +section "rules derived from Init and Done"
  1.1104 +
  1.1105 +  lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;  
  1.1106 +     \<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}  
  1.1107 +            .init c. {set_lvars l .; R};   
  1.1108 +         G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}  
  1.1109 +  .Init (super c). {Q}\<rbrakk> \<Longrightarrow>  
  1.1110 +  G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"
  1.1111 +apply (erule ax_derivs.Init)
  1.1112 +apply  (simp (no_asm_simp))
  1.1113 +apply assumption
  1.1114 +done
  1.1115 +
  1.1116 +lemma ax_Init_Skip_lemma: 
  1.1117 +"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}
  1.1118 +  .Skip. {(set_lvars l .; P)::'a assn}"
  1.1119 +apply (rule allI)
  1.1120 +apply (rule ax_SkipI)
  1.1121 +apply clarsimp
  1.1122 +done
  1.1123 +
  1.1124 +lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object; 
  1.1125 +       P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);  
  1.1126 +       G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>  
  1.1127 +       G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"
  1.1128 +apply (rule_tac C = "initd C" in ax_cases)
  1.1129 +apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1.1130 +apply (simp (no_asm))
  1.1131 +apply (erule (1) ax_InitS)
  1.1132 +apply  simp
  1.1133 +apply  (rule ax_Init_Skip_lemma)
  1.1134 +apply (erule conseq1)
  1.1135 +apply force
  1.1136 +done
  1.1137 +
  1.1138 +lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>
  1.1139 +  {Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)} 
  1.1140 +       .Init Object. {(P \<and>. initd Object)::'a assn}"
  1.1141 +apply (rule ax_derivs.Init)
  1.1142 +apply   (drule class_Object, force)
  1.1143 +apply (simp_all (no_asm))
  1.1144 +apply (rule_tac [2] ax_Init_Skip_lemma)
  1.1145 +apply (rule ax_SkipI, force)
  1.1146 +done
  1.1147 +
  1.1148 +lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;  
  1.1149 +       (P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>  
  1.1150 +  G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"
  1.1151 +apply (rule_tac C = "initd Object" in ax_cases)
  1.1152 +apply  (rule conseq1, rule ax_derivs.Done, clarsimp)
  1.1153 +apply (erule ax_Init_Object [THEN conseq1])
  1.1154 +apply force
  1.1155 +done
  1.1156 +
  1.1157 +
  1.1158 +section "introduction rules for Alloc and SXAlloc"
  1.1159 +
  1.1160 +lemma ax_SXAlloc_Normal: "G,A\<turnstile>{P} .c. {Normal Q} \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"
  1.1161 +apply (erule conseq2)
  1.1162 +apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)
  1.1163 +done
  1.1164 +
  1.1165 +lemma ax_Alloc: 
  1.1166 +  "G,A\<turnstile>{P} t\<succ> {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1.1167 + Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>. 
  1.1168 +    heap_free (Suc (Suc 0))}
  1.1169 +   \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"
  1.1170 +apply (erule conseq2)
  1.1171 +apply (auto elim!: halloc_elim_cases)
  1.1172 +done
  1.1173 +
  1.1174 +lemma ax_Alloc_Arr: 
  1.1175 + "G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>  
  1.1176 +  (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1.1177 +  Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>. 
  1.1178 +   heap_free (Suc (Suc 0))} \<Longrightarrow>  
  1.1179 + G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"
  1.1180 +apply (erule conseq2)
  1.1181 +apply (auto elim!: halloc_elim_cases)
  1.1182 +done
  1.1183 +
  1.1184 +lemma ax_SXAlloc_catch_SXcpt: 
  1.1185 + "\<lbrakk>G,A\<turnstile>{P} t\<succ> {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>  
  1.1186 +  (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>  
  1.1187 +  Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))  
  1.1188 +  \<and>. heap_free (Suc (Suc 0))}\<rbrakk> \<Longrightarrow>  
  1.1189 +  G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"
  1.1190 +apply (erule conseq2)
  1.1191 +apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)
  1.1192 +done
  1.1193 +
  1.1194 +end