# HG changeset patch
# User nipkow
# Date 822403555 -3600
# Node ID 6803ecb9b198d3081fa078f5733bd0e18da07df8
# Parent  19a256c8086d1cacda3f238ffc5d9b2c5fd963d7
Added vcwp

diff -r 19a256c8086d -r 6803ecb9b198 src/HOL/IMP/VC.ML
--- 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";
diff -r 19a256c8086d -r 6803ecb9b198 src/HOL/IMP/VC.thy
--- 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