Up to index of Isabelle/Bali5
theory AxSem = Evaln + TypeSafe(* Title: isabelle/Bali/AxSem.thy
ID: $Id: AxSem.thy,v 1.109 2000/11/25 23:58:27 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 entry)
* multiple results with semantical substitution mechnism not requiring a stack
* because of dynamic method binding, terms 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:
* all triples in a derivation are of the same type (due to weak polymorphism)
*)
AxSem = Evaln + TypeSafe +
types res = vals (* result entry *)
syntax
Val :: "val \<Rightarrow> res"
Var :: "var \<Rightarrow> res"
Vals :: "val list \<Rightarrow> res"
translations
"Val x" => "(In1 x)"
"Var x" => "(In2 x)"
"Vals x" => "(In3 x)"
syntax
"Val_" :: [pttrn] => pttrn ("Val:_" [951] 950)
"Var_" :: [pttrn] => pttrn ("Var:_" [951] 950)
"Vals_" :: [pttrn] => pttrn ("Vals:_" [951] 950)
translations
"\<lambda>Val:v . b" == "(\<lambda>v. b) \<circ> the_In1"
"\<lambda>Var:v . b" == "(\<lambda>v. b) \<circ> the_In2"
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> the_In3"
(* relation on result values, state and auxiliary variables *)
types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
"res" <= (type) "AxSem.res"
"a assn" <= (type) "vals \<Rightarrow> state \<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)"
subst_res :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<leftarrow>_" [60,61] 60)
"P\<leftarrow>w \<equiv> \<lambda>Y. P w"
subst_Bool :: "'a assn \<Rightarrow> bool \<Rightarrow> 'a assn" ("_\<leftarrow>=_" [60,61] 60)
"P\<leftarrow>=b \<equiv> \<lambda>Y s Z. \<exists>v. P (Val v) s Z \<and> (normal s \<longrightarrow> the_Bool v=b)"
peek_res :: "(res \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
"peek_res Pf \<equiv> \<lambda>Y. Pf Y Y"
peek_st :: "(st \<Rightarrow> 'a assn) \<Rightarrow> 'a assn"
"peek_st P \<equiv> \<lambda>Y s. P (snd s) Y s"
ign_res :: " 'a assn \<Rightarrow> 'a assn" ("_\<down>" [1000] 1000)
"P\<down> \<equiv> \<lambda>Y s Z. \<exists>Y. P Y s Z"
syntax
Normal :: "'a assn \<Rightarrow> 'a assn"
"@peek_res" :: "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:. P" == "peek_res (\<lambda>w. P)"
"\<lambda>s.. P" == "peek_st (\<lambda>s. P)"
constdefs
ign_res_eq :: "'a assn \<Rightarrow> res \<Rightarrow> 'a assn" ("_\<down>=_" [60,61] 60)
"P\<down>=w \<equiv> \<lambda>Y:. P\<down> \<and>. (\<lambda>s. Y=w)"
RefVar :: "(state \<Rightarrow> vvar × state) \<Rightarrow> 'a assn \<Rightarrow> 'a assn"(infixr "..;" 13)
"vf ..; P \<equiv> \<lambda>Y s. let (v,s') = vf s in P (Var v) 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 (Val (Addr a)) 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) (** should be
something like triple = \<forall>'a. 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} tf-\<succ> {Q} | ms} \<equiv> (\<lambda>(C,sig). {Normal(P C sig)} tf 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> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_|\<Turnstile>_" [61,58,58] 57)
ax_derivs :: "prog \<Rightarrow> ('b triples × 'a triples) set"
syntax
triples_valid:: "prog \<Rightarrow> nat \<Rightarrow> 'a triples \<Rightarrow> bool"
( "_||=_:_" [61,0, 58] 57)
ax_valid :: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_|=_" [61,58,58] 57)
ax_Derivs:: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_||-_" [61,58,58] 57)
ax_Deriv :: "prog \<Rightarrow> 'b 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> 'b triples \<Rightarrow> 'a triple \<Rightarrow> bool"
( "_,_\<Turnstile>_" [61,58,58] 57)
ax_Derivs:: "prog \<Rightarrow> 'b triples \<Rightarrow> 'a triples \<Rightarrow> bool"
("_,_|\<turnstile>_" [61,58,58] 57)
ax_Deriv :: "prog \<Rightarrow> 'b 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>Y' s'. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y',s') \<longrightarrow> Q 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>Y' s'.
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
Q 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>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
(* variables *)
LVar " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
FVar "\<lbrakk>G,A\<turnstile>{Normal P} .init C. {Q};
G,A\<turnstile>{Q} e-\<succ> {\<lambda>Val:a:. fvar C stat fn a ..; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} {C,stat}e..fn=\<succ> {R}"
AVar "\<lbrakk>G,A\<turnstile>{Normal P} e1-\<succ> {Q};
\<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; 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\<leftarrow>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\<leftarrow>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\<leftarrow>Val v)} Lit v-\<succ> {P}"
Super " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Val (val_this s))} Super-\<succ> {P}"
Acc "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {\<lambda>Var:(v,f):. Q\<leftarrow>Val v}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} Acc va-\<succ> {Q}"
Ass "\<lbrakk>G,A\<turnstile>{Normal P} va=\<succ> {Q};
\<forall>vf. G,A\<turnstile>{Q\<leftarrow>Var vf} e-\<succ> {\<lambda>Val:v:. assign (snd vf) v .; R}\<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'\<leftarrow>=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}; \<forall>a. G,A\<turnstile>{Q\<leftarrow>Val a} args\<doteq>\<succ> {R a};
\<forall>a vs D l. G,A\<turnstile>{(R a\<leftarrow>Vals vs \<and>.
(\<lambda>s. D = target mode (snd s) a cT \<and> l = locals (snd s)) ;.
init_lvars G D (mn,pTs) mode a vs) \<and>.
(\<lambda>s. normal s \<longrightarrow> G\<turnstile>mode\<rightarrow>D\<preceq>t)}
Methd D (mn,pTs)-\<succ> {set_lvars l .; S}\<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\<leftarrow>Vals [])} []\<doteq>\<succ> {P}"
Cons "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q};
\<forall>v. G,A\<turnstile>{Q\<leftarrow>Val v} es\<doteq>\<succ> {\<lambda>Vals:vs:. R\<leftarrow>Vals (v#vs)}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal P} e#es\<doteq>\<succ> {R}"
(* statements *)
Skip "G,A\<turnstile>{Normal (P\<leftarrow>\<bullet>)} .Skip. {P}"
Expr "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {Q\<leftarrow>\<bullet>}\<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'\<leftarrow>=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'\<leftarrow>=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>{Normal (P'\<leftarrow>=True)} .c. {P}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{P} .While(e) c. {(P'\<leftarrow>=False)\<down>=\<bullet>}"
Throw "\<lbrakk>G,A\<turnstile>{Normal P} e-\<succ> {\<lambda>Val:a:. xupd (throw a) .; Q\<leftarrow>\<bullet>}\<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. {Q};
\<forall>x. G,A\<turnstile>{Q \<and>. (\<lambda>s. x = fst s) ;. xupd (\<lambda>x. None)}
.c2. {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\<leftarrow>\<bullet> \<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). {Q};
\<forall>l. G,A\<turnstile>{Q \<and>. (\<lambda>s. l = locals (snd s)) ;. set_lvars empty}
.ini. {set_lvars l .; R}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{Normal (P \<and>. Not \<circ> initd C)} .init C. {R}"
rules (** these terms are the same as above, but with generalized typing **)
polymorphic_conseq
"\<forall>Y s Z . P Y s Z \<longrightarrow> (\<exists>P' Q'. G,A\<turnstile>{P'} t\<succ> {Q'} \<and> (\<forall>Y' s'.
(\<forall>Y Z'. P' Y s Z' \<longrightarrow> Q' Y' s' Z') \<longrightarrow>
Q Y' s' Z ))
\<Longrightarrow> G,A\<turnstile>{P } t\<succ> {Q }"
polymorphic_Loop
"\<lbrakk>G,A\<turnstile>{P} e-\<succ> {P'}; G,A\<turnstile>{Normal (P'\<leftarrow>=True)} .c. {P}\<rbrakk> \<Longrightarrow>
G,A\<turnstile>{P} .While(e) c. {(P'\<leftarrow>=False)\<down>=\<bullet>}"
end
theorem assn_imp_def2:
(P \<Rightarrow> Q) = (ALL Y s Z. P Y s Z --> Q Y s Z)
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 assn_supd_def2:
(P ;. f) Y s' Z = (EX s. P Y s Z & s' = f s)
theorem supd_assn_def2:
(f .; P) Y s = P Y (f s)
theorem supd_assn_supdD:
(f .; Q ;. f) Y s Z ==> Q Y s Z
theorem supd_assn_supdI:
Q Y s Z ==> (f .; Q ;. f) Y s 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_commut:
(P \<and>. p \<and>. q) = (P \<and>. q \<and>. p)
theorem peek_and_Normal:
(Normal P \<and>. p) = Normal (P \<and>. p)
theorem subst_res_def2:
(P\<leftarrow>w) Y = P w
theorem subst_subst_res:
P\<leftarrow>w\<leftarrow>v = P\<leftarrow>w
theorem peek_and_subst_res:
(P \<and>. p)\<leftarrow>w = (P\<leftarrow>w \<and>. p)
theorem subst_Bool_def2:
(P\<leftarrow>=b) Y s Z = (EX v. P (In1 v) s Z & (normal s --> the_Bool v = b))
theorem subst_Bool_the_BoolI:
P (In1 b) s Z ==> (P\<leftarrow>=the_Bool b) Y s Z
theorem peek_res_def2:
peek_res P Y = P Y Y
theorem peek_res_subst_res:
peek_res P\<leftarrow>w = P w\<leftarrow>w
theorem peek_subst_res_allI:
(!!a. T a (P (f a)\<leftarrow>f a)) ==> ALL a. T a (peek_res P\<leftarrow>f a)
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_st:
(\<lambda>s.. peek_st (P s)) = (\<lambda>s.. P s s)
theorem peek_st_split:
peek_st P = (%Y s. P (snd s) Y s)
theorem peek_st_subst_res:
peek_st P\<leftarrow>w = (\<lambda>s.. P s\<leftarrow>w)
theorem peek_st_Normal:
(\<lambda>s.. Normal (P s)) = Normal (peek_st P)
theorem ign_res_def2:
P\<down> Y s Z = (EX Y. P Y s Z)
theorem ign_ign_res:
P\<down>\<down> = P\<down>
theorem ign_subst_res:
P\<down>\<leftarrow>w = P\<down>
theorem peek_and_ign_res:
(P \<and>. p)\<down> = (P\<down> \<and>. p)
theorem ign_res_eq_def2:
(P\<down>=w) Y s Z = ((EX Y. P Y s Z) & Y = w)
theorem ign_ign_res_eq:
(P\<down>=w)\<down> = P\<down>
theorem ign_res_eq_subst_res:
P\<down>=w\<leftarrow>w = P\<down>
theorem subst_Bool_ign_res_eq:
(P\<leftarrow>=b\<down>=x) Y s Z = ((P\<leftarrow>=b) Y s Z & Y = x)
theorem RefVar_def2:
(vf ..; P) Y s = P (In2 (fst (vf s))) (snd (vf s))
theorem Alloc_def2:
Alloc G otag P Y s Z = (ALL s' a. G|-s -halloc otag>a-> s' --> P (In1 (Addr a)) 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 Y' s'. G|-s -t>-n-> (Y', s') --> Q 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 Y' s'. (ALL Y Z'. P' Y s Z' --> Q' Y' s' Z') --> Q Y' s' Z) |]
==> G,A|-{P} t> {Q}
theorem conseq12':
[| G,A|-{P'} t> {Q'};
ALL s Y' s'.
(ALL Y Z. P' Y s Z --> Q' Y' s' Z) --> (ALL Y Z. P Y s Z --> Q 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 Y' s'. (ALL Y Z'. P' Y s Z' --> Q' Y' s' Z') --> Q 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 ax_escape:
ALL Y s Z. P Y s Z --> G,A|-{%Y' s' Z'. (Y', s') = (Y, s)} t> {%Y s Z'. Q Y s Z}
==> G,A|-{P} t> {Q}
theorem ax_constant:
(C ==> G,A|-{P} t> {Q}) ==> G,A|-{%Y s Z. C & P Y s Z} t> {Q}
theorem ax_impossible:
G,A|-{%Y s Z. False} t> {Q}
theorem ax_nochange_lemma:
[| P Y s; All (op = w) |] ==> P w s
theorem ax_nochange:
G,A|-{%Y s. op = (Y, s)} t> {%Y s. op = (Y, s)} ==> G,A|-{P} t> {P}
theorem ax_trivial:
G,A|-{P} t> {%Y s Z. True}
theorem ax_disj:
[| G,A|-{P1} t> {Q1}; G,A|-{P2} t> {Q2} |]
==> G,A|-{%Y s Z. P1 Y s Z | P2 Y s Z} t> {%Y s Z. Q1 Y s Z | Q2 Y s Z}
theorem ax_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 ax_subst_Val_allI:
ALL v. G,A|-{P' v\<leftarrow>In1 v} t> {Q v}
==> ALL v. G,A|-{(\<lambda>w:. P' (the_In1 w))\<leftarrow>In1 v} t> {Q v}
theorem ax_subst_Var_allI:
ALL v. G,A|-{P' v\<leftarrow>In2 v} t> {Q v}
==> ALL v. G,A|-{(\<lambda>w:. P' (the_In2 w))\<leftarrow>In2 v} t> {Q v}
theorem ax_subst_Vals_allI:
ALL v. G,A|-{P' v\<leftarrow>In3 v} t> {Q v}
==> ALL v. G,A|-{(\<lambda>w:. P' (the_In3 w))\<leftarrow>In3 v} t> {Q v}
theorem ax_Lit2:
G,A|-{Normal P} Lit v-> {Normal (P\<down>=In1 v)}
theorem ax_Lit2_test_complete:
G,A|-{Normal (P\<leftarrow>In1 v)} Lit v-> {P}
theorem ax_LVar2:
G,A|-{Normal P} LVar vn=> {Normal (\<lambda>s.. P\<down>=In2 (lvar vn s))}
theorem ax_Super2:
G,A|-{Normal P} Super->
{Normal (\<lambda>s.. P\<down>=In1 (the (locals s (Inr ()))))}
theorem ax_Nil2:
G,A|-{Normal P} []#> {Normal (P\<down>=In3 [])}
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|-{P\<leftarrow>In1 arbitrary \<and>. Not o normal} x-> {P}
G,A|-{P\<leftarrow>In2 arbitrary \<and>. Not o normal} x=> {P}
G,A|-{P\<leftarrow>In3 arbitrary \<and>. Not o normal} x#> {P}
G,A|-{P\<leftarrow>dummy_res \<and>. Not o normal} .x. {P}
theorem ax_Skip:
G,A|-{P\<leftarrow>dummy_res} .Skip. {P}
theorem ax_SkipI:
P \<Rightarrow> Q\<leftarrow>dummy_res ==> G,A|-{P} .Skip. {Q}
theorem ax_Call_Static:
[| the (cmethd G C (mn, pTs)) = (md, (m, pns, rT), lvars, bdy);
ALL vs l.
G,A|-{R\<leftarrow>In3 vs \<and>. (%s. l = locals (snd s)) ;.
init_lvars G C (mn, pTs) Static any_Addr vs}
Methd C (mn, pTs)-> {set_lvars l .; S};
G,A|-{Normal P} e-> {Q}; G,A|-{Q\<down>} args#> {R} |]
==> 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\<turnstile>IntVir\<rightarrow>C\<preceq>t;
ALL a vs l.
G,A|-{R a\<leftarrow>In3 vs \<and>. (%s. l = locals (snd s)) ;.
init_lvars G C (mn, pTs) IntVir a vs}
Methd C (mn, pTs)-> {set_lvars l .; S};
ALL a. G,A|-{Q\<leftarrow>In1 a} args#>
{R a \<and>. (%s. C = obj_class (lookup_obj (snd s) a))};
G,A|-{Normal P} e-> {Q} |]
==> 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_StatRef:
G,A|-{Normal (P\<leftarrow>In1 Null)} StatRef rt-> {P}
theorem ax_InitS:
[| the (class G C) = (sc, si, fs, ms, ini); C ~= Object;
ALL l. G,A|-{Q \<and>. (%s. l = locals (snd s)) ;. set_lvars empty} .ini.
{set_lvars l .; R};
G,A|-{Normal (P \<and>. Not o initd C ;. supd (init_class_obj G C))}
.init sc. {Q} |]
==> G,A|-{Normal (P \<and>. Not o initd C)} .init C. {R}
theorem ax_Init_Skip_lemma:
ALL l. G,A|-{P\<leftarrow>dummy_res \<and>. (%s. l = locals (snd s)) ;.
set_lvars l'}
.Skip. {set_lvars l .; P}
theorem ax_triv_InitS:
[| the (class G C) = (sc, si, fs, ms, Skip); C ~= Object;
P\<leftarrow>dummy_res \<Rightarrow> (supd (init_class_obj G C) .; P);
G,A|-{Normal (P \<and>. initd C)} .init sc.
{(P \<and>. initd C)\<leftarrow>dummy_res} |]
==> G,A|-{Normal P\<leftarrow>dummy_res} .init C. {P \<and>. initd C}
theorem ax_Init_Object:
wf_prog G
==> G,A|-{Normal
(supd (init_class_obj G Object) .; P\<leftarrow>dummy_res \<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\<leftarrow>dummy_res} .init Object. {P \<and>. initd Object}
theorem ax_SXAlloc_Normal:
G,A|-{P} .c. {Normal Q} ==> G,A|-{P} .c. {SXAlloc G Q}
theorem ax_Alloc:
G,A|-{P} t>
{Normal
(%Y (x, s) Z.
ALL a. new_Addr (heap s) = Some a -->
Q (In1 (Addr a)) (Norm (init_obj G (CInst C) (Inl a) s)) Z) \<and>.
heap_free 2}
==> G,A|-{P} t> {Alloc G (CInst C) Q}
theorem ax_Alloc_Arr:
G,A|-{P} t>
{\<lambda>Val:i:. Normal
(%Y (x, s) Z.
¬ the_Intg i < #0 &
(ALL a. new_Addr (heap s) = Some a -->
Q (In1 (Addr a))
(Norm (init_obj G (Arr T (the_Intg i)) (Inl a)
s))
Z)) \<and>.
heap_free 2}
==> G,A|-{P} t>
{\<lambda>Val:i:. xupd (check_neg i) .; Alloc G (Arr T (the_Intg i)) Q}
theorem ax_SXAlloc_catch_SXcpt:
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)) \<and>.
heap_free 2}
==> G,A|-{P} t> {SXAlloc G (%Y s Z. Q Y s Z & G,s\<turnstile>catch SXcpt xn)}