src/HOL/Option.thy
changeset 41372 551eb49a6e91
parent 40968 a6fcd305f7dc
child 41505 6d19301074cf
     1.1 --- a/src/HOL/Option.thy	Tue Dec 21 16:14:46 2010 +0100
     1.2 +++ b/src/HOL/Option.thy	Tue Dec 21 17:52:23 2010 +0100
     1.3 @@ -81,14 +81,21 @@
     1.4      "map f o sum_case g h = sum_case (map f o g) (map f o h)"
     1.5    by (rule ext) (simp split: sum.split)
     1.6  
     1.7 -type_lifting Option.map proof -
     1.8 -  fix f g x
     1.9 -  show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x"
    1.10 -    by (cases x) simp_all
    1.11 +type_lifting map: Option.map proof -
    1.12 +  fix f g
    1.13 +  show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)"
    1.14 +  proof
    1.15 +    fix x
    1.16 +    show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x"
    1.17 +      by (cases x) simp_all
    1.18 +  qed
    1.19  next
    1.20 -  fix x
    1.21 -  show "Option.map (\<lambda>x. x) x = x"
    1.22 -    by (cases x) simp_all
    1.23 +  show "Option.map id = id"
    1.24 +  proof
    1.25 +    fix x
    1.26 +    show "Option.map id x = id x"
    1.27 +      by (cases x) simp_all
    1.28 +  qed
    1.29  qed
    1.30  
    1.31  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where