ARMSTRNG

:: Armstrong's Axioms
:: by William W. Armstrong , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received October 25, 2002
:: Copyright (c) 2002 Association of Mizar Users

:: ARMSTRNG semantic presentation

Lm1: now

let n be Element of NAT ; :: thesis:
let X be non empty set ; :: thesis:
let t be Tuple of n,X; :: thesis:
len t = n by FINSEQ_2:109;
hence dom t = Seg n by FINSEQ_1:def 3; :: thesis:

end;

theorem Th1: :: ARMSTRNG:1

for B being set st B is (B2) holds
for X being set
for S being finite Subset-Family of X st X in B & S c= B holds
Intersect S in B

proof end;

registration

cluster non empty reflexive antisymmetric transitive set ;
existence

proof end;

end;

theorem Th2: :: ARMSTRNG:2

for R being non empty antisymmetric transitive Relation
for X being finite Subset of (field R) st X <> {} holds
ex x being Element of X st x is_maximal_wrt X,R

proof end;

scheme :: ARMSTRNG:sch 1
SubsetSEq{ F₁() -> set , P₁[ set ] } :

for X1, X2 being Subset of F₁() st ( for y being set holds
( y in X1 iff P₁[y] ) ) & ( for y being set holds
( y in X2 iff P₁[y] ) ) holds
X1 = X2

proof end;

definition

let X be set ;
let R be Relation;
func R Maximal_in X -> Subset of X means :Def1: :: ARMSTRNG:def 1
for x being set holds
( x in it iff x is_maximal_wrt X,R );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Maximal_in ARMSTRNG:def 1 :

definition

let x, X be set ;
pred x is_/\-irreducible_in X means :Def2: :: ARMSTRNG:def 2
( x in X & ( for z, y being set st z in X & y in X & x = z /\ y & not x = z holds
x = y ) );

end;

:: deftheorem Def2 defines is_/\-irreducible_in ARMSTRNG:def 2 :

notation

let x, X be set ;
antonym x is_/\-reducible_in X for x is_/\-irreducible_in X;

end;

definition

let X be non empty set ;
func /\-IRR X -> Subset of X means :Def3: :: ARMSTRNG:def 3
for x being set holds
( x in it iff x is_/\-irreducible_in X );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines /\-IRR ARMSTRNG:def 3 :

scheme :: ARMSTRNG:sch 2
FinIntersect{ F₁() -> non empty finite set , P₁[ set ] } :

for x being set st x in F₁() holds
P₁[x]

provided

A1: for x being set st x is_/\-irreducible_in F₁() holds
P₁[x] and
A2: for x, y being set st x in F₁() & y in F₁() & P₁[x] & P₁[y] holds
P₁[x /\ y]

proof end;

theorem Th3: :: ARMSTRNG:3

for X being non empty finite set
for x being Element of X ex A being non empty Subset of X st
( x = meet A & ( for s being set st s in A holds
s is_/\-irreducible_in X ) )

proof end;

definition

let X be set ;
let B be Subset-Family of X;
attr B is (B1) means :Def4: :: ARMSTRNG:def 4
X in B;

end;

:: deftheorem Def4 defines (B1) ARMSTRNG:def 4 :

notation

let B be set ;
synonym (B2) B for cap-closed B;

end;

registration

let X be set ;
cluster (B2) (B1) Element of bool (bool X);
existence

proof end;

end;

theorem Th4: :: ARMSTRNG:4

for X being set
for B being non empty Subset-Family of X st B is (B2) holds
for x being Element of B st x is_/\-irreducible_in B & x <> X holds
for S being finite Subset-Family of X st S c= B & x = Intersect S holds
x in S

proof end;

registration

let X, D be non empty set ;
let n be Element of NAT ;
cluster -> FinSequence-yielding Relation of X,n -tuples_on D;
coherence

proof end;

end;

registration

let f be FinSequence-yielding Function;
let x be set ;
cluster f . x -> FinSequence-like ;
coherence

proof end;

end;

definition

let n be Element of NAT ;
let p, q be Tuple of n,BOOLEAN ;
func p '&' q -> Tuple of n,BOOLEAN means :Def5: :: ARMSTRNG:def 5
for i being set st i in Seg n holds
it . i = (p /. i) '&' (q /. i);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines '&' ARMSTRNG:def 5 :

theorem Th5: :: ARMSTRNG:5

for n being Element of NAT
for p being Tuple of n,BOOLEAN holds (n -BinarySequence 0 ) '&' p = n -BinarySequence 0

proof end;

theorem :: ARMSTRNG:6

for n being Element of NAT
for p being Tuple of n,BOOLEAN holds ('not' (n -BinarySequence 0 )) '&' p = p

proof end;

theorem :: ARMSTRNG:7

canceled;

theorem Th8: :: ARMSTRNG:8

for n, i being Element of NAT st i < n holds
( (n -BinarySequence (2 to_power i)) . (i + 1) = 1 & ( for j being Element of NAT st j in Seg n & j <> i + 1 holds
(n -BinarySequence (2 to_power i)) . j = 0 ) )

proof end;

definition

attr c₁ is strict;
struct DB-Rel -> ;
aggr DB-Rel(# Attributes, Domains, Relationship #) -> DB-Rel ;
sel Attributes c₁ -> non empty finite set ;
sel Domains c₁ -> V14 ManySortedSet of the Attributes of c₁;
sel Relationship c₁ -> Subset of (product the Domains of c₁);

end;

definition

let X be set ;
mode Subset-Relation of X is Relation of bool X;
mode Dependency-set of X is Relation of bool X;

end;

registration

let X be set ;
cluster non empty finite Relation of bool X, bool X;
existence

proof end;

end;

definition

let X be set ;
canceled;
func Dependencies X -> Dependency-set of X equals :: ARMSTRNG:def 7
[:(bool X),(bool X):];
coherence by RELSET_1:def 1;

end;

:: deftheorem ARMSTRNG:def 6 :

:: deftheorem defines Dependencies ARMSTRNG:def 7 :

definition

let X be set ;
mode Dependency of X is Element of Dependencies X;

end;

registration

let X be set ;
cluster Dependencies X -> non empty ;
coherence ;

end;

definition

let X be set ;
let F be non empty Dependency-set of X;
:: original: Element
redefine mode Element of F -> Dependency of X;
correctness

proof end;

end;

theorem Th9: :: ARMSTRNG:9

for X, x being set holds
( x in Dependencies X iff ex a, b being Subset of X st x = [a,b] )

proof end;

theorem Th10: :: ARMSTRNG:10

for X, x being set
for F being Dependency-set of X st x in F holds
ex a, b being Subset of X st x = [a,b]

proof end;

definition

let R be DB-Rel ;
let A, B be Subset of the Attributes of R;
pred A >|> B,R means :Def8: :: ARMSTRNG:def 8
for f, g being Element of the Relationship of R st f | A = g | A holds
f | B = g | B;

end;

:: deftheorem Def8 defines >|> ARMSTRNG:def 8 :

notation

let R be DB-Rel ;
let A, B be Subset of the Attributes of R;
synonym A,B holds_in R for A >|> B,R;

end;

definition

let R be DB-Rel ;
func Dependency-str R -> Dependency-set of the Attributes of R equals :: ARMSTRNG:def 9
{ [A,B] where A, B is Subset of the Attributes of R : A >|> B,R } ;
coherence

proof end;

end;

:: deftheorem defines Dependency-str ARMSTRNG:def 9 :

theorem :: ARMSTRNG:11

canceled;

theorem Th12: :: ARMSTRNG:12

for R being DB-Rel
for A, B being Subset of the Attributes of R holds
( [A,B] in Dependency-str R iff A >|> B,R )

proof end;

definition

let X be set ;
let P, Q be Dependency of X;
pred P >= Q means :Def10: :: ARMSTRNG:def 10
( P `1 c= Q `1 & Q `2 c= P `2 );
reflexivity ;

end;

:: deftheorem Def10 defines >= ARMSTRNG:def 10 :

notation

let X be set ;
let P, Q be Dependency of X;
synonym Q <= P for P >= Q;
synonym P is_at_least_as_informative_as Q for P >= Q;

end;

theorem Th13: :: ARMSTRNG:13

for X being set
for P, Q being Dependency of X st P <= Q & Q <= P holds
P = Q

proof end;

theorem Th14: :: ARMSTRNG:14

for X being set
for P, Q, S being Dependency of X st P <= Q & Q <= S holds
P <= S

proof end;

definition

let X be set ;
let A, B be Subset of X;
:: original: [
redefine func [A,B] -> Dependency of X;
coherence by ZFMISC_1:def 2;

end;

theorem Th15: :: ARMSTRNG:15

for X being set
for A, B, A', B' being Subset of X holds
( [A,B] >= [A',B'] iff ( A c= A' & B' c= B ) )

proof end;

definition

let X be set ;
func Dependencies-Order X -> Relation of Dependencies X equals :: ARMSTRNG:def 11
{ [P,Q] where P, Q is Dependency of X : P <= Q } ;
coherence

proof end;

end;

:: deftheorem defines Dependencies-Order ARMSTRNG:def 11 :

theorem :: ARMSTRNG:16

for X, x being set holds
( x in Dependencies-Order X iff ex P, Q being Dependency of X st
( x = [P,Q] & P <= Q ) ) ;

theorem Th17: :: ARMSTRNG:17

for X being set holds dom (Dependencies-Order X) = [:(bool X),(bool X):]

proof end;

theorem Th18: :: ARMSTRNG:18

for X being set holds rng (Dependencies-Order X) = [:(bool X),(bool X):]

proof end;

theorem Th19: :: ARMSTRNG:19

for X being set holds field (Dependencies-Order X) = [:(bool X),(bool X):]

proof end;

registration

let X be set ;
cluster Dependencies-Order X -> non empty ;
coherence by Th17, RELAT_1:60;
cluster Dependencies-Order X -> total reflexive antisymmetric transitive ;
coherence

proof end;

end;

notation

let X be set ;
let F be Dependency-set of X;
synonym (F2) F for transitive X;
synonym (DC1) F for transitive X;

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (F1) means :Def12: :: ARMSTRNG:def 12
for A being Subset of X holds [A,A] in F;

end;

:: deftheorem Def12 defines (F1) ARMSTRNG:def 12 :

notation

let X be set ;
let F be Dependency-set of X;
synonym (DC2) F for (F1) F;

end;

theorem Th20: :: ARMSTRNG:20

for X being set
for F being Dependency-set of X holds
( F is (F2) iff for A, B, C being Subset of X st [A,B] in F & [B,C] in F holds
[A,C] in F )

proof end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (F3) means :Def13: :: ARMSTRNG:def 13
for A, B, A', B' being Subset of X st [A,B] in F & [A,B] >= [A',B'] holds
[A',B'] in F;
attr F is (F4) means :Def14: :: ARMSTRNG:def 14
for A, B, A', B' being Subset of X st [A,B] in F & [A',B'] in F holds
[(A \/ A'),(B \/ B')] in F;

end;

:: deftheorem Def13 defines (F3) ARMSTRNG:def 13 :

:: deftheorem Def14 defines (F4) ARMSTRNG:def 14 :

theorem Th21: :: ARMSTRNG:21

for X being set holds
( Dependencies X is (F1) & Dependencies X is (F2) & Dependencies X is (F3) & Dependencies X is (F4) )

proof end;

registration

let X be set ;
cluster non empty (F2) (F1) (F3) (F4) Relation of bool X, bool X;
existence

proof end;

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is full_family means :Def15: :: ARMSTRNG:def 15
( F is (F1) & F is (F2) & F is (F3) & F is (F4) );

end;

:: deftheorem Def15 defines full_family ARMSTRNG:def 15 :

registration

let X be set ;
cluster full_family Relation of bool X, bool X;
existence

proof end;

end;

definition

let X be set ;
mode Full-family of X is full_family Dependency-set of X;

end;

theorem :: ARMSTRNG:22

for X being finite set
for F being Dependency-set of X holds F is finite ;

registration

let X be finite set ;
cluster finite Relation of bool X, bool X;
existence

proof end;

cluster -> finite Relation of bool X, bool X;
coherence ;

end;

registration

let X be set ;
cluster full_family -> (F2) (F1) (F3) (F4) Relation of bool X, bool X;
coherence by Def15;
cluster (F2) (F1) (F3) (F4) -> full_family Relation of bool X, bool X;
correctness by Def15;

end;

definition

let X be set ;
let F be Dependency-set of X;
attr F is (DC3) means :Def16: :: ARMSTRNG:def 16
for A, B being Subset of X st B c= A holds
[A,B] in F;

end;

:: deftheorem Def16 defines (DC3) ARMSTRNG:def 16 :

registration

let X be set ;
cluster (F1) (F3) -> (DC3) Relation of bool X, bool X;
coherence

proof end;

cluster (F2) (DC3) -> (F1) (F3) Relation of bool X, bool X;
coherence

proof end;

end;

registration

let X be set ;
cluster non empty (F2) (F4) (DC3) Relation of bool X, bool X;
existence

proof end;

end;

theorem :: ARMSTRNG:23

for X being set
for F being