--- a/src/HOL/Option.thy Tue Dec 21 16:14:46 2010 +0100
+++ b/src/HOL/Option.thy Tue Dec 21 17:52:23 2010 +0100
@@ -81,14 +81,21 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
-type_lifting Option.map proof -
- fix f g x
- show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
- by (cases x) simp_all
+type_lifting map: Option.map proof -
+ fix f g
+ show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
+ proof
+ fix x
+ show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
+ by (cases x) simp_all
+ qed
next
- fix x
- show "Option.map (\<lambda>x. x) x = x"
- by (cases x) simp_all
+ show "Option.map id = id"
+ proof
+ fix x
+ show "Option.map id x = id x"
+ by (cases x) simp_all
+ qed
qed
primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where