--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Thu Jun 06 12:20:04 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Thu Jun 06 15:49:01 2013 +0200
@@ -36,7 +36,7 @@
lemma wp_If[simp]:
"wp (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
- (\<lambda>s. (bval b s \<longrightarrow> wp c\<^isub>1 Q s) \<and> (\<not> bval b s \<longrightarrow> wp c\<^isub>2 Q s))"
+ (\<lambda>s. if bval b s then wp c\<^isub>1 Q s else wp c\<^isub>2 Q s)"
by (rule ext) (auto simp: wp_def)
lemma wp_While_If:
--- a/src/HOL/IMP/VCG.thy Thu Jun 06 12:20:04 2013 +0200
+++ b/src/HOL/IMP/VCG.thy Thu Jun 06 15:49:01 2013 +0200
@@ -31,8 +31,7 @@
"pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
"pre (c\<^isub>1;; c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
"pre (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q =
- (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
- (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
+ (\<lambda>s. if bval b s then pre c\<^isub>1 Q s else pre c\<^isub>2 Q s)" |
"pre ({I} WHILE b DO c) Q = I"
text{* Verification condition: *}