src/HOL/Library/Finite_Lattice.thy
author hoelzl
Thu, 17 Jan 2013 11:59:12 +0100
changeset 50936 b28f258ebc1a
parent 50634 009a9fdabbad
child 51115 7dbd6832a689
permissions -rw-r--r--
countablility of finite subsets and rational numbers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50634
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     1
(* Author: Alessandro Coglio *)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     2
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     3
theory Finite_Lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     4
imports Product_Lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     5
begin
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     6
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     7
text {* A non-empty finite lattice is a complete lattice.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     8
Since types are never empty in Isabelle/HOL,
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
     9
a type of classes @{class finite} and @{class lattice}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    10
should also have class @{class complete_lattice}.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    11
A type class is defined
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    12
that extends classes @{class finite} and @{class lattice}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    13
with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    14
along with assumptions that define these operators
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    15
in terms of the ones of classes @{class finite} and @{class lattice}.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    16
The resulting class is a subclass of @{class complete_lattice}.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    17
Classes @{class bot} and @{class top} already include assumptions that suffice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    18
to define the operators @{const bot} and @{const top} (as proved below),
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    19
and so no explicit assumptions on these two operators are needed
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    20
in the following type class.%
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    21
\footnote{The Isabelle/HOL library does not provide
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    22
syntactic classes for the operators @{const bot} and @{const top}.} *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    23
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    24
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    25
assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    26
assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    27
-- "No explicit assumptions on @{const bot} or @{const top}."
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    28
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    29
instance finite_lattice_complete \<subseteq> bounded_lattice ..
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    30
-- "This subclass relation eases the proof of the next two lemmas."
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    31
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    32
lemma finite_lattice_complete_bot_def:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    33
  "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    34
by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    35
-- "Derived definition of @{const bot}."
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    36
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    37
lemma finite_lattice_complete_top_def:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    38
  "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    39
by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    40
-- "Derived definition of @{const top}."
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    41
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    42
text {* The definitional assumptions
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    43
on the operators @{const Inf} and @{const Sup}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    44
of class @{class finite_lattice_complete}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    45
ensure that they yield infimum and supremum,
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    46
as required for a complete lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    47
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    48
lemma finite_lattice_complete_Inf_lower:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    49
  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    50
unfolding Inf_def by (metis finite_code le_inf_iff fold_inf_le_inf)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    51
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    52
lemma finite_lattice_complete_Inf_greatest:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    53
  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<le> x \<Longrightarrow> z \<le> Inf A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    54
unfolding Inf_def by (metis finite_code inf_le_fold_inf inf_top_right)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    55
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    56
lemma finite_lattice_complete_Sup_upper:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    57
  "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Sup A \<ge> x"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    58
unfolding Sup_def by (metis finite_code le_sup_iff sup_le_fold_sup)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    59
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    60
lemma finite_lattice_complete_Sup_least:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    61
  "\<forall>x::'a::finite_lattice_complete \<in> A. z \<ge> x \<Longrightarrow> z \<ge> Sup A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    62
unfolding Sup_def by (metis finite_code fold_sup_le_sup sup_bot_right)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    63
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    64
instance finite_lattice_complete \<subseteq> complete_lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    65
proof
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    66
qed (auto simp:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    67
 finite_lattice_complete_Inf_lower
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    68
 finite_lattice_complete_Inf_greatest
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    69
 finite_lattice_complete_Sup_upper
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    70
 finite_lattice_complete_Sup_least)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    71
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    72
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    73
text {* The product of two finite lattices is already a finite lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    74
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    75
lemma finite_Inf_prod:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    76
  "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    77
  Finite_Set.fold inf top A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    78
by (metis Inf_fold_inf finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    79
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    80
lemma finite_Sup_prod:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    81
  "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    82
  Finite_Set.fold sup bot A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    83
by (metis Sup_fold_sup finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    84
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    85
instance prod ::
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    86
  (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    87
proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    88
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    89
text {* Functions with a finite domain and with a finite lattice as codomain
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    90
already form a finite lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    91
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    92
lemma finite_Inf_fun:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    93
  "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    94
  Finite_Set.fold inf top A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    95
by (metis Inf_fold_inf finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    96
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    97
lemma finite_Sup_fun:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    98
  "Sup (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
    99
  Finite_Set.fold sup bot A"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   100
by (metis Sup_fold_sup finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   101
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   102
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   103
proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   104
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   105
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   106
subsection {* Finite Distributive Lattices *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   107
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   108
text {* A finite distributive lattice is a complete lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   109
whose @{const inf} and @{const sup} operators
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   110
distribute over @{const Sup} and @{const Inf}. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   111
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   112
class finite_distrib_lattice_complete =
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   113
  distrib_lattice + finite_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   114
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   115
lemma finite_distrib_lattice_complete_sup_Inf:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   116
  "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   117
apply (rule finite_induct)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   118
apply (metis finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   119
apply (metis INF_empty Inf_empty sup_top_right)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   120
apply (metis INF_insert Inf_insert sup_inf_distrib1)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   121
done
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   122
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   123
lemma finite_distrib_lattice_complete_inf_Sup:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   124
  "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   125
apply (rule finite_induct)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   126
apply (metis finite_code)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   127
apply (metis SUP_empty Sup_empty inf_bot_right)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   128
apply (metis SUP_insert Sup_insert inf_sup_distrib1)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   129
done
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   130
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   131
instance finite_distrib_lattice_complete \<subseteq> complete_distrib_lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   132
proof
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   133
qed (auto simp:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   134
 finite_distrib_lattice_complete_sup_Inf
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   135
 finite_distrib_lattice_complete_inf_Sup)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   136
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   137
text {* The product of two finite distributive lattices
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   138
is already a finite distributive lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   139
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   140
instance prod ::
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   141
  (finite_distrib_lattice_complete, finite_distrib_lattice_complete)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   142
  finite_distrib_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   143
..
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   144
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   145
text {* Functions with a finite domain
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   146
and with a finite distributive lattice as codomain
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   147
already form a finite distributive lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   148
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   149
instance "fun" ::
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   150
  (finite, finite_distrib_lattice_complete) finite_distrib_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   151
..
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   152
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   153
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   154
subsection {* Linear Orders *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   155
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   156
text {* A linear order is a distributive lattice.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   157
Since in Isabelle/HOL
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   158
a subclass must have all the parameters of its superclasses,
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   159
class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   160
So class @{class linorder} is extended with
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   161
the operators @{const inf} and @{const sup},
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   162
along with assumptions that define these operators
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   163
in terms of the ones of class @{class linorder}.
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   164
The resulting class is a subclass of @{class distrib_lattice}. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   165
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   166
class linorder_lattice = linorder + inf + sup +
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   167
assumes inf_def: "inf x y = (if x \<le> y then x else y)"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   168
assumes sup_def: "sup x y = (if x \<ge> y then x else y)"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   169
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   170
text {* The definitional assumptions
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   171
on the operators @{const inf} and @{const sup}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   172
of class @{class linorder_lattice}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   173
ensure that they yield infimum and supremum,
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   174
and that they distribute over each other,
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   175
as required for a distributive lattice. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   176
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   177
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   178
unfolding inf_def by (metis (full_types) linorder_linear)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   179
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   180
lemma linorder_lattice_inf_le2: "inf (x::'a::linorder_lattice) y \<le> y"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   181
unfolding inf_def by (metis (full_types) linorder_linear)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   182
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   183
lemma linorder_lattice_inf_greatest:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   184
  "(x::'a::linorder_lattice) \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> inf y z"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   185
unfolding inf_def by (metis (full_types))
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   186
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   187
lemma linorder_lattice_sup_ge1: "sup (x::'a::linorder_lattice) y \<ge> x"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   188
unfolding sup_def by (metis (full_types) linorder_linear)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   189
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   190
lemma linorder_lattice_sup_ge2: "sup (x::'a::linorder_lattice) y \<ge> y"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   191
unfolding sup_def by (metis (full_types) linorder_linear)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   192
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   193
lemma linorder_lattice_sup_least:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   194
  "(x::'a::linorder_lattice) \<ge> y \<Longrightarrow> x \<ge> z \<Longrightarrow> x \<ge> sup y z"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   195
by (auto simp: sup_def)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   196
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   197
lemma linorder_lattice_sup_inf_distrib1:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   198
  "sup (x::'a::linorder_lattice) (inf y z) = inf (sup x y) (sup x z)"
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   199
by (auto simp: inf_def sup_def)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   200
 
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   201
instance linorder_lattice \<subseteq> distrib_lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   202
proof                                                     
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   203
qed (auto simp:
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   204
 linorder_lattice_inf_le1
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   205
 linorder_lattice_inf_le2
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   206
 linorder_lattice_inf_greatest
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   207
 linorder_lattice_sup_ge1
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   208
 linorder_lattice_sup_ge2
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   209
 linorder_lattice_sup_least
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   210
 linorder_lattice_sup_inf_distrib1)
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   211
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   212
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   213
subsection {* Finite Linear Orders *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   214
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   215
text {* A (non-empty) finite linear order is a complete linear order. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   216
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   217
class finite_linorder_complete = linorder_lattice + finite_lattice_complete
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   218
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   219
instance finite_linorder_complete \<subseteq> complete_linorder ..
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   220
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   221
text {* A (non-empty) finite linear order is a complete lattice
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   222
whose @{const inf} and @{const sup} operators
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   223
distribute over @{const Sup} and @{const Inf}. *}
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   224
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   225
instance finite_linorder_complete \<subseteq> finite_distrib_lattice_complete ..
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   226
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   227
009a9fdabbad new theory Library/Finite_Lattice
nipkow
parents:
diff changeset
   228
end