Quelle Orders.thy Sprache: Isabelle

(*  Title:      HOL/Lattice/Orders.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section \<open>Orders\<close>

theory Orders imports Main begin

subsection \<open>Ordered structures\<close>

text \<open>
  We define several classes of ordered structures over some type \<^typ>\<open>'a\<close> with relation \<open>\<sqsubseteq> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.  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).
\<close>

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 \<open>Duality\<close>

text \<open>
  The \emph{dual} of an ordered structure is an isomorphic copy of the
  underlying type, with the \<open>\<sqsubseteq>\<close> relation defined as the inverse
  of the original one.
\<close>

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 \<open>
  \medskip Functions \<^term>\<open>dual\<close> and \<^term>\<open>undual\<close> are inverse to
  each other; this entails the following fundamental properties.
\<close>

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 \<open>
  \medskip Since \<^term>\<open>dual\<close> (and \<^term>\<open>undual\<close>) are both injective
  and surjective, the basic logical connectives (equality,
  quantification etc.) are transferred as follows.
\<close>

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' \<in> 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 \<open>Transforming orders\<close>

subsubsection \<open>Duals\<close>

text \<open>
  The classes of quasi, partial, and linear orders are all closed
  under formation of dual structures.
\<close>

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 \<open>Binary products \label{sec:prod-order}\<close>

text \<open>
  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.
\<close>

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 \<open>General products \label{sec:fun-order}\<close>

text \<open>
  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.
\<close>

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

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.