|
1 theory QuotOption |
|
2 imports QuotMain |
|
3 begin |
|
4 |
|
5 fun |
|
6 option_rel |
|
7 where |
|
8 "option_rel R None None = True" |
|
9 | "option_rel R (Some x) None = False" |
|
10 | "option_rel R None (Some x) = False" |
|
11 | "option_rel R (Some x) (Some y) = R x y" |
|
12 |
|
13 fun |
|
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_map, option_rel)]] |
|
20 |
|
21 lemma option_quotient[quot_thm]: |
|
22 assumes q: "Quotient R Abs Rep" |
|
23 shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
|
24 apply (unfold Quotient_def) |
|
25 apply (rule conjI) |
|
26 apply (rule allI) |
|
27 apply (case_tac a) |
|
28 apply (simp_all add: Quotient_abs_rep[OF q]) |
|
29 apply (rule conjI) |
|
30 apply (rule allI) |
|
31 apply (case_tac a) |
|
32 apply (simp_all add: Quotient_rel_rep[OF q]) |
|
33 apply (rule allI)+ |
|
34 apply (case_tac r) |
|
35 apply (case_tac s) |
|
36 apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
37 apply (case_tac s) |
|
38 apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
39 using q |
|
40 unfolding Quotient_def |
|
41 apply metis |
|
42 done |
|
43 |
|
44 lemma option_rel_some: |
|
45 assumes e: "equivp R" |
|
46 and a: "option_rel R (Some a) = option_rel R (Some aa)" |
|
47 shows "R a aa" |
|
48 using a apply(drule_tac x="Some aa" in fun_cong) |
|
49 apply(simp add: equivp_reflp[OF e]) |
|
50 done |
|
51 |
|
52 lemma option_equivp[quot_equiv]: |
|
53 assumes a: "equivp R" |
|
54 shows "equivp (option_rel R)" |
|
55 unfolding equivp_def |
|
56 apply(rule allI)+ |
|
57 apply(case_tac x) |
|
58 apply(case_tac y) |
|
59 apply(simp_all) |
|
60 apply(unfold not_def) |
|
61 apply(rule impI) |
|
62 apply(drule_tac x="None" in fun_cong) |
|
63 apply simp |
|
64 apply(case_tac y) |
|
65 apply(simp_all) |
|
66 apply(unfold not_def) |
|
67 apply(rule impI) |
|
68 apply(drule_tac x="None" in fun_cong) |
|
69 apply simp |
|
70 apply(rule iffI) |
|
71 apply(rule ext) |
|
72 apply(case_tac xa) |
|
73 apply(auto) |
|
74 apply(rule equivp_transp[OF a]) |
|
75 apply(rule equivp_symp[OF a]) |
|
76 apply(assumption)+ |
|
77 apply(rule equivp_transp[OF a]) |
|
78 apply(assumption)+ |
|
79 apply(simp only: option_rel_some[OF a]) |
|
80 done |
|
81 |
|
82 end |