12854

1 
(* Title: isabelle/Bali/AxSem.thy


2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1998 Technische Universitaet Muenchen


5 
*)


6 


7 
header {* Axiomatic semantics of Java expressions and statements


8 
(see also Eval.thy)


9 
*}


10 


11 
theory AxSem = Evaln + TypeSafe:


12 


13 
text {*


14 
design issues:


15 
\begin{itemize}


16 
\item a strong version of validity for triples with premises, namely one that


17 
takes the recursive depth needed to complete execution, enables


18 
correctness proof


19 
\item auxiliary variables are handled firstclass (> Thomas Kleymann)


20 
\item expressions not flattened to elementary assignments (as usual for


21 
axiomatic semantics) but treated firstclass => explicit result value


22 
handling


23 
\item intermediate values not on triple, but on assertion level


24 
(with result entry)


25 
\item multiple results with semantical substitution mechnism not requiring a


26 
stack


27 
\item because of dynamic method binding, terms need to be dependent on state.


28 
this is also useful for conditional expressions and statements


29 
\item result values in triples exactly as in eval relation (also for xcpt


30 
states)


31 
\item validity: additional assumption of state conformance and welltypedness,


32 
which is required for soundness and thus rule hazard required of completeness


33 
\end{itemize}


34 


35 
restrictions:


36 
\begin{itemize}


37 
\item all triples in a derivation are of the same type (due to weak


38 
polymorphism)


39 
\end{itemize}


40 
*}


41 


42 


43 


44 
types res = vals (* result entry *)


45 
syntax


46 
Val :: "val \<Rightarrow> res"


47 
Var :: "var \<Rightarrow> res"


48 
Vals :: "val list \<Rightarrow> res"


49 
translations


50 
"Val x" => "(In1 x)"


51 
"Var x" => "(In2 x)"


52 
"Vals x" => "(In3 x)"


53 


54 
syntax


55 
"Val_" :: "[pttrn] => pttrn" ("Val:_" [951] 950)


56 
"Var_" :: "[pttrn] => pttrn" ("Var:_" [951] 950)


57 
"Vals_" :: "[pttrn] => pttrn" ("Vals:_" [951] 950)


58 


59 
translations


60 
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> the_In1"


61 
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> the_In2"


62 
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> the_In3"


63 


64 
(* relation on result values, state and auxiliary variables *)


65 
types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"


66 
translations


67 
"res" <= (type) "AxSem.res"


68 
"a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"


69 


70 
constdefs


71 
assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)


72 
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"


73 


74 
lemma assn_imp_def2 [iff]: "(P \<Rightarrow> Q) = (\<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z)"


75 
apply (unfold assn_imp_def)


76 
apply (rule HOL.refl)


77 
done


78 


79 


80 
section "assertion transformers"


81 


82 
subsection "peekand"


83 


84 
constdefs


85 
peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)


86 
"P \<and>. p \<equiv> \<lambda>Y s Z. P Y s Z \<and> p s"


87 


88 
lemma peek_and_def2 [simp]: "peek_and P p Y s = (\<lambda>Z. (P Y s Z \<and> p s))"


89 
apply (unfold peek_and_def)


90 
apply (simp (no_asm))


91 
done


92 


93 
lemma peek_and_Not [simp]: "(P \<and>. (\<lambda>s. \<not> f s)) = (P \<and>. Not \<circ> f)"


94 
apply (rule ext)


95 
apply (rule ext)


96 
apply (simp (no_asm))


97 
done


98 


99 
lemma peek_and_and [simp]: "peek_and (peek_and P p) p = peek_and P p"


100 
apply (unfold peek_and_def)


101 
apply (simp (no_asm))


102 
done


103 


104 
lemma peek_and_commut: "(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)"


105 
apply (rule ext)


106 
apply (rule ext)


107 
apply (rule ext)


108 
apply auto


109 
done


110 


111 
syntax


112 
Normal :: "'a assn \<Rightarrow> 'a assn"


113 
translations


114 
"Normal P" == "P \<and>. normal"


115 


116 
lemma peek_and_Normal [simp]: "peek_and (Normal P) p = Normal (peek_and P p)"


117 
apply (rule ext)


118 
apply (rule ext)


119 
apply (rule ext)


120 
apply auto


121 
done


122 


123 
subsection "assnsupd"


124 


125 
constdefs


126 
assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)


127 
"P ;. f \<equiv> \<lambda>Y s' Z. \<exists>s. P Y s Z \<and> s' = f s"


128 


129 
lemma assn_supd_def2 [simp]: "assn_supd P f Y s' Z = (\<exists>s. P Y s Z \<and> s' = f s)"


130 
apply (unfold assn_supd_def)


131 
apply (simp (no_asm))


132 
done


133 


134 
subsection "supdassn"


135 


136 
constdefs


137 
supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)


138 
"f .; P \<equiv> \<lambda>Y s. P Y (f s)"


139 


140 


141 
lemma supd_assn_def2 [simp]: "(f .; P) Y s = P Y (f s)"


142 
apply (unfold supd_assn_def)


143 
apply (simp (no_asm))


144 
done


145 


146 
lemma supd_assn_supdD [elim]: "((f .; Q) ;. f) Y s Z \<Longrightarrow> Q Y s Z"


147 
apply auto


148 
done


149 


150 
lemma supd_assn_supdI [elim]: "Q Y s Z \<Longrightarrow> (f .; (Q ;. f)) Y s Z"


151 
apply (auto simp del: split_paired_Ex)


152 
done


153 


154 
subsection "substres"


155 


156 
constdefs


157 
subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_" [60,61] 60)


158 
"P\<leftarrow>w \<equiv> \<lambda>Y. P w"


159 


160 
lemma subst_res_def2 [simp]: "(P\<leftarrow>w) Y = P w"


161 
apply (unfold subst_res_def)


162 
apply (simp (no_asm))


163 
done


164 


165 
lemma subst_subst_res [simp]: "P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w"


166 
apply (rule ext)


167 
apply (simp (no_asm))


168 
done


169 


170 
lemma peek_and_subst_res [simp]: "(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)"


171 
apply (rule ext)


172 
apply (rule ext)


173 
apply (simp (no_asm))


174 
done


175 


176 
(*###Do not work for some strange (unification?) reason


177 
lemma subst_res_Val_beta [simp]: "(\<lambda>Y. P (the_In1 Y))\<leftarrow>Val v = (\<lambda>Y. P v)"


178 
apply (rule ext)


179 
by simp


180 


181 
lemma subst_res_Var_beta [simp]: "(\<lambda>Y. P (the_In2 Y))\<leftarrow>Var vf = (\<lambda>Y. P vf)";


182 
apply (rule ext)


183 
by simp


184 


185 
lemma subst_res_Vals_beta [simp]: "(\<lambda>Y. P (the_In3 Y))\<leftarrow>Vals vs = (\<lambda>Y. P vs)";


186 
apply (rule ext)


187 
by simp


188 
*)


189 


190 
subsection "substBool"


191 


192 
constdefs


193 
subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)


194 
"P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"


195 


196 
lemma subst_Bool_def2 [simp]:


197 
"(P\<leftarrow>=b) Y s Z = (\<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b))"


198 
apply (unfold subst_Bool_def)


199 
apply (simp (no_asm))


200 
done


201 


202 
lemma subst_Bool_the_BoolI: "P (Val b) s Z \<Longrightarrow> (P\<leftarrow>=the_Bool b) Y s Z"


203 
apply auto


204 
done


205 


206 
subsection "peekres"


207 


208 
constdefs


209 
peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"


210 
"peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"


211 


212 
syntax


213 
"@peek_res" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_:. _" [0,3] 3)


214 
translations


215 
"\<lambda>w:. P" == "peek_res (\<lambda>w. P)"


216 


217 
lemma peek_res_def2 [simp]: "peek_res P Y = P Y Y"


218 
apply (unfold peek_res_def)


219 
apply (simp (no_asm))


220 
done


221 


222 
lemma peek_res_subst_res [simp]: "peek_res P\<leftarrow>w = P w\<leftarrow>w"


223 
apply (rule ext)


224 
apply (simp (no_asm))


225 
done


226 


227 
(* unused *)


228 
lemma peek_subst_res_allI:


229 
"(\<And>a. T a (P (f a)\<leftarrow>f a)) \<Longrightarrow> \<forall>a. T a (peek_res P\<leftarrow>f a)"


230 
apply (rule allI)


231 
apply (simp (no_asm))


232 
apply fast


233 
done


234 


235 
subsection "ignres"


236 


237 
constdefs


238 
ign_res :: " 'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)


239 
"P\<down> \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"


240 


241 
lemma ign_res_def2 [simp]: "P\<down> Y s Z = (\<exists>Y. P Y s Z)"


242 
apply (unfold ign_res_def)


243 
apply (simp (no_asm))


244 
done


245 


246 
lemma ign_ign_res [simp]: "P\<down>\<down> = P\<down>"


247 
apply (rule ext)


248 
apply (rule ext)


249 
apply (rule ext)


250 
apply (simp (no_asm))


251 
done


252 


253 
lemma ign_subst_res [simp]: "P\<down>\<leftarrow>w = P\<down>"


254 
apply (rule ext)


255 
apply (rule ext)


256 
apply (rule ext)


257 
apply (simp (no_asm))


258 
done


259 


260 
lemma peek_and_ign_res [simp]: "(P \<and>. p)\<down> = (P\<down> \<and>. p)"


261 
apply (rule ext)


262 
apply (rule ext)


263 
apply (rule ext)


264 
apply (simp (no_asm))


265 
done


266 


267 
subsection "peekst"


268 


269 
constdefs


270 
peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"


271 
"peek_st P \<equiv> \<lambda>Y s. P (store s) Y s"


272 


273 
syntax


274 
"@peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_.. _" [0,3] 3)


275 
translations


276 
"\<lambda>s.. P" == "peek_st (\<lambda>s. P)"


277 


278 
lemma peek_st_def2 [simp]: "(\<lambda>s.. Pf s) Y s = Pf (store s) Y s"


279 
apply (unfold peek_st_def)


280 
apply (simp (no_asm))


281 
done


282 


283 
lemma peek_st_triv [simp]: "(\<lambda>s.. P) = P"


284 
apply (rule ext)


285 
apply (rule ext)


286 
apply (simp (no_asm))


287 
done


288 


289 
lemma peek_st_st [simp]: "(\<lambda>s.. \<lambda>s'.. P s s') = (\<lambda>s.. P s s)"


290 
apply (rule ext)


291 
apply (rule ext)


292 
apply (simp (no_asm))


293 
done


294 


295 
lemma peek_st_split [simp]: "(\<lambda>s.. \<lambda>Y s'. P s Y s') = (\<lambda>Y s. P (store s) Y s)"


296 
apply (rule ext)


297 
apply (rule ext)


298 
apply (simp (no_asm))


299 
done


300 


301 
lemma peek_st_subst_res [simp]: "(\<lambda>s.. P s)\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)"


302 
apply (rule ext)


303 
apply (simp (no_asm))


304 
done


305 


306 
lemma peek_st_Normal [simp]: "(\<lambda>s..(Normal (P s))) = Normal (\<lambda>s.. P s)"


307 
apply (rule ext)


308 
apply (rule ext)


309 
apply (simp (no_asm))


310 
done


311 


312 
subsection "ignreseq"


313 


314 
constdefs


315 
ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_" [60,61] 60)


316 
"P\<down>=w \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"


317 


318 
lemma ign_res_eq_def2 [simp]: "(P\<down>=w) Y s Z = ((\<exists>Y. P Y s Z) \<and> Y=w)"


319 
apply (unfold ign_res_eq_def)


320 
apply auto


321 
done


322 


323 
lemma ign_ign_res_eq [simp]: "(P\<down>=w)\<down> = P\<down>"


324 
apply (rule ext)


325 
apply (rule ext)


326 
apply (rule ext)


327 
apply (simp (no_asm))


328 
done


329 


330 
(* unused *)


331 
lemma ign_res_eq_subst_res: "P\<down>=w\<leftarrow>w = P\<down>"


332 
apply (rule ext)


333 
apply (rule ext)


334 
apply (rule ext)


335 
apply (simp (no_asm))


336 
done


337 


338 
(* unused *)


339 
lemma subst_Bool_ign_res_eq: "((P\<leftarrow>=b)\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z \<and> Y=x)"


340 
apply (simp (no_asm))


341 
done


342 


343 
subsection "RefVar"


344 


345 
constdefs


346 
RefVar :: "(state \<Rightarrow> vvar \<times> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13)


347 
"vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) s'"


348 


349 
lemma RefVar_def2 [simp]: "(vf ..; P) Y s =


350 
P (Var (fst (vf s))) (snd (vf s))"


351 
apply (unfold RefVar_def Let_def)


352 
apply (simp (no_asm) add: split_beta)


353 
done


354 


355 
subsection "allocation"


356 


357 
constdefs


358 
Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"


359 
"Alloc G otag P \<equiv> \<lambda>Y s Z.


360 
\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z"


361 


362 
SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"


363 
"SXAlloc G P \<equiv> \<lambda>Y s Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z"


364 


365 


366 
lemma Alloc_def2 [simp]: "Alloc G otag P Y s Z =


367 
(\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> P (Val (Addr a)) s' Z)"


368 
apply (unfold Alloc_def)


369 
apply (simp (no_asm))


370 
done


371 


372 
lemma SXAlloc_def2 [simp]:


373 
"SXAlloc G P Y s Z = (\<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P Y s' Z)"


374 
apply (unfold SXAlloc_def)


375 
apply (simp (no_asm))


376 
done


377 


378 
section "validity"


379 


380 
constdefs


381 
type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool"


382 
"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)"


383 


384 
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be


385 
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)


386 
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)


387 
types 'a triples = "'a triple set"


388 


389 
syntax


390 


391 
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"


392 
("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75)


393 
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"


394 
("{(1_)}/ _>/ {(1_)}" [3,80,3] 75)


395 
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"


396 
("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75)


397 
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple"


398 
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75)


399 


400 
syntax (xsymbols)


401 


402 
triple :: "['a assn, term ,'a assn] \<Rightarrow> 'a triple"


403 
("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75)


404 
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"


405 
("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75)


406 
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"


407 
("{(1_)}/ _\<succ>/ {(1_)}" [3,80,3] 75)


408 
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"


409 
("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)


410 


411 
translations


412 
"{P} e\<succ> {Q}" == "{P} In1l e\<succ> {Q}"


413 
"{P} e=\<succ> {Q}" == "{P} In2 e\<succ> {Q}"


414 
"{P} e\<doteq>\<succ> {Q}" == "{P} In3 e\<succ> {Q}"


415 
"{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"


416 


417 
lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"


418 
apply (rule injI)


419 
apply auto


420 
done


421 


422 
lemma triple_inj_eq: "({P} t\<succ> {Q} = {P'} t'\<succ> {Q'} ) = (P=P' \<and> t=t' \<and> Q=Q')"


423 
apply auto


424 
done


425 


426 
constdefs


427 
mtriples :: "('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<Rightarrow> 'sig \<Rightarrow> expr) \<Rightarrow>


428 
('c \<Rightarrow> 'sig \<Rightarrow> 'a assn) \<Rightarrow> ('c \<times> 'sig) set \<Rightarrow> 'a triples"


429 
("{{(1_)}/ _\<succ>/ {(1_)}  _}"[3,65,3,65]75)


430 
"{{P} tf\<succ> {Q}  ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf C sig\<succ> {Q C sig})`ms"


431 


432 
consts


433 


434 
triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"


435 
( "_\<Turnstile>_:_" [61,0, 58] 57)


436 
ax_valids :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"


437 
("_,_\<Turnstile>_" [61,58,58] 57)


438 
ax_derivs :: "prog \<Rightarrow> ('b triples \<times> 'a triples) set"


439 


440 
syntax


441 


442 
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"


443 
( "_=_:_" [61,0, 58] 57)


444 
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"


445 
( "_,_=_" [61,58,58] 57)


446 
ax_Derivs:: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"


447 
("_,__" [61,58,58] 57)


448 
ax_Deriv :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"


449 
( "_,__" [61,58,58] 57)


450 


451 
syntax (xsymbols)


452 


453 
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"


454 
( "_\<Turnstile>_:_" [61,0, 58] 57)


455 
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"


456 
( "_,_\<Turnstile>_" [61,58,58] 57)


457 
ax_Derivs:: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"


458 
("_,_\<turnstile>_" [61,58,58] 57)


459 
ax_Deriv :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"


460 
( "_,_\<turnstile>_" [61,58,58] 57)


461 


462 
defs triple_valid_def: "G\<Turnstile>n:t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>


463 
\<forall>Y s Z. P Y s Z \<longrightarrow> type_ok G t s \<longrightarrow>


464 
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q Y' s' Z)"


465 
translations "G\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"


466 
defs ax_valids_def:"G,A\<Turnstile>ts \<equiv> \<forall>n. G\<Turnstile>n:A \<longrightarrow> G\<Turnstile>n:ts"


467 
translations "G,A \<Turnstile>t" == "G,A\<Turnstile>{t}"


468 
"G,A\<turnstile>ts" == "(A,ts) \<in> ax_derivs G"


469 
"G,A \<turnstile>t" == "G,A\<turnstile>{t}"


470 


471 
lemma triple_valid_def2: "G\<Turnstile>n:{P} t\<succ> {Q} =


472 
(\<forall>Y s Z. P Y s Z


473 
\<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>


474 
(\<forall>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s')\<longrightarrow> Q Y' s' Z))"


475 
apply (unfold triple_valid_def type_ok_def)


476 
apply (simp (no_asm))


477 
done


478 


479 


480 
declare split_paired_All [simp del] split_paired_Ex [simp del]


481 
declare split_if [split del] split_if_asm [split del]


482 
option.split [split del] option.split_asm [split del]


483 
ML_setup {*


484 
simpset_ref() := simpset() delloop "split_all_tac";


485 
claset_ref () := claset () delSWrapper "split_all_tac"


486 
*}


487 


488 


489 
inductive "ax_derivs G" intros


490 


491 
empty: " G,A\<turnstile>{}"


492 
insert:"\<lbrakk>G,A\<turnstile>t; G,A\<turnstile>ts\<rbrakk> \<Longrightarrow>


493 
G,A\<turnstile>insert t ts"


494 


495 
asm: "ts\<subseteq>A \<Longrightarrow> G,A\<turnstile>ts"


496 


497 
(* could be added for convenience and efficiency, but is not necessary


498 
cut: "\<lbrakk>G,A'\<turnstile>ts; G,A\<turnstile>A'\<rbrakk> \<Longrightarrow>


499 
G,A \<turnstile>ts"


500 
*)


501 
weaken:"\<lbrakk>G,A\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A\<turnstile>ts"


502 


503 
conseq:"\<forall>Y s Z . P Y s Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'.


504 
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>


505 
Q Y' s' Z ))


506 
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"


507 


508 
hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"


509 


510 
Abrupt: "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"


511 


512 
(* variables *)


513 
LVar: " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"


514 


515 
FVar: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Q};


516 
G,A\<turnstile>{Q} e\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>


517 
G,A\<turnstile>{Normal P} {C,stat}e..fn=\<succ> {R}"


518 


519 
AVar: "\<lbrakk>G,A\<turnstile>{Normal P} e1\<succ> {Q};


520 
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2\<succ> {\<lambda>Val:i:. avar G i a ..; R}\<rbrakk> \<Longrightarrow>


521 
G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"


522 
(* expressions *)


523 


524 
NewC: "\<lbrakk>G,A\<turnstile>{Normal P} .Init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>


525 
G,A\<turnstile>{Normal P} NewC C\<succ> {Q}"


526 


527 
NewA: "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q}; G,A\<turnstile>{Q} e\<succ>


528 
{\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk> \<Longrightarrow>


529 
G,A\<turnstile>{Normal P} New T[e]\<succ> {R}"


530 


531 
Cast: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:v:. \<lambda>s..


532 
abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) .; Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>


533 
G,A\<turnstile>{Normal P} Cast T e\<succ> {Q}"


534 


535 
Inst: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:v:. \<lambda>s..


536 
Q\<leftarrow>Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>


537 
G,A\<turnstile>{Normal P} e InstOf T\<succ> {Q}"


538 


539 
Lit: "G,A\<turnstile>{Normal (P\<leftarrow>Val v)} Lit v\<succ> {P}"


540 


541 
Super:" G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super\<succ> {P}"


542 


543 
Acc: "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>


544 
G,A\<turnstile>{Normal P} Acc va\<succ> {Q}"


545 


546 
Ass: "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};


547 
\<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<rbrakk> \<Longrightarrow>


548 
G,A\<turnstile>{Normal P} va:=e\<succ> {R}"


549 


550 
Cond: "\<lbrakk>G,A \<turnstile>{Normal P} e0\<succ> {P'};


551 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} (if b then e1 else e2)\<succ> {Q}\<rbrakk> \<Longrightarrow>


552 
G,A\<turnstile>{Normal P} e0 ? e1 : e2\<succ> {Q}"


553 


554 
Call:


555 
"\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};


556 
\<forall>a vs invC declC l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.


557 
(\<lambda>s. declC=invocation_declclass G mode (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> \<and>


558 
invC = invocation_class mode (store s) a statT \<and>


559 
l = locals (store s)) ;.


560 
init_lvars G declC \<lparr>name=mn,parTs=pTs\<rparr> mode a vs) \<and>.


561 
(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>invC\<preceq>statT)}


562 
Methd declC \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S}\<rbrakk> \<Longrightarrow>


563 
G,A\<turnstile>{Normal P} {statT,mode}e\<cdot>mn({pTs}args)\<succ> {S}"


564 


565 
Methd:"\<lbrakk>G,A\<union> {{P} Methd\<succ> {Q}  ms} \<turnstile> {{P} body G\<succ> {Q}  ms}\<rbrakk> \<Longrightarrow>


566 
G,A\<turnstile>{{P} Methd\<succ> {Q}  ms}"


567 


568 
Body: "\<lbrakk>G,A\<turnstile>{Normal P} .Init D. {Q};


569 
G,A\<turnstile>{Q} .c. {\<lambda>s.. abupd (absorb Ret) .; R\<leftarrow>(In1 (the (locals s Result)))}\<rbrakk>


570 
\<Longrightarrow>


571 
G,A\<turnstile>{Normal P} Body D c\<succ> {R}"


572 


573 
(* expression lists *)


574 


575 
Nil: "G,A\<turnstile>{Normal (P\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"


576 


577 
Cons: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q};


578 
\<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>


579 
G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"


580 


581 
(* statements *)


582 


583 
Skip: "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit>)} .Skip. {P}"


584 


585 
Expr: "\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>


586 
G,A\<turnstile>{Normal P} .Expr e. {Q}"


587 


588 
Lab: "\<lbrakk>G,A\<turnstile>{Normal P} .c. {abupd (absorb (Break l)) .; Q}\<rbrakk> \<Longrightarrow>


589 
G,A\<turnstile>{Normal P} .l\<bullet> c. {Q}"


590 


591 
Comp: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};


592 
G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>


593 
G,A\<turnstile>{Normal P} .c1;;c2. {R}"


594 


595 
If: "\<lbrakk>G,A \<turnstile>{Normal P} e\<succ> {P'};


596 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>


597 
G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"


598 
(* unfolding variant of Loop, not needed here


599 
LoopU:"\<lbrakk>G,A \<turnstile>{Normal P} e\<succ> {P'};


600 
\<forall>b. G,A\<turnstile>{P'\<leftarrow>=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>


601 
\<Longrightarrow> G,A\<turnstile>{Normal P} .While(e) c. {Q}"


602 
*)


603 
Loop: "\<lbrakk>G,A\<turnstile>{P} e\<succ> {P'};


604 
G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>


605 
G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"


606 
(** Beware of polymorphic_Loop below: should be identical terms **)


607 


608 
Do: "G,A\<turnstile>{Normal (abupd (\<lambda>a. (Some (Jump j))) .; P\<leftarrow>\<diamondsuit>)} .Do j. {P}"


609 


610 
Throw:"\<lbrakk>G,A\<turnstile>{Normal P} e\<succ> {\<lambda>Val:a:. abupd (throw a) .; Q\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>


611 
G,A\<turnstile>{Normal P} .Throw e. {Q}"


612 


613 
Try: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};


614 
G,A\<turnstile>{Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};


615 
(Q \<and>. (\<lambda>s. \<not>G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>


616 
G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"


617 


618 
Fin: "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};


619 
\<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. abupd (\<lambda>x. None)}


620 
.c2. {abupd (abrupt_if (x\<noteq>None) x) .; R}\<rbrakk> \<Longrightarrow>


621 
G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"


622 


623 
Done: "G,A\<turnstile>{Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P}"


624 


625 
Init: "\<lbrakk>the (class G C) = c;


626 
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}


627 
.(if C = Object then Skip else Init (super c)). {Q};


628 
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}


629 
.init c. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>


630 
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R}"


631 


632 
axioms (** these terms are the same as above, but with generalized typing **)


633 
polymorphic_conseq:


634 
"\<forall>Y s Z . P Y s Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'.


635 
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>


636 
Q Y' s' Z ))


637 
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"


638 


639 
polymorphic_Loop:


640 
"\<lbrakk>G,A\<turnstile>{P} e\<succ> {P'};


641 
G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {abupd (absorb (Cont l)) .; P}\<rbrakk> \<Longrightarrow>


642 
G,A\<turnstile>{P} .l\<bullet> While(e) c. {(P'\<leftarrow>=False)\<down>=\<diamondsuit>}"


643 


644 
constdefs


645 
adapt_pre :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn \<Rightarrow> 'a assn"


646 
"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)"


647 


648 


649 
section "rules derived by induction"


650 


651 
lemma cut_valid: "\<lbrakk>G,A'\<Turnstile>ts; G,A\<Turnstile>A'\<rbrakk> \<Longrightarrow> G,A\<Turnstile>ts"


652 
apply (unfold ax_valids_def)


653 
apply fast


654 
done


655 


656 
(*if cut is available


657 
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>


658 
G,A\<turnstile>ts"


659 
b y etac ax_derivs.cut 1;


660 
b y eatac ax_derivs.asm 1 1;


661 
qed "ax_thin";


662 
*)


663 
lemma ax_thin [rule_format (no_asm)]:


664 
"G,(A'::'a triple set)\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A\<turnstile>ts"


665 
apply (erule ax_derivs.induct)


666 
apply (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")


667 
apply (rule ax_derivs.empty)


668 
apply (erule (1) ax_derivs.insert)


669 
apply (fast intro: ax_derivs.asm)


670 
(*apply (fast intro: ax_derivs.cut) *)


671 
apply (fast intro: ax_derivs.weaken)


672 
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)


673 
(* 31 subgoals *)


674 
prefer 16 (* Methd *)


675 
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)


676 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))


677 
THEN_ALL_NEW Blast_tac) *})


678 
apply (erule ax_derivs.Call)


679 
apply clarify


680 
apply blast


681 


682 
apply (rule allI)+


683 
apply (drule spec)+


684 
apply blast


685 
done


686 


687 
lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"


688 
apply (erule ax_thin)


689 
apply fast


690 
done


691 


692 
lemma subset_mtriples_iff:


693 
"ts \<subseteq> {{P} mb\<succ> {Q}  ms} = (\<exists>ms'. ms'\<subseteq>ms \<and> ts = {{P} mb\<succ> {Q}  ms'})"


694 
apply (unfold mtriples_def)


695 
apply (rule subset_image_iff)


696 
done


697 


698 
lemma weaken:


699 
"G,(A::'a triple set)\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A\<turnstile>ts"


700 
apply (erule ax_derivs.induct)


701 
(*36 subgoals*)


702 
apply (tactic "ALLGOALS strip_tac")


703 
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),


704 
etac disjE, fast_tac (claset() addSIs [thm "ax_derivs.empty"])]))*})


705 
apply (tactic "TRYALL hyp_subst_tac")


706 
apply (simp, rule ax_derivs.empty)


707 
apply (drule subset_insertD)


708 
apply (blast intro: ax_derivs.insert)


709 
apply (fast intro: ax_derivs.asm)


710 
(*apply (blast intro: ax_derivs.cut) *)


711 
apply (fast intro: ax_derivs.weaken)


712 
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))


713 
(*31 subgoals*)


714 
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))


715 
THEN_ALL_NEW Fast_tac) *})


716 
(*1 subgoal*)


717 
apply (clarsimp simp add: subset_mtriples_iff)


718 
apply (rule ax_derivs.Methd)


719 
apply (drule spec)


720 
apply (erule impE)


721 
apply (rule exI)


722 
apply (erule conjI)


723 
apply (rule HOL.refl)


724 
oops (* dead end, Methd is to blame *)


725 


726 


727 
section "rules derived from conseq"


728 


729 
lemma conseq12: "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'};


730 
\<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>


731 
Q Y' s' Z)\<rbrakk>


732 
\<Longrightarrow> G,A\<turnstile>{P ::'a assn} t\<succ> {Q }"


733 
apply (rule polymorphic_conseq)


734 
apply clarsimp


735 
apply blast


736 
done


737 


738 
(*unused, but nice variant*)


739 
lemma conseq12': "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'}; \<forall>s Y' s'.


740 
(\<forall>Y Z. P' Y s Z \<longrightarrow> Q' Y' s' Z) \<longrightarrow>


741 
(\<forall>Y Z. P Y s Z \<longrightarrow> Q Y' s' Z)\<rbrakk>


742 
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"


743 
apply (erule conseq12)


744 
apply fast


745 
done


746 


747 
lemma conseq12_from_conseq12': "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q'};


748 
\<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>


749 
Q Y' s' Z)\<rbrakk>


750 
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"


751 
apply (erule conseq12')


752 
apply blast


753 
done


754 


755 
lemma conseq1: "\<lbrakk>G,A\<turnstile>{P'} t\<succ> {Q}; P \<Rightarrow> P'\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q}"


756 
apply (erule conseq12)


757 
apply blast


758 
done


759 


760 
lemma conseq2: "\<lbrakk>G,A\<turnstile>{P} t\<succ> {Q'}; Q' \<Rightarrow> Q\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"


761 
apply (erule conseq12)


762 
apply blast


763 
done


764 


765 
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>


766 
G,A\<turnstile>{P} t\<succ> {Q}"


767 
apply (rule polymorphic_conseq)


768 
apply force


769 
done


770 


771 
(* unused *)


772 
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}"


773 
apply (rule ax_escape (* unused *))


774 
apply clarify


775 
apply (rule conseq12)


776 
apply fast


777 
apply auto


778 
done


779 
(*alternative (more direct) proof:


780 
apply (rule ax_derivs.conseq) *)(* unused *)(*


781 
apply (fast)


782 
*)


783 


784 


785 
lemma ax_impossible [intro]: "G,A\<turnstile>{\<lambda>Y s Z. False} t\<succ> {Q}"


786 
apply (rule ax_escape)


787 
apply clarify


788 
done


789 


790 
(* unused *)


791 
lemma ax_nochange_lemma: "\<lbrakk>P Y s; All (op = w)\<rbrakk> \<Longrightarrow> P w s"


792 
apply auto


793 
done


794 
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}"


795 
apply (erule conseq12)


796 
apply auto


797 
apply (erule (1) ax_nochange_lemma)


798 
done


799 


800 
(* unused *)


801 
lemma ax_trivial: "G,A\<turnstile>{P} t\<succ> {\<lambda>Y s Z. True}"


802 
apply (rule polymorphic_conseq(* unused *))


803 
apply auto


804 
done


805 


806 
(* unused *)


807 
lemma ax_disj: "\<lbrakk>G,A\<turnstile>{P1} t\<succ> {Q1}; G,A\<turnstile>{P2} t\<succ> {Q2}\<rbrakk> \<Longrightarrow>


808 
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}"


809 
apply (rule ax_escape (* unused *))


810 
apply safe


811 
apply (erule conseq12, fast)+


812 
done


813 


814 
(* unused *)


815 
lemma ax_supd_shuffle: "(\<exists>Q. G,A\<turnstile>{P} .c1. {Q} \<and> G,A\<turnstile>{Q ;. f} .c2. {R}) =


816 
(\<exists>Q'. G,A\<turnstile>{P} .c1. {f .; Q'} \<and> G,A\<turnstile>{Q'} .c2. {R})"


817 
apply (best elim!: conseq1 conseq2)


818 
done


819 


820 
lemma ax_cases: "\<lbrakk>G,A\<turnstile>{P \<and>. C} t\<succ> {Q};


821 
G,A\<turnstile>{P \<and>. Not \<circ> C} t\<succ> {Q}\<rbrakk> \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"


822 
apply (unfold peek_and_def)


823 
apply (rule ax_escape)


824 
apply clarify


825 
apply (case_tac "C s")


826 
apply (erule conseq12, force)+


827 
done


828 
(*alternative (more direct) proof:


829 
apply (rule rtac ax_derivs.conseq) *)(* unused *)(*


830 
apply clarify


831 
apply (case_tac "C s")


832 
apply force+


833 
*)


834 


835 
lemma ax_adapt: "G,A\<turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"


836 
apply (unfold adapt_pre_def)


837 
apply (erule conseq12)


838 
apply fast


839 
done


840 


841 
lemma adapt_pre_adapts: "G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{adapt_pre P Q Q'} t\<succ> {Q'}"


842 
apply (unfold adapt_pre_def)


843 
apply (simp add: ax_valids_def triple_valid_def2)


844 
apply fast


845 
done


846 


847 


848 
lemma adapt_pre_weakest:


849 
"\<forall>G (A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>


850 
P' \<Rightarrow> adapt_pre P Q (Q'::'a assn)"


851 
apply (unfold adapt_pre_def)


852 
apply (drule spec)


853 
apply (drule_tac x = "{}" in spec)


854 
apply (drule_tac x = "In1r Skip" in spec)


855 
apply (simp add: ax_valids_def triple_valid_def2)


856 
oops


857 


858 
(*


859 
Goal "\<forall>(A::'a triple set) t. G,A\<Turnstile>{P} t\<succ> {Q} \<longrightarrow> G,A\<Turnstile>{P'} t\<succ> {Q'} \<Longrightarrow>


860 
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}"


861 
b y fatac ax_sound 1 1;


862 
b y asm_full_simp_tac (simpset() addsimps [ax_valids_def,triple_valid_def2]) 1;


863 
b y rtac ax_no_hazard 1;


864 
b y etac conseq12 1;


865 
b y Clarify_tac 1;


866 
b y case_tac "\<forall>Z. \<not>P Y s Z" 1;


867 
b y smp_tac 2 1;


868 
b y etac thin_rl 1;


869 
b y etac thin_rl 1;


870 
b y clarsimp_tac (claset(), simpset() addsimps [type_ok_def]) 1;


871 
b y subgoal_tac "G\<Turnstile>n:A" 1;


872 
b y smp_tac 1 1;


873 
b y smp_tac 3 1;


874 
b y etac impE 1;


875 
back();


876 
b y Fast_tac 1;


877 
b y


878 
b y rotate_tac 2 1;


879 
b y etac thin_rl 1;


880 
b y etac thin_rl 2;


881 
b y etac thin_rl 2;


882 
b y Clarify_tac 2;


883 
b y dtac spec 2;


884 
b y EVERY'[dtac spec, mp_tac] 2;


885 
b y thin_tac "\<forall>n Y s Z. ?PP n Y s Z" 2;


886 
b y thin_tac "P' Y s Z" 2;


887 
b y Blast_tac 2;


888 
b y smp_tac 3 1;


889 
b y case_tac "\<forall>Z. \<not>P Y s Z" 1;


890 
b y dres_inst_tac [("x","In1r Skip")] spec 1;


891 
b y Full_simp_tac 1;


892 
*)


893 


894 
lemma peek_and_forget1_Normal:


895 
"G,A\<turnstile>{Normal P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. p)} t\<succ> {Q}"


896 
apply (erule conseq1)


897 
apply (simp (no_asm))


898 
done


899 


900 
lemma peek_and_forget1: "G,A\<turnstile>{P} t\<succ> {Q} \<Longrightarrow> G,A\<turnstile>{P \<and>. p} t\<succ> {Q}"


901 
apply (erule conseq1)


902 
apply (simp (no_asm))


903 
done


904 


905 
lemmas ax_NormalD = peek_and_forget1 [of _ _ _ _ _ normal]


906 


907 
lemma peek_and_forget2: "G,A\<turnstile>{P} t\<succ> {Q \<and>. p} \<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Q}"


908 
apply (erule conseq2)


909 
apply (simp (no_asm))


910 
done


911 


912 
lemma ax_subst_Val_allI: "\<forall>v. G,A\<turnstile>{(P' v )\<leftarrow>Val v} t\<succ> {Q v} \<Longrightarrow>


913 
\<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In1 w))\<leftarrow>Val v} t\<succ> {Q v}"


914 
apply (force elim!: conseq1)


915 
done


916 


917 
lemma ax_subst_Var_allI: "\<forall>v. G,A\<turnstile>{(P' v )\<leftarrow>Var v} t\<succ> {Q v} \<Longrightarrow>


918 
\<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In2 w))\<leftarrow>Var v} t\<succ> {Q v}"


919 
apply (force elim!: conseq1)


920 
done


921 


922 
lemma ax_subst_Vals_allI: "(\<forall>v. G,A\<turnstile>{( P' v )\<leftarrow>Vals v} t\<succ> {Q v}) \<Longrightarrow>


923 
\<forall>v. G,A\<turnstile>{(\<lambda>w:. P' (the_In3 w))\<leftarrow>Vals v} t\<succ> {Q v}"


924 
apply (force elim!: conseq1)


925 
done


926 


927 


928 
section "alternative axioms"


929 


930 
lemma ax_Lit2:


931 
"G,(A::'a triple set)\<turnstile>{Normal P::'a assn} Lit v\<succ> {Normal (P\<down>=Val v)}"


932 
apply (rule ax_derivs.Lit [THEN conseq1])


933 
apply force


934 
done


935 
lemma ax_Lit2_test_complete:


936 
"G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val v)::'a assn} Lit v\<succ> {P}"


937 
apply (rule ax_Lit2 [THEN conseq2])


938 
apply force


939 
done


940 


941 
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))}"


942 
apply (rule ax_derivs.LVar [THEN conseq1])


943 
apply force


944 
done


945 


946 
lemma ax_Super2: "G,(A::'a triple set)\<turnstile>


947 
{Normal P::'a assn} Super\<succ> {Normal (\<lambda>s.. P\<down>=Val (val_this s))}"


948 
apply (rule ax_derivs.Super [THEN conseq1])


949 
apply force


950 
done


951 


952 
lemma ax_Nil2:


953 
"G,(A::'a triple set)\<turnstile>{Normal P::'a assn} []\<doteq>\<succ> {Normal (P\<down>=Vals [])}"


954 
apply (rule ax_derivs.Nil [THEN conseq1])


955 
apply force


956 
done


957 


958 


959 
section "misc derived structural rules"


960 


961 
(* unused *)


962 
lemma ax_finite_mtriples_lemma: "\<lbrakk>F \<subseteq> ms; finite ms; \<forall>(C,sig)\<in>ms.


963 
G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig\<succ> {Q C sig}\<rbrakk> \<Longrightarrow>


964 
G,A\<turnstile>{{P} mb\<succ> {Q}  F}"


965 
apply (frule (1) finite_subset)


966 
apply (erule make_imp)


967 
apply (erule thin_rl)


968 
apply (erule finite_induct)


969 
apply (unfold mtriples_def)


970 
apply (clarsimp intro!: ax_derivs.empty ax_derivs.insert)+


971 
apply force


972 
done


973 
lemmas ax_finite_mtriples = ax_finite_mtriples_lemma [OF subset_refl]


974 


975 
lemma ax_derivs_insertD:


976 
"G,(A::'a triple set)\<turnstile>insert (t::'a triple) ts \<Longrightarrow> G,A\<turnstile>t \<and> G,A\<turnstile>ts"


977 
apply (fast intro: ax_derivs.weaken)


978 
done


979 


980 
lemma ax_methods_spec:


981 
"\<lbrakk>G,(A::'a triple set)\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"


982 
apply (erule ax_derivs.weaken)


983 
apply (force del: image_eqI intro: rev_image_eqI)


984 
done


985 


986 
(* this version is used to avoid using the cut rule *)


987 
lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>


988 
((\<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>


989 
G,A\<turnstile>split f ` F \<longrightarrow> G,A\<turnstile>split g ` F"


990 
apply (frule (1) finite_subset)


991 
apply (erule make_imp)


992 
apply (erule thin_rl)


993 
apply (erule finite_induct)


994 
apply clarsimp+


995 
apply (drule ax_derivs_insertD)


996 
apply (rule ax_derivs.insert)


997 
apply (simp (no_asm_simp) only: split_tupled_all)


998 
apply (auto elim: ax_methods_spec)


999 
done


1000 
lemmas ax_finite_pointwise = ax_finite_pointwise_lemma [OF subset_refl]


1001 


1002 
lemma ax_no_hazard:


1003 
"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}"


1004 
apply (erule ax_cases)


1005 
apply (rule ax_derivs.hazard [THEN conseq1])


1006 
apply force


1007 
done


1008 


1009 
lemma ax_free_wt:


1010 
"(\<exists>T L C. \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>t\<Colon>T)


1011 
\<longrightarrow> G,(A::'a triple set)\<turnstile>{Normal P} t\<succ> {Q::'a assn} \<Longrightarrow>


1012 
G,A\<turnstile>{Normal P} t\<succ> {Q}"


1013 
apply (rule ax_no_hazard)


1014 
apply (rule ax_escape)


1015 
apply clarify


1016 
apply (erule mp [THEN conseq12])


1017 
apply (auto simp add: type_ok_def)


1018 
done


1019 


1020 
ML {*


1021 
bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))


1022 
*}


1023 
declare ax_Abrupts [intro!]


1024 


1025 
lemmas ax_Normal_cases = ax_cases [of _ _ normal]


1026 


1027 
lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}"


1028 
apply (rule ax_Normal_cases)


1029 
apply (rule ax_derivs.Skip)


1030 
apply fast


1031 
done


1032 
lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]


1033 


1034 


1035 
section "derived rules for methd call"


1036 


1037 
lemma ax_Call_known_DynT:


1038 
"\<lbrakk>G\<turnstile>IntVir\<rightarrow>C\<preceq>statT;


1039 
\<forall>a vs l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.


1040 
init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> IntVir a vs)}


1041 
Methd C \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S};


1042 
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ>


1043 
{R a \<and>. (\<lambda>s. C = obj_class (the (heap (store s) (the_Addr a))) \<and>


1044 
C = invocation_declclass


1045 
G IntVir (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr> )};


1046 
G,(A::'a triple set)\<turnstile>{Normal P} e\<succ> {Q::'a assn}\<rbrakk>


1047 
\<Longrightarrow> G,A\<turnstile>{Normal P} {statT,IntVir}e\<cdot>mn({pTs}args)\<succ> {S}"


1048 
apply (erule ax_derivs.Call)


1049 
apply safe


1050 
apply (erule spec)


1051 
apply (rule ax_escape, clarsimp)


1052 
apply (drule spec, drule spec, drule spec,erule conseq12)


1053 
apply force


1054 
done


1055 


1056 


1057 
lemma ax_Call_Static:


1058 
"\<lbrakk>\<forall>a vs l. G,A\<turnstile>{R a\<leftarrow>Vals vs \<and>. (\<lambda>s. l = locals (store s)) ;.


1059 
init_lvars G C \<lparr>name=mn,parTs=pTs\<rparr> Static any_Addr vs}


1060 
Methd C \<lparr>name=mn,parTs=pTs\<rparr>\<succ> {set_lvars l .; S};


1061 
G,A\<turnstile>{Normal P} e\<succ> {Q};


1062 
\<forall> a. G,(A::'a triple set)\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {(R::val \<Rightarrow> 'a assn) a


1063 
\<and>. (\<lambda> s. C=invocation_declclass


1064 
G Static (store s) a statT \<lparr>name=mn,parTs=pTs\<rparr>)}


1065 
\<rbrakk> \<Longrightarrow> G,A\<turnstile>{Normal P} {statT,Static}e\<cdot>mn({pTs}args)\<succ> {S}"


1066 
apply (erule ax_derivs.Call)


1067 
apply safe


1068 
apply (erule spec)


1069 
apply (rule ax_escape, clarsimp)


1070 
apply (erule_tac V = "?P \<longrightarrow> ?Q" in thin_rl)


1071 
apply (drule spec,drule spec,drule spec, erule conseq12)


1072 
apply (force simp add: init_lvars_def)


1073 
done


1074 


1075 
lemma ax_Methd1:


1076 
"\<lbrakk>G,A\<union>{{P} Methd\<succ> {Q}  ms}\<turnstile> {{P} body G\<succ> {Q}  ms}; (C,sig)\<in> ms\<rbrakk> \<Longrightarrow>


1077 
G,A\<turnstile>{Normal (P C sig)} Methd C sig\<succ> {Q C sig}"


1078 
apply (drule ax_derivs.Methd)


1079 
apply (unfold mtriples_def)


1080 
apply (erule (1) ax_methods_spec)


1081 
done


1082 


1083 
lemma ax_MethdN:


1084 
"G,insert({Normal P} Methd C sig\<succ> {Q}) A\<turnstile>


1085 
{Normal P} body G C sig\<succ> {Q} \<Longrightarrow>


1086 
G,A\<turnstile>{Normal P} Methd C sig\<succ> {Q}"


1087 
apply (rule ax_Methd1)


1088 
apply (rule_tac [2] singletonI)


1089 
apply (unfold mtriples_def)


1090 
apply clarsimp


1091 
done


1092 


1093 
lemma ax_StatRef:


1094 
"G,(A::'a triple set)\<turnstile>{Normal (P\<leftarrow>Val Null)} StatRef rt\<succ> {P::'a assn}"


1095 
apply (rule ax_derivs.Cast)


1096 
apply (rule ax_Lit2 [THEN conseq2])


1097 
apply clarsimp


1098 
done


1099 


1100 
section "rules derived from Init and Done"


1101 


1102 
lemma ax_InitS: "\<lbrakk>the (class G C) = c; C \<noteq> Object;


1103 
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars empty}


1104 
.init c. {set_lvars l .; R};


1105 
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}


1106 
.Init (super c). {Q}\<rbrakk> \<Longrightarrow>


1107 
G,(A::'a triple set)\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .Init C. {R::'a assn}"


1108 
apply (erule ax_derivs.Init)


1109 
apply (simp (no_asm_simp))


1110 
apply assumption


1111 
done


1112 


1113 
lemma ax_Init_Skip_lemma:


1114 
"\<forall>l. G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit> \<and>. (\<lambda>s. l = locals (store s)) ;. set_lvars l'}


1115 
.Skip. {(set_lvars l .; P)::'a assn}"


1116 
apply (rule allI)


1117 
apply (rule ax_SkipI)


1118 
apply clarsimp


1119 
done


1120 


1121 
lemma ax_triv_InitS: "\<lbrakk>the (class G C) = c;init c = Skip; C \<noteq> Object;


1122 
P\<leftarrow>\<diamondsuit> \<Rightarrow> (supd (init_class_obj G C) .; P);


1123 
G,A\<turnstile>{Normal (P \<and>. initd C)} .Init (super c). {(P \<and>. initd C)\<leftarrow>\<diamondsuit>}\<rbrakk> \<Longrightarrow>


1124 
G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init C. {(P \<and>. initd C)::'a assn}"


1125 
apply (rule_tac C = "initd C" in ax_cases)


1126 
apply (rule conseq1, rule ax_derivs.Done, clarsimp)


1127 
apply (simp (no_asm))


1128 
apply (erule (1) ax_InitS)


1129 
apply simp


1130 
apply (rule ax_Init_Skip_lemma)


1131 
apply (erule conseq1)


1132 
apply force


1133 
done


1134 


1135 
lemma ax_Init_Object: "wf_prog G \<Longrightarrow> G,(A::'a triple set)\<turnstile>


1136 
{Normal ((supd (init_class_obj G Object) .; P\<leftarrow>\<diamondsuit>) \<and>. Not \<circ> initd Object)}


1137 
.Init Object. {(P \<and>. initd Object)::'a assn}"


1138 
apply (rule ax_derivs.Init)


1139 
apply (drule class_Object, force)


1140 
apply (simp_all (no_asm))


1141 
apply (rule_tac [2] ax_Init_Skip_lemma)


1142 
apply (rule ax_SkipI, force)


1143 
done


1144 


1145 
lemma ax_triv_Init_Object: "\<lbrakk>wf_prog G;


1146 
(P::'a assn) \<Rightarrow> (supd (init_class_obj G Object) .; P)\<rbrakk> \<Longrightarrow>


1147 
G,(A::'a triple set)\<turnstile>{Normal P\<leftarrow>\<diamondsuit>} .Init Object. {P \<and>. initd Object}"


1148 
apply (rule_tac C = "initd Object" in ax_cases)


1149 
apply (rule conseq1, rule ax_derivs.Done, clarsimp)


1150 
apply (erule ax_Init_Object [THEN conseq1])


1151 
apply force


1152 
done


1153 


1154 


1155 
section "introduction rules for Alloc and SXAlloc"


1156 


1157 
lemma ax_SXAlloc_Normal: "G,A\<turnstile>{P} .c. {Normal Q} \<Longrightarrow> G,A\<turnstile>{P} .c. {SXAlloc G Q}"


1158 
apply (erule conseq2)


1159 
apply (clarsimp elim!: sxalloc_elim_cases simp add: split_tupled_all)


1160 
done


1161 


1162 
lemma ax_Alloc:


1163 
"G,A\<turnstile>{P} t\<succ> {Normal (\<lambda>Y (x,s) Z. (\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>


1164 
Q (Val (Addr a)) (Norm(init_obj G (CInst C) (Heap a) s)) Z)) \<and>.


1165 
heap_free (Suc (Suc 0))}


1166 
\<Longrightarrow> G,A\<turnstile>{P} t\<succ> {Alloc G (CInst C) Q}"


1167 
apply (erule conseq2)


1168 
apply (auto elim!: halloc_elim_cases)


1169 
done


1170 


1171 
lemma ax_Alloc_Arr:


1172 
"G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. Normal (\<lambda>Y (x,s) Z. \<not>the_Intg i<0 \<and>


1173 
(\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>


1174 
Q (Val (Addr a)) (Norm (init_obj G (Arr T (the_Intg i)) (Heap a) s)) Z)) \<and>.


1175 
heap_free (Suc (Suc 0))} \<Longrightarrow>


1176 
G,A\<turnstile>{P} t\<succ> {\<lambda>Val:i:. abupd (check_neg i) .; Alloc G (Arr T(the_Intg i)) Q}"


1177 
apply (erule conseq2)


1178 
apply (auto elim!: halloc_elim_cases)


1179 
done


1180 


1181 
lemma ax_SXAlloc_catch_SXcpt:


1182 
"\<lbrakk>G,A\<turnstile>{P} t\<succ> {(\<lambda>Y (x,s) Z. x=Some (Xcpt (Std xn)) \<and>


1183 
(\<forall>a. new_Addr (heap s) = Some a \<longrightarrow>


1184 
Q Y (Some (Xcpt (Loc a)),init_obj G (CInst (SXcpt xn)) (Heap a) s) Z))


1185 
\<and>. heap_free (Suc (Suc 0))}\<rbrakk> \<Longrightarrow>


1186 
G,A\<turnstile>{P} t\<succ> {SXAlloc G (\<lambda>Y s Z. Q Y s Z \<and> G,s\<turnstile>catch SXcpt xn)}"


1187 
apply (erule conseq2)


1188 
apply (auto elim!: sxalloc_elim_cases halloc_elim_cases)


1189 
done


1190 


1191 
end
