33 assumes q1: "Quotient R1 Abs1 Rep1" |
33 assumes q1: "Quotient R1 Abs1 Rep1" |
34 assumes q2: "Quotient R2 Abs2 Rep2" |
34 assumes q2: "Quotient R2 Abs2 Rep2" |
35 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
35 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
36 by auto |
36 by auto |
37 |
37 |
38 lemma pair_prs: |
38 lemma pair_prs_aux: |
39 assumes q1: "Quotient R1 Abs1 Rep1" |
39 assumes q1: "Quotient R1 Abs1 Rep1" |
40 assumes q2: "Quotient R2 Abs2 Rep2" |
40 assumes q2: "Quotient R2 Abs2 Rep2" |
41 shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)" |
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]) |
42 by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
43 |
|
44 term Pair |
|
45 |
|
46 lemma pair_prs[quot_preserve]: |
|
47 assumes q1: "Quotient R1 Abs1 Rep1" |
|
48 assumes q2: "Quotient R2 Abs2 Rep2" |
|
49 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
|
50 apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2]) |
|
51 apply(simp) |
|
52 done |
|
53 |
|
54 |
|
55 |
43 |
56 |
44 (* TODO: Is the quotient assumption q1 necessary? *) |
57 (* TODO: Is the quotient assumption q1 necessary? *) |
45 (* TODO: Aren't there hard to use later? *) |
58 (* TODO: Aren't there hard to use later? *) |
46 lemma fst_rsp: |
59 lemma fst_rsp: |
47 assumes q1: "Quotient R1 Abs1 Rep1" |
60 assumes q1: "Quotient R1 Abs1 Rep1" |
75 assumes q1: "Quotient R1 Abs1 Rep1" |
88 assumes q1: "Quotient R1 Abs1 Rep1" |
76 assumes q2: "Quotient R2 Abs2 Rep2" |
89 assumes q2: "Quotient R2 Abs2 Rep2" |
77 shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" |
90 shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" |
78 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
91 by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) |
79 |
92 |
|
93 |
|
94 section {* general setup for products *} |
|
95 |
|
96 declare [[map * = (prod_fun, prod_rel)]] |
|
97 |
|
98 lemmas [quot_thm] = prod_quotient |
|
99 lemmas [quot_respect] = pair_rsp |
|
100 lemmas [quot_equiv] = prod_equivp |
|
101 |
80 end |
102 end |