--- a/src/HOL/IMP/VC.ML Tue Jan 23 11:33:46 1996 +0100
+++ b/src/HOL/IMP/VC.ML Tue Jan 23 14:25:55 1996 +0100
@@ -77,3 +77,8 @@
by(Asm_simp_tac 1);
by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
qed "vc_complete";
+
+goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
+by(acom.induct_tac "c" 1);
+by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
+qed "vcwp_vc_wp";
--- a/src/HOL/IMP/VC.thy Tue Jan 23 11:33:46 1996 +0100
+++ b/src/HOL/IMP/VC.thy Tue Jan 23 14:25:55 1996 +0100
@@ -18,6 +18,7 @@
consts
vc,wp :: acom => assn => assn
+ vcwp :: "acom => assn => assn * assn"
astrip :: acom => com
primrec wp acom
@@ -41,5 +42,25 @@
astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)"
astrip_Aif "astrip (Aif b c d) = ifC b (astrip c) (astrip d)"
astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
-
+
+(* simultaneous computation of vc and wp: *)
+primrec vcwp acom
+ vcwp_Askip
+ "vcwp Askip Q = (%s.True, Q)"
+ vcwp_Aass
+ "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"
+ vcwp_Asemi
+ "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
+ (vcc,wpc) = vcwp c wpd
+ in (%s. vcc s & vcd s, wpc))"
+ vcwp_Aif
+ "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
+ (vcc,wpc) = vcwp c Q
+ in (%s. vcc s & vcd s,
+ %s.(B b s-->wpc s) & (~B b s-->wpd s)))"
+ vcwp_Awhile
+ "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
+ in (%s. (I s & ~B b s --> Q s) &
+ (I s & B b s --> wpc s) & vcc s, I))"
+
end