From 66d87cd55034181681acda2cec72fbe65fc187e1 Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Date: Thu, 7 Mar 2019 17:07:25 +1100
Subject: [PATCH] lib: OptionMonad: add more obind decomposition, oassert simps

---
 lib/Monad_WP/OptionMonad.thy | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy
index 3802a2a34..f4b6d2143 100644
--- a/lib/Monad_WP/OptionMonad.thy
+++ b/lib/Monad_WP/OptionMonad.thy
@@ -188,6 +188,14 @@ lemma in_oassert_eq [simp]:
   "(oassert P s = Some v) = P"
   by (simp add: oassert_def)
 
+lemma oassert_True [simp]:
+  "oassert True = oreturn ()"
+  by (simp add: oassert_def)
+
+lemma oassert_False [simp]:
+  "oassert False = ofail"
+  by (simp add: oassert_def)
+
 lemma oassertE:
   "\<lbrakk> oassert P s = Some v; P \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
   by simp
@@ -196,6 +204,10 @@ lemma in_obind_eq:
   "((f |>> g) s = Some v) = (\<exists>v'. f s = Some v' \<and> g v' s = Some v)"
   by (simp add: obind_def split: option.splits)
 
+lemma obind_eqI:
+  "\<lbrakk> f s = f s' ; \<And>x. f s = Some x \<Longrightarrow> g x s = g' x s' \<rbrakk> \<Longrightarrow> obind f g s = obind f g' s'"
+  by (simp add: obind_def split: option.splits)
+
 lemma obindE:
   "\<lbrakk> (f |>> g) s = Some v;
      \<And>v'. \<lbrakk>f s = Some v'; g v' s = Some v\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"