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