# HG changeset patch
# User krauss
# Date 1329554818 -3600
# Node ID c4cf9d03c352eb5073a42b6ce9265b5ad8e554af
# Parent  4f9f61f9b535ab670149d244b68bc608fa22ec72
added congruence rules for Option.{map|bind}

diff -r 4f9f61f9b535 -r c4cf9d03c352 src/HOL/FunDef.thy
--- 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
diff -r 4f9f61f9b535 -r c4cf9d03c352 src/HOL/Option.thy
--- 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 *}