From adc7499aea798e4c2ce1466dc78e3db059fecd27 Mon Sep 17 00:00:00 2001
From: Michael McInerney <michael.mcinerney@proofcraft.systems>
Date: Thu, 9 Mar 2023 20:33:39 +1030
Subject: [PATCH] lib: add ifME_liftE

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

diff --git a/lib/Monads/More_NonDetMonadVCG.thy b/lib/Monads/More_NonDetMonadVCG.thy
index 6e310e2c1..ea9c9caf6 100644
--- a/lib/Monads/More_NonDetMonadVCG.thy
+++ b/lib/Monads/More_NonDetMonadVCG.thy
@@ -370,6 +370,10 @@ lemma ifM_throwError_returnOk:
                       validE_def bind_def
                split: if_splits)
 
+lemma ifME_liftE:
+  "ifME (liftE test) a b = ifM test a b"
+  by (simp add: ifME_def ifM_def liftE_bindE)
+
 lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp
 
 lemma select_f_inv: