|
1 (* Title: QuotProd.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
1 theory QuotProd |
4 theory QuotProd |
2 imports QuotMain |
5 imports QuotMain |
3 begin |
6 begin |
4 |
7 |
|
8 section {* Quotient infrastructure for product type *} |
|
9 |
5 fun |
10 fun |
6 prod_rel |
11 prod_rel |
7 where |
12 where |
8 "prod_rel R1 R2 = (\<lambda>(a,b) (c,d). R1 a c \<and> R2 b d)" |
13 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
9 |
14 |
10 declare [[map * = (prod_fun, prod_rel)]] |
15 declare [[map * = (prod_fun, prod_rel)]] |
11 |
16 |
12 |
17 |
13 lemma prod_equivp[quot_equiv]: |
18 lemma prod_equivp[quot_equiv]: |
14 assumes a: "equivp R1" |
19 assumes a: "equivp R1" |
15 assumes b: "equivp R2" |
20 assumes b: "equivp R2" |
16 shows "equivp (prod_rel R1 R2)" |
21 shows "equivp (prod_rel R1 R2)" |
17 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
22 apply(rule equivpI) |
18 apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) |
23 unfolding reflp_def symp_def transp_def |
19 apply(simp only: equivp_symp[OF a]) |
24 apply(simp_all add: split_paired_all) |
20 apply(simp only: equivp_symp[OF b]) |
25 apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b]) |
21 using equivp_transp[OF a] apply blast |
26 apply(blast intro: equivp_symp[OF a] equivp_symp[OF b]) |
22 using equivp_transp[OF b] apply blast |
27 apply(blast intro: equivp_transp[OF a] equivp_transp[OF b]) |
23 done |
28 done |
24 |
29 |
25 lemma prod_quotient[quot_thm]: |
30 lemma prod_quotient[quot_thm]: |
26 assumes q1: "Quotient R1 Abs1 Rep1" |
31 assumes q1: "Quotient R1 Abs1 Rep1" |
27 assumes q2: "Quotient R2 Abs2 Rep2" |
32 assumes q2: "Quotient R2 Abs2 Rep2" |
28 shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" |
33 shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" |
29 unfolding Quotient_def |
34 unfolding Quotient_def |
30 using q1 q2 |
35 apply(simp add: split_paired_all) |
31 apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep) |
36 apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]) |
32 using Quotient_rel[OF q1] Quotient_rel[OF q2] |
37 apply(simp add: Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2]) |
33 by blast |
38 using q1 q2 |
|
39 unfolding Quotient_def |
|
40 apply(blast) |
|
41 done |
34 |
42 |
35 lemma pair_rsp[quot_respect]: |
43 lemma Pair_rsp[quot_respect]: |
36 assumes q1: "Quotient R1 Abs1 Rep1" |
44 assumes q1: "Quotient R1 Abs1 Rep1" |
37 assumes q2: "Quotient R2 Abs2 Rep2" |
45 assumes q2: "Quotient R2 Abs2 Rep2" |
38 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
46 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
39 by simp |
47 by simp |
40 |
48 |
41 lemma pair_prs[quot_preserve]: |
49 lemma Pair_prs[quot_preserve]: |
42 assumes q1: "Quotient R1 Abs1 Rep1" |
50 assumes q1: "Quotient R1 Abs1 Rep1" |
43 assumes q2: "Quotient R2 Abs2 Rep2" |
51 assumes q2: "Quotient R2 Abs2 Rep2" |
44 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
52 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
45 apply(simp add: expand_fun_eq) |
53 apply(simp add: expand_fun_eq) |
46 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
54 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
47 done |
55 done |
48 |
56 |
49 lemma fst_rsp[quot_respect]: |
57 lemma fst_rsp[quot_respect]: |
50 assumes "Quotient R1 Abs1 Rep1" |
58 assumes "Quotient R1 Abs1 Rep1" |
51 assumes "Quotient R2 Abs2 Rep2" |
59 assumes "Quotient R2 Abs2 Rep2" |
52 shows "(prod_rel R1 R2 ===> R1) fst fst" |
60 shows "(prod_rel R1 R2 ===> R1) fst fst" |
54 |
62 |
55 lemma fst_prs[quot_preserve]: |
63 lemma fst_prs[quot_preserve]: |
56 assumes q1: "Quotient R1 Abs1 Rep1" |
64 assumes q1: "Quotient R1 Abs1 Rep1" |
57 assumes q2: "Quotient R2 Abs2 Rep2" |
65 assumes q2: "Quotient R2 Abs2 Rep2" |
58 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
66 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
59 apply(simp add: expand_fun_eq) |
67 apply(simp add: expand_fun_eq) |
60 apply(simp add: Quotient_abs_rep[OF q1]) |
68 apply(simp add: Quotient_abs_rep[OF q1]) |
61 done |
69 done |
62 |
70 |
63 lemma snd_rsp[quot_respect]: |
71 lemma snd_rsp[quot_respect]: |
64 assumes "Quotient R1 Abs1 Rep1" |
72 assumes "Quotient R1 Abs1 Rep1" |
65 assumes "Quotient R2 Abs2 Rep2" |
73 assumes "Quotient R2 Abs2 Rep2" |
66 shows "(prod_rel R1 R2 ===> R2) snd snd" |
74 shows "(prod_rel R1 R2 ===> R2) snd snd" |
68 |
76 |
69 lemma snd_prs[quot_preserve]: |
77 lemma snd_prs[quot_preserve]: |
70 assumes q1: "Quotient R1 Abs1 Rep1" |
78 assumes q1: "Quotient R1 Abs1 Rep1" |
71 assumes q2: "Quotient R2 Abs2 Rep2" |
79 assumes q2: "Quotient R2 Abs2 Rep2" |
72 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
80 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
73 apply(simp add: expand_fun_eq) |
81 apply(simp add: expand_fun_eq) |
74 apply(simp add: Quotient_abs_rep[OF q2]) |
82 apply(simp add: Quotient_abs_rep[OF q2]) |
75 done |
83 done |
76 |
84 |
77 lemma prod_fun_id[id_simps]: |
85 lemma prod_fun_id[id_simps]: |
78 shows "prod_fun id id \<equiv> id" |
86 shows "prod_fun id id \<equiv> id" |
79 by (rule eq_reflection) |
87 by (rule eq_reflection) (simp add: prod_fun_def) |
80 (simp add: prod_fun_def) |
|
81 |
88 |
82 lemma prod_rel_eq[id_simps]: |
89 lemma prod_rel_eq[id_simps]: |
83 shows "prod_rel (op =) (op =) \<equiv> (op =)" |
90 shows "prod_rel (op =) (op =) \<equiv> (op =)" |
84 apply (rule eq_reflection) |
91 apply (rule eq_reflection) |
85 apply (rule ext)+ |
92 apply (simp add: expand_fun_eq) |
86 apply auto |
|
87 done |
93 done |
88 |
94 |
89 end |
95 end |