| author | Christian Urban <urbanc@in.tum.de> |
| Thu, 14 Jan 2010 12:23:59 +0100 | |
| changeset 874 | ab8a58973861 |
| parent 829 | 42b90994ac77 |
| child 923 | 0419b20ee83c |
| permissions | -rw-r--r-- |
| 698 | 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 |
||
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
698
diff
changeset
|
19 |
declare [[map option = (option_map, option_rel)]] |
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
698
diff
changeset
|
20 |
|
| 698 | 21 |
|
22 |
lemma option_quotient[quot_thm]: |
|
23 |
assumes q: "Quotient R Abs Rep" |
|
24 |
shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" |
|
25 |
apply (unfold Quotient_def) |
|
26 |
apply (rule conjI) |
|
27 |
apply (rule allI) |
|
28 |
apply (case_tac a) |
|
29 |
apply (simp_all add: Quotient_abs_rep[OF q]) |
|
30 |
apply (rule conjI) |
|
31 |
apply (rule allI) |
|
32 |
apply (case_tac a) |
|
33 |
apply (simp_all add: Quotient_rel_rep[OF q]) |
|
34 |
apply (rule allI)+ |
|
35 |
apply (case_tac r) |
|
36 |
apply (case_tac s) |
|
37 |
apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
38 |
apply (case_tac s) |
|
39 |
apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q]) |
|
40 |
using q |
|
41 |
unfolding Quotient_def |
|
42 |
apply metis |
|
43 |
done |
|
44 |
||
45 |
lemma option_rel_some: |
|
46 |
assumes e: "equivp R" |
|
47 |
and a: "option_rel R (Some a) = option_rel R (Some aa)" |
|
48 |
shows "R a aa" |
|
49 |
using a apply(drule_tac x="Some aa" in fun_cong) |
|
50 |
apply(simp add: equivp_reflp[OF e]) |
|
51 |
done |
|
52 |
||
53 |
lemma option_equivp[quot_equiv]: |
|
54 |
assumes a: "equivp R" |
|
55 |
shows "equivp (option_rel R)" |
|
56 |
unfolding equivp_def |
|
57 |
apply(rule allI)+ |
|
58 |
apply(case_tac x) |
|
59 |
apply(case_tac y) |
|
60 |
apply(simp_all) |
|
61 |
apply(unfold not_def) |
|
62 |
apply(rule impI) |
|
63 |
apply(drule_tac x="None" in fun_cong) |
|
64 |
apply simp |
|
65 |
apply(case_tac y) |
|
66 |
apply(simp_all) |
|
67 |
apply(unfold not_def) |
|
68 |
apply(rule impI) |
|
69 |
apply(drule_tac x="None" in fun_cong) |
|
70 |
apply simp |
|
71 |
apply(rule iffI) |
|
72 |
apply(rule ext) |
|
73 |
apply(case_tac xa) |
|
74 |
apply(auto) |
|
75 |
apply(rule equivp_transp[OF a]) |
|
76 |
apply(rule equivp_symp[OF a]) |
|
77 |
apply(assumption)+ |
|
78 |
apply(rule equivp_transp[OF a]) |
|
79 |
apply(assumption)+ |
|
80 |
apply(simp only: option_rel_some[OF a]) |
|
81 |
done |
|
82 |
||
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
83 |
lemma option_map_id[id_simps]: "option_map id \<equiv> id" |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
84 |
apply (rule eq_reflection) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
85 |
apply (rule ext) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
86 |
apply (case_tac x) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
87 |
apply (auto) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
88 |
done |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
89 |
|
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
90 |
lemma option_rel_eq[id_simps]: "option_rel op = \<equiv> op =" |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
91 |
apply (rule eq_reflection) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
92 |
apply (rule ext)+ |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
93 |
apply (case_tac x) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
94 |
apply auto |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
95 |
apply (case_tac xa) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
96 |
apply auto |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
97 |
apply (case_tac xa) |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
98 |
apply auto |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
99 |
done |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
100 |
|
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
779
diff
changeset
|
101 |
end |