1 (* Title: Quotient_Option.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 theory Quotient_Option |
|
5 imports Quotient Quotient_Syntax |
|
6 begin |
|
7 |
|
8 section {* Quotient infrastructure for the option type. *} |
|
9 |
|
10 fun |
|
11 option_rel |
|
12 where |
|
13 "option_rel R None None = True" |
|
14 | "option_rel R (Some x) None = False" |
|
15 | "option_rel R None (Some x) = False" |
|
16 | "option_rel R (Some x) (Some y) = R x y" |
|
17 |
|
18 declare [[map option = (Option.map, option_rel)]] |
|
19 |
|
20 text {* should probably be in Option.thy *} |
|
21 lemma split_option_all: |
|
22 shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))" |
|
23 apply(auto) |
|
24 apply(case_tac x) |
|
25 apply(simp_all) |
|
26 done |
|
27 |
|
28 lemma option_quotient[quot_thm]: |
|
29 assumes q: "Quotient R Abs Rep" |
|
30 shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
|
31 unfolding Quotient_def |
|
32 apply(simp add: split_option_all) |
|
33 apply(simp add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
|
34 using q |
|
35 unfolding Quotient_def |
|
36 apply(blast) |
|
37 done |
|
38 |
|
39 lemma option_equivp[quot_equiv]: |
|
40 assumes a: "equivp R" |
|
41 shows "equivp (option_rel R)" |
|
42 apply(rule equivpI) |
|
43 unfolding reflp_def symp_def transp_def |
|
44 apply(simp_all add: split_option_all) |
|
45 apply(blast intro: equivp_reflp[OF a]) |
|
46 apply(blast intro: equivp_symp[OF a]) |
|
47 apply(blast intro: equivp_transp[OF a]) |
|
48 done |
|
49 |
|
50 lemma option_None_rsp[quot_respect]: |
|
51 assumes q: "Quotient R Abs Rep" |
|
52 shows "option_rel R None None" |
|
53 by simp |
|
54 |
|
55 lemma option_Some_rsp[quot_respect]: |
|
56 assumes q: "Quotient R Abs Rep" |
|
57 shows "(R ===> option_rel R) Some Some" |
|
58 by simp |
|
59 |
|
60 lemma option_None_prs[quot_preserve]: |
|
61 assumes q: "Quotient R Abs Rep" |
|
62 shows "Option.map Abs None = None" |
|
63 by simp |
|
64 |
|
65 lemma option_Some_prs[quot_preserve]: |
|
66 assumes q: "Quotient R Abs Rep" |
|
67 shows "(Rep ---> Option.map Abs) Some = Some" |
|
68 apply(simp add: expand_fun_eq) |
|
69 apply(simp add: Quotient_abs_rep[OF q]) |
|
70 done |
|
71 |
|
72 lemma option_map_id[id_simps]: |
|
73 shows "Option.map id = id" |
|
74 by (simp add: expand_fun_eq split_option_all) |
|
75 |
|
76 lemma option_rel_eq[id_simps]: |
|
77 shows "option_rel (op =) = (op =)" |
|
78 by (simp add: expand_fun_eq split_option_all) |
|
79 |
|
80 end |
|