:: Algebra of Normal Forms
:: by Andrzej Trybulec
::
:: Received October 5, 1990
:: Copyright (c) 1990-2017 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 XBOOLE_0, FINSUB_1, SUBSET_1, ZFMISC_1, TARSKI, MCART_1, BINOP_1,
FUNCT_1, SETWISEO, RELAT_1, FINSET_1, ORDINAL4, STRUCT_0, LATTICES,
EQREL_1, NORMFORM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
FUNCT_2, FINSET_1, BINOP_1, DOMAIN_1, FINSUB_1, SETWISEO, STRUCT_0,
LATTICES;
constructors PARTFUN1, BINOP_1, DOMAIN_1, FINSET_1, SETWISEO, LATTICES,
RELSET_1, XTUPLE_0;
registrations SUBSET_1, FINSUB_1, LATTICES, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
:: A u x i l i a r y t h e o r e m s
:: Part 1. BOOLEan operations on pairs & relations between pairs
reserve A, B for non empty preBoolean set,
x, y for Element of [:A,B:];
definition
let A,B,x,y;
pred x c= y means
:: NORMFORM:def 1
x`1 c= y`1 & x`2 c= y`2;
reflexivity;
func x \/ y -> Element of [:A, B:] equals
:: NORMFORM:def 2
[x`1 \/ y`1, x`2 \/ y`2];
commutativity;
idempotence;
func x /\ y -> Element of [:A, B:] equals
:: NORMFORM:def 3
[x`1 /\ y`1, x`2 /\ y`2];
commutativity;
idempotence;
func x \ y -> Element of [:A, B:] equals
:: NORMFORM:def 4
[x`1 \ y`1, x`2 \ y`2];
func x \+\ y -> Element of [:A, B:] equals
:: NORMFORM:def 5
[x`1 \+\ y`1, x`2 \+\ y`2];
commutativity;
end;
reserve X for set,
a,b,c for Element of [:A,B:];
theorem :: NORMFORM:1
a c= b & b c= a implies a = b;
theorem :: NORMFORM:2
a c= b & b c= c implies a c= c;
theorem :: NORMFORM:3
(a \/ b) \/ c = a \/ (b \/ c);
theorem :: NORMFORM:4
(a /\ b) /\ c = a /\ (b /\ c);
theorem :: NORMFORM:5
a /\ (b \/ c) = a /\ b \/ a /\ c;
theorem :: NORMFORM:6
a \/ (b /\ a) = a;
theorem :: NORMFORM:7
a /\ (b \/ a) = a;
theorem :: NORMFORM:8
a \/ (b /\ c) = (a \/ b) /\ (a \/ c);
theorem :: NORMFORM:9
a c= c & b c= c implies a \/ b c= c;
theorem :: NORMFORM:10
a c= a \/ b & b c= a \/ b;
theorem :: NORMFORM:11
a = a \/ b implies b c= a;
theorem :: NORMFORM:12
a c= b implies c \/ a c= c \/ b & a \/ c c= b \/ c;
theorem :: NORMFORM:13
a\b \/ b = a \/ b;
theorem :: NORMFORM:14
a \ b c= c implies a c= b \/ c;
theorem :: NORMFORM:15
a c= b \/ c implies a \ c c= b;
reserve a for Element of [:Fin X, Fin X:];
definition
let A be set;
func FinPairUnion A -> BinOp of [:Fin A, Fin A:] means
:: NORMFORM:def 6
for x,y being Element of [:Fin A, Fin A:] holds it.(x,y) = x \/ y;
end;
reserve A for set;
definition
let X be non empty set, A be set;
let B be Element of Fin X;
let f be Function of X, [:Fin A, Fin A:];
func FinPairUnion(B,f) -> Element of [:Fin A, Fin A:] equals
:: NORMFORM:def 7
FinPairUnion A $$(B,f);
end;
registration
let A be set;
cluster FinPairUnion A -> commutative idempotent associative;
end;
theorem :: NORMFORM:16
for X being non empty set for f being Function of X, [:Fin A,Fin A:]
for B being Element of Fin X for x being Element of X st x in B holds f.x c=
FinPairUnion(B,f);
theorem :: NORMFORM:17
[{}.A, {}.A] is_a_unity_wrt FinPairUnion A;
theorem :: NORMFORM:18
FinPairUnion A is having_a_unity;
theorem :: NORMFORM:19
the_unity_wrt FinPairUnion A = [{}.A, {}.A];
theorem :: NORMFORM:20
for x being Element of [:Fin A, Fin A:] holds the_unity_wrt
FinPairUnion A c= x;
theorem :: NORMFORM:21
for X being non empty set for f being (Function of X,[:Fin A,Fin A:]),
B being (Element of Fin X) for c being Element of [:Fin A, Fin A:] st for x
being Element of X st x in B holds f.x c= c holds FinPairUnion(B,f) c= c;
theorem :: NORMFORM:22
for X being non empty set, B being Element of Fin X for f,g being
Function of X,[:Fin A,Fin A:] st f|B = g|B holds FinPairUnion(B,f) =
FinPairUnion(B,g);
:: Part 2. Disjoint pairs of finite sets
definition
let X;
func DISJOINT_PAIRS(X) -> Subset of [:Fin X, Fin X:] equals
:: NORMFORM:def 8
{ a : a`1 misses
a`2 };
end;
registration
let X;
cluster DISJOINT_PAIRS(X) -> non empty;
end;
theorem :: NORMFORM:23
for y being Element of [:Fin X, Fin X:] holds y in
DISJOINT_PAIRS X iff y`1 misses y`2;
reserve x,y for Element of [:Fin X, Fin X:],
a,b for Element of DISJOINT_PAIRS X;
theorem :: NORMFORM:24
y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies (y \/ x in
DISJOINT_PAIRS X iff y`1 /\ x`2 \/ x`1 /\ y`2 = {});
theorem :: NORMFORM:25
a`1 misses a`2;
theorem :: NORMFORM:26
x c= b implies x is Element of DISJOINT_PAIRS X;
theorem :: NORMFORM:27
not (ex x being set st x in a`1 & x in a`2);
theorem :: NORMFORM:28
not a \/ b in DISJOINT_PAIRS X implies ex p being Element of X st p in
a`1 & p in b`2 or p in b`1 & p in a`2;
theorem :: NORMFORM:29
x`1 misses x`2 implies x is Element of DISJOINT_PAIRS X;
theorem :: NORMFORM:30
for V,W being set st V c= a`1 & W c= a`2 holds [V,W] is Element of
DISJOINT_PAIRS X;
reserve A for set,
x for Element of [:Fin A, Fin A:],
a,b,c,d,s,t for Element of DISJOINT_PAIRS A,
B,C,D for Element of Fin DISJOINT_PAIRS A;
definition
let A;
func Normal_forms_on A -> Subset of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 9
{ B : a in B
& b in B & a c= b implies a = b};
end;
registration
let A;
cluster Normal_forms_on A -> non empty;
end;
reserve K,L,M for Element of Normal_forms_on A;
theorem :: NORMFORM:31
{} in Normal_forms_on A;
theorem :: NORMFORM:32
B in Normal_forms_on A & a in B & b in B & a c= b implies a = b;
theorem :: NORMFORM:33
(for a,b st a in B & b in B & a c= b holds a = b) implies B in
Normal_forms_on A;
definition
let A,B;
func mi B -> Element of Normal_forms_on A equals
:: NORMFORM:def 10
{ t : s in B & s c= t iff s
= t };
let C;
func B^C -> Element of Fin DISJOINT_PAIRS A equals
:: NORMFORM:def 11
DISJOINT_PAIRS A /\ { s
\/ t: s in B & t in C };
end;
theorem :: NORMFORM:34
x in B^C implies ex b,c st b in B & c in C & x = b \/ c;
theorem :: NORMFORM:35
b in B & c in C & b \/ c in DISJOINT_PAIRS A implies b \/ c in B ^C;
theorem :: NORMFORM:36
a in mi B implies a in B & (b in B & b c= a implies b = a);
theorem :: NORMFORM:37
a in mi B implies a in B;
theorem :: NORMFORM:38
a in mi B & b in B & b c= a implies b = a;
theorem :: NORMFORM:39
a in B & (for b st b in B & b c= a holds b = a) implies a in mi B;
theorem :: NORMFORM:40
mi B c= B;
theorem :: NORMFORM:41
b in B implies ex c st c c= b & c in mi B;
theorem :: NORMFORM:42
mi K = K;
theorem :: NORMFORM:43
mi (B \/ C) c= mi B \/ C;
theorem :: NORMFORM:44
mi(mi B \/ C) = mi (B \/ C);
theorem :: NORMFORM:45
mi(B \/ mi C) = mi (B \/ C);
theorem :: NORMFORM:46
B c= C implies B ^ D c= C ^ D;
theorem :: NORMFORM:47
mi(B ^ C) c= mi B ^ C;
theorem :: NORMFORM:48
B^C = C^B;
theorem :: NORMFORM:49
B c= C implies D ^ B c= D ^ C;
theorem :: NORMFORM:50
mi(mi B ^ C) = mi (B ^ C);
theorem :: NORMFORM:51
mi(B ^ mi C) = mi (B ^ C);
theorem :: NORMFORM:52
K^(L^M) = K^L^M;
theorem :: NORMFORM:53
K^(L \/ M) = K^L \/ K^M;
theorem :: NORMFORM:54
B c= B ^ B;
theorem :: NORMFORM:55
mi(K ^ K) = mi K;
definition
let A;
func NormForm A -> strict LattStr means
:: NORMFORM:def 12
the carrier of it =
Normal_forms_on A & for B, C being Element of Normal_forms_on A holds (the
L_join of it).(B, C) = mi (B \/ C) & (the L_meet of it).(B, C) = mi (B^C);
end;
registration
let A;
cluster NormForm A -> non empty;
end;
reserve K, L, M for Element of Normal_forms_on A;
registration
let A;
cluster NormForm A -> Lattice-like;
end;
registration
let A;
cluster NormForm A -> distributive lower-bounded;
end;
theorem :: NORMFORM:56
{} is Element of NormForm A;
theorem :: NORMFORM:57
Bottom NormForm A = {};