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