From bd7a6113aeef5c64aeb9e916eafd17c7f5af34eb Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Sat, 17 Nov 2018 08:43:56 +1100
Subject: [PATCH] lib: more library lemmas for OptionMonad

---
 lib/Monad_WP/OptionMonad.thy   | 41 ++++++++++++++++++++++++++++++++++
 lib/Monad_WP/OptionMonadND.thy |  1 +
 2 files changed, 42 insertions(+)

diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy
index ed2fe2022..3802a2a34 100644
--- a/lib/Monad_WP/OptionMonad.thy
+++ b/lib/Monad_WP/OptionMonad.thy
@@ -28,6 +28,10 @@ definition
 where
   "f |> g \<equiv> \<lambda>s. case f s of None \<Rightarrow> None | Some x \<Rightarrow> g x"
 
+abbreviation opt_map_Some :: "('s \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 's \<rightharpoonup> 'b" (infixl "||>" 54) where
+  "f ||> g \<equiv> f |> (Some \<circ> g)"
+lemmas opt_map_Some_def = opt_map_def
+
 lemma opt_map_cong [fundef_cong]:
   "\<lbrakk> f = f'; \<And>v s. f s = Some v \<Longrightarrow> g v = g' v\<rbrakk> \<Longrightarrow> f |> g = f' |> g'"
   by (rule ext) (simp add: opt_map_def split: option.splits)
@@ -216,6 +220,43 @@ lemma oreturnOkE:
 lemmas omonadE [elim!] =
   opt_mapE obindE oreturnE ofailE othrowE oreturnOkE oassertE
 
+lemma in_opt_map_Some_eq:
+  "((f ||> g) x = Some y) = (\<exists>v. f x = Some v \<and> g v = y)"
+  by (simp add: in_opt_map_eq)
+
+lemma in_opt_map_None_eq[simp]:
+  "((f ||> g) x = None) = (f x = None)"
+  by (simp add: opt_map_def split: option.splits)
+
+lemma oreturn_comp[simp]:
+  "oreturn x \<circ> f = oreturn x"
+  by (simp add: oreturn_def K_def o_def)
+
+lemma ofail_comp[simp]:
+  "ofail \<circ> f = ofail"
+  by (auto simp: ofail_def K_def)
+
+lemma oassert_comp[simp]:
+  "oassert P \<circ> f = oassert P"
+  by (simp add: oassert_def)
+
+lemma fail_apply[simp]:
+  "ofail s = None"
+  by (simp add: ofail_def K_def)
+
+lemma oassert_apply[simp]:
+  "oassert P s = (if P then Some () else None)"
+  by (simp add: oassert_def)
+
+lemma oreturn_apply[simp]:
+  "oreturn x s = Some x"
+  by simp
+
+lemma oapply_apply[simp]:
+  "oapply x s = s x"
+  by (simp add: oapply_def)
+
+
 section \<open>"While" loops over option monad.\<close>
 
 text \<open>
diff --git a/lib/Monad_WP/OptionMonadND.thy b/lib/Monad_WP/OptionMonadND.thy
index 531c9a32a..2dc4b9a02 100644
--- a/lib/Monad_WP/OptionMonadND.thy
+++ b/lib/Monad_WP/OptionMonadND.thy
@@ -112,6 +112,7 @@ lemmas omonad_simps [simp] =
   gets_the_return gets_the_fail gets_the_returnOk
   gets_the_throwError gets_the_assert
 
+lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq Let_def
 
 
 section "Relation between option monad loops and non-deterministic monad loops."