From e8465698038044a4cd0fca206326e94ca09a4c5d Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Fri, 15 Mar 2024 21:53:03 +1030
Subject: [PATCH] lib/monads: add reader_case_option_wp

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
---
 lib/Monads/reader_option/Reader_Option_VCG.thy | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
index d7f77bae3f..512b271222 100644
--- a/lib/Monads/reader_option/Reader_Option_VCG.thy
+++ b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -114,6 +114,11 @@ lemma ovalid_if_split:
   "\<lbrakk> P \<Longrightarrow> \<lblot>Q\<rblot> f \<lblot>S\<rblot>; \<not>P \<Longrightarrow> \<lblot>R\<rblot> g \<lblot>S\<rblot> \<rbrakk> \<Longrightarrow> \<lblot>\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not>P \<longrightarrow> R s)\<rblot> if P then f else g \<lblot>S\<rblot>"
   by simp
 
+lemma reader_case_option_wp[wp]:
+  "\<lbrakk>\<And>x. \<lblot>P x\<rblot> m x \<lblot>Q\<rblot>; \<lblot>P'\<rblot> m' \<lblot>Q\<rblot>\<rbrakk>
+   \<Longrightarrow> \<lblot>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (\<forall>y. x = Some y \<longrightarrow> P y s)\<rblot> case_option m' m x \<lblot>Q\<rblot>"
+  by (cases x; simp)
+
 lemma ovalid_case_prod[wp]:
   assumes "(\<And>x y. ovalid (P x y) (B x y) Q)"
   shows "ovalid (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q"