From 08fe7d1a63213288536a4765aa7d2d2a46e9729a Mon Sep 17 00:00:00 2001
From: Michael McInerney <m.mcinerney@unsw.edu.au>
Date: Thu, 13 Jan 2022 20:09:21 +1100
Subject: [PATCH] lib: move map_set definition to OptionMonad.thy

Signed-off-by: Michael McInerney <m.mcinerney@unsw.edu.au>
---
 lib/Monad_WP/OptionMonad.thy | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy
index 0433658c3..0fa924114 100644
--- a/lib/Monad_WP/OptionMonad.thy
+++ b/lib/Monad_WP/OptionMonad.thy
@@ -142,6 +142,9 @@ declare None_upd_eq[simp]
 lemma "\<lbrakk> (f |> g) x = None; g v = None \<rbrakk> \<Longrightarrow> f(x \<mapsto> v) |> g = f |> g"
   by simp
 
+definition map_set :: "('a \<Rightarrow> 'b set option) \<Rightarrow> 'a \<Rightarrow> 'b set" where
+  "map_set f \<equiv> case_option {} id \<circ> f"
+
 (* opt_pred *)
 
 abbreviation