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
`