:: Boolean Properties of Lattices
::  by Agnieszka Julia Marasik
::
:: Received March 28, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies LATTICES, SUBSET_1, XBOOLE_0, EQREL_1, PBOOLE;
 notations STRUCT_0, LATTICES;
 constructors LATTICES;
 registrations LATTICES;


begin :: General Lattices

reserve L for Lattice;
reserve X,Y,Z,V for Element of L;

definition
  let L,X,Y;
  func X \ Y -> Element of L equals
:: BOOLEALG:def 1
  X "/\" Y`;
end;

definition
  let L,X,Y;
  func X \+\ Y -> Element of L equals
:: BOOLEALG:def 2
  (X \ Y) "\/" (Y \ X);
end;

definition
  let L,X,Y;
  redefine pred X = Y means
:: BOOLEALG:def 3

  X [= Y & Y [= X;
end;

definition
  let L,X,Y;
  pred X meets Y means
:: BOOLEALG:def 4

  X "/\" Y <> Bottom L;
end;

notation
  let L,X,Y;
  antonym X misses Y for X meets Y;
end;

theorem :: BOOLEALG:1
  X "\/" Y [= Z implies X [= Z;

theorem :: BOOLEALG:2
  X "/\" Y [= X "\/" Z;

theorem :: BOOLEALG:3
  X [= Z implies X \ Y [= Z;

theorem :: BOOLEALG:4
  X \ Y [= Z & Y \ X [= Z implies X \+\ Y [= Z;

theorem :: BOOLEALG:5
  X = Y "\/" Z iff Y [= X & Z [= X & for V st Y [= V & Z [= V holds X [= V;

theorem :: BOOLEALG:6
  X = Y "/\" Z iff X [= Y & X [= Z & for V st V [= Y & V [= Z holds V [= X;

theorem :: BOOLEALG:7
  X meets X iff X <> Bottom L;

definition
  let L, X, Y;
  redefine pred X meets Y;
  symmetry;
  redefine func X \+\ Y;
  commutativity;
  redefine pred X misses Y;
  symmetry;
end;

begin

begin :: Distributive Lattices

reserve L for D_Lattice;
reserve X,Y,Z for Element of L;

theorem :: BOOLEALG:8
  (X "/\" Y) "\/" (X "/\" Z) = X implies X [= Y "\/" Z;

begin :: Distributive Bounded Lattices

reserve L for 0_Lattice;
reserve X,Y,Z for Element of L;

theorem :: BOOLEALG:9
  X [= Bottom L implies X = Bottom L;

theorem :: BOOLEALG:10
  X [= Y & X [= Z & Y "/\" Z = Bottom L implies X = Bottom L;

theorem :: BOOLEALG:11
  X "\/" Y = Bottom L iff X = Bottom L & Y = Bottom L;

theorem :: BOOLEALG:12
  X [= Y & Y "/\" Z = Bottom L implies X "/\" Z = Bottom L;

theorem :: BOOLEALG:13
  X meets Y & Y [= Z implies X meets Z;

theorem :: BOOLEALG:14
  X meets Y "/\" Z implies X meets Y & X meets Z;

theorem :: BOOLEALG:15
  X meets Y \ Z implies X meets Y;

theorem :: BOOLEALG:16
  X misses Bottom L;

theorem :: BOOLEALG:17
  X misses Z & Y [= Z implies X misses Y;

theorem :: BOOLEALG:18
  X misses Y or X misses Z implies X misses Y "/\" Z;

theorem :: BOOLEALG:19
  X [= Y & X [= Z & Y misses Z implies X = Bottom L;

theorem :: BOOLEALG:20
  X misses Y implies (Z "/\" X) misses (Z "/\" Y);

begin :: Boolean Lattices

reserve L for B_Lattice;
reserve X,Y,Z,V for Element of L;

theorem :: BOOLEALG:21
  X \ Y [= Z implies X [= Y "\/" Z;

theorem :: BOOLEALG:22
  X [= Y implies Z \ Y [= Z \ X;

theorem :: BOOLEALG:23
  X [= Y & Z [= V implies X \ V [= Y \ Z;

theorem :: BOOLEALG:24
  X [= Y "\/" Z implies X \ Y [= Z;

theorem :: BOOLEALG:25
  X` [= (X "/\" Y)`;

theorem :: BOOLEALG:26
  (X "\/" Y)` [= X`;

theorem :: BOOLEALG:27
  X [= Y \ X implies X = Bottom L;

theorem :: BOOLEALG:28
  X [= Y implies Y = X "\/" (Y \ X);

theorem :: BOOLEALG:29
  X \ Y = Bottom L iff X [= Y;

theorem :: BOOLEALG:30
  X [= (Y "\/" Z) & X "/\" Z = Bottom L implies X [= Y;

theorem :: BOOLEALG:31
  X "\/" Y = (X \ Y) "\/" Y;

theorem :: BOOLEALG:32
  X \ (X "\/" Y) = Bottom L;

theorem :: BOOLEALG:33
  X \ X "/\" Y = X \ Y;

theorem :: BOOLEALG:34
  (X \ Y) "/\" Y = Bottom L;

theorem :: BOOLEALG:35
  X "\/" (Y \ X) = X "\/" Y;

theorem :: BOOLEALG:36
  (X "/\" Y) "\/" (X \ Y) = X;

theorem :: BOOLEALG:37
  X \ (Y \ Z) = (X \ Y) "\/" (X "/\" Z);

theorem :: BOOLEALG:38
  X \ (X \ Y) = X "/\" Y;

theorem :: BOOLEALG:39
  (X "\/" Y) \ Y = X \ Y;

theorem :: BOOLEALG:40
  X "/\" Y = Bottom L iff X \ Y = X;

theorem :: BOOLEALG:41
  X \ (Y "\/" Z) = (X \ Y) "/\" (X \ Z);

theorem :: BOOLEALG:42
  X \ (Y "/\" Z) = (X \ Y) "\/" (X \ Z);

theorem :: BOOLEALG:43
  X "/\" (Y \ Z) = X "/\" Y \ X "/\" Z;

theorem :: BOOLEALG:44
  (X "\/" Y) \ (X "/\" Y) = (X \ Y) "\/" (Y \ X);

theorem :: BOOLEALG:45
  (X \ Y) \ Z = X \ (Y "\/" Z);

theorem :: BOOLEALG:46
  X \ Y = Y \ X implies X = Y;

theorem :: BOOLEALG:47
  X \ Bottom L = X;

theorem :: BOOLEALG:48
  (X \ Y)` = X` "\/" Y;

theorem :: BOOLEALG:49
  X meets Y "\/" Z iff X meets Y or X meets Z;

theorem :: BOOLEALG:50
  X "/\" Y misses X \ Y;

theorem :: BOOLEALG:51
  X misses Y "\/" Z iff X misses Y & X misses Z;

theorem :: BOOLEALG:52
  (X \ Y) misses Y;

theorem :: BOOLEALG:53
  X misses Y implies (X "\/" Y) \ Y = X;

theorem :: BOOLEALG:54
  X` "\/" Y` = X "\/" Y & X misses X` & Y misses Y` implies X = Y` & Y = X`;

theorem :: BOOLEALG:55
  X` "\/" Y` = X "\/" Y & Y misses X` & X misses Y` implies X = X` & Y = Y`;

theorem :: BOOLEALG:56
  X \+\ Bottom L = X;

theorem :: BOOLEALG:57
  X \+\ X = Bottom L;

theorem :: BOOLEALG:58
  X "/\" Y misses X \+\ Y;

theorem :: BOOLEALG:59
  X "\/" Y = X \+\ (Y \ X);

theorem :: BOOLEALG:60
  X \+\ (X "/\" Y) = X \ Y;

theorem :: BOOLEALG:61
  X "\/" Y = (X \+\ Y) "\/" (X "/\" Y);

theorem :: BOOLEALG:62
  (X \+\ Y) \+\ (X "/\" Y) = X "\/" Y;

theorem :: BOOLEALG:63
  (X \+\ Y) \+\ (X "\/" Y) = X "/\" Y;

theorem :: BOOLEALG:64
  X \+\ Y = (X "\/" Y) \ (X "/\" Y);

theorem :: BOOLEALG:65
  (X \+\ Y) \ Z = (X \ (Y "\/" Z)) "\/" (Y \ (X "\/" Z));

theorem :: BOOLEALG:66
  X \ (Y \+\ Z) = (X \ (Y "\/" Z)) "\/" (X "/\" Y "/\" Z);

theorem :: BOOLEALG:67
  (X \+\ Y) \+\ Z = X \+\ (Y \+\ Z);

theorem :: BOOLEALG:68
  (X \+\ Y)` = (X "/\" Y) "\/" (X` "/\" Y`);