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