(* Title: HOL/Lattice/Orders.thy

Author: Markus Wenzel, TU Muenchen

*)

header {* Orders *}

theory Orders imports Main begin

subsection {* Ordered structures *}

text {*

We define several classes of ordered structures over some type @{typ

'a} with relation @{text "\<sqsubseteq> :: '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)

notation (xsymbols)

leq (infixl "\<sqsubseteq>" 50)

class quasi_order = leq +

assumes leq_refl [intro?]: "x \<sqsubseteq> x"

assumes leq_trans [trans]: "x \<sqsubseteq> y ==> y \<sqsubseteq> z ==> x \<sqsubseteq> z"

class partial_order = quasi_order +

assumes leq_antisym [trans]: "x \<sqsubseteq> y ==> y \<sqsubseteq> x ==> x = y"

class linear_order = partial_order +

assumes leq_linear: "x \<sqsubseteq> y ∨ y \<sqsubseteq> x"

lemma linear_order_cases:

"((x::'a::linear_order) \<sqsubseteq> y ==> C) ==> (y \<sqsubseteq> 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 @{text \<sqsubseteq>} 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' \<sqsubseteq> y' ≡ undual y' \<sqsubseteq> undual x'"

instance ..

end

lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> x')"

by (simp add: leq_dual_def)

lemma dual_leq [iff?]: "(dual x \<sqsubseteq> dual y) = (y \<sqsubseteq> x)"

by (simp add: leq_dual_def)

text {*

\medskip Functions @{term dual} and @{term 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 @{term dual} (and @{term 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_compose [symmetric])

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' \<sqsubseteq> undual x'" .. thus "x' \<sqsubseteq> x'" ..

assume "y' \<sqsubseteq> z'" hence "undual z' \<sqsubseteq> undual y'" ..

also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..

finally show "x' \<sqsubseteq> z'" ..

qed

instance dual :: (partial_order) partial_order

proof

fix x' y' :: "'a::partial_order dual"

assume "y' \<sqsubseteq> x'" hence "undual x' \<sqsubseteq> undual y'" ..

also assume "x' \<sqsubseteq> y'" hence "undual y' \<sqsubseteq> undual x'" ..

finally show "x' = y'" ..

qed

instance dual :: (linear_order) linear_order

proof

fix x' y' :: "'a::linear_order dual"

show "x' \<sqsubseteq> y' ∨ y' \<sqsubseteq> x'"

proof (rule linear_order_cases)

assume "undual y' \<sqsubseteq> undual x'"

hence "x' \<sqsubseteq> y'" .. thus ?thesis ..

next

assume "undual x' \<sqsubseteq> undual y'"

hence "y' \<sqsubseteq> 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 \<sqsubseteq> q ≡ fst p \<sqsubseteq> fst q ∧ snd p \<sqsubseteq> snd q"

instance ..

end

lemma leq_prodI [intro?]:

"fst p \<sqsubseteq> fst q ==> snd p \<sqsubseteq> snd q ==> p \<sqsubseteq> q"

by (unfold leq_prod_def) blast

lemma leq_prodE [elim?]:

"p \<sqsubseteq> q ==> (fst p \<sqsubseteq> fst q ==> snd p \<sqsubseteq> 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 \<sqsubseteq> p"

proof

show "fst p \<sqsubseteq> fst p" ..

show "snd p \<sqsubseteq> snd p" ..

qed

assume pq: "p \<sqsubseteq> q" and qr: "q \<sqsubseteq> r"

show "p \<sqsubseteq> r"

proof

from pq have "fst p \<sqsubseteq> fst q" ..

also from qr have "… \<sqsubseteq> fst r" ..

finally show "fst p \<sqsubseteq> fst r" .

from pq have "snd p \<sqsubseteq> snd q" ..

also from qr have "… \<sqsubseteq> snd r" ..

finally show "snd p \<sqsubseteq> 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 \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"

show "p = q"

proof

from pq have "fst p \<sqsubseteq> fst q" ..

also from qp have "… \<sqsubseteq> fst p" ..

finally show "fst p = fst q" .

from pq have "snd p \<sqsubseteq> snd q" ..

also from qp have "… \<sqsubseteq> 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 \<sqsubseteq> g ≡ ∀x. f x \<sqsubseteq> g x"

instance ..

end

lemma leq_funI [intro?]: "(!!x. f x \<sqsubseteq> g x) ==> f \<sqsubseteq> g"

by (unfold leq_fun_def) blast

lemma leq_funD [dest?]: "f \<sqsubseteq> g ==> f x \<sqsubseteq> 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 \<sqsubseteq> f"

proof

fix x show "f x \<sqsubseteq> f x" ..

qed

assume fg: "f \<sqsubseteq> g" and gh: "g \<sqsubseteq> h"

show "f \<sqsubseteq> h"

proof

fix x from fg have "f x \<sqsubseteq> g x" ..

also from gh have "… \<sqsubseteq> h x" ..

finally show "f x \<sqsubseteq> h x" .

qed

qed

instance "fun" :: (type, partial_order) partial_order

proof

fix f g :: "'a => 'b::partial_order"

assume fg: "f \<sqsubseteq> g" and gf: "g \<sqsubseteq> f"

show "f = g"

proof

fix x from fg have "f x \<sqsubseteq> g x" ..

also from gf have "… \<sqsubseteq> f x" ..

finally show "f x = g x" .

qed

qed

end