(*  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 typ‹'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 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_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