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