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