12 |
12 |
13 lemma prod_equivp[quot_equiv]: |
13 lemma prod_equivp[quot_equiv]: |
14 assumes a: "equivp R1" |
14 assumes a: "equivp R1" |
15 assumes b: "equivp R2" |
15 assumes b: "equivp R2" |
16 shows "equivp (prod_rel R1 R2)" |
16 shows "equivp (prod_rel R1 R2)" |
17 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
17 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
18 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
18 apply (auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
19 apply(simp only: equivp_symp[OF a]) |
19 apply (simp only: equivp_symp[OF a]) |
20 apply(simp only: equivp_symp[OF b]) |
20 apply (simp only: equivp_symp[OF b]) |
21 using equivp_transp[OF a] apply blast |
21 using equivp_transp[OF a] apply blast |
22 using equivp_transp[OF b] apply blast |
22 using equivp_transp[OF b] apply blast |
23 done |
23 done |
24 |
24 |
25 lemma prod_quotient[quot_thm]: |
25 lemma prod_quotient[quot_thm]: |
26 assumes q1: "Quotient R1 Abs1 Rep1" |
26 assumes q1: "Quotient R1 Abs1 Rep1" |
27 assumes q2: "Quotient R2 Abs2 Rep2" |
27 assumes q2: "Quotient R2 Abs2 Rep2" |
28 shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" |
28 shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" |
29 unfolding Quotient_def |
29 unfolding Quotient_def |
30 using q1 q2 |
30 using q1 q2 |
31 apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep) |
31 apply (simp add: Quotient_abs_rep Quotient_rel_rep) |
32 using Quotient_rel[OF q1] Quotient_rel[OF q2] |
32 using Quotient_rel[OF q1] Quotient_rel[OF q2] |
33 by blast |
33 by blast |
34 |
34 |
35 lemma pair_rsp[quot_respect]: |
35 lemma pair_rsp[quot_respect]: |
36 assumes q1: "Quotient R1 Abs1 Rep1" |
36 assumes q1: "Quotient R1 Abs1 Rep1" |
37 assumes q2: "Quotient R2 Abs2 Rep2" |
37 assumes q2: "Quotient R2 Abs2 Rep2" |
38 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
38 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
39 by simp |
39 by simp |
40 |
40 |
41 lemma pair_prs[quot_preserve]: |
41 lemma pair_prs[quot_preserve]: |
42 assumes q1: "Quotient R1 Abs1 Rep1" |
42 assumes q1: "Quotient R1 Abs1 Rep1" |
43 assumes q2: "Quotient R2 Abs2 Rep2" |
43 assumes q2: "Quotient R2 Abs2 Rep2" |
44 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
44 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
45 apply(simp add: expand_fun_eq) |
45 apply (simp add: expand_fun_eq) |
46 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
46 apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
47 done |
47 done |
48 |
48 |
49 lemma fst_rsp[quot_respect]: |
49 lemma fst_rsp[quot_respect]: |
50 assumes "Quotient R1 Abs1 Rep1" |
50 assumes "Quotient R1 Abs1 Rep1" |
51 assumes "Quotient R2 Abs2 Rep2" |
51 assumes "Quotient R2 Abs2 Rep2" |
52 shows "(prod_rel R1 R2 ===> R1) fst fst" |
52 shows "(prod_rel R1 R2 ===> R1) fst fst" |
54 |
54 |
55 lemma fst_prs[quot_preserve]: |
55 lemma fst_prs[quot_preserve]: |
56 assumes q1: "Quotient R1 Abs1 Rep1" |
56 assumes q1: "Quotient R1 Abs1 Rep1" |
57 assumes q2: "Quotient R2 Abs2 Rep2" |
57 assumes q2: "Quotient R2 Abs2 Rep2" |
58 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
58 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
59 apply(simp add: expand_fun_eq) |
59 apply (simp add: expand_fun_eq) |
60 apply(simp add: Quotient_abs_rep[OF q1]) |
60 apply (simp add: Quotient_abs_rep[OF q1]) |
61 done |
61 done |
62 |
62 |
63 lemma snd_rsp[quot_respect]: |
63 lemma snd_rsp[quot_respect]: |
64 assumes "Quotient R1 Abs1 Rep1" |
64 assumes "Quotient R1 Abs1 Rep1" |
65 assumes "Quotient R2 Abs2 Rep2" |
65 assumes "Quotient R2 Abs2 Rep2" |
66 shows "(prod_rel R1 R2 ===> R2) snd snd" |
66 shows "(prod_rel R1 R2 ===> R2) snd snd" |
67 by simp |
67 by simp |
68 |
68 |
69 lemma snd_prs[quot_preserve]: |
69 lemma snd_prs[quot_preserve]: |
70 assumes q1: "Quotient R1 Abs1 Rep1" |
70 assumes q1: "Quotient R1 Abs1 Rep1" |
71 assumes q2: "Quotient R2 Abs2 Rep2" |
71 assumes q2: "Quotient R2 Abs2 Rep2" |
72 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
72 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
73 apply(simp add: expand_fun_eq) |
73 apply (simp add: expand_fun_eq) |
74 apply(simp add: Quotient_abs_rep[OF q2]) |
74 apply (simp add: Quotient_abs_rep[OF q2]) |
75 done |
75 done |
76 |
76 |
77 lemma prod_fun_id[id_simps]: |
77 lemma prod_fun_id[id_simps]: |
78 shows "prod_fun id id \<equiv> id" |
78 shows "prod_fun id id = id" |
79 by (rule eq_reflection) |
79 by (simp add: prod_fun_def) |
80 (simp add: prod_fun_def) |
|
81 |
80 |
82 lemma prod_rel_eq[id_simps]: |
81 lemma prod_rel_eq[id_simps]: |
83 shows "prod_rel (op =) (op =) \<equiv> (op =)" |
82 shows "(prod_rel (op =) (op =)) = (op =)" |
84 apply (rule eq_reflection) |
|
85 apply (rule ext)+ |
83 apply (rule ext)+ |
86 apply auto |
84 apply auto |
87 done |
85 done |
88 |
86 |
89 end |
87 end |