equal
deleted
inserted
replaced
79 |
79 |
80 lemma option_map_o_sum_case [simp]: |
80 lemma option_map_o_sum_case [simp]: |
81 "map f o sum_case g h = sum_case (map f o g) (map f o h)" |
81 "map f o sum_case g h = sum_case (map f o g) (map f o h)" |
82 by (rule ext) (simp split: sum.split) |
82 by (rule ext) (simp split: sum.split) |
83 |
83 |
84 type_mapper Option.map proof - |
84 type_lifting Option.map proof - |
85 fix f g x |
85 fix f g x |
86 show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x" |
86 show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x" |
87 by (cases x) simp_all |
87 by (cases x) simp_all |
88 next |
88 next |
89 fix x |
89 fix x |