250 |
255 |
251 lemma inf_sup_distrib2: |
256 lemma inf_sup_distrib2: |
252 "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
257 "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)" |
253 by(simp add:ACI inf_sup_distrib1) |
258 by(simp add:ACI inf_sup_distrib1) |
254 |
259 |
|
260 lemma dual_distrib_lattice: |
|
261 "distrib_lattice (op \<ge>) (op >) sup inf" |
|
262 by (rule distrib_lattice.intro, rule dual_lattice) |
|
263 (unfold_locales, fact inf_sup_distrib1) |
|
264 |
255 lemmas distrib = |
265 lemmas distrib = |
256 sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
266 sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 |
|
267 |
|
268 end |
|
269 |
|
270 |
|
271 subsection {* Boolean algebras *} |
|
272 |
|
273 class boolean_algebra = distrib_lattice + top + bot + minus + uminus + |
|
274 assumes inf_compl_bot: "x \<sqinter> - x = bot" |
|
275 and sup_compl_top: "x \<squnion> - x = top" |
|
276 assumes diff_eq: "x - y = x \<sqinter> - y" |
|
277 begin |
|
278 |
|
279 lemma dual_boolean_algebra: |
|
280 "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) top bot" |
|
281 by (rule boolean_algebra.intro, rule dual_distrib_lattice) |
|
282 (unfold_locales, |
|
283 auto simp add: inf_compl_bot sup_compl_top diff_eq less_le_not_le) |
|
284 |
|
285 lemma compl_inf_bot: |
|
286 "- x \<sqinter> x = bot" |
|
287 by (simp add: inf_commute inf_compl_bot) |
|
288 |
|
289 lemma compl_sup_top: |
|
290 "- x \<squnion> x = top" |
|
291 by (simp add: sup_commute sup_compl_top) |
|
292 |
|
293 lemma inf_bot_left [simp]: |
|
294 "bot \<sqinter> x = bot" |
|
295 by (rule inf_absorb1) simp |
|
296 |
|
297 lemma inf_bot_right [simp]: |
|
298 "x \<sqinter> bot = bot" |
|
299 by (rule inf_absorb2) simp |
|
300 |
|
301 lemma sup_top_left [simp]: |
|
302 "top \<squnion> x = top" |
|
303 by (rule sup_absorb1) simp |
|
304 |
|
305 lemma sup_top_right [simp]: |
|
306 "x \<squnion> top = top" |
|
307 by (rule sup_absorb2) simp |
|
308 |
|
309 lemma inf_top_left [simp]: |
|
310 "top \<sqinter> x = x" |
|
311 by (rule inf_absorb2) simp |
|
312 |
|
313 lemma inf_top_right [simp]: |
|
314 "x \<sqinter> top = x" |
|
315 by (rule inf_absorb1) simp |
|
316 |
|
317 lemma sup_bot_left [simp]: |
|
318 "bot \<squnion> x = x" |
|
319 by (rule sup_absorb2) simp |
|
320 |
|
321 lemma sup_bot_right [simp]: |
|
322 "x \<squnion> bot = x" |
|
323 by (rule sup_absorb1) simp |
|
324 |
|
325 lemma compl_unique: |
|
326 assumes "x \<sqinter> y = bot" |
|
327 and "x \<squnion> y = top" |
|
328 shows "- x = y" |
|
329 proof - |
|
330 have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)" |
|
331 using inf_compl_bot assms(1) by simp |
|
332 then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)" |
|
333 by (simp add: inf_commute) |
|
334 then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)" |
|
335 by (simp add: inf_sup_distrib1) |
|
336 then have "- x \<sqinter> top = y \<sqinter> top" |
|
337 using sup_compl_top assms(2) by simp |
|
338 then show "- x = y" by (simp add: inf_top_right) |
|
339 qed |
|
340 |
|
341 lemma double_compl [simp]: |
|
342 "- (- x) = x" |
|
343 using compl_inf_bot compl_sup_top by (rule compl_unique) |
|
344 |
|
345 lemma compl_eq_compl_iff [simp]: |
|
346 "- x = - y \<longleftrightarrow> x = y" |
|
347 proof |
|
348 assume "- x = - y" |
|
349 then have "- x \<sqinter> y = bot" |
|
350 and "- x \<squnion> y = top" |
|
351 by (simp_all add: compl_inf_bot compl_sup_top) |
|
352 then have "- (- x) = y" by (rule compl_unique) |
|
353 then show "x = y" by simp |
|
354 next |
|
355 assume "x = y" |
|
356 then show "- x = - y" by simp |
|
357 qed |
|
358 |
|
359 lemma compl_bot_eq [simp]: |
|
360 "- bot = top" |
|
361 proof - |
|
362 from sup_compl_top have "bot \<squnion> - bot = top" . |
|
363 then show ?thesis by simp |
|
364 qed |
|
365 |
|
366 lemma compl_top_eq [simp]: |
|
367 "- top = bot" |
|
368 proof - |
|
369 from inf_compl_bot have "top \<sqinter> - top = bot" . |
|
370 then show ?thesis by simp |
|
371 qed |
|
372 |
|
373 lemma compl_inf [simp]: |
|
374 "- (x \<sqinter> y) = - x \<squnion> - y" |
|
375 proof (rule compl_unique) |
|
376 have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ((x \<sqinter> y) \<sqinter> - x) \<squnion> ((x \<sqinter> y) \<sqinter> - y)" |
|
377 by (rule inf_sup_distrib1) |
|
378 also have "... = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))" |
|
379 by (simp only: inf_commute inf_assoc inf_left_commute) |
|
380 finally show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = bot" |
|
381 by (simp add: inf_compl_bot) |
|
382 next |
|
383 have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (x \<squnion> (- x \<squnion> - y)) \<sqinter> (y \<squnion> (- x \<squnion> - y))" |
|
384 by (rule sup_inf_distrib2) |
|
385 also have "... = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))" |
|
386 by (simp only: sup_commute sup_assoc sup_left_commute) |
|
387 finally show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = top" |
|
388 by (simp add: sup_compl_top) |
|
389 qed |
|
390 |
|
391 lemma compl_sup [simp]: |
|
392 "- (x \<squnion> y) = - x \<sqinter> - y" |
|
393 proof - |
|
394 interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" top bot |
|
395 by (rule dual_boolean_algebra) |
|
396 then show ?thesis by simp |
|
397 qed |
257 |
398 |
258 end |
399 end |
259 |
400 |
260 |
401 |
261 subsection {* Uniqueness of inf and sup *} |
402 subsection {* Uniqueness of inf and sup *} |