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_lifting Option.map proof - |
84 type_lifting map: Option.map proof - |
85 fix f g x |
85 fix f g |
86 show "Option.map f (Option.map g x) = Option.map (\<lambda>x. f (g x)) x" |
86 show "Option.map f \<circ> Option.map g = Option.map (f \<circ> g)" |
87 by (cases x) simp_all |
87 proof |
|
88 fix x |
|
89 show "(Option.map f \<circ> Option.map g) x= Option.map (f \<circ> g) x" |
|
90 by (cases x) simp_all |
|
91 qed |
88 next |
92 next |
89 fix x |
93 show "Option.map id = id" |
90 show "Option.map (\<lambda>x. x) x = x" |
94 proof |
91 by (cases x) simp_all |
95 fix x |
|
96 show "Option.map id x = id x" |
|
97 by (cases x) simp_all |
|
98 qed |
92 qed |
99 qed |
93 |
100 |
94 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where |
101 primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where |
95 bind_lzero: "bind None f = None" | |
102 bind_lzero: "bind None f = None" | |
96 bind_lunit: "bind (Some x) f = f x" |
103 bind_lunit: "bind (Some x) f = f x" |