Added wp_while.
--- a/src/HOL/IMP/Hoare.ML Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/Hoare.ML Tue Mar 18 18:02:19 1997 +0100
@@ -23,53 +23,75 @@
by (Fast_tac 1);
qed "hoare_sound";
-goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
+goalw Hoare.thy [wp_def] "wp SKIP Q = Q";
by (Simp_tac 1);
-qed "swp_SKIP";
+qed "wp_SKIP";
-goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
by (Simp_tac 1);
-qed "swp_Ass";
+qed "wp_Ass";
-goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)";
+goalw Hoare.thy [wp_def] "wp (c;d) Q = wp c (wp d Q)";
by (Simp_tac 1);
by (rtac ext 1);
by (Fast_tac 1);
-qed "swp_Semi";
+qed "wp_Semi";
-goalw Hoare.thy [swp_def]
- "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \
-\ (~b s --> swp d Q s))";
+goalw Hoare.thy [wp_def]
+ "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & \
+\ (~b s --> wp d Q s))";
by (Simp_tac 1);
by (rtac ext 1);
by (Fast_tac 1);
-qed "swp_If";
+qed "wp_If";
-goalw Hoare.thy [swp_def]
- "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
+goalw Hoare.thy [wp_def]
+ "!!s. b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
by (stac C_While_If 1);
by (Asm_simp_tac 1);
-qed "swp_While_True";
+qed "wp_While_True";
-goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
+goalw Hoare.thy [wp_def] "!!s. ~b s ==> wp (WHILE b DO c) Q s = Q s";
by (stac C_While_If 1);
by (Asm_simp_tac 1);
-qed "swp_While_False";
+qed "wp_While_False";
-Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
+Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
(*Not suitable for rewriting: LOOPS!*)
-goal Hoare.thy "swp (WHILE b DO c) Q s = \
-\ (if b s then swp (c;WHILE b DO c) Q s else Q s)";
+goal Hoare.thy "wp (WHILE b DO c) Q s = \
+\ (if b s then wp (c;WHILE b DO c) Q s else Q s)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-qed "swp_While_if";
+qed "wp_While_if";
+goal thy
+ "wp (WHILE b DO c) Q s = \
+\ (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
+by(simp_tac (!simpset setloop(split_tac[expand_if])) 1);
+br iffI 1;
+ br weak_coinduct 1;
+ by(Best_tac 1);
+ by(safe_tac (!claset));
+ by(rotate_tac ~1 1);
+ by(Asm_full_simp_tac 1);
+ by(rotate_tac ~1 1);
+ by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (!simpset addsimps [wp_def,Gamma_def]) 1);
+by(strip_tac 1);
+br mp 1;
+ ba 2;
+be induct2 1;
+by(fast_tac (!claset addSIs [monoI]) 1);
+by(stac gfp_Tarski 1);
+ by(fast_tac (!claset addSIs [monoI]) 1);
+by(Fast_tac 1);
+qed "wp_While";
Delsimps [C_while];
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
-goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
+goal Hoare.thy "!Q. |- {wp c Q} c {Q}";
by (com.induct_tac "c" 1);
by (ALLGOALS Simp_tac);
by (REPEAT_FIRST Fast_tac);
@@ -90,11 +112,11 @@
by (Asm_full_simp_tac 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
-qed_spec_mp "swp_is_pre";
+qed_spec_mp "wp_is_pre";
goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
-by (rtac (swp_is_pre RSN (2,hoare.conseq)) 1);
+by (rtac (wp_is_pre RSN (2,hoare.conseq)) 1);
by (Fast_tac 2);
-by (rewrite_goals_tac [hoare_valid_def,swp_def]);
+by (rewrite_goals_tac [hoare_valid_def,wp_def]);
by (Fast_tac 1);
qed "hoare_relative_complete";
--- a/src/HOL/IMP/Hoare.thy Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/Hoare.thy Tue Mar 18 18:02:19 1997 +0100
@@ -6,7 +6,7 @@
Inductive definition of Hoare logic
*)
-Hoare = Denotation +
+Hoare = Denotation + Gfp +
types assn = state => bool
@@ -29,7 +29,7 @@
conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
|- {P'}c{Q'}"
-constdefs swp :: com => assn => assn
- "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
+constdefs wp :: com => assn => assn
+ "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
end
--- 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";
--- a/src/HOL/IMP/VC.thy Tue Mar 18 17:03:55 1997 +0100
+++ b/src/HOL/IMP/VC.thy Tue Mar 18 18:02:19 1997 +0100
@@ -5,7 +5,7 @@
acom: annotated commands
vc: verification-conditions
-wp: weakest (liberal) precondition
+awp: weakest (liberal) precondition
*)
VC = Hoare +
@@ -17,24 +17,24 @@
| Awhile bexp assn acom
consts
- vc,wp :: acom => assn => assn
- vcwp :: "acom => assn => assn * assn"
+ vc,awp :: acom => assn => assn
+ vcawp :: "acom => assn => assn * assn"
astrip :: acom => com
-primrec wp acom
- "wp Askip Q = Q"
- "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
- "wp (Asemi c d) Q = wp c (wp d Q)"
- "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))"
- "wp (Awhile b I c) Q = I"
+primrec awp acom
+ "awp Askip Q = Q"
+ "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
+ "awp (Asemi c d) Q = awp c (awp d Q)"
+ "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
+ "awp (Awhile b I c) Q = I"
primrec vc acom
"vc Askip Q = (%s.True)"
"vc (Aass x a) Q = (%s.True)"
- "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
+ "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
"vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"
"vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
- (I s & b s --> wp c I s) & vc c I s)"
+ (I s & b s --> awp c I s) & vc c I s)"
primrec astrip acom
"astrip Askip = SKIP"
@@ -43,19 +43,19 @@
"astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
"astrip (Awhile b I c) = (WHILE b DO astrip c)"
-(* simultaneous computation of vc and wp: *)
-primrec vcwp acom
- "vcwp Askip Q = (%s.True, Q)"
- "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
- "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 b c d) Q = (let (vcd,wpd) = vcwp d Q;
- (vcc,wpc) = vcwp c Q
- in (%s. vcc s & vcd s,
- %s.(b s-->wpc s) & (~b s-->wpd s)))"
- "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
- in (%s. (I s & ~b s --> Q s) &
- (I s & b s --> wpc s) & vcc s, I))"
+(* simultaneous computation of vc and awp: *)
+primrec vcawp acom
+ "vcawp Askip Q = (%s.True, Q)"
+ "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
+ "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
+ (vcc,wpc) = vcawp c wpd
+ in (%s. vcc s & vcd s, wpc))"
+ "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
+ (vcc,wpc) = vcawp c Q
+ in (%s. vcc s & vcd s,
+ %s.(b s --> wpc s) & (~b s --> wpd s)))"
+ "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
+ in (%s. (I s & ~b s --> Q s) &
+ (I s & b s --> wpc s) & vcc s, I))"
end