|
1 theory QuotSum |
|
2 imports QuotMain |
|
3 begin |
|
4 |
|
5 fun |
|
6 sum_rel |
|
7 where |
|
8 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
|
9 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
|
10 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
|
11 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
|
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 |
|
19 declare [[map * = (sum_map, sum_rel)]] |
|
20 |
|
21 lemma sum_equivp[quot_equiv]: |
|
22 assumes a: "equivp R1" |
|
23 assumes b: "equivp R2" |
|
24 shows "equivp (sum_rel R1 R2)" |
|
25 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
|
26 apply(auto) |
|
27 apply(case_tac x) |
|
28 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
|
29 apply(case_tac x) |
|
30 apply(case_tac y) |
|
31 prefer 3 |
|
32 apply(case_tac y) |
|
33 apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b]) |
|
34 apply(case_tac x) |
|
35 apply(case_tac y) |
|
36 apply(case_tac z) |
|
37 prefer 3 |
|
38 apply(case_tac z) |
|
39 prefer 5 |
|
40 apply(case_tac y) |
|
41 apply(case_tac z) |
|
42 prefer 3 |
|
43 apply(case_tac z) |
|
44 apply(auto) |
|
45 apply(metis equivp_transp[OF b]) |
|
46 apply(metis equivp_transp[OF a]) |
|
47 done |
|
48 |
|
49 lemma sum_fun_fun: |
|
50 assumes q1: "Quotient R1 Abs1 Rep1" |
|
51 assumes q2: "Quotient R2 Abs2 Rep2" |
|
52 shows "sum_rel R1 R2 r s = |
|
53 (sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)" |
|
54 using q1 q2 |
|
55 apply(case_tac r) |
|
56 apply(case_tac s) |
|
57 apply(simp_all) |
|
58 prefer 2 |
|
59 apply(case_tac s) |
|
60 apply(auto) |
|
61 unfolding Quotient_def |
|
62 apply metis+ |
|
63 done |
|
64 |
|
65 lemma sum_quotient[quot_thm]: |
|
66 assumes q1: "Quotient R1 Abs1 Rep1" |
|
67 assumes q2: "Quotient R2 Abs2 Rep2" |
|
68 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
|
69 unfolding Quotient_def |
|
70 apply(rule conjI) |
|
71 apply(rule allI) |
|
72 apply(case_tac a) |
|
73 apply(simp add: Quotient_abs_rep[OF q1]) |
|
74 apply(simp add: Quotient_abs_rep[OF q2]) |
|
75 apply(rule conjI) |
|
76 apply(rule allI) |
|
77 apply(case_tac a) |
|
78 apply(simp add: Quotient_rel_rep[OF q1]) |
|
79 apply(simp add: Quotient_rel_rep[OF q2]) |
|
80 apply(rule allI)+ |
|
81 apply(rule sum_fun_fun[OF q1 q2]) |
|
82 done |
|
83 |
|
84 end |