21 |
21 |
22 lemma sum_equivp[quot_equiv]: |
22 lemma sum_equivp[quot_equiv]: |
23 assumes a: "equivp R1" |
23 assumes a: "equivp R1" |
24 assumes b: "equivp R2" |
24 assumes b: "equivp R2" |
25 shows "equivp (sum_rel R1 R2)" |
25 shows "equivp (sum_rel R1 R2)" |
26 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
26 apply(rule equivpI) |
27 apply(auto) |
27 unfolding reflp_def symp_def transp_def |
28 apply(case_tac x) |
28 apply(auto) |
29 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
29 apply(case_tac [!] x) |
30 apply(case_tac x) |
30 apply(simp_all add: equivp_reflp[OF a] equivp_reflp[OF b]) |
31 apply(case_tac y) |
31 apply(case_tac [!] y) |
32 prefer 3 |
32 apply(simp_all add: equivp_symp[OF a] equivp_symp[OF b]) |
33 apply(case_tac y) |
33 apply(case_tac [!] z) |
34 apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b]) |
34 apply(simp_all) |
35 apply(case_tac x) |
35 apply(rule equivp_transp[OF a]) |
36 apply(case_tac y) |
36 apply(assumption)+ |
37 apply(case_tac z) |
37 apply(rule equivp_transp[OF b]) |
38 prefer 3 |
38 apply(assumption)+ |
39 apply(case_tac z) |
39 done |
40 prefer 5 |
|
41 apply(case_tac y) |
|
42 apply(case_tac z) |
|
43 prefer 3 |
|
44 apply(case_tac z) |
|
45 apply(auto) |
|
46 apply(metis equivp_transp[OF b]) |
|
47 apply(metis equivp_transp[OF a]) |
|
48 done |
|
49 |
40 |
|
41 (* |
50 lemma sum_fun_fun: |
42 lemma sum_fun_fun: |
51 assumes q1: "Quotient R1 Abs1 Rep1" |
43 assumes q1: "Quotient R1 Abs1 Rep1" |
52 assumes q2: "Quotient R2 Abs2 Rep2" |
44 assumes q2: "Quotient R2 Abs2 Rep2" |
53 shows "sum_rel R1 R2 r s = |
45 shows "sum_rel R1 R2 r s = |
54 (sum_rel R1 R2 r r \<and> sum_rel R1 R2 s s \<and> sum_map Abs1 Abs2 r = sum_map Abs1 Abs2 s)" |
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)" |
60 apply(case_tac s) |
52 apply(case_tac s) |
61 apply(auto) |
53 apply(auto) |
62 unfolding Quotient_def |
54 unfolding Quotient_def |
63 apply metis+ |
55 apply metis+ |
64 done |
56 done |
|
57 *) |
65 |
58 |
66 lemma sum_quotient[quot_thm]: |
59 lemma sum_quotient[quot_thm]: |
67 assumes q1: "Quotient R1 Abs1 Rep1" |
60 assumes q1: "Quotient R1 Abs1 Rep1" |
68 assumes q2: "Quotient R2 Abs2 Rep2" |
61 assumes q2: "Quotient R2 Abs2 Rep2" |
69 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
62 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
70 unfolding Quotient_def |
63 unfolding Quotient_def |
71 apply(rule conjI) |
64 apply(auto) |
72 apply(rule allI) |
|
73 apply(case_tac a) |
65 apply(case_tac a) |
74 apply(simp add: Quotient_abs_rep[OF q1]) |
66 apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
75 apply(simp add: Quotient_abs_rep[OF q2]) |
67 Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
76 apply(rule conjI) |
|
77 apply(rule allI) |
|
78 apply(case_tac a) |
68 apply(case_tac a) |
79 apply(simp add: Quotient_rel_rep[OF q1]) |
69 apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1] |
80 apply(simp add: Quotient_rel_rep[OF q2]) |
70 Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
81 apply(rule allI)+ |
71 apply(case_tac [!] r) |
82 apply(rule sum_fun_fun[OF q1 q2]) |
72 apply(case_tac [!] s) |
|
73 apply(simp_all) |
|
74 using q1 q2 |
|
75 unfolding Quotient_def |
|
76 apply(blast)+ |
83 done |
77 done |
84 |
78 |
85 lemma sum_map_id[id_simps]: "sum_map id id \<equiv> id" |
79 lemma sum_map_id[id_simps]: |
|
80 shows "sum_map id id \<equiv> id" |
86 apply (rule eq_reflection) |
81 apply (rule eq_reflection) |
87 apply (rule ext) |
82 apply (rule ext) |
88 apply (case_tac x) |
83 apply (case_tac x) |
89 apply (auto) |
84 apply (auto) |
90 done |
85 done |
91 |
86 |
92 lemma sum_rel_eq[id_simps]: "sum_rel op = op = \<equiv> op =" |
87 lemma sum_rel_eq[id_simps]: |
|
88 "sum_rel op = op = \<equiv> op =" |
93 apply (rule eq_reflection) |
89 apply (rule eq_reflection) |
94 apply (rule ext)+ |
90 apply (rule ext)+ |
95 apply (case_tac x) |
91 apply (case_tac x) |
96 apply auto |
92 apply auto |
97 apply (case_tac xa) |
93 apply (case_tac xa) |