equal
deleted
inserted
replaced
258 by simp |
258 by simp |
259 |
259 |
260 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)" |
260 lemma bind_map_option: "bind (map_option f x) g = bind x (g \<circ> f)" |
261 by(cases x) simp_all |
261 by(cases x) simp_all |
262 |
262 |
263 lemma set_bind_option [simp]: "set_option (bind x f) = UNION (set_option x) (set_option \<circ> f)" |
263 lemma set_bind_option [simp]: "set_option (bind x f) = (\<Union>((set_option \<circ> f) ` set_option x))" |
264 by(cases x) auto |
264 by(cases x) auto |
265 |
265 |
266 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)" |
266 lemma map_conv_bind_option: "map_option f x = Option.bind x (Some \<circ> f)" |
267 by(cases x) simp_all |
267 by(cases x) simp_all |
268 |
268 |