--- a/src/HOL/FunDef.thy Fri Feb 17 15:42:26 2012 +0100
+++ b/src/HOL/FunDef.thy Sat Feb 18 09:46:58 2012 +0100
@@ -147,7 +147,7 @@
lemmas [fundef_cong] =
if_cong image_cong INT_cong UN_cong
- bex_cong ball_cong imp_cong
+ bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
lemma split_cong [fundef_cong]:
"(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
--- a/src/HOL/Option.thy Fri Feb 17 15:42:26 2012 +0100
+++ b/src/HOL/Option.thy Sat Feb 18 09:46:58 2012 +0100
@@ -81,6 +81,9 @@
"map f o sum_case g h = sum_case (map f o g) (map f o h)"
by (rule ext) (simp split: sum.split)
+lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
+by (cases x) auto
+
enriched_type map: Option.map proof -
fix f g
show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
@@ -111,7 +114,11 @@
lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
by (cases x) auto
+lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
+by (cases x) auto
+
hide_const (open) set map bind
+hide_fact (open) map_cong bind_cong
subsubsection {* Code generator setup *}