1 (* Title: HOL/Library/Quotient_Product.thy |
1 (* Title: HOL/Library/Quotient_Product.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk, Christian Urban and Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 header {* Quotient infrastructure for the product type *} |
5 header {* Quotient infrastructure for the product type *} |
6 |
6 |
7 theory Quotient_Product |
7 theory Quotient_Product |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
|
10 |
|
11 subsection {* Relator for product type *} |
10 |
12 |
11 definition |
13 definition |
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 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'c \<Rightarrow> 'b \<times> 'd \<Rightarrow> bool" |
13 where |
15 where |
14 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
16 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
19 |
21 |
20 lemma map_pair_id [id_simps]: |
22 lemma map_pair_id [id_simps]: |
21 shows "map_pair id id = id" |
23 shows "map_pair id id = id" |
22 by (simp add: fun_eq_iff) |
24 by (simp add: fun_eq_iff) |
23 |
25 |
24 lemma prod_rel_eq [id_simps]: |
26 lemma prod_rel_eq [id_simps, relator_eq]: |
25 shows "prod_rel (op =) (op =) = (op =)" |
27 shows "prod_rel (op =) (op =) = (op =)" |
26 by (simp add: fun_eq_iff) |
28 by (simp add: fun_eq_iff) |
27 |
29 |
28 lemma prod_equivp [quot_equiv]: |
30 lemma prod_equivp [quot_equiv]: |
29 assumes "equivp R1" |
31 assumes "equivp R1" |
30 assumes "equivp R2" |
32 assumes "equivp R2" |
31 shows "equivp (prod_rel R1 R2)" |
33 shows "equivp (prod_rel R1 R2)" |
32 using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) |
34 using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE) |
|
35 |
|
36 lemma right_total_prod_rel [transfer_rule]: |
|
37 assumes "right_total R1" and "right_total R2" |
|
38 shows "right_total (prod_rel R1 R2)" |
|
39 using assms unfolding right_total_def prod_rel_def by auto |
|
40 |
|
41 lemma right_unique_prod_rel [transfer_rule]: |
|
42 assumes "right_unique R1" and "right_unique R2" |
|
43 shows "right_unique (prod_rel R1 R2)" |
|
44 using assms unfolding right_unique_def prod_rel_def by auto |
|
45 |
|
46 lemma bi_total_prod_rel [transfer_rule]: |
|
47 assumes "bi_total R1" and "bi_total R2" |
|
48 shows "bi_total (prod_rel R1 R2)" |
|
49 using assms unfolding bi_total_def prod_rel_def by auto |
|
50 |
|
51 lemma bi_unique_prod_rel [transfer_rule]: |
|
52 assumes "bi_unique R1" and "bi_unique R2" |
|
53 shows "bi_unique (prod_rel R1 R2)" |
|
54 using assms unfolding bi_unique_def prod_rel_def by auto |
|
55 |
|
56 subsection {* Correspondence rules for transfer package *} |
|
57 |
|
58 lemma Pair_transfer [transfer_rule]: "(A ===> B ===> prod_rel A B) Pair Pair" |
|
59 unfolding fun_rel_def prod_rel_def by simp |
|
60 |
|
61 lemma fst_transfer [transfer_rule]: "(prod_rel A B ===> A) fst fst" |
|
62 unfolding fun_rel_def prod_rel_def by simp |
|
63 |
|
64 lemma snd_transfer [transfer_rule]: "(prod_rel A B ===> B) snd snd" |
|
65 unfolding fun_rel_def prod_rel_def by simp |
|
66 |
|
67 lemma prod_case_transfer [transfer_rule]: |
|
68 "((A ===> B ===> C) ===> prod_rel A B ===> C) prod_case prod_case" |
|
69 unfolding fun_rel_def prod_rel_def by simp |
|
70 |
|
71 lemma curry_transfer [transfer_rule]: |
|
72 "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" |
|
73 unfolding curry_def by correspondence |
|
74 |
|
75 lemma map_pair_transfer [transfer_rule]: |
|
76 "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) |
|
77 map_pair map_pair" |
|
78 unfolding map_pair_def [abs_def] by correspondence |
|
79 |
|
80 lemma prod_rel_transfer [transfer_rule]: |
|
81 "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> |
|
82 prod_rel A C ===> prod_rel B D ===> op =) prod_rel prod_rel" |
|
83 unfolding fun_rel_def by auto |
|
84 |
|
85 subsection {* Setup for lifting package *} |
|
86 |
|
87 lemma Quotient_prod: |
|
88 assumes "Quotient R1 Abs1 Rep1 T1" |
|
89 assumes "Quotient R2 Abs2 Rep2 T2" |
|
90 shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) |
|
91 (map_pair Rep1 Rep2) (prod_rel T1 T2)" |
|
92 using assms unfolding Quotient_alt_def by auto |
|
93 |
|
94 declare [[map prod = (prod_rel, Quotient_prod)]] |
|
95 |
|
96 subsection {* Rules for quotient package *} |
33 |
97 |
34 lemma prod_quotient [quot_thm]: |
98 lemma prod_quotient [quot_thm]: |
35 assumes "Quotient3 R1 Abs1 Rep1" |
99 assumes "Quotient3 R1 Abs1 Rep1" |
36 assumes "Quotient3 R2 Abs2 Rep2" |
100 assumes "Quotient3 R2 Abs2 Rep2" |
37 shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" |
101 shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" |
47 |
111 |
48 lemma Pair_rsp [quot_respect]: |
112 lemma Pair_rsp [quot_respect]: |
49 assumes q1: "Quotient3 R1 Abs1 Rep1" |
113 assumes q1: "Quotient3 R1 Abs1 Rep1" |
50 assumes q2: "Quotient3 R2 Abs2 Rep2" |
114 assumes q2: "Quotient3 R2 Abs2 Rep2" |
51 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
115 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
52 by (auto simp add: prod_rel_def) |
116 by (rule Pair_transfer) |
53 |
117 |
54 lemma Pair_prs [quot_preserve]: |
118 lemma Pair_prs [quot_preserve]: |
55 assumes q1: "Quotient3 R1 Abs1 Rep1" |
119 assumes q1: "Quotient3 R1 Abs1 Rep1" |
56 assumes q2: "Quotient3 R2 Abs2 Rep2" |
120 assumes q2: "Quotient3 R2 Abs2 Rep2" |
57 shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" |
121 shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" |
83 shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" |
147 shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" |
84 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) |
148 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) |
85 |
149 |
86 lemma split_rsp [quot_respect]: |
150 lemma split_rsp [quot_respect]: |
87 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
151 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
88 unfolding prod_rel_def fun_rel_def |
152 by (rule prod_case_transfer) |
89 by auto |
|
90 |
153 |
91 lemma split_prs [quot_preserve]: |
154 lemma split_prs [quot_preserve]: |
92 assumes q1: "Quotient3 R1 Abs1 Rep1" |
155 assumes q1: "Quotient3 R1 Abs1 Rep1" |
93 and q2: "Quotient3 R2 Abs2 Rep2" |
156 and q2: "Quotient3 R2 Abs2 Rep2" |
94 shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" |
157 shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" |
95 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) |
158 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) |
96 |
159 |
97 lemma [quot_respect]: |
160 lemma [quot_respect]: |
98 shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> |
161 shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> |
99 prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" |
162 prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" |
100 by (auto simp add: fun_rel_def) |
163 by (rule prod_rel_transfer) |
101 |
164 |
102 lemma [quot_preserve]: |
165 lemma [quot_preserve]: |
103 assumes q1: "Quotient3 R1 abs1 rep1" |
166 assumes q1: "Quotient3 R1 abs1 rep1" |
104 and q2: "Quotient3 R2 abs2 rep2" |
167 and q2: "Quotient3 R2 abs2 rep2" |
105 shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> |
168 shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> |