From 0e0e0cafa46716f7a01265dfb22c30184e9bbe4b Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Tue, 1 Aug 2023 16:16:51 +1000
Subject: [PATCH] lib/monads: add select_wp and alternative_wp to wp set for
 Nondet monad

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Monads/nondet/Nondet_VCG.thy | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/lib/Monads/nondet/Nondet_VCG.thy b/lib/Monads/nondet/Nondet_VCG.thy
index db77c40cc..6cf3fa976 100644
--- a/lib/Monads/nondet/Nondet_VCG.thy
+++ b/lib/Monads/nondet/Nondet_VCG.thy
@@ -554,7 +554,7 @@ lemma alternativeE_R_wp:
   unfolding validE_R_def
   by (rule alternativeE_wp)
 
-lemma alternative_R_wp:
+lemma alternativeE_E_wp:
   "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> g -, \<lbrace>Q\<rbrace>"
   unfolding validE_E_def
   by (rule alternativeE_wp)
@@ -1009,6 +1009,11 @@ lemmas [wp] = hoare_vcg_prop
               gets_the_wp
               gets_map_wp'
               liftE_wp
+              alternative_wp
+              alternativeE_R_wp
+              alternativeE_E_wp
+              alternativeE_wp
+              select_wp
               select_f_wp
               state_select_wp
               condition_wp