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