--- a/src/HOL/IMP/VC.ML Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/VC.ML Tue Mar 18 18:02:19 1997 +0100
@@ -12,7 +12,7 @@
val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
-goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}";
+goal VC.thy "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
by (acom.induct_tac "c" 1);
by (ALLGOALS Simp_tac);
by (Fast_tac 1);
@@ -29,25 +29,25 @@
by (ALLGOALS(fast_tac HOL_cs));
qed "vc_sound";
-goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)";
+goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
by (acom.induct_tac "c" 1);
by (ALLGOALS Asm_simp_tac);
by (EVERY1[rtac allI, rtac allI, rtac impI]);
by (EVERY1[etac allE, etac allE, etac mp]);
by (EVERY1[etac allE, etac allE, etac mp, atac]);
-qed_spec_mp "wp_mono";
+qed_spec_mp "awp_mono";
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
by (acom.induct_tac "c" 1);
by (ALLGOALS Asm_simp_tac);
by (safe_tac HOL_cs);
by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
-by (fast_tac (HOL_cs addEs [wp_mono]) 1);
+by (fast_tac (HOL_cs addEs [awp_mono]) 1);
qed_spec_mp "vc_mono";
goal VC.thy
"!!P c Q. |- {P}c{Q} ==> \
-\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))";
+\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
by (etac hoare.induct 1);
by (res_inst_tac [("x","Askip")] exI 1);
by (Simp_tac 1);
@@ -56,7 +56,7 @@
by (SELECT_GOAL(safe_tac HOL_cs)1);
by (res_inst_tac [("x","Asemi ac aca")] exI 1);
by (Asm_simp_tac 1);
- by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+ by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
by (SELECT_GOAL(safe_tac HOL_cs)1);
by (res_inst_tac [("x","Aif b ac aca")] exI 1);
by (Asm_simp_tac 1);
@@ -66,10 +66,10 @@
by (safe_tac HOL_cs);
by (res_inst_tac [("x","ac")] exI 1);
by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1);
+by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
qed "vc_complete";
-goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)";
+goal VC.thy "!Q. vcawp c Q = (vc c Q, awp c Q)";
by (acom.induct_tac "c" 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def])));
-qed "vcwp_vc_wp";
+qed "vcawp_vc_awp";