# HG changeset patch
# User krauss
# Date 1283715556 -7200
# Node ID aabd6d4a5c3abcfcbb6cc969281bf8c2b4959d34
# Parent  b6530978c14de4a36480c24e397eb583a43c0065
added Option.bind

diff -r b6530978c14d -r aabd6d4a5c3a src/HOL/Option.thy
--- 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 *}