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