|
1 theory QuotProd |
|
2 imports QuotScript |
|
3 begin |
|
4 |
|
5 fun |
|
6 prod_rel |
|
7 where |
|
8 "prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)" |
|
9 |
|
10 (* prod_fun is a good mapping function *) |
|
11 |
|
12 lemma prod_equivp: |
|
13 assumes a: "equivp R1" |
|
14 assumes b: "equivp R2" |
|
15 shows "equivp (prod_rel R1 R2)" |
|
16 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
|
17 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
|
18 apply(simp only: equivp_symp[OF a]) |
|
19 apply(simp only: equivp_symp[OF b]) |
|
20 using equivp_transp[OF a] apply blast |
|
21 using equivp_transp[OF b] apply blast |
|
22 done |
|
23 |
|
24 lemma prod_quotient: |
|
25 assumes q1: "Quotient R1 Abs1 Rep1" |
|
26 assumes q2: "Quotient R2 Abs2 Rep2" |
|
27 shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" |
|
28 unfolding Quotient_def |
|
29 apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2]) |
|
30 using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast |
|
31 |
|
32 lemma pair_rsp: |
|
33 assumes q1: "Quotient R1 Abs1 Rep1" |
|
34 assumes q2: "Quotient R2 Abs2 Rep2" |
|
35 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
|
36 by auto |
|
37 |
|
38 lemma pair_prs: |
|
39 assumes q1: "Quotient R1 Abs1 Rep1" |
|
40 assumes q2: "Quotient R2 Abs2 Rep2" |
|
41 shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)" |
|
42 by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
43 |
|
44 (* TODO: Is the quotient assumption q1 necessary? *) |
|
45 (* TODO: Aren't there hard to use later? *) |
|
46 lemma fst_rsp: |
|
47 assumes q1: "Quotient R1 Abs1 Rep1" |
|
48 assumes q2: "Quotient R2 Abs2 Rep2" |
|
49 assumes a: "(prod_rel R1 R2) p1 p2" |
|
50 shows "R1 (fst p1) (fst p2)" |
|
51 using a |
|
52 apply(case_tac p1) |
|
53 apply(case_tac p2) |
|
54 apply(auto) |
|
55 done |
|
56 |
|
57 lemma snd_rsp: |
|
58 assumes q1: "Quotient R1 Abs1 Rep1" |
|
59 assumes q2: "Quotient R2 Abs2 Rep2" |
|
60 assumes a: "(prod_rel R1 R2) p1 p2" |
|
61 shows "R2 (snd p1) (snd p2)" |
|
62 using a |
|
63 apply(case_tac p1) |
|
64 apply(case_tac p2) |
|
65 apply(auto) |
|
66 done |
|
67 |
|
68 lemma fst_prs: |
|
69 assumes q1: "Quotient R1 Abs1 Rep1" |
|
70 assumes q2: "Quotient R2 Abs2 Rep2" |
|
71 shows "Abs1 (fst ((prod_fun Rep1 Rep2) p)) = fst p" |
|
72 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q1]) |
|
73 |
|
74 lemma snd_prs: |
|
75 assumes q1: "Quotient R1 Abs1 Rep1" |
|
76 assumes q2: "Quotient R2 Abs2 Rep2" |
|
77 shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" |
|
78 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
|
79 |
|
80 end |