|
1 (* Title: QuotOption.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
1 theory QuotOption |
4 theory QuotOption |
2 imports QuotMain |
5 imports QuotMain |
3 begin |
6 begin |
|
7 |
|
8 section {* Quotient infrastructure for option type *} |
4 |
9 |
5 fun |
10 fun |
6 option_rel |
11 option_rel |
7 where |
12 where |
8 "option_rel R None None = True" |
13 "option_rel R None None = True" |
9 | "option_rel R (Some x) None = False" |
14 | "option_rel R (Some x) None = False" |
10 | "option_rel R None (Some x) = False" |
15 | "option_rel R None (Some x) = False" |
11 | "option_rel R (Some x) (Some y) = R x y" |
16 | "option_rel R (Some x) (Some y) = R x y" |
12 |
17 |
13 fun |
18 declare [[map option = (Option.map, option_rel)]] |
14 option_map |
|
15 where |
|
16 "option_map f None = None" |
|
17 | "option_map f (Some x) = Some (f x)" |
|
18 |
|
19 declare [[map option = (option_map, option_rel)]] |
|
20 |
|
21 |
19 |
22 lemma option_quotient[quot_thm]: |
20 lemma option_quotient[quot_thm]: |
23 assumes q: "Quotient R Abs Rep" |
21 assumes q: "Quotient R Abs Rep" |
24 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
22 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
25 apply(unfold Quotient_def) |
23 unfolding Quotient_def |
26 apply(auto) |
24 apply(auto) |
27 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
25 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
28 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
26 apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
29 apply(case_tac [!] r) |
27 apply(case_tac [!] r) |
30 apply(case_tac [!] s) |
28 apply(case_tac [!] s) |
61 shows "(R ===> option_rel R) Some Some" |
59 shows "(R ===> option_rel R) Some Some" |
62 by simp |
60 by simp |
63 |
61 |
64 lemma option_None_prs[quot_preserve]: |
62 lemma option_None_prs[quot_preserve]: |
65 assumes q: "Quotient R Abs Rep" |
63 assumes q: "Quotient R Abs Rep" |
66 shows "option_map Abs None = None" |
64 shows "Option.map Abs None = None" |
67 by simp |
65 by simp |
68 |
66 |
69 lemma option_Some_prs[quot_respect]: |
67 lemma option_Some_prs[quot_respect]: |
70 assumes q: "Quotient R Abs Rep" |
68 assumes q: "Quotient R Abs Rep" |
71 shows "(Rep ---> option_map Abs) Some = Some" |
69 shows "(Rep ---> Option.map Abs) Some = Some" |
72 apply(simp add: expand_fun_eq) |
70 apply(simp add: expand_fun_eq) |
73 apply(simp add: Quotient_abs_rep[OF q]) |
71 apply(simp add: Quotient_abs_rep[OF q]) |
74 done |
72 done |
75 |
73 |
76 lemma option_map_id[id_simps]: |
74 lemma option_map_id[id_simps]: |
77 shows "option_map id \<equiv> id" |
75 shows "Option.map id \<equiv> id" |
78 apply (rule eq_reflection) |
76 apply (rule eq_reflection) |
79 apply (auto simp add: expand_fun_eq) |
77 apply (auto simp add: expand_fun_eq) |
80 apply (case_tac x) |
78 apply (case_tac x) |
81 apply (auto) |
79 apply (auto) |
82 done |
80 done |