# HG changeset patch
# User haftmann
# Date 1290096076 -3600
# Node ID efb0d78785386b0e0c89998609284eea8327e0d3
# Parent  6c28ab8b81665d44ccc8fb443d8e81282fba15a3
mapper for option type

diff -r 6c28ab8b8166 -r efb0d7878538 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Option.thy	Thu Nov 18 17:01:16 2010 +0100
@@ -81,6 +81,16 @@
     "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_mapper 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
+next
+  fix x
+  show "Option.map (\<lambda>x. x) x = x"
+    by (cases x) simp_all
+qed
+
 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"