src/HOL/Option.thy
changeset 39149 aabd6d4a5c3a
parent 38857 97775f3e8722
child 39150 c4ff5fd8db99
     1.1 --- a/src/HOL/Option.thy	Sat Sep 04 21:14:40 2010 +0200
     1.2 +++ b/src/HOL/Option.thy	Sun Sep 05 21:39:16 2010 +0200
     1.3 @@ -81,8 +81,20 @@
     1.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
     1.5    by (rule ext) (simp split: sum.split)
     1.6  
     1.7 +primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
     1.8 +bind_lzero: "bind None f = None" |
     1.9 +bind_lunit: "bind (Some x) f = f x"
    1.10  
    1.11 -hide_const (open) set map
    1.12 +lemma bind_runit[simp]: "bind x Some = x"
    1.13 +by (cases x) auto
    1.14 +
    1.15 +lemma bind_assoc[simp]: "bind (bind x f) g = bind x (\<lambda>y. bind (f y) g)"
    1.16 +by (cases x) auto
    1.17 +
    1.18 +lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
    1.19 +by (cases x) auto
    1.20 +
    1.21 +hide_const (open) set map bind
    1.22  
    1.23  subsubsection {* Code generator setup *}
    1.24