src/HOL/Lattice/Orders.thy
 author wenzelm Thu May 24 17:25:53 2012 +0200 (2012-05-24) changeset 47988 e4b69e10b990 parent 40702 cf26dd7395e4 child 56154 f0a927235162 permissions -rw-r--r--
tuned proofs;
1 (*  Title:      HOL/Lattice/Orders.thy
2     Author:     Markus Wenzel, TU Muenchen
3 *)
5 header {* Orders *}
7 theory Orders imports Main begin
9 subsection {* Ordered structures *}
11 text {*
12   We define several classes of ordered structures over some type @{typ
13   'a} with relation @{text "\<sqsubseteq> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool"}.  For a
14   \emph{quasi-order} that relation is required to be reflexive and
15   transitive, for a \emph{partial order} it also has to be
16   anti-symmetric, while for a \emph{linear order} all elements are
17   required to be related (in either direction).
18 *}
20 class leq =
21   fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
23 notation (xsymbols)
24   leq  (infixl "\<sqsubseteq>" 50)
26 class quasi_order = leq +
27   assumes leq_refl [intro?]: "x \<sqsubseteq> x"
28   assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
30 class partial_order = quasi_order +
31   assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
33 class linear_order = partial_order +
34   assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
36 lemma linear_order_cases:
37     "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> C"
38   by (insert leq_linear) blast
41 subsection {* Duality *}
43 text {*
44   The \emph{dual} of an ordered structure is an isomorphic copy of the
45   underlying type, with the @{text \<sqsubseteq>} relation defined as the inverse
46   of the original one.
47 *}
49 datatype 'a dual = dual 'a
51 primrec undual :: "'a dual \<Rightarrow> 'a" where
52   undual_dual: "undual (dual x) = x"
54 instantiation dual :: (leq) leq
55 begin
57 definition
58   leq_dual_def: "x' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
60 instance ..
62 end
64 lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"
65   by (simp add: leq_dual_def)
67 lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"
68   by (simp add: leq_dual_def)
70 text {*
71   \medskip Functions @{term dual} and @{term undual} are inverse to
72   each other; this entails the following fundamental properties.
73 *}
75 lemma dual_undual [simp]: "dual (undual x') = x'"
76   by (cases x') simp
78 lemma undual_dual_id [simp]: "undual o dual = id"
79   by (rule ext) simp
81 lemma dual_undual_id [simp]: "dual o undual = id"
82   by (rule ext) simp
84 text {*
85   \medskip Since @{term dual} (and @{term undual}) are both injective
86   and surjective, the basic logical connectives (equality,
87   quantification etc.) are transferred as follows.
88 *}
90 lemma undual_equality [iff?]: "(undual x' = undual y') = (x' = y')"
91   by (cases x', cases y') simp
93 lemma dual_equality [iff?]: "(dual x = dual y) = (x = y)"
94   by simp
96 lemma dual_ball [iff?]: "(\<forall>x \<in> A. P (dual x)) = (\<forall>x' \<in> dual  A. P x')"
97 proof
98   assume a: "\<forall>x \<in> A. P (dual x)"
99   show "\<forall>x' \<in> dual  A. P x'"
100   proof
101     fix x' assume x': "x' \<in> dual  A"
102     have "undual x' \<in> A"
103     proof -
104       from x' have "undual x' \<in> undual  dual  A" by simp
105       thus "undual x' \<in> A" by (simp add: image_compose [symmetric])
106     qed
107     with a have "P (dual (undual x'))" ..
108     also have "\<dots> = x'" by simp
109     finally show "P x'" .
110   qed
111 next
112   assume a: "\<forall>x' \<in> dual  A. P x'"
113   show "\<forall>x \<in> A. P (dual x)"
114   proof
115     fix x assume "x \<in> A"
116     hence "dual x \<in> dual  A" by simp
117     with a show "P (dual x)" ..
118   qed
119 qed
121 lemma range_dual [simp]: "surj dual"
122 proof -
123   have "\<And>x'. dual (undual x') = x'" by simp
124   thus "surj dual" by (rule surjI)
125 qed
127 lemma dual_all [iff?]: "(\<forall>x. P (dual x)) = (\<forall>x'. P x')"
128 proof -
129   have "(\<forall>x \<in> UNIV. P (dual x)) = (\<forall>x' \<in> dual  UNIV. P x')"
130     by (rule dual_ball)
131   thus ?thesis by simp
132 qed
134 lemma dual_ex: "(\<exists>x. P (dual x)) = (\<exists>x'. P x')"
135 proof -
136   have "(\<forall>x. \<not> P (dual x)) = (\<forall>x'. \<not> P x')"
137     by (rule dual_all)
138   thus ?thesis by blast
139 qed
141 lemma dual_Collect: "{dual x| x. P (dual x)} = {x'. P x'}"
142 proof -
143   have "{dual x| x. P (dual x)} = {x'. \<exists>x''. x' = x'' \<and> P x''}"
144     by (simp only: dual_ex [symmetric])
145   thus ?thesis by blast
146 qed
149 subsection {* Transforming orders *}
151 subsubsection {* Duals *}
153 text {*
154   The classes of quasi, partial, and linear orders are all closed
155   under formation of dual structures.
156 *}
158 instance dual :: (quasi_order) quasi_order
159 proof
160   fix x' y' z' :: "'a::quasi_order dual"
161   have "undual x' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..
162   assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..
163   also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
164   finally show "x' \<sqsubseteq> z'" ..
165 qed
167 instance dual :: (partial_order) partial_order
168 proof
169   fix x' y' :: "'a::partial_order dual"
170   assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..
171   also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..
172   finally show "x' = y'" ..
173 qed
175 instance dual :: (linear_order) linear_order
176 proof
177   fix x' y' :: "'a::linear_order dual"
178   show "x' \<sqsubseteq> y' \<or> y' \<sqsubseteq> x'"
179   proof (rule linear_order_cases)
180     assume "undual y' \<sqsubseteq> undual x'"
181     hence "x' \<sqsubseteq> y'" .. thus ?thesis ..
182   next
183     assume "undual x' \<sqsubseteq> undual y'"
184     hence "y' \<sqsubseteq> x'" .. thus ?thesis ..
185   qed
186 qed
189 subsubsection {* Binary products \label{sec:prod-order} *}
191 text {*
192   The classes of quasi and partial orders are closed under binary
193   products.  Note that the direct product of linear orders need
194   \emph{not} be linear in general.
195 *}
197 instantiation prod :: (leq, leq) leq
198 begin
200 definition
201   leq_prod_def: "p \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
203 instance ..
205 end
207 lemma leq_prodI [intro?]:
208     "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> q"
209   by (unfold leq_prod_def) blast
211 lemma leq_prodE [elim?]:
212     "p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
213   by (unfold leq_prod_def) blast
215 instance prod :: (quasi_order, quasi_order) quasi_order
216 proof
217   fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
218   show "p \<sqsubseteq> p"
219   proof
220     show "fst p \<sqsubseteq> fst p" ..
221     show "snd p \<sqsubseteq> snd p" ..
222   qed
223   assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"
224   show "p \<sqsubseteq> r"
225   proof
226     from pq have "fst p \<sqsubseteq> fst q" ..
227     also from qr have "\<dots> \<sqsubseteq> fst r" ..
228     finally show "fst p \<sqsubseteq> fst r" .
229     from pq have "snd p \<sqsubseteq> snd q" ..
230     also from qr have "\<dots> \<sqsubseteq> snd r" ..
231     finally show "snd p \<sqsubseteq> snd r" .
232   qed
233 qed
235 instance prod :: (partial_order, partial_order) partial_order
236 proof
237   fix p q :: "'a::partial_order \<times> 'b::partial_order"
238   assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"
239   show "p = q"
240   proof
241     from pq have "fst p \<sqsubseteq> fst q" ..
242     also from qp have "\<dots> \<sqsubseteq> fst p" ..
243     finally show "fst p = fst q" .
244     from pq have "snd p \<sqsubseteq> snd q" ..
245     also from qp have "\<dots> \<sqsubseteq> snd p" ..
246     finally show "snd p = snd q" .
247   qed
248 qed
251 subsubsection {* General products \label{sec:fun-order} *}
253 text {*
254   The classes of quasi and partial orders are closed under general
255   products (function spaces).  Note that the direct product of linear
256   orders need \emph{not} be linear in general.
257 *}
259 instantiation "fun" :: (type, leq) leq
260 begin
262 definition
263   leq_fun_def: "f \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
265 instance ..
267 end
269 lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
270   by (unfold leq_fun_def) blast
272 lemma leq_funD [dest?]: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x"
273   by (unfold leq_fun_def) blast
275 instance "fun" :: (type, quasi_order) quasi_order
276 proof
277   fix f g h :: "'a \<Rightarrow> 'b::quasi_order"
278   show "f \<sqsubseteq> f"
279   proof
280     fix x show "f x \<sqsubseteq> f x" ..
281   qed
282   assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"
283   show "f \<sqsubseteq> h"
284   proof
285     fix x from fg have "f x \<sqsubseteq> g x" ..
286     also from gh have "\<dots> \<sqsubseteq> h x" ..
287     finally show "f x \<sqsubseteq> h x" .
288   qed
289 qed
291 instance "fun" :: (type, partial_order) partial_order
292 proof
293   fix f g :: "'a \<Rightarrow> 'b::partial_order"
294   assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"
295   show "f = g"
296   proof
297     fix x from fg have "f x \<sqsubseteq> g x" ..
298     also from gf have "\<dots> \<sqsubseteq> f x" ..
299     finally show "f x = g x" .
300   qed
301 qed
303 end