From 212ea6724acaadb0df1c3bd9da57bc6db4f6b80f Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
Date: Wed, 17 Apr 2019 00:08:55 +1000
Subject: [PATCH] lib: add obind_eqI_full to OptionMonad

Sometimes after showing equality of the heads of the obind, we need this
result in proof of equality of the tails.
---
 lib/Monad_WP/OptionMonad.thy | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy
index bee69c828..1d1eee899 100644
--- a/lib/Monad_WP/OptionMonad.thy
+++ b/lib/Monad_WP/OptionMonad.thy
@@ -223,6 +223,14 @@ 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)
 
+(* full form of obind_eqI; the second equality makes more sense flipped here, as we end up
+   with "f s = Some x ; f s' = f s" preventing "Some x = ..." *)
+lemma obind_eqI_full:
+  "\<lbrakk> f s = f s' ; \<And>x. \<lbrakk> f s = Some x; f s' = f s \<rbrakk> \<Longrightarrow> g x s = g' x s' \<rbrakk>
+   \<Longrightarrow> obind f g s = obind f g' s'"
+  by (drule sym[where s="f s"]) (* prevent looping *)
+     (clarsimp simp: 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"