# HG changeset patch
# User Gerwin Klein <gerwin.klein@nicta.com.au>
# Date 1345728742 -7200
# Node ID b2dea007e55eb5020abf5376d6ff60eba9ddf5ac
# Parent  4cd4ef1ef4a4a503dc554708ea8f8fe8f5667c28
remove Hoare dependency from Fold.thy

diff -r 4cd4ef1ef4a4 -r b2dea007e55e src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Aug 22 23:45:49 2012 +0200
+++ b/src/HOL/IMP/Fold.thy	Thu Aug 23 15:32:22 2012 +0200
@@ -12,14 +12,14 @@
 "simp_const (N n) _ = N n" |
 "simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
 "simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
-  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')" 
+  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
 
 definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
 
 theorem aval_simp_const[simp]:
 assumes "approx t s"
 shows "aval (simp_const a t) s = aval a s"
-  using assms 
+  using assms
   by (induct a) (auto simp: approx_def split: aexp.split option.split)
 
 theorem aval_simp_const_N:
@@ -45,7 +45,7 @@
   (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
 "defs (c1;c2) t = (defs c2 o defs c1) t" |
 "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
-"defs (WHILE b DO c) t = t |` (-lnames c)" 
+"defs (WHILE b DO c) t = t |` (-lnames c)"
 
 primrec fold where
 "fold SKIP _ = SKIP" |
@@ -71,10 +71,10 @@
   shows "merge t1 t2 |` S = t |` S"
 proof -
   from assms
-  have "\<forall>x. (t1 |` S) x = (t |` S) x" 
+  have "\<forall>x. (t1 |` S) x = (t |` S) x"
    and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
   thus ?thesis
-    by (auto simp: merge_def restrict_map_def 
+    by (auto simp: merge_def restrict_map_def
              split: if_splits intro: ext)
 qed
 
@@ -83,13 +83,13 @@
   "defs c t |` (- lnames c) = t |` (- lnames c)"
 proof (induction c arbitrary: t)
   case (Seq c1 c2)
-  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
+  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
     by simp
-  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
+  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
   from Seq
-  have "defs c2 (defs c1 t) |` (- lnames c2) = 
+  have "defs c2 (defs c1 t) |` (- lnames c2) =
         defs c1 t |` (- lnames c2)"
     by simp
   hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
@@ -100,12 +100,12 @@
 next
   case (If b c1 c2)
   hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
-  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
+  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
   from If
   have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
-  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) = 
+  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
          t |` (- lnames c2) |` (-lnames c1)" by simp
   ultimately
   show ?case by (auto simp: Int_commute intro: merge_restrict)
@@ -144,10 +144,6 @@
   thus ?case by (simp add: defs_restrict)
 qed
 
-corollary approx_defs_inv [simp]:
-  "\<Turnstile> {approx t} c {approx (defs c t)}"
-  by (simp add: hoare_valid_def big_step_pres_approx)
-
 
 lemma big_step_pres_approx_restrict:
   "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
@@ -156,7 +152,7 @@
   thus ?case by (clarsimp simp: approx_def)
 next
   case (Seq c1 s1 s2 c2 s3)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
     by (simp add: Int_commute)
   hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
     by (rule Seq)
@@ -167,25 +163,21 @@
   thus ?case by simp
 next
   case (IfTrue b s c1 s' c2)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" 
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
     by (simp add: Int_commute)
-  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'" 
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
     by (rule IfTrue)
-  thus ?case by (simp add: Int_commute) 
+  thus ?case by (simp add: Int_commute)
 next
   case (IfFalse b s c2 s' c1)
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s" 
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
     by simp
-  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'" 
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
     by (rule IfFalse)
   thus ?case by simp
 qed auto
 
 
-lemma approx_restrict_inv:
-  "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
-  by (simp add: hoare_valid_def big_step_pres_approx_restrict)
-
 declare assign_simp [simp]
 
 lemma approx_eq:
@@ -196,22 +188,22 @@
   case Assign
   show ?case by (simp add: equiv_up_to_def)
 next
-  case Seq 
-  thus ?case by (auto intro!: equiv_up_to_seq)
+  case Seq
+  thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx)
 next
   case If
   thus ?case by (auto intro!: equiv_up_to_if_weak)
 next
   case (While b c)
-  hence "approx (t |` (- lnames c)) \<Turnstile> 
+  hence "approx (t |` (- lnames c)) \<Turnstile>
          WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
-    by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
-  thus ?case 
+    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict)
+  thus ?case
     by (auto intro: equiv_up_to_weaken approx_map_le)
 qed
-  
+
 
-lemma approx_empty [simp]: 
+lemma approx_empty [simp]:
   "approx empty = (\<lambda>_. True)"
   by (auto intro!: ext simp: approx_def)
 
@@ -246,22 +238,22 @@
 lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))"
   by (cases b) auto
 
-lemma and_Bc_eq: 
+lemma and_Bc_eq:
   "(and a b = Bc v) =
-   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or> 
+   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or>
     (\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))"
   by (rule and.induct) auto
 
 lemma less_Bc_eq [simp]:
   "(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
   by (rule less.induct) auto
-    
+
 theorem bvalsimp_const_Bc:
 assumes "approx t s"
 shows "bsimp_const b t = Bc v \<Longrightarrow> bval b s = v"
   using assms
   by (induct b arbitrary: v)
-     (auto simp: approx_def and_Bc_eq aval_simp_const_N 
+     (auto simp: approx_def and_Bc_eq aval_simp_const_N
            split: bexp.splits bool.splits)
 
 
@@ -274,7 +266,7 @@
     Bc True \<Rightarrow> bdefs c1 t
   | Bc False \<Rightarrow> bdefs c2 t
   | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
-"bdefs (WHILE b DO c) t = t |` (-lnames c)" 
+"bdefs (WHILE b DO c) t = t |` (-lnames c)"
 
 
 primrec bfold where
@@ -294,13 +286,13 @@
   "bdefs c t |` (- lnames c) = t |` (- lnames c)"
 proof (induction c arbitrary: t)
   case (Seq c1 c2)
-  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
+  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
     by simp
-  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
+  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
   from Seq
-  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
+  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
         bdefs c1 t |` (- lnames c2)"
     by simp
   hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
@@ -311,22 +303,22 @@
 next
   case (If b c1 c2)
   hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
-  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
+  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
          t |` (- lnames c1) |` (-lnames c2)" by simp
   moreover
   from If
   have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
-  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) = 
+  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
          t |` (- lnames c2) |` (-lnames c1)" by simp
   ultimately
-  show ?case 
-    by (auto simp: Int_commute intro: merge_restrict 
+  show ?case
+    by (auto simp: Int_commute intro: merge_restrict
              split: bexp.splits bool.splits)
 qed (auto split: aexp.split bexp.split bool.split)
 
 
 lemma big_step_pres_approx_b:
-  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
+  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
 proof (induction arbitrary: t rule: big_step_induct)
   case Skip thus ?case by simp
 next
@@ -352,7 +344,7 @@
                  split: bexp.splits bool.splits)
 next
   case WhileFalse
-  thus ?case 
+  thus ?case
     by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def
                  split: bexp.splits bool.splits)
 next
@@ -361,15 +353,11 @@
   with WhileTrue
   have "approx (bdefs c t |` (- lnames c)) s3"
     by simp
-  thus ?case 
+  thus ?case
     by (simp add: bdefs_restrict)
 qed
 
-corollary approx_bdefs_inv [simp]:
-  "\<Turnstile> {approx t} c {approx (bdefs c t)}"
-  by (simp add: hoare_valid_def big_step_pres_approx_b)
-
-lemma bfold_equiv: 
+lemma bfold_equiv:
   "approx t \<Turnstile> c \<sim> bfold c t"
 proof (induction c arbitrary: t)
   case SKIP show ?case by simp
@@ -378,28 +366,28 @@
   thus ?case by (simp add: equiv_up_to_def)
 next
   case Seq
-  thus ?case by (auto intro!: equiv_up_to_seq)           
+  thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx_b)
 next
   case (If b c1 c2)
-  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
+  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
                    IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
-    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
+    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
   thus ?case using If
-    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits 
+    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits
                  intro: equiv_up_to_trans)
   next
   case (While b c)
-  hence "approx (t |` (- lnames c)) \<Turnstile> 
+  hence "approx (t |` (- lnames c)) \<Turnstile>
                    WHILE b DO c \<sim>
-                   WHILE bsimp_const b (t |` (- lnames c)) 
-                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'") 
-    by (auto intro: equiv_up_to_while_weak approx_restrict_inv 
+                   WHILE bsimp_const b (t |` (- lnames c))
+                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
+    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict
              simp: bequiv_up_to_def)
   hence "approx t \<Turnstile> ?W \<sim> ?W'"
     by (auto intro: equiv_up_to_weaken approx_map_le)
   thus ?case
-    by (auto split: bexp.splits bool.splits 
-             intro: equiv_up_to_while_False 
+    by (auto split: bexp.splits bool.splits
+             intro: equiv_up_to_while_False
              simp: bvalsimp_const_Bc)
 qed
 
diff -r 4cd4ef1ef4a4 -r b2dea007e55e src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 22 23:45:49 2012 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Aug 23 15:32:22 2012 +0200
@@ -1,17 +1,19 @@
 header "Semantic Equivalence up to a Condition"
 
 theory Sem_Equiv
-imports Hoare_Sound_Complete
+imports Big_Step
 begin
 
+type_synonym assn = "state \<Rightarrow> bool"
+
 definition
   equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
 where
   "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
 
-definition 
+definition
   bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
-where 
+where
   "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
 
 lemma equiv_up_to_True:
@@ -27,11 +29,11 @@
   by (unfold equiv_up_to_def) blast
 
 lemma equiv_up_toD1:
-  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s'"
   by (unfold equiv_up_to_def) blast
 
 lemma equiv_up_toD2:
-  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s'"
   by (unfold equiv_up_to_def) blast
 
 
@@ -60,32 +62,28 @@
   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
   by (auto simp: bequiv_up_to_def)
 
-
-lemma equiv_up_to_hoare:
-  "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
-  unfolding hoare_valid_def equiv_up_to_def by blast
-
-lemma equiv_up_to_hoare_eq:
-  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
-  by (rule equiv_up_to_hoare)
+lemma bequiv_up_to_subst:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P s \<Longrightarrow> bval b s = bval b' s"
+  by (simp add: bequiv_up_to_def)
 
 
 lemma equiv_up_to_seq:
-  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
+  (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
   P \<Turnstile> (c; d) \<sim> (c'; d')"
-  by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
+  by (clarsimp simp: equiv_up_to_def) blast
 
 lemma equiv_up_to_while_lemma:
-  shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 
+  shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
          P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
-         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
-         \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
-         P s \<Longrightarrow> 
-         d = WHILE b DO c \<Longrightarrow> 
-         (WHILE b' DO c', s) \<Rightarrow> s'"  
+         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
+         (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
+         P s \<Longrightarrow>
+         d = WHILE b DO c \<Longrightarrow>
+         (WHILE b' DO c', s) \<Rightarrow> s'"
 proof (induction rule: big_step_induct)
   case (WhileTrue b s1 c s2 s3)
-  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
+  hence IH: "P s2 \<Longrightarrow> (WHILE b' DO c', s2) \<Rightarrow> s3" by auto
   from WhileTrue.prems
   have "P \<Turnstile> b <\<sim>> b'" by simp
   with `bval b s1` `P s1`
@@ -97,38 +95,46 @@
   have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
   moreover
   from WhileTrue.prems
-  have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
+  have "\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'" by simp
   with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
-  have "P s2" by (simp add: hoare_valid_def)
+  have "P s2" by simp
   hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
-  ultimately 
+  ultimately
   show ?case by blast
 next
   case WhileFalse
   thus ?case by (auto simp: bequiv_up_to_def)
-qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
+qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+
 
 lemma bequiv_context_subst:
   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
   by (auto simp: bequiv_up_to_def)
 
 lemma equiv_up_to_while:
-  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
-   \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
-   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
-  apply (safe intro!: equiv_up_toI)
-   apply (auto intro: equiv_up_to_while_lemma)[1]
-  apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
-  apply (drule equiv_up_to_sym [THEN iffD1])
-  apply (drule bequiv_up_to_sym [THEN iffD1])
-  apply (auto intro: equiv_up_to_while_lemma)[1]
-  done
+  assumes b: "P \<Turnstile> b <\<sim>> b'"
+  assumes c: "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'"
+  assumes I: "\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'"
+  shows "P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+proof -
+  from b have b': "P \<Turnstile> b' <\<sim>> b" by (simp add: bequiv_up_to_sym)
+
+  from c b have c': "(\<lambda>s. P s \<and> bval b' s) \<Turnstile> c' \<sim> c"
+    by (simp add: equiv_up_to_sym bequiv_context_subst)
+
+  from I
+  have I': "\<And>s s'. (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b' s \<Longrightarrow> P s'"
+    by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])
+
+  note equiv_up_to_while_lemma [OF _ b c]
+       equiv_up_to_while_lemma [OF _ b' c']
+  thus ?thesis using I I' by (auto intro!: equiv_up_toI)
+qed
 
 lemma equiv_up_to_while_weak:
-  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow>
+   (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
    P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
-  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken 
-               simp: hoare_valid_def)
+  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)
 
 lemma equiv_up_to_if:
   "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
@@ -142,7 +148,7 @@
 
 lemma equiv_up_to_if_True [intro!]:
   "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
-  by (auto simp: equiv_up_to_def) 
+  by (auto simp: equiv_up_to_def)
 
 lemma equiv_up_to_if_False [intro!]:
   "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
@@ -154,7 +160,7 @@
 
 lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
  by (induct rule: big_step_induct) auto
-  
+
 lemma equiv_up_to_while_True [intro!,simp]:
   "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   unfolding equiv_up_to_def