--- a/src/HOL/Hoare/Hoare.ML Sun Mar 26 20:38:23 2000 +0200
+++ b/src/HOL/Hoare/Hoare.ML Sun Mar 26 22:29:33 2000 +0200
@@ -16,14 +16,14 @@
by (Auto_tac);
qed "BasicRule";
-Goalw [Valid_def] "[| Valid P c1 Q; Valid Q c2 R |] ==> Valid P (c1;c2) R";
+Goalw [Valid_def] "Valid P c1 Q ==> Valid Q c2 R ==> Valid P (c1;c2) R";
by (Asm_simp_tac 1);
by (Blast_tac 1);
qed "SeqRule";
Goalw [Valid_def]
- "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
-\ Valid w c1 q; Valid w' c2 q |] \
+ "p <= {s. (s:b --> s:w) & (s~:b --> s:w')} \
+\ ==> Valid w c1 q ==> Valid w' c2 q \
\ ==> Valid p (Cond b c1 c2) q";
by (Asm_simp_tac 1);
by (Blast_tac 1);
@@ -38,14 +38,21 @@
val lemma = result() RS spec RS spec RS mp RS mp;
Goalw [Valid_def]
- "[| p <= i; Valid (i Int b) c i; i Int (-b) <= q |] \
-\ ==> Valid p (While b i c) q";
+ "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
+\ ==> Valid p (While b j c) q";
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (dtac lemma 1);
by (assume_tac 2);
by (Blast_tac 1);
by (Blast_tac 1);
+qed "WhileRule'";
+
+Goal
+ "p <= i ==> Valid (i Int b) c i ==> i Int (-b) <= q \
+\ ==> Valid p (While b i c) q";
+by (rtac WhileRule' 1);
+by (ALLGOALS assume_tac);
qed "WhileRule";
(*** The tactics ***)