|
1 (* Title: HOL/Library/Product_Order.thy |
|
2 Author: Brian Huffman |
|
3 *) |
|
4 |
|
5 header {* Pointwise order on product types *} |
|
6 |
|
7 theory Product_Order |
|
8 imports "~~/src/HOL/Library/Product_plus" |
|
9 begin |
|
10 |
|
11 subsection {* Pointwise ordering *} |
|
12 |
|
13 instantiation prod :: (ord, ord) ord |
|
14 begin |
|
15 |
|
16 definition |
|
17 "x \<le> y \<longleftrightarrow> fst x \<le> fst y \<and> snd x \<le> snd y" |
|
18 |
|
19 definition |
|
20 "(x::'a \<times> 'b) < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
|
21 |
|
22 instance .. |
|
23 |
|
24 end |
|
25 |
|
26 lemma fst_mono: "x \<le> y \<Longrightarrow> fst x \<le> fst y" |
|
27 unfolding less_eq_prod_def by simp |
|
28 |
|
29 lemma snd_mono: "x \<le> y \<Longrightarrow> snd x \<le> snd y" |
|
30 unfolding less_eq_prod_def by simp |
|
31 |
|
32 lemma Pair_mono: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> (x, y) \<le> (x', y')" |
|
33 unfolding less_eq_prod_def by simp |
|
34 |
|
35 lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d" |
|
36 unfolding less_eq_prod_def by simp |
|
37 |
|
38 instance prod :: (preorder, preorder) preorder |
|
39 proof |
|
40 fix x y z :: "'a \<times> 'b" |
|
41 show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
|
42 by (rule less_prod_def) |
|
43 show "x \<le> x" |
|
44 unfolding less_eq_prod_def |
|
45 by fast |
|
46 assume "x \<le> y" and "y \<le> z" thus "x \<le> z" |
|
47 unfolding less_eq_prod_def |
|
48 by (fast elim: order_trans) |
|
49 qed |
|
50 |
|
51 instance prod :: (order, order) order |
|
52 by default auto |
|
53 |
|
54 |
|
55 subsection {* Binary infimum and supremum *} |
|
56 |
|
57 instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf |
|
58 begin |
|
59 |
|
60 definition |
|
61 "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))" |
|
62 |
|
63 lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)" |
|
64 unfolding inf_prod_def by simp |
|
65 |
|
66 lemma fst_inf [simp]: "fst (inf x y) = inf (fst x) (fst y)" |
|
67 unfolding inf_prod_def by simp |
|
68 |
|
69 lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)" |
|
70 unfolding inf_prod_def by simp |
|
71 |
|
72 instance |
|
73 by default auto |
|
74 |
|
75 end |
|
76 |
|
77 instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup |
|
78 begin |
|
79 |
|
80 definition |
|
81 "sup x y = (sup (fst x) (fst y), sup (snd x) (snd y))" |
|
82 |
|
83 lemma sup_Pair_Pair [simp]: "sup (a, b) (c, d) = (sup a c, sup b d)" |
|
84 unfolding sup_prod_def by simp |
|
85 |
|
86 lemma fst_sup [simp]: "fst (sup x y) = sup (fst x) (fst y)" |
|
87 unfolding sup_prod_def by simp |
|
88 |
|
89 lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)" |
|
90 unfolding sup_prod_def by simp |
|
91 |
|
92 instance |
|
93 by default auto |
|
94 |
|
95 end |
|
96 |
|
97 instance prod :: (lattice, lattice) lattice .. |
|
98 |
|
99 instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice |
|
100 by default (auto simp add: sup_inf_distrib1) |
|
101 |
|
102 |
|
103 subsection {* Top and bottom elements *} |
|
104 |
|
105 instantiation prod :: (top, top) top |
|
106 begin |
|
107 |
|
108 definition |
|
109 "top = (top, top)" |
|
110 |
|
111 lemma fst_top [simp]: "fst top = top" |
|
112 unfolding top_prod_def by simp |
|
113 |
|
114 lemma snd_top [simp]: "snd top = top" |
|
115 unfolding top_prod_def by simp |
|
116 |
|
117 lemma Pair_top_top: "(top, top) = top" |
|
118 unfolding top_prod_def by simp |
|
119 |
|
120 instance |
|
121 by default (auto simp add: top_prod_def) |
|
122 |
|
123 end |
|
124 |
|
125 instantiation prod :: (bot, bot) bot |
|
126 begin |
|
127 |
|
128 definition |
|
129 "bot = (bot, bot)" |
|
130 |
|
131 lemma fst_bot [simp]: "fst bot = bot" |
|
132 unfolding bot_prod_def by simp |
|
133 |
|
134 lemma snd_bot [simp]: "snd bot = bot" |
|
135 unfolding bot_prod_def by simp |
|
136 |
|
137 lemma Pair_bot_bot: "(bot, bot) = bot" |
|
138 unfolding bot_prod_def by simp |
|
139 |
|
140 instance |
|
141 by default (auto simp add: bot_prod_def) |
|
142 |
|
143 end |
|
144 |
|
145 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice .. |
|
146 |
|
147 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra |
|
148 by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq) |
|
149 |
|
150 |
|
151 subsection {* Complete lattice operations *} |
|
152 |
|
153 instantiation prod :: (complete_lattice, complete_lattice) complete_lattice |
|
154 begin |
|
155 |
|
156 definition |
|
157 "Sup A = (SUP x:A. fst x, SUP x:A. snd x)" |
|
158 |
|
159 definition |
|
160 "Inf A = (INF x:A. fst x, INF x:A. snd x)" |
|
161 |
|
162 instance |
|
163 by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def |
|
164 INF_lower SUP_upper le_INF_iff SUP_le_iff) |
|
165 |
|
166 end |
|
167 |
|
168 lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)" |
|
169 unfolding Sup_prod_def by simp |
|
170 |
|
171 lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)" |
|
172 unfolding Sup_prod_def by simp |
|
173 |
|
174 lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)" |
|
175 unfolding Inf_prod_def by simp |
|
176 |
|
177 lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)" |
|
178 unfolding Inf_prod_def by simp |
|
179 |
|
180 lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))" |
|
181 by (simp add: SUP_def fst_Sup image_image) |
|
182 |
|
183 lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" |
|
184 by (simp add: SUP_def snd_Sup image_image) |
|
185 |
|
186 lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" |
|
187 by (simp add: INF_def fst_Inf image_image) |
|
188 |
|
189 lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" |
|
190 by (simp add: INF_def snd_Inf image_image) |
|
191 |
|
192 lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" |
|
193 by (simp add: SUP_def Sup_prod_def image_image) |
|
194 |
|
195 lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" |
|
196 by (simp add: INF_def Inf_prod_def image_image) |
|
197 |
|
198 |
|
199 text {* Alternative formulations for set infima and suprema over the product |
|
200 of two complete lattices: *} |
|
201 |
|
202 lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))" |
|
203 by (auto simp: Inf_prod_def INF_def) |
|
204 |
|
205 lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))" |
|
206 by (auto simp: Sup_prod_def SUP_def) |
|
207 |
|
208 lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))" |
|
209 by (auto simp: INF_def Inf_prod_def image_compose) |
|
210 |
|
211 lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))" |
|
212 by (auto simp: SUP_def Sup_prod_def image_compose) |
|
213 |
|
214 lemma INF_prod_alt_def: |
|
215 "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))" |
|
216 by (metis fst_INF snd_INF surjective_pairing) |
|
217 |
|
218 lemma SUP_prod_alt_def: |
|
219 "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))" |
|
220 by (metis fst_SUP snd_SUP surjective_pairing) |
|
221 |
|
222 |
|
223 subsection {* Complete distributive lattices *} |
|
224 |
|
225 (* Contribution: Alessandro Coglio *) |
|
226 |
|
227 instance prod :: |
|
228 (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice |
|
229 proof |
|
230 case goal1 thus ?case |
|
231 by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF) |
|
232 next |
|
233 case goal2 thus ?case |
|
234 by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP) |
|
235 qed |
|
236 |
|
237 end |
|
238 |