src/HOL/Lattices.thy
author nipkow
Sun Nov 12 19:22:10 2006 +0100 (2006-11-12)
changeset 21312 1d39091a3208
parent 21249 d594c58e24ed
child 21381 79e065f2be95
permissions -rw-r--r--
started reorgnization of lattice theories
haftmann@21249
     1
(*  Title:      HOL/Lattices.thy
haftmann@21249
     2
    ID:         $Id$
haftmann@21249
     3
    Author:     Tobias Nipkow
haftmann@21249
     4
*)
haftmann@21249
     5
haftmann@21249
     6
header {* Lattices via Locales *}
haftmann@21249
     7
haftmann@21249
     8
theory Lattices
haftmann@21249
     9
imports Orderings
haftmann@21249
    10
begin
haftmann@21249
    11
haftmann@21249
    12
subsection{* Lattices *}
haftmann@21249
    13
haftmann@21249
    14
text{* This theory of lattice locales only defines binary sup and inf
haftmann@21249
    15
operations. The extension to finite sets is done in theory @{text
haftmann@21249
    16
Finite_Set}. In the longer term it may be better to define arbitrary
haftmann@21249
    17
sups and infs via @{text THE}. *}
haftmann@21249
    18
haftmann@21249
    19
locale lower_semilattice = partial_order +
haftmann@21249
    20
  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
nipkow@21312
    21
  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
haftmann@21249
    22
  and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
haftmann@21249
    23
haftmann@21249
    24
locale upper_semilattice = partial_order +
haftmann@21249
    25
  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
nipkow@21312
    26
  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
haftmann@21249
    27
  and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
haftmann@21249
    28
haftmann@21249
    29
locale lattice = lower_semilattice + upper_semilattice
haftmann@21249
    30
haftmann@21249
    31
lemma (in lower_semilattice) inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
haftmann@21249
    32
by(blast intro: antisym inf_le1 inf_le2 inf_least)
haftmann@21249
    33
haftmann@21249
    34
lemma (in upper_semilattice) sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
haftmann@21249
    35
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest)
haftmann@21249
    36
haftmann@21249
    37
lemma (in lower_semilattice) inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
haftmann@21249
    38
by(blast intro: antisym inf_le1 inf_le2 inf_least trans del:refl)
haftmann@21249
    39
haftmann@21249
    40
lemma (in upper_semilattice) sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
haftmann@21249
    41
by(blast intro!: antisym sup_ge1 sup_ge2 intro: sup_greatest trans del:refl)
haftmann@21249
    42
haftmann@21249
    43
lemma (in lower_semilattice) inf_idem[simp]: "x \<sqinter> x = x"
haftmann@21249
    44
by(blast intro: antisym inf_le1 inf_le2 inf_least refl)
haftmann@21249
    45
haftmann@21249
    46
lemma (in upper_semilattice) sup_idem[simp]: "x \<squnion> x = x"
haftmann@21249
    47
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl)
haftmann@21249
    48
haftmann@21249
    49
lemma (in lower_semilattice) inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
haftmann@21249
    50
by (simp add: inf_assoc[symmetric])
haftmann@21249
    51
haftmann@21249
    52
lemma (in upper_semilattice) sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
haftmann@21249
    53
by (simp add: sup_assoc[symmetric])
haftmann@21249
    54
haftmann@21249
    55
lemma (in lattice) inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
haftmann@21249
    56
by(blast intro: antisym inf_le1 inf_least sup_ge1)
haftmann@21249
    57
haftmann@21249
    58
lemma (in lattice) sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
haftmann@21249
    59
by(blast intro: antisym sup_ge1 sup_greatest inf_le1)
haftmann@21249
    60
haftmann@21249
    61
lemma (in lower_semilattice) inf_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
haftmann@21249
    62
by(blast intro: antisym inf_le1 inf_least refl)
haftmann@21249
    63
haftmann@21249
    64
lemma (in upper_semilattice) sup_absorb: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
haftmann@21249
    65
by(blast intro: antisym sup_ge2 sup_greatest refl)
haftmann@21249
    66
haftmann@21249
    67
haftmann@21249
    68
lemma (in lower_semilattice) less_eq_inf_conv [simp]:
haftmann@21249
    69
 "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
haftmann@21249
    70
by(blast intro: antisym inf_le1 inf_le2 inf_least refl trans)
haftmann@21249
    71
haftmann@21249
    72
lemmas (in lower_semilattice) below_inf_conv = less_eq_inf_conv
haftmann@21249
    73
  -- {* a duplicate for backward compatibility *}
haftmann@21249
    74
haftmann@21249
    75
lemma (in upper_semilattice) above_sup_conv[simp]:
haftmann@21249
    76
 "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
haftmann@21249
    77
by(blast intro: antisym sup_ge1 sup_ge2 sup_greatest refl trans)
haftmann@21249
    78
haftmann@21249
    79
haftmann@21249
    80
text{* Towards distributivity: if you have one of them, you have them all. *}
haftmann@21249
    81
haftmann@21249
    82
lemma (in lattice) distrib_imp1:
haftmann@21249
    83
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
haftmann@21249
    84
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
    85
proof-
haftmann@21249
    86
  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
haftmann@21249
    87
  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
haftmann@21249
    88
  also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
haftmann@21249
    89
    by(simp add:inf_sup_absorb inf_commute)
haftmann@21249
    90
  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
haftmann@21249
    91
  finally show ?thesis .
haftmann@21249
    92
qed
haftmann@21249
    93
haftmann@21249
    94
lemma (in lattice) distrib_imp2:
haftmann@21249
    95
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
    96
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
haftmann@21249
    97
proof-
haftmann@21249
    98
  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
haftmann@21249
    99
  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
haftmann@21249
   100
  also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
haftmann@21249
   101
    by(simp add:sup_inf_absorb sup_commute)
haftmann@21249
   102
  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
haftmann@21249
   103
  finally show ?thesis .
haftmann@21249
   104
qed
haftmann@21249
   105
haftmann@21249
   106
text{* A package of rewrite rules for deciding equivalence wrt ACI: *}
haftmann@21249
   107
haftmann@21249
   108
lemma (in lower_semilattice) inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
haftmann@21249
   109
proof -
haftmann@21249
   110
  have "x \<sqinter> (y \<sqinter> z) = (y \<sqinter> z) \<sqinter> x" by (simp only: inf_commute)
haftmann@21249
   111
  also have "... = y \<sqinter> (z \<sqinter> x)" by (simp only: inf_assoc)
haftmann@21249
   112
  also have "z \<sqinter> x = x \<sqinter> z" by (simp only: inf_commute)
haftmann@21249
   113
  finally(back_subst) show ?thesis .
haftmann@21249
   114
qed
haftmann@21249
   115
haftmann@21249
   116
lemma (in upper_semilattice) sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
haftmann@21249
   117
proof -
haftmann@21249
   118
  have "x \<squnion> (y \<squnion> z) = (y \<squnion> z) \<squnion> x" by (simp only: sup_commute)
haftmann@21249
   119
  also have "... = y \<squnion> (z \<squnion> x)" by (simp only: sup_assoc)
haftmann@21249
   120
  also have "z \<squnion> x = x \<squnion> z" by (simp only: sup_commute)
haftmann@21249
   121
  finally(back_subst) show ?thesis .
haftmann@21249
   122
qed
haftmann@21249
   123
haftmann@21249
   124
lemma (in lower_semilattice) inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
haftmann@21249
   125
proof -
haftmann@21249
   126
  have "x \<sqinter> (x \<sqinter> y) = (x \<sqinter> x) \<sqinter> y" by(simp only:inf_assoc)
haftmann@21249
   127
  also have "\<dots> = x \<sqinter> y" by(simp)
haftmann@21249
   128
  finally show ?thesis .
haftmann@21249
   129
qed
haftmann@21249
   130
haftmann@21249
   131
lemma (in upper_semilattice) sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
haftmann@21249
   132
proof -
haftmann@21249
   133
  have "x \<squnion> (x \<squnion> y) = (x \<squnion> x) \<squnion> y" by(simp only:sup_assoc)
haftmann@21249
   134
  also have "\<dots> = x \<squnion> y" by(simp)
haftmann@21249
   135
  finally show ?thesis .
haftmann@21249
   136
qed
haftmann@21249
   137
haftmann@21249
   138
haftmann@21249
   139
lemmas (in lower_semilattice) inf_ACI =
haftmann@21249
   140
 inf_commute inf_assoc inf_left_commute inf_left_idem
haftmann@21249
   141
haftmann@21249
   142
lemmas (in upper_semilattice) sup_ACI =
haftmann@21249
   143
 sup_commute sup_assoc sup_left_commute sup_left_idem
haftmann@21249
   144
haftmann@21249
   145
lemmas (in lattice) ACI = inf_ACI sup_ACI
haftmann@21249
   146
haftmann@21249
   147
haftmann@21249
   148
subsection{* Distributive lattices *}
haftmann@21249
   149
haftmann@21249
   150
locale distrib_lattice = lattice +
haftmann@21249
   151
  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
haftmann@21249
   152
haftmann@21249
   153
lemma (in distrib_lattice) sup_inf_distrib2:
haftmann@21249
   154
 "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
haftmann@21249
   155
by(simp add:ACI sup_inf_distrib1)
haftmann@21249
   156
haftmann@21249
   157
lemma (in distrib_lattice) inf_sup_distrib1:
haftmann@21249
   158
 "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
haftmann@21249
   159
by(rule distrib_imp2[OF sup_inf_distrib1])
haftmann@21249
   160
haftmann@21249
   161
lemma (in distrib_lattice) inf_sup_distrib2:
haftmann@21249
   162
 "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
haftmann@21249
   163
by(simp add:ACI inf_sup_distrib1)
haftmann@21249
   164
haftmann@21249
   165
lemmas (in distrib_lattice) distrib =
haftmann@21249
   166
  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
haftmann@21249
   167
haftmann@21249
   168
haftmann@21249
   169
subsection {* Least value operator and min/max -- properties *}
haftmann@21249
   170
 
haftmann@21249
   171
(*FIXME: derive more of the min/max laws generically via semilattices*)
haftmann@21249
   172
haftmann@21249
   173
lemma LeastI2_order:
haftmann@21249
   174
  "[| P (x::'a::order);
haftmann@21249
   175
      !!y. P y ==> x <= y;
haftmann@21249
   176
      !!x. [| P x; ALL y. P y --> x \<le> y |] ==> Q x |]
haftmann@21249
   177
   ==> Q (Least P)"
haftmann@21249
   178
  apply (unfold Least_def)
haftmann@21249
   179
  apply (rule theI2)
haftmann@21249
   180
    apply (blast intro: order_antisym)+
haftmann@21249
   181
  done
haftmann@21249
   182
haftmann@21249
   183
lemma Least_equality:
haftmann@21249
   184
    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
haftmann@21249
   185
  apply (simp add: Least_def)
haftmann@21249
   186
  apply (rule the_equality)
haftmann@21249
   187
  apply (auto intro!: order_antisym)
haftmann@21249
   188
  done
haftmann@21249
   189
haftmann@21249
   190
lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
haftmann@21249
   191
  by (simp add: min_def)
haftmann@21249
   192
haftmann@21249
   193
lemma max_leastL: "(!!x. least <= x) ==> max least x = x"
haftmann@21249
   194
  by (simp add: max_def)
haftmann@21249
   195
haftmann@21249
   196
lemma min_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> min x least = least"
haftmann@21249
   197
  apply (simp add: min_def)
haftmann@21249
   198
  apply (blast intro: order_antisym)
haftmann@21249
   199
  done
haftmann@21249
   200
haftmann@21249
   201
lemma max_leastR: "(\<And>x\<Colon>'a\<Colon>order. least \<le> x) \<Longrightarrow> max x least = x"
haftmann@21249
   202
  apply (simp add: max_def)
haftmann@21249
   203
  apply (blast intro: order_antisym)
haftmann@21249
   204
  done
haftmann@21249
   205
haftmann@21249
   206
lemma min_of_mono:
haftmann@21249
   207
    "(!!x y. (f x <= f y) = (x <= y)) ==> min (f m) (f n) = f (min m n)"
haftmann@21249
   208
  by (simp add: min_def)
haftmann@21249
   209
haftmann@21249
   210
lemma max_of_mono:
haftmann@21249
   211
    "(!!x y. (f x <= f y) = (x <= y)) ==> max (f m) (f n) = f (max m n)"
haftmann@21249
   212
  by (simp add: max_def)
haftmann@21249
   213
haftmann@21249
   214
text{* Instantiate locales: *}
haftmann@21249
   215
haftmann@21249
   216
interpretation min_max:
haftmann@21249
   217
  lower_semilattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
haftmann@21249
   218
apply unfold_locales
haftmann@21249
   219
apply(simp add:min_def linorder_not_le order_less_imp_le)
haftmann@21249
   220
apply(simp add:min_def linorder_not_le order_less_imp_le)
haftmann@21249
   221
apply(simp add:min_def linorder_not_le order_less_imp_le)
haftmann@21249
   222
done
haftmann@21249
   223
haftmann@21249
   224
interpretation min_max:
haftmann@21249
   225
  upper_semilattice["op \<le>" "op <" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
haftmann@21249
   226
apply unfold_locales
haftmann@21249
   227
apply(simp add: max_def linorder_not_le order_less_imp_le)
haftmann@21249
   228
apply(simp add: max_def linorder_not_le order_less_imp_le)
haftmann@21249
   229
apply(simp add: max_def linorder_not_le order_less_imp_le)
haftmann@21249
   230
done
haftmann@21249
   231
haftmann@21249
   232
interpretation min_max:
haftmann@21249
   233
  lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
haftmann@21249
   234
  by unfold_locales
haftmann@21249
   235
haftmann@21249
   236
interpretation min_max:
haftmann@21249
   237
  distrib_lattice["op \<le>" "op <" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
haftmann@21249
   238
apply unfold_locales
haftmann@21249
   239
apply(rule_tac x=x and y=y in linorder_le_cases)
haftmann@21249
   240
apply(rule_tac x=x and y=z in linorder_le_cases)
haftmann@21249
   241
apply(rule_tac x=y and y=z in linorder_le_cases)
haftmann@21249
   242
apply(simp add:min_def max_def)
haftmann@21249
   243
apply(simp add:min_def max_def)
haftmann@21249
   244
apply(rule_tac x=y and y=z in linorder_le_cases)
haftmann@21249
   245
apply(simp add:min_def max_def)
haftmann@21249
   246
apply(simp add:min_def max_def)
haftmann@21249
   247
apply(rule_tac x=x and y=z in linorder_le_cases)
haftmann@21249
   248
apply(rule_tac x=y and y=z in linorder_le_cases)
haftmann@21249
   249
apply(simp add:min_def max_def)
haftmann@21249
   250
apply(simp add:min_def max_def)
haftmann@21249
   251
apply(rule_tac x=y and y=z in linorder_le_cases)
haftmann@21249
   252
apply(simp add:min_def max_def)
haftmann@21249
   253
apply(simp add:min_def max_def)
haftmann@21249
   254
done
haftmann@21249
   255
haftmann@21249
   256
lemma le_max_iff_disj: "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)"
haftmann@21249
   257
  apply(simp add:max_def)
haftmann@21249
   258
  apply (insert linorder_linear)
haftmann@21249
   259
  apply (blast intro: order_trans)
haftmann@21249
   260
  done
haftmann@21249
   261
haftmann@21249
   262
lemmas le_maxI1 = min_max.sup_ge1
haftmann@21249
   263
lemmas le_maxI2 = min_max.sup_ge2
haftmann@21249
   264
haftmann@21249
   265
lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
haftmann@21249
   266
  apply (simp add: max_def order_le_less)
haftmann@21249
   267
  apply (insert linorder_less_linear)
haftmann@21249
   268
  apply (blast intro: order_less_trans)
haftmann@21249
   269
  done
haftmann@21249
   270
haftmann@21249
   271
lemma max_less_iff_conj [simp]:
haftmann@21249
   272
    "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
haftmann@21249
   273
  apply (simp add: order_le_less max_def)
haftmann@21249
   274
  apply (insert linorder_less_linear)
haftmann@21249
   275
  apply (blast intro: order_less_trans)
haftmann@21249
   276
  done
haftmann@21249
   277
haftmann@21249
   278
lemma min_less_iff_conj [simp]:
haftmann@21249
   279
    "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
haftmann@21249
   280
  apply (simp add: order_le_less min_def)
haftmann@21249
   281
  apply (insert linorder_less_linear)
haftmann@21249
   282
  apply (blast intro: order_less_trans)
haftmann@21249
   283
  done
haftmann@21249
   284
haftmann@21249
   285
lemma min_le_iff_disj: "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)"
haftmann@21249
   286
  apply (simp add: min_def)
haftmann@21249
   287
  apply (insert linorder_linear)
haftmann@21249
   288
  apply (blast intro: order_trans)
haftmann@21249
   289
  done
haftmann@21249
   290
haftmann@21249
   291
lemma min_less_iff_disj: "!!z::'a::linorder. (min x y < z) = (x < z | y < z)"
haftmann@21249
   292
  apply (simp add: min_def order_le_less)
haftmann@21249
   293
  apply (insert linorder_less_linear)
haftmann@21249
   294
  apply (blast intro: order_less_trans)
haftmann@21249
   295
  done
haftmann@21249
   296
haftmann@21249
   297
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
haftmann@21249
   298
               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
haftmann@21249
   299
haftmann@21249
   300
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
haftmann@21249
   301
               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
haftmann@21249
   302
haftmann@21249
   303
lemma split_min:
haftmann@21249
   304
    "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
haftmann@21249
   305
  by (simp add: min_def)
haftmann@21249
   306
haftmann@21249
   307
lemma split_max:
haftmann@21249
   308
    "P (max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))"
haftmann@21249
   309
  by (simp add: max_def)
haftmann@21249
   310
haftmann@21249
   311
text {* ML legacy bindings *}
haftmann@21249
   312
haftmann@21249
   313
ML {*
haftmann@21249
   314
val Least_def = thm "Least_def";
haftmann@21249
   315
val Least_equality = thm "Least_equality";
haftmann@21249
   316
val min_def = thm "min_def";
haftmann@21249
   317
val min_of_mono = thm "min_of_mono";
haftmann@21249
   318
val max_def = thm "max_def";
haftmann@21249
   319
val max_of_mono = thm "max_of_mono";
haftmann@21249
   320
val min_leastL = thm "min_leastL";
haftmann@21249
   321
val max_leastL = thm "max_leastL";
haftmann@21249
   322
val min_leastR = thm "min_leastR";
haftmann@21249
   323
val max_leastR = thm "max_leastR";
haftmann@21249
   324
val le_max_iff_disj = thm "le_max_iff_disj";
haftmann@21249
   325
val le_maxI1 = thm "le_maxI1";
haftmann@21249
   326
val le_maxI2 = thm "le_maxI2";
haftmann@21249
   327
val less_max_iff_disj = thm "less_max_iff_disj";
haftmann@21249
   328
val max_less_iff_conj = thm "max_less_iff_conj";
haftmann@21249
   329
val min_less_iff_conj = thm "min_less_iff_conj";
haftmann@21249
   330
val min_le_iff_disj = thm "min_le_iff_disj";
haftmann@21249
   331
val min_less_iff_disj = thm "min_less_iff_disj";
haftmann@21249
   332
val split_min = thm "split_min";
haftmann@21249
   333
val split_max = thm "split_max";
haftmann@21249
   334
*}
haftmann@21249
   335
haftmann@21249
   336
end