author | haftmann |
Thu, 14 Feb 2013 14:14:55 +0100 | |
changeset 51115 | 7dbd6832a689 |
parent 50573 | src/HOL/Library/Product_Lattice.thy@765c22baa1c9 |
child 51542 | 738598beeb26 |
permissions | -rw-r--r-- |
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
1 |
(* Title: HOL/Library/Product_Order.thy |
44006 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
5 |
header {* Pointwise order on product types *} |
44006 | 6 |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
7 |
theory Product_Order |
44006 | 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 |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
164 |
INF_lower SUP_upper le_INF_iff SUP_le_iff) |
44006 | 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))" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
181 |
by (simp add: SUP_def fst_Sup image_image) |
44006 | 182 |
|
183 |
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
184 |
by (simp add: SUP_def snd_Sup image_image) |
44006 | 185 |
|
186 |
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
187 |
by (simp add: INF_def fst_Inf image_image) |
44006 | 188 |
|
189 |
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
190 |
by (simp add: INF_def snd_Inf image_image) |
44006 | 191 |
|
192 |
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
193 |
by (simp add: SUP_def Sup_prod_def image_image) |
44006 | 194 |
|
195 |
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)" |
|
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44006
diff
changeset
|
196 |
by (simp add: INF_def Inf_prod_def image_image) |
44006 | 197 |
|
50535 | 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 |
||
50573 | 225 |
(* Contribution: Alessandro Coglio *) |
50535 | 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 |
||
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
50573
diff
changeset
|
237 |
end |
50535 | 238 |