src/HOL/Lattices.thy
author haftmann
Wed Nov 15 17:05:40 2006 +0100 (2006-11-15)
changeset 21381 79e065f2be95
parent 21312 1d39091a3208
child 21619 dea0914773f7
permissions -rw-r--r--
reworking of min/max lemmas
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@21381
   169
subsection {* min/max on linear orders as special case of inf/sup *}
haftmann@21249
   170
haftmann@21249
   171
interpretation min_max:
haftmann@21381
   172
  distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
haftmann@21249
   173
apply unfold_locales
haftmann@21381
   174
apply (simp add: min_def linorder_not_le order_less_imp_le)
haftmann@21381
   175
apply (simp add: min_def linorder_not_le order_less_imp_le)
haftmann@21381
   176
apply (simp add: min_def linorder_not_le order_less_imp_le)
haftmann@21381
   177
apply (simp add: max_def linorder_not_le order_less_imp_le)
haftmann@21381
   178
apply (simp add: max_def linorder_not_le order_less_imp_le)
haftmann@21381
   179
unfolding min_def max_def by auto
haftmann@21249
   180
haftmann@21249
   181
lemmas le_maxI1 = min_max.sup_ge1
haftmann@21249
   182
lemmas le_maxI2 = min_max.sup_ge2
haftmann@21381
   183
 
haftmann@21249
   184
lemmas max_ac = min_max.sup_assoc min_max.sup_commute
haftmann@21249
   185
               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
haftmann@21249
   186
haftmann@21249
   187
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
haftmann@21249
   188
               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
haftmann@21249
   189
haftmann@21249
   190
text {* ML legacy bindings *}
haftmann@21249
   191
haftmann@21249
   192
ML {*
haftmann@21249
   193
val Least_def = thm "Least_def";
haftmann@21249
   194
val Least_equality = thm "Least_equality";
haftmann@21249
   195
val min_def = thm "min_def";
haftmann@21249
   196
val min_of_mono = thm "min_of_mono";
haftmann@21249
   197
val max_def = thm "max_def";
haftmann@21249
   198
val max_of_mono = thm "max_of_mono";
haftmann@21249
   199
val min_leastL = thm "min_leastL";
haftmann@21249
   200
val max_leastL = thm "max_leastL";
haftmann@21249
   201
val min_leastR = thm "min_leastR";
haftmann@21249
   202
val max_leastR = thm "max_leastR";
haftmann@21249
   203
val le_max_iff_disj = thm "le_max_iff_disj";
haftmann@21249
   204
val le_maxI1 = thm "le_maxI1";
haftmann@21249
   205
val le_maxI2 = thm "le_maxI2";
haftmann@21249
   206
val less_max_iff_disj = thm "less_max_iff_disj";
haftmann@21249
   207
val max_less_iff_conj = thm "max_less_iff_conj";
haftmann@21249
   208
val min_less_iff_conj = thm "min_less_iff_conj";
haftmann@21249
   209
val min_le_iff_disj = thm "min_le_iff_disj";
haftmann@21249
   210
val min_less_iff_disj = thm "min_less_iff_disj";
haftmann@21249
   211
val split_min = thm "split_min";
haftmann@21249
   212
val split_max = thm "split_max";
haftmann@21249
   213
*}
haftmann@21249
   214
haftmann@21249
   215
end