Up to index of Isabelle/Bali4
theory AxSem = Evaln + TypeSafe(* Title: isabelle/Bali/AxSem.thy
ID: $Id: AxSem.thy,v 1.101 2000/09/04 16:58:04 oheimb Exp $
Author: David von Oheimb
Copyright 1998 Technische Universitaet Muenchen
Axiomatic semantics of Java expressions and statements (see also Eval.thy)
design issues:
* a strong version of validity for triples with premises, namely one that takes
the recursive depth needed to complete execution, enables correctness proof
* auxiliary variables are handled first-class (-> Thomas Kleymann)
* expressions not flattened to elementary assignments (as usual for axiomatic
semantics) but treated first-class => explicit result value handling
* intermediate values not on triple, but on assertion level (with result stack)
* because of dynamic method binding, term need to be dependent on state.
this is also useful for conditional expressions and statements
* result values in triples exactly as in eval relation (also for xcpt states)
* validity: additional assumption of state conformance and well-typedness,
which is required for soundness and thus rule hazard required of completeness
restrictions:
* the rule of consequence could be polymorphic i.e. different types for P and P'
but the inductive definition scheme cannot handle this
*)
AxSem = Evaln + TypeSafe +
datatype res (* result stack entry *)
= Res vals
| Xcpt xopt
| Lcls locals
| DynT tname
syntax
Val :: "val \<Rightarrow> res"
Var :: "var \<Rightarrow> res"
Vals :: "val list \<Rightarrow> res"
translations
"Val x" == "Res (In1 x)"
"Var x" == "Res (In2 x)"
"Vals x" == "Res (In3 x)"
constdefs
the_Res :: "res \<Rightarrow> vals"
"the_Res y \<equiv> \<epsilon>x. y = Res x"
the_Xcpt :: "res \<Rightarrow> xopt"
"the_Xcpt y \<equiv> \<epsilon>x. y = Xcpt x"
the_Lcls :: "res \<Rightarrow> (lname, val) table"
"the_Lcls y \<equiv> \<epsilon>l. y = Lcls l"
res :: "term \<Rightarrow> vals \<Rightarrow> res list \<Rightarrow> res list"
"res t v Y \<equiv> if is_stmt t then Y else Res v#Y"
syntax
"Val_" :: [pttrn] => pttrn ("Val:_" [951] 950)
"Var_" :: [pttrn] => pttrn ("Var:_" [951] 950)
"Vals_" :: [pttrn] => pttrn ("Vals:_" [951] 950)
"Xcpt_" :: [pttrn] => pttrn ("Xcpt:_" [951] 950)
"Lcls_" :: [pttrn] => pttrn ("Lcls:_" [951] 950)
translations
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> (the_In1 \<circ> the_Res)"
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> (the_In2 \<circ> the_Res)"
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> (the_In3 \<circ> the_Res)"
"\<lambda>Xcpt:x. b" == "(\<lambda>x. b) \<circ> the_Xcpt"
"\<lambda>Lcls:l. b" == "(\<lambda>l. b) \<circ> the_Lcls"
(* relation on result values, state and auxiliary variables *)
types rstate = "res list × state"
'a assn = "rstate \<Rightarrow> 'a \<Rightarrow> bool"
translations
"res" <= (type) "AxSem.res"
"rstate" <= (type) "res list × state"
"a assn" <= (type) "rstate \<Rightarrow> a \<Rightarrow> bool"
constdefs
assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25)
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P (Y,s) Z \<longrightarrow> Q (Y,s) Z"
peek_and :: "'a assn \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> 'a assn" (infixl "\<and>." 13)
"P \<and>. p \<equiv> \<lambda>(Y,s) Z. P (Y,s) Z \<and> p s"
assn_supd :: "'a assn \<Rightarrow> (state \<Rightarrow> state) \<Rightarrow> 'a assn" (infixl ";." 13)
"P ;. f \<equiv> \<lambda>(Y,s') Z. \<exists>s. P (Y,s) Z \<and> s' = f s"
supd_assn :: "(state \<Rightarrow> state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn" (infixr ".;" 13)
"f .; P \<equiv> \<lambda>(Y,s). P (Y,f s)"
res_push :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<up>#_" [60,61] 60)
"P\<up>#w \<equiv> \<lambda>(Y,s). P (w#Y,s)"
res_eqpop :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>#_" [60,61] 60)
"P\<down>#w \<equiv> \<lambda>(Y,s) Z. \<exists>Y'. Y=w#Y' \<and> P (Y',s) Z"
res_pop :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
"res_pop Pf \<equiv> \<lambda>(w#Y,s). Pf w (Y,s)"
peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
"peek_st Pf \<equiv> \<lambda>(Y,s). Pf (snd s) (Y,s)"
syntax
Normal :: "'a assn \<Rightarrow> 'a assn"
"@res_pop" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_#. _" [0,3] 3)
"@peek_st" :: "pttrn \<Rightarrow> 'a assn \<Rightarrow> 'a assn" ("\<lambda>_: _" [0,3] 3)
translations
"Normal P" == "P \<and>. normal"
"\<lambda>w#ws#. P" == "res_pop (\<lambda>w. \<lambda>ws#. P)"
"\<lambda>w#. P" == "res_pop (\<lambda>w. P)"
"\<lambda>s: P" == "peek_st (\<lambda>s. P)"
constdefs
res_ign :: " 'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
"P\<down> \<equiv> \<lambda>w#. P"
Bool_assn :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<up>#Bool=_"[60,61] 60)
"P\<up>#Bool=b \<equiv>\<lambda>(Y,s) Z. \<exists>v. (P\<up>#Val v) (Y,s) Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
constdefs
RefVar :: "(val \<Rightarrow> state \<Rightarrow> vvar × state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
"RefVar vf P \<equiv> \<lambda>(Val:a#Y,s). let (v,s') = vf a s in (P\<up>#Var v) (Y,s')"
Alloc :: "prog \<Rightarrow> obj_tag \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
"Alloc G otag P \<equiv> \<lambda>(Y,s) Z.
\<forall>s' a. G\<turnstile>s \<midarrow>halloc otag\<succ>a\<rightarrow> s'\<longrightarrow> (P\<up>#Val (Addr a)) (Y,s') Z"
SXAlloc :: "prog \<Rightarrow> 'a assn \<Rightarrow> 'a assn"
"SXAlloc G P \<equiv> \<lambda>(Y,s) Z. \<forall>s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<longrightarrow> P (Y,s') Z"
type_ok :: "prog \<Rightarrow> term \<Rightarrow> state \<Rightarrow> bool"
"type_ok G t s \<equiv> \<exists>L T. (normal s \<longrightarrow> (G,L)\<turnstile>t\<Colon>T) \<and> s\<Colon>\<preceq>(G,L)"
datatype 'a triple = triple ('a assn) term ('a assn)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
types 'a triples = 'a triple set
syntax
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _=>/ {(1_)}" [3,80,3] 75)
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _->/ {(1_)}" [3,80,3] 75)
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _#>/ {(1_)}" [3,65,3] 75)
stmt_triple :: "['a assn, stmt, 'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ ._./ {(1_)}" [3,65,3] 75)
syntax (xsymbols)
triple :: "['a assn, term ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _\<succ>/ {(1_)}" [3,65,3] 75)
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _=\<succ>/ {(1_)}" [3,80,3] 75)
expr_triple :: "['a assn, expr ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _-\<succ>/ {(1_)}" [3,80,3] 75)
exprs_triple :: "['a assn, expr list ,'a assn] \<Rightarrow> 'a triple"
("{(1_)}/ _\<doteq>\<succ>/ {(1_)}" [3,65,3] 75)
translations
"{P} e-\<succ> {Q}" == "{P} In1l e\<succ> {Q}"
"{P} e=\<succ> {Q}" == "{P} In2 e\<succ> {Q}"
"{P} e\<doteq>\<succ> {Q}" == "{P} In3 e\<succ> {Q}"
"{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
constdefs
mtriples :: "('c\<Rightarrow> 'sig\<Rightarrow> 'a assn) \<Rightarrow> ('c\<Rightarrow> 'sig\<Rightarrow> expr) \<Rightarrow>
('c\<Rightarrow> 'sig\<Rightarrow> 'a assn) \<Rightarrow> ('c × 'sig)set \<Rightarrow> 'a triples"
("{{(1_)}/ _-\<succ>/ {(1_)} | _}"[3,65,3,65]75)
"{{P} mb-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} mb C sig-\<succ> {Q C sig})``ms"
consts
triple_valid :: "prog \<Rightarrow> nat \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_\<Turnstile>_:_" [61,0, 58] 57)
ax_valids :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_|\<Turnstile>_" [61,58,58] 57)
ax_derivs :: "prog \<Rightarrow> ('a triples × 'a triples) set"
syntax
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
( "_||=_:_" [61,0, 58] 57)
ax_valid :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_|=_" [61,58,58] 57)
ax_Derivs:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_||-_" [61,58,58] 57)
ax_Deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_|-_" [61,58,58] 57)
syntax (xsymbols)
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
( "_|\<Turnstile>_:_" [61,0, 58] 57)
ax_valid :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_\<Turnstile>_" [61,58,58] 57)
ax_Derivs:: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_|\<turnstile>_" [61,58,58] 57)
ax_Deriv :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_\<turnstile>_" [61,58,58] 57)
defs triple_valid_def "G\<Turnstile>n:t \<equiv> case t of {P} t\<succ> {Q} \<Rightarrow>
\<forall>Y s Z. P (Y,s) Z \<longrightarrow> type_ok G t s \<longrightarrow>
(\<forall>w s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<longrightarrow> Q (res t w Y,s') Z)"
translations "G|\<Turnstile>n:ts" == "Ball ts (triple_valid G n)"
defs ax_valids_def "G,A|\<Turnstile>ts \<equiv> \<forall>n. G|\<Turnstile>n:A \<longrightarrow> G|\<Turnstile>n:ts"
translations "G,A \<Turnstile>t" == "G,A|\<Turnstile>{t}"
"G,A|\<turnstile>ts" == "(A,ts) \<in> ax_derivs G"
"G,A \<turnstile>t" == "G,A|\<turnstile>{t}"
inductive "ax_derivs G" intrs
empty " G,A|\<turnstile>{}"
insert"\<lbrakk>G,A\<turnstile>t; G,A|\<turnstile>ts\<rbrakk> \<Longrightarrow>
G,A|\<turnstile>insert t ts"
asm "ts\<subseteq>A \<Longrightarrow> G,A|\<turnstile>ts"
(* could be added for convenience and efficiency, but is not necessary
cut "\<lbrakk>G,A'|\<turnstile>ts; G,A|\<turnstile>A'\<rbrakk> \<Longrightarrow>
G,A |\<turnstile>ts"
*)
weaken"\<lbrakk>G,A|\<turnstile>ts'; ts \<subseteq> ts'\<rbrakk> \<Longrightarrow> G,A|\<turnstile>ts"
conseq"\<forall>Y s Z . P (Y ,s) Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>w s'.
(\<forall>Y' Z'. P' (Y',s) Z' \<longrightarrow> Q' (res t w Y',s') Z')
\<longrightarrow> Q (res t w Y ,s') Z ))
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
hazard"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
Xcpt "G,A\<turnstile>{(\<lambda>(Y,s). P (res t (arbitrary3 t) Y,s)) \<and>. Not \<circ> normal} t\<succ> {P}"
(* variables *)
LVar " G,A\<turnstile>{Normal (\<lambda>s: P\<up>#Var (lvar vn s))} LVar vn=\<succ> {P}"
FVar "\<lbrakk>G,A\<turnstile>{Normal P} .init C. {Q};
G,A\<turnstile>{Q} e-\<succ> {RefVar (fvar C stat fn) R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} {C,stat}e..fn=\<succ> {R}"
AVar "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
G,A\<turnstile>{Q} e2-\<succ> {\<lambda>Val:i#. RefVar (avar G i) R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e1.[e2]=\<succ> {R}"
(* expressions *)
NewC "\<lbrakk>G,A\<turnstile>{Normal P} .init C. {Alloc G (CInst C) Q}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} NewC C-\<succ> {Q}"
NewA "\<lbrakk>G,A\<turnstile>{Normal P} .init_comp_ty T. {Q};
G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:i#. xupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) R}\<rbrakk>
\<Longrightarrow> G,A\<turnstile>{Normal P} New T[e]-\<succ> {R}"
Cast "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v#. \<lambda>s:
xupd (raise_if (¬G,s\<turnstile>v fits T) ClassCast) .; Q\<up>#Val v}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} Cast T e-\<succ> {Q}"
Inst "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:v#. \<lambda>s:
Q\<up>#Val (Bool (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T))}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e InstOf T-\<succ> {Q}"
Lit "G,A\<turnstile>{Normal (P\<up>#Val v)} Lit v-\<succ> {P}"
Super " G,A\<turnstile>{Normal (\<lambda>s: P\<up>#Val (val_this s))} Super-\<succ> {P}"
Acc "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f)#. Q\<up>#Val v}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
Ass "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:v#Var:(w,f)#. assign f v .; R\<up>#Val v}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} va:=e-\<succ> {R}"
Cond "\<lbrakk>G,A \<turnstile>{Normal P} e0-\<succ> {P'};
\<forall>b. G,A\<turnstile>{P'\<up>#Bool=b} (if b then e1 else e2)-\<succ> {Q}\<rbrakk>
\<Longrightarrow> G,A\<turnstile>{Normal P} e0 ? e1 : e2-\<succ> {Q}"
Call "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
G,A\<turnstile>{Q} args\<doteq>\<succ> {\<lambda>Vals:vs#Val:a#. \<lambda>s: let D=target mode s a cT
in (init_lvars G D (mn,pTs) mode a vs .; R\<up>#DynT D\<up>#Lcls (locals s))};
\<forall>D. G,A\<turnstile>{R\<up>#DynT D\<and>.(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>D\<preceq>t)} Methd D (mn,pTs)-\<succ>
{\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v}\<rbrakk>\<Longrightarrow>
G,A\<turnstile>{Normal P} {t,cT,mode}e..mn({pTs}args)-\<succ> {S}"
Methd "\<lbrakk>G,A\<union> {{P} Methd-\<succ> {Q} | ms} |\<turnstile> {{P} body G-\<succ> {Q} | ms}\<rbrakk> \<Longrightarrow>
G,A|\<turnstile>{{P} Methd-\<succ> {Q} | ms}"
Body "\<lbrakk>G,A\<turnstile>{Normal P} .init D. {Q}; G,A\<turnstile>{Q} .c. {R}; G,A\<turnstile>{R} e-\<succ> {S}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} Body D c e-\<succ> {S}"
(* expression lists *)
Nil "G,A\<turnstile>{Normal (P\<up>#Vals [])} []\<doteq>\<succ> {P}"
Cons "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
G,A\<turnstile>{Q} es\<doteq>\<succ> {\<lambda>Vals:vs#Val:v#. R\<up>#Vals (v#vs)}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
(* statements *)
Skip "G,A\<turnstile>{Normal P} .Skip. {P}"
Expr "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<down>}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .Expr e. {Q}"
Comp "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {Q};
G,A\<turnstile>{Q} .c2. {R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .c1;;c2. {R}"
If "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
\<forall>b. G,A\<turnstile>{P'\<up>#Bool=b} .(if b then c1 else c2). {Q}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .If(e) c1 Else c2. {Q}"
(* unfolding variant of Loop, not needed here
LoopU "\<lbrakk>G,A \<turnstile>{Normal P} e-\<succ> {P'};
\<forall>b. G,A\<turnstile>{P'\<up>#Bool=b} .(if b then c;;While(e) c else Skip).{Q}\<rbrakk>
\<Longrightarrow> G,A\<turnstile>{Normal P} .While(e) c. {Q}"
*)
Loop "\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; G,A\<turnstile>{P'\<up>#Bool=True} .c. {P}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{P} .While(e) c. {P'\<up>#Bool=False}"
Throw "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a#. xupd (throw a) .; Q}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .Throw e. {Q}"
Try "\<lbrakk>G,A\<turnstile>{Normal P} .c1. {SXAlloc G Q};
G,A\<turnstile>{Q \<and>. (\<lambda>s. G,s\<turnstile>catch C) ;. new_xcpt_var vn} .c2. {R};
(Q \<and>. (\<lambda>s. ¬G,s\<turnstile>catch C)) \<Rightarrow> R\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} .Try c1 Catch(C vn) c2. {R}"
Fin "\<lbrakk>G,A\<turnstile>{Normal P}.c1.{\<lambda>(Y,(x,s)). (Q\<up>#Xcpt x) (Y,Norm s)};
G,A\<turnstile>{Normal Q}.c2.{\<lambda>Xcpt:x'#. xupd (xcpt_if (x'\<noteq>None) x') .; R}\<rbrakk>
\<Longrightarrow> G,A\<turnstile>{Normal P} .c1 Finally c2. {R}"
Done " G,A\<turnstile>{Normal (P \<and>. initd C)} .init C. {P}"
Init "\<lbrakk>the (class G C) = (sc,si,fs,ms,ini);
G,A\<turnstile>{Normal ((P \<and>. Not \<circ> initd C) ;. supd (init_class_obj G C))}
.(if C = Object then Skip else init sc).
{\<lambda>s: Q\<up>#Lcls (locals s)};
G,A\<turnstile>{Q ;. set_lvars empty} .ini. {\<lambda>Lcls:l#. set_lvars l .; R}\<rbrakk>
\<Longrightarrow> G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .init C. {R}"
end
theorem assn_imp_def2:
(P \<Rightarrow> Q) = (ALL Y s Z. P (Y, s) Z --> Q (Y, s) Z)
theorem lsplit_partial_beta:
(lsplit P o f) Y s Z = ((%a#Y. P a Y s Z) o f) Y
theorem assn_lsplit_conc:
(%Y s Z. (lsplit (P s Z) o f) Y) = (%a#Y s Z. P s Z a Y) o f
theorem split_paired_All_aux:
(ALL Z. split P Z --> Q Z) = (ALL Y s. P Y s --> Q (Y, s))
theorem inj_triple:
inj (split (%P. split (triple P)))
theorem triple_inj_eq:
({P} t> {Q} = {P'} t'> {Q'}) = (P = P' & t = t' & Q = Q')
theorem split_paired_All_rstate:
(ALL Z. P Z) = (ALL Y s. P (Y, s))
theorem the_Res_Res:
the_Res (Res x) = x
theorem the_Xcpt_Xcpt:
the_Xcpt (Xcpt x) = x
theorem the_Lcls_Lcls:
the_Lcls (Lcls x) = x
theorem assn_supd_def2:
(P ;. f) Ys Z = (EX s. P (fst Ys, s) Z & snd Ys = f s)
theorem supd_assn_def2:
(f .; P) (Y, s) = P (Y, f s)
theorem split_supd_assn:
(f .; split P) = (%(Y, s). P Y (f s))
theorem supd_assn_supdD:
(f .; Q ;. f) Ys Z ==> Q Ys Z
theorem supd_assn_supdI:
Q Ys Z ==> (f .; Q ;. f) Ys Z
theorem peek_and_def2:
(P \<and>. p) (Y, s) = (%Z. P (Y, s) Z & p s)
theorem peek_and_Not:
(P \<and>. (%s. ¬ f s)) = (P \<and>. Not o f)
theorem peek_and_and:
(P \<and>. p \<and>. p) = (P \<and>. p)
theorem peek_and_Normal:
(Normal P \<and>. p) = Normal (P \<and>. p)
theorem upd_res_Normal:
(%(Y, s). (Normal P) (f Y s, s)) = Normal (%(Y, s). P (f Y s, s))
theorems res_rews:
res (In1l x) v Y == Res v # Y
res (In2 x) v Y == Res v # Y
res (In3 x) v Y == Res v # Y
res (In1r x) v Y == Y
theorem res_partial_inj:
(res t w' Y' = res t w Y) = ((is_stmt t | w' = w) & Y' = Y)
theorem res_push_def2:
(P\<up>#w) (Y, s) = P (w # Y, s)
theorem split_res_push:
split P\<up>#w = split (%Y. P (w # Y))
theorem split_lsplit_res_push:
split (lsplit (P o f'))\<up>#f x = split (P (f' (f x)))
theorem peek_and_push:
(P \<and>. p)\<up>#w = (P\<up>#w \<and>. p)
theorem res_pop_def2:
res_pop Pf (p # Y, s) = Pf p (Y, s)
theorem res_pop_res_push:
res_pop (P o f)\<up>#w = P (f w)
theorem res_eqpop_def2:
(P\<down>#w) (Y, s) Z = (EX Y'. Y = w # Y' & P (Y', s) Z)
theorem res_eqpop_push:
P\<down>#w\<up>#w = P
theorem res_ign_def2:
P\<down> (y # Y, s) = P (Y, s)
theorem res_ign_push:
P\<down>\<up>#w = P
theorem peek_st_def2:
peek_st Pf (Y, s) = Pf (snd s) (Y, s)
theorem peek_st_triv:
(\<lambda>s: P) = P
theorem peek_st_split:
(\<lambda>s: split (P s)) = (%(Y, s). P (snd s) Y s)
theorem peek_st_res_push:
peek_st P\<up>#w = (\<lambda>s: P s\<up>#w)
theorem peek_st_st:
(\<lambda>s: peek_st (P s)) = (\<lambda>s: P s s)
theorem Bool_assn_def2:
(P\<up>#Bool=b) (Y, s) Z = (EX v. P (Val v # Y, s) Z & (normal s --> the_Bool v = b))
theorem Bool_assn_the_BoolI:
P (Val b # Y, s) Z ==> (P\<up>#Bool=the_Bool b) (Y, s) Z
theorem RefVar_def2:
RefVar vf P (Val a # Y, s) = (P\<up>#Var (fst (vf a s))) (Y, snd (vf a s))
theorem Alloc_def2:
Alloc G otag P (Y, s) Z = (ALL s' a. G|-s -halloc otag>a-> s' --> P (Val (Addr a) # Y, s') Z)
theorem SXAlloc_def2:
SXAlloc G P (Y, s) Z = (ALL s'. G|-s -sxalloc-> s' --> P (Y, s') Z)
theorem triple_valid_def2:
G\<Turnstile>n:{P} t> {Q} =
(ALL Y s Z.
P (Y, s) Z -->
(EX L. (normal s --> (EX T. (G, L)|-t::T)) & s\<Colon>\<preceq>(G, L)) -->
(ALL w s'. (s, t, n, w, s') : evaln G --> Q (res t w Y, s') Z))
theorem cut_valid:
[| G,A'|\<Turnstile>ts; G,A|\<Turnstile>A' |] ==> G,A|\<Turnstile>ts
theorem ax_thin:
[| G,A'||-ts; A' <= A |] ==> G,A||-ts
theorem ax_thin_insert:
G,A|-t ==> G,insert x A|-t
theorem subset_mtriples_iff:
(ts <= {{P} mb-\<succ> {Q} | ms}) =
(EX ms'. ms' <= ms & ts = {{P} mb-\<succ> {Q} | ms'})
theorem conseq12:
[| G,A|-{P'} t> {Q'};
ALL Y s Z.
P (Y, s) Z -->
(ALL w s'.
(ALL Y' Z'. P' (Y', s) Z' --> Q' (res t w Y', s') Z') -->
Q (res t w Y, s') Z) |]
==> G,A|-{P} t> {Q}
theorem conseq12':
[| G,A|-{P'} t> {Q'};
ALL s w s'.
(ALL Y Z. P' (Y, s) Z --> Q' (res t w Y, s') Z) -->
(ALL Y Z. P (Y, s) Z --> Q (res t w Y, s') Z) |]
==> G,A|-{P} t> {Q}
theorem conseq12_from_conseq12':
[| G,A|-{P'} t> {Q'};
ALL Y s Z.
P (Y, s) Z -->
(ALL w s'.
(ALL Y' Z'. P' (Y', s) Z' --> Q' (res t w Y', s') Z') -->
Q (res t w Y, s') Z) |]
==> G,A|-{P} t> {Q}
theorem conseq1:
[| G,A|-{P'} t> {Q}; P \<Rightarrow> P' |] ==> G,A|-{P} t> {Q}
theorem conseq2:
[| G,A|-{P} t> {Q'}; Q' \<Rightarrow> Q |] ==> G,A|-{P} t> {Q}
theorem escape:
ALL Y s Z. P (Y, s) Z --> G,A|-{%Ys' Z'. Ys' = (Y, s)} t> {%Ys Z'. Q Ys Z}
==> G,A|-{P} t> {Q}
theorem constant:
(C ==> G,A|-{split P} t> {Q}) ==> G,A|-{%(Y, s) Z. C & P Y s Z} t> {Q}
theorem impossible:
G,A|-{%Ys Z. False} t> {Q}
theorem ax_trivial:
G,A|-{P} t> {%Ys Z. True}
theorem ax_disj:
[| G,A|-{P1} t> {Q1}; G,A|-{P2} t> {Q2} |]
==> G,A|-{%Ys Z. P1 Ys Z | P2 Ys Z} t> {%Ys Z. Q1 Ys Z | Q2 Ys Z}
theorem supd_shuffle:
(EX Q. G,A|-{P} .c1. {Q} & G,A|-{Q ;. f} .c2. {R}) =
(EX Q'. G,A|-{P} .c1. {f .; Q'} & G,A|-{Q'} .c2. {R})
theorem ax_cases:
[| G,A|-{P \<and>. C} t> {Q}; G,A|-{P \<and>. Not o C} t> {Q} |]
==> G,A|-{P} t> {Q}
theorem peek_and_forget1_Normal:
G,A|-{Normal P} t> {Q} ==> G,A|-{Normal (P \<and>. p)} t> {Q}
theorem peek_and_forget1:
G,A|-{P} t> {Q} ==> G,A|-{P \<and>. p} t> {Q}
theorem ax_NormalD:
G,A|-{P} t> {Q} ==> G,A|-{Normal P} t> {Q}
theorem peek_and_forget2:
G,A|-{P} t> {Q \<and>. p} ==> G,A|-{P} t> {Q}
theorem nochange:
G,A|-{op =} t> {op =} ==> G,A|-{P} t> {P}
theorem exists_res:
G,A|-{P} t> {Q}
==> G,A|-{P} t> {%(Y, s) Z. EX v Y'. Y = res t v Y' & Q (Y, s) Z}
theorem extend_res:
G,A|-{P} t> {Q}
==> G,A|-{P\<up>#y} t>
{%(Y, s) Z. EX v Y'. Y = res t v Y' & Q (res t v (y # Y'), s) Z}
theorem extend_res_stmt:
G,A|-{P} .c. {Q} ==> G,A|-{P\<up>#y} .c. {Q\<up>#y}
theorem ax_LVar2:
G,A|-{Normal P} LVar vn=> {Normal (\<lambda>s: P\<down>#Var (lvar vn s))}
theorem ax_Lit2:
G,A|-{Normal P} Lit v-> {Normal (P\<down>#Val v)}
theorem ax_Super2:
G,A|-{Normal P} Super->
{Normal (\<lambda>s: P\<down>#Val (the (locals s (Inr ()))))}
theorem ax_Nil2:
G,A|-{Normal P} []#> {Normal (P\<down>#Vals [])}
theorem ax_finite_mtriples:
[| finite F; ALL (C, sig):F. G,A|-{Normal (P C sig)} mb C sig-> {Q C sig} |]
==> G,A||-{{P} mb-\<succ> {Q} | F}
theorem ax_derivs_insertD:
G,A||-insert t ts ==> G,A|-t & G,A||-ts
theorem ax_methods_spec:
[| G,A||-split f `` ms; (C, sig) : ms |] ==> G,A|-f C sig
theorem ax_finite_pointwise:
[| finite F; (ALL (C, sig):F. G,A|-f C sig) --> (ALL (C, sig):F. G,A|-g C sig);
G,A||-split f `` F |]
==> G,A||-split g `` F
theorem ax_no_hazard:
G,A|-{P \<and>. type_ok G t} t> {Q} ==> G,A|-{P} t> {Q}
theorem ax_free_wt:
(EX T L. (G, L)|-t::T) --> G,A|-{Normal P} t> {Q} ==> G,A|-{Normal P} t> {Q}
theorems ax_Xcpts:
G,A|-{(%(Y, s). P (Val arbitrary # Y, s)) \<and>. Not o normal} x-> {P}
G,A|-{(%(Y, s). P (Var arbitrary # Y, s)) \<and>. Not o normal} x=> {P}
G,A|-{(%(Y, s). P (Vals arbitrary # Y, s)) \<and>. Not o normal} x#> {P}
G,A|-{P \<and>. Not o normal} .x. {P}
theorem ax_Skip:
G,A|-{P} .Skip. {P}
theorem ax_SkipI:
P \<Rightarrow> Q ==> G,A|-{P} .Skip. {Q}
theorem ax_Call_Static:
[| the (cmethd G C (mn, pTs)) = (md, (m, pns, rT), lvars, bdy);
G,A|-{Normal P} e-> {Q\<down>};
G,A|-{Q} args#>
{\<lambda>Vals:vs#. \<lambda>s: set_lvars
(init_vals (table_of lvars)(pns[|->]vs) (+)
empty) .;
R\<up>#Lcls (locals s)};
G,A|-{R} Methd C (mn, pTs)->
{\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v} |]
==> G,A|-{Normal P} {t,ClassT C,Static}e..mn( {pTs}args)-> {S}
theorem ax_Call_known_DynT:
[| the (cmethd G C (mn, pTs)) = (md, (m, pns, rT), lvars, bdy);
G,A|-{Normal P} e-> {Q};
G,A|-{Q} args#>
{\<lambda>Vals:vs#
Val:a#. (\<lambda>s: (%(x, s).
((np a) x,
set_locals
(init_vals (table_of lvars)(pns[|->]vs
) (+)¬False ?\<mapsto>a)
s)) .;
R\<up>#Lcls (locals s)) \<and>.
(%s. C = obj_class (lookup_obj (snd s) a))};
G,A|-{R \<and>.
(%s. normal s --> G\<turnstile>IntVir\<rightarrow>C\<preceq>t)}
Methd C (mn, pTs)-> {\<lambda>Val:v#Lcls:l#. set_lvars l .; S\<up>#Val v} |]
==> G,A|-{Normal P} {t,cT,IntVir}e..mn( {pTs}args)-> {S}
theorem ax_Methd1:
[| G,A Un {{P} Methd-\<succ> {Q} | ms}||-{{P} body G-\<succ> {Q} | ms};
(C, sig) : ms |]
==> G,A|-{Normal (P C sig)} Methd C sig-> {Q C sig}
theorem ax_MethdN:
G,insert ({Normal P} Methd C sig-> {Q}) A|-{Normal P} body G C sig-> {Q}
==> G,A|-{Normal P} Methd C sig-> {Q}
theorem ax_InitS:
[| the (class G C) = (sc, si, fs, ms, ini); C ~= Object;
G,A|-{Normal (P \<and>. Not o initd C ;. supd (init_class_obj G C))}
.init sc. {\<lambda>s: Q\<up>#Lcls (locals s)};
G,A|-{Q ;. set_lvars empty} .ini. {\<lambda>Lcls:l#. set_lvars l .; R} |]
==> G,A|-{Normal (P \<and>. Not o initd C)} .init C. {R}
theorem ax_triv_InitS:
[| the (class G C) = (sc, si, fs, ms, Skip); C ~= Object;
P \<Rightarrow> (supd (init_class_obj G C) .; P);
G,A|-{Normal (P \<and>. initd C)} .init sc. {P \<and>. initd C} |]
==> G,A|-{Normal P} .init C. {P \<and>. initd C}
theorem ax_Init_Object:
wf_prog G
==> G,A|-{Normal
(supd (init_class_obj G Object) .; P \<and>. Not o initd Object)}
.init Object. {P \<and>. initd Object}
theorem ax_triv_Init_Object:
[| wf_prog G; P \<Rightarrow> (supd (init_class_obj G Object) .; P) |]
==> G,A|-{Normal P} .init Object. {P \<and>. initd Object}
theorem ax_Alloc_Normal:
[| enough_mem;
G,A|-{P} t>
{%(Y, x, s) Z.
x = None &
(ALL a. new_Addr (heap s) = Some a -->
Q (Val (Addr a) # Y, Norm (init_obj G (CInst C) (Inl a) s))
Z)} |]
==> G,A|-{P} t> {Alloc G (CInst C) Q}
theorem ax_SXAlloc_Normal:
G,A|-{P} .c. {Normal Q} ==> G,A|-{P} .c. {SXAlloc G Q}
theorem ax_SXAlloc_catch_SXcpt:
[| enough_mem;
G,A|-{P} t>
{%(Y, x, s) Z.
x = Some (StdXcpt xn) &
(ALL a. new_Addr (heap s) = Some a -->
Q (Y, Some (XcptLoc a), init_obj G (CInst (SXcpt xn)) (Inl a) s)
Z)} |]
==> G,A|-{P} t> {SXAlloc G (Q \<and>. (%s. G,s\<turnstile>catch SXcpt xn))}