| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 26 Jan 2010 00:18:48 +0100 | |
| changeset 932 | 7781c7cbd27e |
| parent 924 | 5455b19ef138 |
| child 929 | e812f58fd128 |
| child 934 | 0b15b83ded4a |
| permissions | -rw-r--r-- |
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
1 |
theory QuotSum |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
2 |
imports QuotMain |
| 0 | 3 |
begin |
4 |
||
5 |
fun |
|
|
545
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
6 |
sum_rel |
| 0 | 7 |
where |
|
545
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
8 |
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
|
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
9 |
| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
|
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
10 |
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
|
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
11 |
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
| 0 | 12 |
|
13 |
fun |
|
14 |
sum_map |
|
15 |
where |
|
16 |
"sum_map f1 f2 (Inl a) = Inl (f1 a)" |
|
17 |
| "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
|
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 "+" = (sum_map, sum_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 |
|
|
545
95371a8b17e1
Cleaning the Quotients file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
538
diff
changeset
|
21 |
|
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
22 |
lemma sum_equivp[quot_equiv]: |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
23 |
assumes a: "equivp R1" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
24 |
assumes b: "equivp R2" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
25 |
shows "equivp (sum_rel R1 R2)" |
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
26 |
apply(rule equivpI) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
27 |
unfolding reflp_def symp_def transp_def |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
28 |
apply(auto) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
29 |
apply(case_tac [!] x) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
30 |
apply(simp_all add: equivp_reflp[OF a] equivp_reflp[OF b]) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
31 |
apply(case_tac [!] y) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
32 |
apply(simp_all add: equivp_symp[OF a] equivp_symp[OF b]) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
33 |
apply(case_tac [!] z) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
34 |
apply(simp_all) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
35 |
apply(rule equivp_transp[OF a]) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
36 |
apply(assumption)+ |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
37 |
apply(rule equivp_transp[OF b]) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
38 |
apply(assumption)+ |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
39 |
done |
| 0 | 40 |
|
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
41 |
(* |
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
42 |
lemma sum_fun_fun: |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
43 |
assumes q1: "Quotient R1 Abs1 Rep1" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
44 |
assumes q2: "Quotient R2 Abs2 Rep2" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
45 |
shows "sum_rel R1 R2 r s = |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
46 |
(sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
47 |
using q1 q2 |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
48 |
apply(case_tac r) |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
49 |
apply(case_tac s) |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
50 |
apply(simp_all) |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
51 |
prefer 2 |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
52 |
apply(case_tac s) |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
53 |
apply(auto) |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
54 |
unfolding Quotient_def |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
55 |
apply metis+ |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
56 |
done |
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
57 |
*) |
| 0 | 58 |
|
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
59 |
lemma sum_quotient[quot_thm]: |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
60 |
assumes q1: "Quotient R1 Abs1 Rep1" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
61 |
assumes q2: "Quotient R2 Abs2 Rep2" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
62 |
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
63 |
unfolding Quotient_def |
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
64 |
apply(auto) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
65 |
apply(case_tac a) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
66 |
apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
67 |
Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
68 |
apply(case_tac a) |
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
69 |
apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
70 |
Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
71 |
apply(case_tac [!] r) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
72 |
apply(case_tac [!] s) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
73 |
apply(simp_all) |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
74 |
using q1 q2 |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
75 |
unfolding Quotient_def |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
76 |
apply(blast)+ |
|
698
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
77 |
done |
|
ed44eaaea63e
Option and Sum quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
613
diff
changeset
|
78 |
|
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
79 |
lemma sum_map_id[id_simps]: |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
80 |
shows "sum_map id 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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
|
|
924
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
87 |
lemma sum_rel_eq[id_simps]: |
|
5455b19ef138
re-inserted lemma in QuotList
Christian Urban <urbanc@in.tum.de>
parents:
829
diff
changeset
|
88 |
"sum_rel op = op = \<equiv> op =" |
|
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 |
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
|
90 |
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
|
91 |
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
|
92 |
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
|
93 |
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
|
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 |
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
|
98 |
|
|
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 |
end |