src/HOL/Lattices.thy
 author nipkow Sun Dec 10 07:12:26 2006 +0100 (2006-12-10) changeset 21733 131dd2a27137 parent 21619 dea0914773f7 child 21734 283461c15fa7 permissions -rw-r--r--
Modified lattice locale
1 (*  Title:      HOL/Lattices.thy
2     ID:         \$Id\$
3     Author:     Tobias Nipkow
4 *)
6 header {* Lattices via Locales *}
8 theory Lattices
9 imports Orderings
10 begin
12 subsection{* Lattices *}
14 text{* This theory of lattice locales only defines binary sup and inf
15 operations. The extension to finite sets is done in theory @{text
16 Finite_Set}. In the longer term it may be better to define arbitrary
17 sups and infs via @{text THE}. *}
19 locale lower_semilattice = partial_order +
20   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
21   assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
22   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
24 locale upper_semilattice = partial_order +
25   fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
26   assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
27   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
29 locale lattice = lower_semilattice + upper_semilattice
31 subsubsection{* Intro and elim rules*}
33 context lower_semilattice
34 begin
36 lemmas antisym_intro[intro!] = antisym
38 lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
39 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
40  apply(blast intro:trans)
41 apply simp
42 done
44 lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
45 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
46  apply(blast intro:trans)
47 apply simp
48 done
50 lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
51 by(blast intro: inf_greatest)
53 lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
54 by(blast intro: trans)
56 lemma less_eq_inf_conv [simp]:
57  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
58 by blast
60 lemmas below_inf_conv = less_eq_inf_conv
61   -- {* a duplicate for backward compatibility *}
63 end
66 context upper_semilattice
67 begin
69 lemmas antisym_intro[intro!] = antisym
71 lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
72 apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
73  apply(blast intro:trans)
74 apply simp
75 done
77 lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
78 apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
79  apply(blast intro:trans)
80 apply simp
81 done
83 lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
84 by(blast intro: sup_least)
86 lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
87 by(blast intro: trans)
89 lemma above_sup_conv[simp]:
90  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
91 by blast
93 end
96 subsubsection{* Equational laws *}
99 context lower_semilattice
100 begin
102 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
103 by blast
105 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
106 by blast
108 lemma inf_idem[simp]: "x \<sqinter> x = x"
109 by blast
111 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
112 by blast
114 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
115 by blast
117 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
118 by blast
120 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
121 by blast
123 lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
125 end
128 context upper_semilattice
129 begin
131 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
132 by blast
134 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
135 by blast
137 lemma sup_idem[simp]: "x \<squnion> x = x"
138 by blast
140 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
141 by blast
143 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
144 by blast
146 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
147 by blast
149 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
150 by blast
152 lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
154 end
156 context lattice
157 begin
159 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
160 by(blast intro: antisym inf_le1 inf_greatest sup_ge1)
162 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
163 by(blast intro: antisym sup_ge1 sup_least inf_le1)
165 lemmas (in lattice) ACI = inf_ACI sup_ACI
167 text{* Towards distributivity: if you have one of them, you have them all. *}
169 lemma distrib_imp1:
170 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
171 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
172 proof-
173   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
174   also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
175   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
177   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
178   finally show ?thesis .
179 qed
181 lemma distrib_imp2:
182 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
183 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
184 proof-
185   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
186   also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
187   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
189   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
190   finally show ?thesis .
191 qed
193 end
196 subsection{* Distributive lattices *}
198 locale distrib_lattice = lattice +
199   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
201 context distrib_lattice
202 begin
204 lemma sup_inf_distrib2:
205  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
208 lemma inf_sup_distrib1:
209  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
210 by(rule distrib_imp2[OF sup_inf_distrib1])
212 lemma inf_sup_distrib2:
213  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
216 lemmas distrib =
217   sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
219 end
222 subsection {* min/max on linear orders as special case of inf/sup *}
224 interpretation min_max:
225   distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
226 apply unfold_locales
227 apply (simp add: min_def linorder_not_le order_less_imp_le)
228 apply (simp add: min_def linorder_not_le order_less_imp_le)
229 apply (simp add: min_def linorder_not_le order_less_imp_le)
230 apply (simp add: max_def linorder_not_le order_less_imp_le)
231 apply (simp add: max_def linorder_not_le order_less_imp_le)
232 unfolding min_def max_def by auto
234 text{* Now we have inherited antisymmetry as an intro-rule on all
235 linear orders. This is a problem because it applies to bool, which is
236 undesirable. *}
238 declare
239  min_max.antisym_intro[rule del]
240  min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
241  min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
242  min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
243  min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
245 lemmas le_maxI1 = min_max.sup_ge1
246 lemmas le_maxI2 = min_max.sup_ge2
248 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
249                mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
251 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
252                mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
254 text {* ML legacy bindings *}
256 ML {*
257 val Least_def = thm "Least_def";
258 val Least_equality = thm "Least_equality";
259 val min_def = thm "min_def";
260 val min_of_mono = thm "min_of_mono";
261 val max_def = thm "max_def";
262 val max_of_mono = thm "max_of_mono";
263 val min_leastL = thm "min_leastL";
264 val max_leastL = thm "max_leastL";
265 val min_leastR = thm "min_leastR";
266 val max_leastR = thm "max_leastR";
267 val le_max_iff_disj = thm "le_max_iff_disj";
268 val le_maxI1 = thm "le_maxI1";
269 val le_maxI2 = thm "le_maxI2";
270 val less_max_iff_disj = thm "less_max_iff_disj";
271 val max_less_iff_conj = thm "max_less_iff_conj";
272 val min_less_iff_conj = thm "min_less_iff_conj";
273 val min_le_iff_disj = thm "min_le_iff_disj";
274 val min_less_iff_disj = thm "min_less_iff_disj";
275 val split_min = thm "split_min";
276 val split_max = thm "split_max";
277 *}
279 end