1128
|
1 |
(* Title: Quotient_Sum.thy
|
934
|
2 |
Author: Cezary Kaliszyk and Christian Urban
|
|
3 |
*)
|
1128
|
4 |
theory Quotient_Sum
|
1129
|
5 |
imports Quotient Quotient_Syntax
|
0
|
6 |
begin
|
|
7 |
|
937
|
8 |
section {* Quotient infrastructure for the sum type. *}
|
|
9 |
|
0
|
10 |
fun
|
545
|
11 |
sum_rel
|
0
|
12 |
where
|
545
|
13 |
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
|
|
14 |
| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
|
|
15 |
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
|
|
16 |
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
|
0
|
17 |
|
|
18 |
fun
|
|
19 |
sum_map
|
|
20 |
where
|
|
21 |
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
|
|
22 |
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
|
|
23 |
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
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>
diff
changeset
|
25 |
|
545
|
26 |
|
934
|
27 |
text {* should probably be in Sum_Type.thy *}
|
1128
|
28 |
lemma split_sum_all:
|
934
|
29 |
shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))"
|
937
|
30 |
apply(auto)
|
|
31 |
apply(case_tac x)
|
|
32 |
apply(simp_all)
|
|
33 |
done
|
934
|
34 |
|
698
|
35 |
lemma sum_equivp[quot_equiv]:
|
|
36 |
assumes a: "equivp R1"
|
|
37 |
assumes b: "equivp R2"
|
|
38 |
shows "equivp (sum_rel R1 R2)"
|
924
|
39 |
apply(rule equivpI)
|
|
40 |
unfolding reflp_def symp_def transp_def
|
934
|
41 |
apply(simp_all add: split_sum_all)
|
|
42 |
apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
|
|
43 |
apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
|
|
44 |
apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
|
924
|
45 |
done
|
0
|
46 |
|
698
|
47 |
lemma sum_quotient[quot_thm]:
|
|
48 |
assumes q1: "Quotient R1 Abs1 Rep1"
|
|
49 |
assumes q2: "Quotient R2 Abs2 Rep2"
|
|
50 |
shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
|
|
51 |
unfolding Quotient_def
|
934
|
52 |
apply(simp add: split_sum_all)
|
|
53 |
apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
|
|
54 |
apply(simp_all add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
|
924
|
55 |
using q1 q2
|
|
56 |
unfolding Quotient_def
|
|
57 |
apply(blast)+
|
698
|
58 |
done
|
|
59 |
|
934
|
60 |
lemma sum_Inl_rsp[quot_respect]:
|
|
61 |
assumes q1: "Quotient R1 Abs1 Rep1"
|
|
62 |
assumes q2: "Quotient R2 Abs2 Rep2"
|
|
63 |
shows "(R1 ===> sum_rel R1 R2) Inl Inl"
|
|
64 |
by simp
|
|
65 |
|
|
66 |
lemma sum_Inr_rsp[quot_respect]:
|
|
67 |
assumes q1: "Quotient R1 Abs1 Rep1"
|
|
68 |
assumes q2: "Quotient R2 Abs2 Rep2"
|
|
69 |
shows "(R2 ===> sum_rel R1 R2) Inr Inr"
|
|
70 |
by simp
|
|
71 |
|
1122
|
72 |
lemma sum_Inl_prs[quot_preserve]:
|
934
|
73 |
assumes q1: "Quotient R1 Abs1 Rep1"
|
|
74 |
assumes q2: "Quotient R2 Abs2 Rep2"
|
|
75 |
shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
|
|
76 |
apply(simp add: expand_fun_eq)
|
|
77 |
apply(simp add: Quotient_abs_rep[OF q1])
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
78 |
done
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
79 |
|
1122
|
80 |
lemma sum_Inr_prs[quot_preserve]:
|
934
|
81 |
assumes q1: "Quotient R1 Abs1 Rep1"
|
|
82 |
assumes q2: "Quotient R2 Abs2 Rep2"
|
|
83 |
shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
|
|
84 |
apply(simp add: expand_fun_eq)
|
|
85 |
apply(simp add: Quotient_abs_rep[OF q2])
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
86 |
done
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
87 |
|
1128
|
88 |
lemma sum_map_id[id_simps]:
|
936
|
89 |
shows "sum_map id id = id"
|
|
90 |
by (simp add: expand_fun_eq split_sum_all)
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
91 |
|
1128
|
92 |
lemma sum_rel_eq[id_simps]:
|
936
|
93 |
shows "sum_rel (op =) (op =) = (op =)"
|
|
94 |
by (simp add: expand_fun_eq split_sum_all)
|
829
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
95 |
|
42b90994ac77
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
96 |
end
|