(* Title: HOL/Lattice/Orders.thy
Author: Markus Wenzel, TU Muenchen
*)
section ‹Orders
›
theory Orders
imports Main
begin
subsection ‹Ordered structures
›
text ‹
We define several
classes of ordered structures over some type
🍋‹'a\ with relation \\ :: 'a
==> 'a \ bool\. For a
\emph{quasi-order} that relation
is required
to be reflexive
and
transitive,
for a
\emph{partial order} it
also has
to be
anti-symmetric, while
for a
\emph{linear order} all elements are
required
to be related (
in either direction).
›
class leq =
fixes leq ::
"'a \ 'a \ bool" (
infixl ‹⊑› 50)
class quasi_order = leq +
assumes leq_refl [intro?]:
"x \ x"
assumes leq_trans [trans]:
"x \ y \ y \ z \ x \ z"
class partial_order = quasi_order +
assumes leq_antisym [trans]:
"x \ y \ y \ x \ x = y"
class linear_order = partial_order +
assumes leq_linear:
"x \ y \ y \ x"
lemma linear_order_cases:
"((x::'a::linear_order) \ y \ C) \ (y \ x \ C) \ C"
by (insert leq_linear) blast
subsection ‹Duality
›
text ‹
The
\emph{dual} of an ordered
structure is an isomorphic copy of the
underlying type,
with the
‹⊑› relation defined as the inverse
of the original one.
›
datatype 'a dual = dual 'a
primrec undual ::
"'a dual \ 'a" where
undual_dual:
"undual (dual x) = x"
instantiation dual :: (leq) leq
begin
definition
leq_dual_def:
"x' \ y' \ undual y' \ undual x'"
instance ..
end
lemma undual_leq [iff?]:
"(undual x' \ undual y') = (y' \ x')"
by (simp add: leq_dual_def)
lemma dual_leq [iff?]:
"(dual x \ dual y) = (y \ x)"
by (simp add: leq_dual_def)
text ‹
\medskip Functions
🍋‹dual
› and 🍋‹undual
› are inverse
to
each other; this entails the following fundamental properties.
›
lemma dual_undual [simp]:
"dual (undual x') = x'"
by (cases x
') simp
lemma undual_dual_id [simp]:
"undual o dual = id"
by (rule ext) simp
lemma dual_undual_id [simp]:
"dual o undual = id"
by (rule ext) simp
text ‹
\medskip Since
🍋‹dual
› (
and 🍋‹undual
›) are both injective
and surjective, the basic logical connectives (equality,
quantification etc.) are transferred as follows.
›
lemma undual_equality [iff?]:
"(undual x' = undual y') = (x' = y')"
by (cases x
', cases y') simp
lemma dual_equality [iff?]:
"(dual x = dual y) = (x = y)"
by simp
lemma dual_ball [iff?]:
"(\x \ A. P (dual x)) = (\x' \ dual ` A. P x')"
proof
assume a:
"\x \ A. P (dual x)"
show "\x' \ dual ` A. P x'"
proof
fix x
' assume x':
"x' \ dual ` A"
have "undual x' \ A"
proof -
from x
' have "undual x' ∈ undual ` dual ` A
" by simp
thus "undual x' \ A" by (simp add: image_comp)
qed
with a
have "P (dual (undual x'))" ..
also have "\ = x'" by simp
finally show "P x'" .
qed
next
assume a:
"\x' \ dual ` A. P x'"
show "\x \ A. P (dual x)"
proof
fix x
assume "x \ A"
hence "dual x \ dual ` A" by simp
with a
show "P (dual x)" ..
qed
qed
lemma range_dual [simp]:
"surj dual"
proof -
have "\x'. dual (undual x') = x'" by simp
thus "surj dual" by (rule surjI)
qed
lemma dual_all [iff?]:
"(\x. P (dual x)) = (\x'. P x')"
proof -
have "(\x \ UNIV. P (dual x)) = (\x' \ dual ` UNIV. P x')"
by (rule dual_ball)
thus ?thesis
by simp
qed
lemma dual_ex:
"(\x. P (dual x)) = (\x'. P x')"
proof -
have "(\x. \ P (dual x)) = (\x'. \ P x')"
by (rule dual_all)
thus ?thesis
by blast
qed
lemma dual_Collect:
"{dual x| x. P (dual x)} = {x'. P x'}"
proof -
have "{dual x| x. P (dual x)} = {x'. \x''. x' = x'' \ P x''}"
by (simp only: dual_ex [symmetric])
thus ?thesis
by blast
qed
subsection ‹Transforming orders
›
subsubsection
‹Duals
›
text ‹
The
classes of quasi, partial,
and linear orders are all closed
under formation of dual structures.
›
instance dual :: (quasi_order) quasi_order
proof
fix x
' y' z
' :: "'a::quasi_order dual
"
have "undual x' \ undual x'" ..
thus "x' \ x'" ..
assume "y' \ z'" hence "undual z' \ undual y'" ..
also assume "x' \ y'" hence "undual y' \ undual x'" ..
finally show "x' \ z'" ..
qed
instance dual :: (partial_order) partial_order
proof
fix x
' y' ::
"'a::partial_order dual"
assume "y' \ x'" hence "undual x' \ undual y'" ..
also assume "x' \ y'" hence "undual y' \ undual x'" ..
finally show "x' = y'" ..
qed
instance dual :: (linear_order) linear_order
proof
fix x
' y' ::
"'a::linear_order dual"
show "x' \ y' \ y' \ x'"
proof (rule linear_order_cases)
assume "undual y' \ undual x'"
hence "x' \ y'" ..
thus ?thesis ..
next
assume "undual x' \ undual y'"
hence "y' \ x'" ..
thus ?thesis ..
qed
qed
subsubsection
‹Binary products
\label{sec:prod-order}
›
text ‹
The
classes of quasi
and partial orders are closed under binary
products.
Note that the direct product of linear orders need
\emph{not} be linear
in general.
›
instantiation prod :: (leq, leq) leq
begin
definition
leq_prod_def:
"p \ q \ fst p \ fst q \ snd p \ snd q"
instance ..
end
lemma leq_prodI [intro?]:
"fst p \ fst q \ snd p \ snd q \ p \ q"
by (unfold leq_prod_def) blast
lemma leq_prodE [elim?]:
"p \ q \ (fst p \ fst q \ snd p \ snd q \ C) \ C"
by (unfold leq_prod_def) blast
instance prod :: (quasi_order, quasi_order) quasi_order
proof
fix p q r ::
"'a::quasi_order \ 'b::quasi_order"
show "p \ p"
proof
show "fst p \ fst p" ..
show "snd p \ snd p" ..
qed
assume pq:
"p \ q" and qr:
"q \ r"
show "p \ r"
proof
from pq
have "fst p \ fst q" ..
also from qr
have "\ \ fst r" ..
finally show "fst p \ fst r" .
from pq
have "snd p \ snd q" ..
also from qr
have "\ \ snd r" ..
finally show "snd p \ snd r" .
qed
qed
instance prod :: (partial_order, partial_order) partial_order
proof
fix p q ::
"'a::partial_order \ 'b::partial_order"
assume pq:
"p \ q" and qp:
"q \ p"
show "p = q"
proof
from pq
have "fst p \ fst q" ..
also from qp
have "\ \ fst p" ..
finally show "fst p = fst q" .
from pq
have "snd p \ snd q" ..
also from qp
have "\ \ snd p" ..
finally show "snd p = snd q" .
qed
qed
subsubsection
‹General products
\label{sec:fun-order}
›
text ‹
The
classes of quasi
and partial orders are closed under general
products (
function spaces).
Note that the direct product of linear
orders need
\emph{not} be linear
in general.
›
instantiation "fun" :: (type, leq) leq
begin
definition
leq_fun_def:
"f \ g \ \x. f x \ g x"
instance ..
end
lemma leq_funI [intro?]:
"(\x. f x \ g x) \ f \ g"
by (unfold leq_fun_def) blast
lemma leq_funD [dest?]:
"f \ g \ f x \ g x"
by (unfold leq_fun_def) blast
instance "fun" :: (type, quasi_order) quasi_order
proof
fix f g h ::
"'a \ 'b::quasi_order"
show "f \ f"
proof
fix x
show "f x \ f x" ..
qed
assume fg:
"f \ g" and gh:
"g \ h"
show "f \ h"
proof
fix x
from fg
have "f x \ g x" ..
also from gh
have "\ \ h x" ..
finally show "f x \ h x" .
qed
qed
instance "fun" :: (type, partial_order) partial_order
proof
fix f g ::
"'a \ 'b::partial_order"
assume fg:
"f \ g" and gf:
"g \ f"
show "f = g"
proof
fix x
from fg
have "f x \ g x" ..
also from gf
have "\ \ f x" ..
finally show "f x = g x" .
qed
qed
end
