178 by (fact inf.commute) |
178 by (fact inf.commute) |
179 |
179 |
180 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
180 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)" |
181 by (fact inf.left_commute) |
181 by (fact inf.left_commute) |
182 |
182 |
183 lemma inf_idem (*[simp]*): "x \<sqinter> x = x" |
183 lemma inf_idem [simp]: "x \<sqinter> x = x" |
184 by (fact inf.idem) |
184 by (fact inf.idem) |
185 |
185 |
186 lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
186 lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y" |
187 by (fact inf.left_idem) |
187 by (fact inf.left_idem) |
188 |
188 |
189 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
189 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x" |
190 by (rule antisym) auto |
190 by (rule antisym) auto |
191 |
191 |
217 by (fact sup.commute) |
217 by (fact sup.commute) |
218 |
218 |
219 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
219 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)" |
220 by (fact sup.left_commute) |
220 by (fact sup.left_commute) |
221 |
221 |
222 lemma sup_idem (*[simp]*): "x \<squnion> x = x" |
222 lemma sup_idem [simp]: "x \<squnion> x = x" |
223 by (fact sup.idem) |
223 by (fact sup.idem) |
224 |
224 |
225 lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
225 lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y" |
226 by (fact sup.left_idem) |
226 by (fact sup.left_idem) |
227 |
227 |
228 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
228 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x" |
229 by (rule antisym) auto |
229 by (rule antisym) auto |
230 |
230 |
241 lemma dual_lattice: |
241 lemma dual_lattice: |
242 "class.lattice sup (op \<ge>) (op >) inf" |
242 "class.lattice sup (op \<ge>) (op >) inf" |
243 by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order) |
243 by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order) |
244 (unfold_locales, auto) |
244 (unfold_locales, auto) |
245 |
245 |
246 lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x" |
246 lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x" |
247 by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
247 by (blast intro: antisym inf_le1 inf_greatest sup_ge1) |
248 |
248 |
249 lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x" |
249 lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x" |
250 by (blast intro: antisym sup_ge1 sup_least inf_le1) |
250 by (blast intro: antisym sup_ge1 sup_least inf_le1) |
251 |
251 |
252 lemmas inf_sup_aci = inf_aci sup_aci |
252 lemmas inf_sup_aci = inf_aci sup_aci |
253 |
253 |
254 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
254 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 |
265 |
265 |
266 lemma distrib_imp1: |
266 lemma distrib_imp1: |
267 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
267 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
268 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
268 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
269 proof- |
269 proof- |
270 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb) |
270 have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp |
271 also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc) |
271 also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" |
|
272 by (simp add: D inf_commute sup_assoc del: sup_inf_absorb) |
272 also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
273 also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)" |
273 by(simp add:inf_sup_absorb inf_commute) |
274 by(simp add:inf_sup_absorb inf_commute) |
274 also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
275 also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D) |
275 finally show ?thesis . |
276 finally show ?thesis . |
276 qed |
277 qed |
277 |
278 |
278 lemma distrib_imp2: |
279 lemma distrib_imp2: |
279 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
280 assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)" |
280 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
281 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" |
281 proof- |
282 proof- |
282 have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb) |
283 have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp |
283 also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc) |
284 also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" |
|
285 by (simp add: D sup_commute inf_assoc del: inf_sup_absorb) |
284 also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
286 also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)" |
285 by(simp add:sup_inf_absorb sup_commute) |
287 by(simp add:sup_inf_absorb sup_commute) |
286 also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
288 also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D) |
287 finally show ?thesis . |
289 finally show ?thesis . |
288 qed |
290 qed |
437 lemma dual_boolean_algebra: |
439 lemma dual_boolean_algebra: |
438 "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>" |
440 "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>" |
439 by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) |
441 by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) |
440 (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) |
442 (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) |
441 |
443 |
442 lemma compl_inf_bot (*[simp]*): |
444 lemma compl_inf_bot [simp]: |
443 "- x \<sqinter> x = \<bottom>" |
445 "- x \<sqinter> x = \<bottom>" |
444 by (simp add: inf_commute inf_compl_bot) |
446 by (simp add: inf_commute inf_compl_bot) |
445 |
447 |
446 lemma compl_sup_top (*[simp]*): |
448 lemma compl_sup_top [simp]: |
447 "- x \<squnion> x = \<top>" |
449 "- x \<squnion> x = \<top>" |
448 by (simp add: sup_commute sup_compl_top) |
450 by (simp add: sup_commute sup_compl_top) |
449 |
451 |
450 lemma compl_unique: |
452 lemma compl_unique: |
451 assumes "x \<sqinter> y = \<bottom>" |
453 assumes "x \<sqinter> y = \<bottom>" |
523 then have "- x \<sqinter> - y = - y" by simp |
525 then have "- x \<sqinter> - y = - y" by simp |
524 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
526 then have "- y \<sqinter> - x = - y" by (simp only: inf_commute) |
525 then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf) |
527 then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf) |
526 qed |
528 qed |
527 |
529 |
528 lemma compl_le_compl_iff (*[simp]*): |
530 lemma compl_le_compl_iff [simp]: |
529 "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x" |
531 "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x" |
530 by (auto dest: compl_mono) |
532 by (auto dest: compl_mono) |
531 |
533 |
532 lemma compl_le_swap1: |
534 lemma compl_le_swap1: |
533 assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y" |
535 assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y" |