--- a/src/HOL/IMP/Hoare_Sound_Complete.thy Wed Jun 12 20:52:09 2013 -0700
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy Thu Jun 13 14:35:05 2013 +0200
@@ -56,21 +56,7 @@
lemma wp_is_pre: "\<turnstile> {wp c Q} c {Q}"
proof(induction c arbitrary: Q)
- case Seq thus ?case by(auto intro: Seq)
-next
- case (If b c1 c2)
- let ?If = "IF b THEN c1 ELSE c2"
- show ?case
- proof(rule hoare.If)
- show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> bval b s} c1 {Q}"
- proof(rule strengthen_pre[OF _ If.IH(1)])
- show "\<forall>s. wp ?If Q s \<and> bval b s \<longrightarrow> wp c1 Q s" by auto
- qed
- show "\<turnstile> {\<lambda>s. wp ?If Q s \<and> \<not> bval b s} c2 {Q}"
- proof(rule strengthen_pre[OF _ If.IH(2)])
- show "\<forall>s. wp ?If Q s \<and> \<not> bval b s \<longrightarrow> wp c2 Q s" by auto
- qed
- qed
+ case If thus ?case by(auto intro: conseq)
next
case (While b c)
let ?w = "WHILE b DO c"
--- a/src/HOL/IMP/Hoare_Total.thy Wed Jun 12 20:52:09 2013 -0700
+++ b/src/HOL/IMP/Hoare_Total.thy Thu Jun 13 14:35:05 2013 +0200
@@ -162,13 +162,13 @@
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}"
proof (induction c arbitrary: Q)
- case SKIP show ?case by simp (blast intro:hoaret.Skip)
+ case SKIP show ?case by (auto intro:hoaret.Skip)
next
- case Assign show ?case by simp (blast intro:hoaret.Assign)
+ case Assign show ?case by (auto intro:hoaret.Assign)
next
- case Seq thus ?case by simp (blast intro:hoaret.Seq)
+ case Seq thus ?case by (auto intro:hoaret.Seq)
next
- case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq)
+ case If thus ?case by (auto intro:hoaret.If hoaret.conseq)
next
case (While b c)
let ?w = "WHILE b DO c"