src/HOL/Hoare/Hoare.ML

 
 Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
 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);
 qed "CondRule";
 

 by (Simp_tac 1);
 by (Blast_tac 1);
 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 ***)
 
 (*****************************************************************************)