From bfce624b2b6ca270edaa94359898e5d7b9567135 Mon Sep 17 00:00:00 2001
From: Thomas Sewell <Thomas.Sewell@data61.csiro.au>
Date: Mon, 16 Jul 2018 15:38:05 +1000
Subject: [PATCH] lib: adjust some congruence rules for strengthen.

Adjusting the strengthen congruence rules for conjunction
and disjunction makes other conjuncts available as assumptions
in strengthening a conjunction. This may be useful occasionally.
---
 lib/Monad_WP/Strengthen.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Monad_WP/Strengthen.thy b/lib/Monad_WP/Strengthen.thy
index 4db14da87..7143a5e8e 100644
--- a/lib/Monad_WP/Strengthen.thy
+++ b/lib/Monad_WP/Strengthen.thy
@@ -418,12 +418,12 @@ lemma strengthen_imp_ord[simp]:
   by (auto simp add: st_def)
 
 lemma strengthen_imp_conj [strg]:
-  "\<lbrakk> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; st F (op \<longrightarrow>) B B' \<rbrakk>
+  "\<lbrakk> A' \<Longrightarrow> st F (op \<longrightarrow>) B B'; B \<Longrightarrow> st F (op \<longrightarrow>) A A' \<rbrakk>
     \<Longrightarrow> st F (op \<longrightarrow>) (A \<and> B) (A' \<and> B')"
   by (cases F, auto)
 
 lemma strengthen_imp_disj [strg]:
-  "\<lbrakk> \<not> B \<Longrightarrow> st F (op \<longrightarrow>) A A'; st F (op \<longrightarrow>) B B' \<rbrakk>
+  "\<lbrakk> \<not> A' \<Longrightarrow> st F (op \<longrightarrow>) B B'; \<not> B \<Longrightarrow> st F (op \<longrightarrow>) A A' \<rbrakk>
     \<Longrightarrow> st F (op \<longrightarrow>) (A \<or> B) (A' \<or> B')"
   by (cases F, auto)