--- a/src/HOL/Option.thy Sat Sep 04 21:14:40 2010 +0200
+++ b/src/HOL/Option.thy Sun Sep 05 21:39:16 2010 +0200
@@ -81,8 +81,20 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
+primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
+bind_lzero: "bind None f = None" |
+bind_lunit: "bind (Some x) f = f x"
-hide_const (open) set map
+lemma bind_runit[simp]: "bind x Some = x"
+by (cases x) auto
+
+lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
+by (cases x) auto
+
+lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
+by (cases x) auto
+
+hide_const (open) set map bind
subsubsection {* Code generator setup *}