added congruence rules for Option.{map|bind}
authorkrauss
Sat Feb 18 09:46:58 2012 +0100 (2012-02-18)
changeset 46526c4cf9d03c352
parent 46512 4f9f61f9b535
child 46527 274bb026da6c
added congruence rules for Option.{map|bind}
src/HOL/FunDef.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/FunDef.thy	Fri Feb 17 15:42:26 2012 +0100
     1.2 +++ b/src/HOL/FunDef.thy	Sat Feb 18 09:46:58 2012 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4  
     1.5  lemmas [fundef_cong] =
     1.6    if_cong image_cong INT_cong UN_cong
     1.7 -  bex_cong ball_cong imp_cong
     1.8 +  bex_cong ball_cong imp_cong Option.map_cong Option.bind_cong
     1.9  
    1.10  lemma split_cong [fundef_cong]:
    1.11    "(\<And>x y. (x, y) = q \<Longrightarrow> f x y = g x y) \<Longrightarrow> p = q
     2.1 --- a/src/HOL/Option.thy	Fri Feb 17 15:42:26 2012 +0100
     2.2 +++ b/src/HOL/Option.thy	Sat Feb 18 09:46:58 2012 +0100
     2.3 @@ -81,6 +81,9 @@
     2.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
     2.5    by (rule ext) (simp split: sum.split)
     2.6  
     2.7 +lemma map_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> map f x = map g y"
     2.8 +by (cases x) auto
     2.9 +
    2.10  enriched_type map: Option.map proof -
    2.11    fix f g
    2.12    show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
    2.13 @@ -111,7 +114,11 @@
    2.14  lemma bind_rzero[simp]: "bind x (\<lambda>x. None) = None"
    2.15  by (cases x) auto
    2.16  
    2.17 +lemma bind_cong: "x = y \<Longrightarrow> (\<And>a. y = Some a \<Longrightarrow> f a = g a) \<Longrightarrow> bind x f = bind y g"
    2.18 +by (cases x) auto
    2.19 +
    2.20  hide_const (open) set map bind
    2.21 +hide_fact (open) map_cong bind_cong
    2.22  
    2.23  subsubsection {* Code generator setup *}
    2.24