# HG changeset patch
# User nipkow
# Date 1371126905 -7200
# Node ID a231e6f897379256266fddbb6c1b37ee14116cea
# Parent  02dfb6bb487a49973ec2662b865fbc9944f5937c
simplified proofs

diff -r 02dfb6bb487a -r a231e6f89737 src/HOL/IMP/Hoare_Sound_Complete.thy
--- 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"
diff -r 02dfb6bb487a -r a231e6f89737 src/HOL/IMP/Hoare_Total.thy
--- 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"