# HG changeset patch
# User lammich <lammich@in.tum.de>
# Date 1415118788 -3600
# Node ID de0a4a76d7aae69d01c4cdebcad76b848396a234
# Parent  4479722497859ff49caab5766e22b102103d7d36
Added Option.bind_split{,_asm,s}

diff -r 447972249785 -r de0a4a76d7aa src/HOL/Option.thy
--- a/src/HOL/Option.thy	Mon Nov 03 15:08:15 2014 +0100
+++ b/src/HOL/Option.thy	Tue Nov 04 17:33:08 2014 +0100
@@ -130,6 +130,17 @@
 lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
 by (cases x) auto
 
+lemma bind_split: "P (bind m f) 
+  \<longleftrightarrow> (m = None \<longrightarrow> P None) \<and> (\<forall>v. m=Some v \<longrightarrow> P (f v))"
+    by (cases m) auto
+
+lemma bind_split_asm: "P (bind m f) = (\<not>(
+    m=None \<and> \<not>P None 
+  \<or> (\<exists>x. m=Some x \<and> \<not>P (f x))))"
+  by (cases m) auto
+
+lemmas bind_splits = bind_split bind_split_asm
+
 definition these :: "'a option set \<Rightarrow> 'a set"
 where
   "these A = the ` {x \<in> A. x \<noteq> None}"