equal
deleted
inserted
replaced
14 option_map |
14 option_map |
15 where |
15 where |
16 "option_map f None = None" |
16 "option_map f None = None" |
17 | "option_map f (Some x) = Some (f x)" |
17 | "option_map f (Some x) = Some (f x)" |
18 |
18 |
19 declare [[map * = (option_map, option_rel)]] |
19 declare [[map option = (option_map, option_rel)]] |
|
20 |
20 |
21 |
21 lemma option_quotient[quot_thm]: |
22 lemma option_quotient[quot_thm]: |
22 assumes q: "Quotient R Abs Rep" |
23 assumes q: "Quotient R Abs Rep" |
23 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
24 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
24 apply (unfold Quotient_def) |
25 apply (unfold Quotient_def) |