author | wenzelm |
Fri, 11 May 2007 17:54:36 +0200 | |
changeset 22936 | 284b56463da8 |
parent 22916 | 8caf6da610e2 |
child 23018 | 1d29bc31b0cb |
permissions | -rw-r--r-- |
21249 | 1 |
(* Title: HOL/Lattices.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
*) |
|
5 |
||
22454 | 6 |
header {* Abstract lattices *} |
21249 | 7 |
|
8 |
theory Lattices |
|
9 |
imports Orderings |
|
10 |
begin |
|
11 |
||
12 |
subsection{* Lattices *} |
|
13 |
||
22454 | 14 |
text{* |
15 |
This theory of lattices only defines binary sup and inf |
|
22916 | 16 |
operations. The extension to complete lattices is done in theory |
17 |
@{text FixedPoint}. |
|
22454 | 18 |
*} |
21249 | 19 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
20 |
class lower_semilattice = order + |
21249 | 21 |
fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
22737 | 22 |
assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" |
23 |
and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" |
|
21733 | 24 |
and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" |
21249 | 25 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
26 |
class upper_semilattice = order + |
21249 | 27 |
fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
22737 | 28 |
assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
29 |
and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
21733 | 30 |
and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x" |
21249 | 31 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
32 |
class lattice = lower_semilattice + upper_semilattice |
21249 | 33 |
|
21733 | 34 |
subsubsection{* Intro and elim rules*} |
35 |
||
36 |
context lower_semilattice |
|
37 |
begin |
|
21249 | 38 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
39 |
lemmas antisym_intro [intro!] = antisym |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
40 |
lemmas (in -) [rule del] = antisym_intro |
21249 | 41 |
|
21734 | 42 |
lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
21733 | 43 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
44 |
apply(blast intro: order_trans) |
21733 | 45 |
apply simp |
46 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
47 |
lemmas (in -) [rule del] = le_infI1 |
21249 | 48 |
|
21734 | 49 |
lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x" |
21733 | 50 |
apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
51 |
apply(blast intro: order_trans) |
21733 | 52 |
apply simp |
53 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
54 |
lemmas (in -) [rule del] = le_infI2 |
21733 | 55 |
|
21734 | 56 |
lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b" |
21733 | 57 |
by(blast intro: inf_greatest) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
58 |
lemmas (in -) [rule del] = le_infI |
21249 | 59 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
60 |
lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P" |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
61 |
by (blast intro: order_trans) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
62 |
lemmas (in -) [rule del] = le_infE |
21249 | 63 |
|
21734 | 64 |
lemma le_inf_iff [simp]: |
21733 | 65 |
"x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)" |
66 |
by blast |
|
67 |
||
21734 | 68 |
lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)" |
22168 | 69 |
by(blast dest:eq_iff[THEN iffD1]) |
21249 | 70 |
|
21733 | 71 |
end |
72 |
||
73 |
||
74 |
context upper_semilattice |
|
75 |
begin |
|
21249 | 76 |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
77 |
lemmas antisym_intro [intro!] = antisym |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
78 |
lemmas (in -) [rule del] = antisym_intro |
21249 | 79 |
|
21734 | 80 |
lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
21733 | 81 |
apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
82 |
apply(blast intro: order_trans) |
21733 | 83 |
apply simp |
84 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
85 |
lemmas (in -) [rule del] = le_supI1 |
21249 | 86 |
|
21734 | 87 |
lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b" |
21733 | 88 |
apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b") |
22384
33a46e6c7f04
prefix of class interpretation not mandatory any longer
haftmann
parents:
22168
diff
changeset
|
89 |
apply(blast intro: order_trans) |
21733 | 90 |
apply simp |
91 |
done |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
92 |
lemmas (in -) [rule del] = le_supI2 |
21733 | 93 |
|
21734 | 94 |
lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x" |
21733 | 95 |
by(blast intro: sup_least) |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
96 |
lemmas (in -) [rule del] = le_supI |
21249 | 97 |
|
21734 | 98 |
lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P" |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
99 |
by (blast intro: order_trans) |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
100 |
lemmas (in -) [rule del] = le_supE |
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
101 |
|
21249 | 102 |
|
21734 | 103 |
lemma ge_sup_conv[simp]: |
21733 | 104 |
"x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)" |
105 |
by blast |
|
106 |
||
21734 | 107 |
lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)" |
22168 | 108 |
by(blast dest:eq_iff[THEN iffD1]) |
21734 | 109 |
|
21733 | 110 |
end |
111 |
||
112 |
||
113 |
subsubsection{* Equational laws *} |
|
21249 | 114 |
|
115 |
||
21733 | 116 |
context lower_semilattice |
117 |
begin |
|
118 |
||
119 |
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)" |
|
120 |
by blast |
|
121 |
||
122 |
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)" |
|
123 |
by blast |
|
124 |
||
125 |
lemma inf_idem[simp]: "x \<sqinter> x = x" |
|
126 |
by blast |
|
127 |
||
128 |
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
|
129 |
by blast |
|
130 |
||
131 |
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
|
132 |
by blast |
|
133 |
||
134 |
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y" |
|
135 |
by blast |
|
136 |
||
137 |
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
|
138 |
by blast |
|
139 |
||
140 |
lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem |
|
141 |
||
142 |
end |
|
143 |
||
144 |
||
145 |
context upper_semilattice |
|
146 |
begin |
|
21249 | 147 |
|
21733 | 148 |
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)" |
149 |
by blast |
|
150 |
||
151 |
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)" |
|
152 |
by blast |
|
153 |
||
154 |
lemma sup_idem[simp]: "x \<squnion> x = x" |
|
155 |
by blast |
|
156 |
||
157 |
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
|
158 |
by blast |
|
159 |
||
160 |
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
|
161 |
by blast |
|
162 |
||
163 |
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y" |
|
164 |
by blast |
|
21249 | 165 |
|
21733 | 166 |
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
167 |
by blast |
|
168 |
||
169 |
lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem |
|
170 |
||
171 |
end |
|
21249 | 172 |
|
21733 | 173 |
context lattice |
174 |
begin |
|
175 |
||
176 |
lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x" |
|
177 |
by(blast intro: antisym inf_le1 inf_greatest sup_ge1) |
|
178 |
||
179 |
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x" |
|
180 |
by(blast intro: antisym sup_ge1 sup_least inf_le1) |
|
181 |
||
21734 | 182 |
lemmas ACI = inf_ACI sup_ACI |
183 |
||
22454 | 184 |
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
185 |
||
21734 | 186 |
text{* Towards distributivity *} |
21249 | 187 |
|
21734 | 188 |
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
189 |
by blast |
|
190 |
||
191 |
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)" |
|
192 |
by blast |
|
193 |
||
194 |
||
195 |
text{* If you have one of them, you have them all. *} |
|
21249 | 196 |
|
21733 | 197 |
lemma distrib_imp1: |
21249 | 198 |
assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
199 |
shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
|
200 |
proof- |
|
201 |
have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) |
|
202 |
also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) |
|
203 |
also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
|
204 |
by(simp add:inf_sup_absorb inf_commute) |
|
205 |
also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
|
206 |
finally show ?thesis . |
|
207 |
qed |
|
208 |
||
21733 | 209 |
lemma distrib_imp2: |
21249 | 210 |
assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
211 |
shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
|
212 |
proof- |
|
213 |
have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) |
|
214 |
also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) |
|
215 |
also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
|
216 |
by(simp add:sup_inf_absorb sup_commute) |
|
217 |
also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
|
218 |
finally show ?thesis . |
|
219 |
qed |
|
220 |
||
21734 | 221 |
(* seems unused *) |
222 |
lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z" |
|
223 |
by blast |
|
224 |
||
21733 | 225 |
end |
21249 | 226 |
|
227 |
||
228 |
subsection{* Distributive lattices *} |
|
229 |
||
22454 | 230 |
class distrib_lattice = lattice + |
21249 | 231 |
assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
232 |
||
21733 | 233 |
context distrib_lattice |
234 |
begin |
|
235 |
||
236 |
lemma sup_inf_distrib2: |
|
21249 | 237 |
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)" |
238 |
by(simp add:ACI sup_inf_distrib1) |
|
239 |
||
21733 | 240 |
lemma inf_sup_distrib1: |
21249 | 241 |
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
242 |
by(rule distrib_imp2[OF sup_inf_distrib1]) |
|
243 |
||
21733 | 244 |
lemma inf_sup_distrib2: |
21249 | 245 |
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
246 |
by(simp add:ACI inf_sup_distrib1) |
|
247 |
||
21733 | 248 |
lemmas distrib = |
21249 | 249 |
sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
250 |
||
21733 | 251 |
end |
252 |
||
21249 | 253 |
|
22454 | 254 |
subsection {* Uniqueness of inf and sup *} |
255 |
||
22737 | 256 |
lemma (in lower_semilattice) inf_unique: |
22454 | 257 |
fixes f (infixl "\<triangle>" 70) |
22737 | 258 |
assumes le1: "\<And>x y. x \<triangle> y \<^loc>\<le> x" and le2: "\<And>x y. x \<triangle> y \<^loc>\<le> y" |
259 |
and greatest: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" |
|
260 |
shows "x \<sqinter> y = x \<triangle> y" |
|
22454 | 261 |
proof (rule antisym) |
22737 | 262 |
show "x \<triangle> y \<^loc>\<le> x \<sqinter> y" by (rule le_infI) (rule le1 le2) |
22454 | 263 |
next |
22737 | 264 |
have leI: "\<And>x y z. x \<^loc>\<le> y \<Longrightarrow> x \<^loc>\<le> z \<Longrightarrow> x \<^loc>\<le> y \<triangle> z" by (blast intro: greatest) |
265 |
show "x \<sqinter> y \<^loc>\<le> x \<triangle> y" by (rule leI) simp_all |
|
22454 | 266 |
qed |
267 |
||
22737 | 268 |
lemma (in upper_semilattice) sup_unique: |
22454 | 269 |
fixes f (infixl "\<nabla>" 70) |
22737 | 270 |
assumes ge1 [simp]: "\<And>x y. x \<^loc>\<le> x \<nabla> y" and ge2: "\<And>x y. y \<^loc>\<le> x \<nabla> y" |
271 |
and least: "\<And>x y z. y \<^loc>\<le> x \<Longrightarrow> z \<^loc>\<le> x \<Longrightarrow> y \<nabla> z \<^loc>\<le> x" |
|
272 |
shows "x \<squnion> y = x \<nabla> y" |
|
22454 | 273 |
proof (rule antisym) |
22737 | 274 |
show "x \<squnion> y \<^loc>\<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2) |
22454 | 275 |
next |
22737 | 276 |
have leI: "\<And>x y z. x \<^loc>\<le> z \<Longrightarrow> y \<^loc>\<le> z \<Longrightarrow> x \<nabla> y \<^loc>\<le> z" by (blast intro: least) |
277 |
show "x \<nabla> y \<^loc>\<le> x \<squnion> y" by (rule leI) simp_all |
|
22454 | 278 |
qed |
279 |
||
280 |
||
22916 | 281 |
subsection {* @{const min}/@{const max} on linear orders as |
282 |
special case of @{const inf}/@{const sup} *} |
|
283 |
||
284 |
lemma (in linorder) distrib_lattice_min_max: |
|
285 |
"distrib_lattice_pred (op \<^loc>\<le>) (op \<^loc><) min max" |
|
286 |
proof unfold_locales |
|
287 |
have aux: "\<And>x y \<Colon> 'a. x \<^loc>< y \<Longrightarrow> y \<^loc>\<le> x \<Longrightarrow> x = y" |
|
288 |
by (auto simp add: less_le antisym) |
|
289 |
fix x y z |
|
290 |
show "max x (min y z) = min (max x y) (max x z)" |
|
291 |
unfolding min_def max_def |
|
292 |
by (auto simp add: intro: antisym, unfold not_le, |
|
293 |
auto intro: less_trans le_less_trans aux) |
|
294 |
qed (auto simp add: min_def max_def not_le less_imp_le) |
|
21249 | 295 |
|
296 |
interpretation min_max: |
|
22454 | 297 |
distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max] |
22916 | 298 |
by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max]) |
21249 | 299 |
|
22454 | 300 |
lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
301 |
by (rule ext)+ auto |
|
21733 | 302 |
|
22454 | 303 |
lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)" |
304 |
by (rule ext)+ auto |
|
21733 | 305 |
|
21249 | 306 |
lemmas le_maxI1 = min_max.sup_ge1 |
307 |
lemmas le_maxI2 = min_max.sup_ge2 |
|
21381 | 308 |
|
21249 | 309 |
lemmas max_ac = min_max.sup_assoc min_max.sup_commute |
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
310 |
mk_left_commute [of max, OF min_max.sup_assoc min_max.sup_commute] |
21249 | 311 |
|
312 |
lemmas min_ac = min_max.inf_assoc min_max.inf_commute |
|
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22384
diff
changeset
|
313 |
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute] |
21249 | 314 |
|
22454 | 315 |
text {* |
316 |
Now we have inherited antisymmetry as an intro-rule on all |
|
317 |
linear orders. This is a problem because it applies to bool, which is |
|
318 |
undesirable. |
|
319 |
*} |
|
320 |
||
321 |
lemmas [rule del] = min_max.antisym_intro min_max.le_infI min_max.le_supI |
|
322 |
min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2 |
|
323 |
min_max.le_infI1 min_max.le_infI2 |
|
324 |
||
325 |
||
326 |
subsection {* Bool as lattice *} |
|
327 |
||
328 |
instance bool :: distrib_lattice |
|
329 |
inf_bool_eq: "inf P Q \<equiv> P \<and> Q" |
|
330 |
sup_bool_eq: "sup P Q \<equiv> P \<or> Q" |
|
331 |
by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) |
|
332 |
||
333 |
||
334 |
text {* duplicates *} |
|
335 |
||
336 |
lemmas inf_aci = inf_ACI |
|
337 |
lemmas sup_aci = sup_ACI |
|
338 |
||
21249 | 339 |
end |