| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 26 Jan 2010 00:18:48 +0100 | |
| changeset 932 | 7781c7cbd27e |
| parent 925 | 8d51795ef54d |
| child 933 | 762f0eae88fd |
| permissions | -rw-r--r-- |
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
1 |
(* Title: QuotOption.thy |
|
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
|
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
3 |
*) |
| 698 | 4 |
theory QuotOption |
5 |
imports QuotMain |
|
6 |
begin |
|
7 |
||
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
8 |
section {* Quotient infrastructure for option type *}
|
|
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
9 |
|
| 698 | 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 |
||
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
18 |
declare [[map option = (Option.map, option_rel)]] |
| 698 | 19 |
|
20 |
lemma option_quotient[quot_thm]: |
|
21 |
assumes q: "Quotient R Abs Rep" |
|
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
22 |
shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)" |
|
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
23 |
unfolding Quotient_def |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
24 |
apply(auto) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
25 |
apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
26 |
apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q]) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
27 |
apply(case_tac [!] r) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
28 |
apply(case_tac [!] s) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
29 |
apply(simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q] ) |
| 698 | 30 |
using q |
31 |
unfolding Quotient_def |
|
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
32 |
apply(blast)+ |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
33 |
done |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
34 |
|
| 698 | 35 |
lemma option_equivp[quot_equiv]: |
36 |
assumes a: "equivp R" |
|
37 |
shows "equivp (option_rel R)" |
|
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
38 |
apply(rule equivpI) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
39 |
unfolding reflp_def symp_def transp_def |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
40 |
apply(auto) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
41 |
apply(case_tac [!] x) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
42 |
apply(simp_all add: equivp_reflp[OF a]) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
43 |
apply(case_tac [!] y) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
44 |
apply(simp_all add: equivp_symp[OF a]) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
45 |
apply(case_tac [!] z) |
| 698 | 46 |
apply(simp_all) |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
47 |
apply(clarify) |
| 698 | 48 |
apply(rule equivp_transp[OF a]) |
49 |
apply(assumption)+ |
|
50 |
done |
|
51 |
||
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
52 |
lemma option_None_rsp[quot_respect]: |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
53 |
assumes q: "Quotient R Abs Rep" |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
54 |
shows "option_rel R None None" |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
55 |
by simp |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
56 |
|
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
57 |
lemma option_Some_rsp[quot_respect]: |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
58 |
assumes q: "Quotient R Abs Rep" |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
59 |
shows "(R ===> option_rel R) Some Some" |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
60 |
by simp |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
61 |
|
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
62 |
lemma option_None_prs[quot_preserve]: |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
63 |
assumes q: "Quotient R Abs Rep" |
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
64 |
shows "Option.map Abs None = None" |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
65 |
by simp |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
66 |
|
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
67 |
lemma option_Some_prs[quot_respect]: |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
68 |
assumes q: "Quotient R Abs Rep" |
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
69 |
shows "(Rep ---> Option.map Abs) Some = Some" |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
70 |
apply(simp add: expand_fun_eq) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
71 |
apply(simp add: Quotient_abs_rep[OF q]) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
72 |
done |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
73 |
|
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
74 |
lemma option_map_id[id_simps]: |
|
932
7781c7cbd27e
used the internal Option.map instead of custom option_map
Christian Urban <urbanc@in.tum.de>
parents:
925
diff
changeset
|
75 |
shows "Option.map id \<equiv> id" |
|
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
|
76 |
apply (rule eq_reflection) |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
77 |
apply (auto simp add: expand_fun_eq) |
|
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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
|
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
82 |
lemma option_rel_eq[id_simps]: |
|
925
8d51795ef54d
ids *cannot* be object equalities
Christian Urban <urbanc@in.tum.de>
parents:
923
diff
changeset
|
83 |
shows "option_rel (op =) \<equiv> (op =)" |
|
923
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
84 |
apply(rule eq_reflection) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
85 |
apply(auto simp add: expand_fun_eq) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
86 |
apply(case_tac x) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
87 |
apply(case_tac [!] xa) |
|
0419b20ee83c
added prs and rsp lemmas for Some and None
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
88 |
apply(auto) |
|
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
|
89 |
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
|
90 |
|
|
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 |
end |