1 (* Title: HOL/Library/Quotient_Product.thy
2 Author: Cezary Kaliszyk and Christian Urban
5 header {* Quotient infrastructure for the product type *}
7 theory Quotient_Product
8 imports Main Quotient_Syntax
12 prod_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool"
14 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
16 lemma prod_rel_apply [simp]:
17 "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
18 by (simp add: prod_rel_def)
20 lemma map_pair_id [id_simps]:
21 shows "map_pair id id = id"
22 by (simp add: fun_eq_iff)
24 lemma prod_rel_eq [id_simps]:
25 shows "prod_rel (op =) (op =) = (op =)"
26 by (simp add: fun_eq_iff)
28 lemma prod_equivp [quot_equiv]:
31 shows "equivp (prod_rel R1 R2)"
32 using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
34 lemma prod_quotient [quot_thm]:
35 assumes "Quotient R1 Abs1 Rep1"
36 assumes "Quotient R2 Abs2 Rep2"
37 shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
38 apply (rule QuotientI)
39 apply (simp add: map_pair.compositionality comp_def map_pair.identity
40 Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
41 apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
42 using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
43 apply (auto simp add: split_paired_all)
46 declare [[map prod = (prod_rel, prod_quotient)]]
48 lemma Pair_rsp [quot_respect]:
49 assumes q1: "Quotient R1 Abs1 Rep1"
50 assumes q2: "Quotient R2 Abs2 Rep2"
51 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
52 by (auto simp add: prod_rel_def)
54 lemma Pair_prs [quot_preserve]:
55 assumes q1: "Quotient R1 Abs1 Rep1"
56 assumes q2: "Quotient R2 Abs2 Rep2"
57 shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
58 apply(simp add: fun_eq_iff)
59 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
62 lemma fst_rsp [quot_respect]:
63 assumes "Quotient R1 Abs1 Rep1"
64 assumes "Quotient R2 Abs2 Rep2"
65 shows "(prod_rel R1 R2 ===> R1) fst fst"
68 lemma fst_prs [quot_preserve]:
69 assumes q1: "Quotient R1 Abs1 Rep1"
70 assumes q2: "Quotient R2 Abs2 Rep2"
71 shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
72 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
74 lemma snd_rsp [quot_respect]:
75 assumes "Quotient R1 Abs1 Rep1"
76 assumes "Quotient R2 Abs2 Rep2"
77 shows "(prod_rel R1 R2 ===> R2) snd snd"
80 lemma snd_prs [quot_preserve]:
81 assumes q1: "Quotient R1 Abs1 Rep1"
82 assumes q2: "Quotient R2 Abs2 Rep2"
83 shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
84 by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
86 lemma split_rsp [quot_respect]:
87 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
88 by (auto intro!: fun_relI elim!: fun_relE)
90 lemma split_prs [quot_preserve]:
91 assumes q1: "Quotient R1 Abs1 Rep1"
92 and q2: "Quotient R2 Abs2 Rep2"
93 shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
94 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
97 shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
98 prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
99 by (auto simp add: fun_rel_def)
101 lemma [quot_preserve]:
102 assumes q1: "Quotient R1 abs1 rep1"
103 and q2: "Quotient R2 abs2 rep2"
104 shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
105 map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
106 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
108 lemma [quot_preserve]:
109 shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
110 (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
113 declare Pair_eq[quot_preserve]