:: Many-Argument Relations
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2018 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 SUBSET_1, NUMBERS, XBOOLE_0, FUNCOP_1, FUNCT_2, RELAT_1, TARSKI,
FINSEQ_1, CARD_3, FUNCT_1, ZFMISC_1, ORDINAL4, CARD_1, XBOOLEAN,
MARGREL1, PARTFUN1, NAT_1, UNIALG_1, FINSEQ_2, UNIALG_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1,
RELAT_1, NAT_1, FUNCT_2, XBOOLEAN, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1,
PARTFUN1;
constructors FUNCOP_1, XCMPLX_0, FINSEQ_1, XBOOLEAN, RELSET_1, CARD_3,
FINSEQ_2, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XBOOLEAN, FINSEQ_1,
FINSEQ_2, ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, CARD_1, CARD_3,
FUNCT_2;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
begin
reserve x,z for set;
reserve k for Element of NAT;
reserve D for non empty set;
definition
let IT be FinSequence-membered set;
redefine attr IT is with_common_domain means
:: MARGREL1:def 1
for a,b being FinSequence st a in IT & b in IT holds len a = len b;
end;
registration
cluster FinSequence-membered with_common_domain for set;
end;
definition
mode relation is FinSequence-membered with_common_domain set;
end;
reserve X for set;
reserve p,r for relation;
reserve a,a1,a2,b for FinSequence;
theorem :: MARGREL1:1
X c= p implies X is relation;
theorem :: MARGREL1:2
{a} is relation;
scheme :: MARGREL1:sch 1
relexist{A() -> set, P[FinSequence]}:
ex r st for a holds a in r iff a in A() & P[a]
provided
for a,b st P[a] & P[b] holds len a = len b;
definition
let p,r;
redefine pred p = r means
:: MARGREL1:def 2
for a holds a in p iff a in r;
end;
registration
cluster empty -> with_common_domain for set;
end;
theorem :: MARGREL1:3
for p st for a holds not a in p holds p = {};
definition
let p;
assume
p <> {};
func the_arity_of p -> Element of NAT means
:: MARGREL1:def 3
for a st a in p holds it = len a;
end;
definition
let k;
mode relation_length of k -> relation means
:: MARGREL1:def 4
for a st a in it holds len a = k;
end;
definition
let X be set;
mode relation of X -> relation means
:: MARGREL1:def 5
for a st a in it holds rng a c= X;
end;
theorem :: MARGREL1:4
{} is relation of X;
theorem :: MARGREL1:5
{} is relation_length of k;
definition
let X, k;
mode relation of X,k -> relation means
:: MARGREL1:def 6
it is relation of X & it is relation_length of k;
end;
definition
let D;
func relations_on D -> set means
:: MARGREL1:def 7
for X holds X in it iff X c= D* &
for a,b being FinSequence of D st a in X & b in X holds len a = len b;
end;
registration
let D;
cluster relations_on D -> non empty;
end;
definition
let D be non empty set;
mode relation of D is Element of relations_on D;
end;
reserve a,b for FinSequence of D;
reserve p,r for Element of relations_on D;
theorem :: MARGREL1:6
X c= r implies X is Element of relations_on D;
theorem :: MARGREL1:7
{a} is Element of relations_on D;
theorem :: MARGREL1:8
for x,y being Element of D holds {<*x,y*>} is Element of relations_on D;
definition
let D,p,r;
redefine pred p = r means
:: MARGREL1:def 8
for a holds a in p iff a in r;
end;
scheme :: MARGREL1:sch 2
relDexist{D() -> non empty set, P[FinSequence of D()]}: ex r being Element
of relations_on D() st for a being FinSequence of D() holds a in r iff P[a]
provided
for a,b being FinSequence of D() st P[a] & P[b] holds len a = len b;
definition
let D;
func empty_rel(D) -> Element of relations_on D means
:: MARGREL1:def 9
not a in it;
end;
theorem :: MARGREL1:9
empty_rel(D) = {};
definition
let D,p;
assume
p <> empty_rel(D);
func the_arity_of p -> Element of NAT means
:: MARGREL1:def 10
a in p implies it = len a;
end;
scheme :: MARGREL1:sch 3
relDexist2{D() -> non empty set, k() -> Element of NAT, P[FinSequence of D()
]}: ex r being Element of relations_on D() st for a being FinSequence of D() st
len a = k() holds a in r iff P[a];
definition
func BOOLEAN -> set equals
:: MARGREL1:def 11
{0,1};
end;
registration
cluster BOOLEAN -> non empty;
end;
definition
redefine func FALSE -> Element of BOOLEAN;
redefine func TRUE -> Element of BOOLEAN;
end;
definition
let x be object;
redefine attr x is boolean means
:: MARGREL1:def 12
x in BOOLEAN;
end;
registration
cluster -> boolean for Element of BOOLEAN;
end;
reserve u,v,w for boolean object;
definition
let v;
redefine func 'not' v equals
:: MARGREL1:def 13
TRUE if v = FALSE otherwise FALSE;
let w;
redefine func v '&' w equals
:: MARGREL1:def 14
TRUE if v = TRUE & w =TRUE otherwise FALSE;
end;
definition
let v be Element of BOOLEAN;
redefine func 'not' v -> Element of BOOLEAN;
let w be Element of BOOLEAN;
redefine func v '&' w -> Element of BOOLEAN;
end;
::$CT
theorem :: MARGREL1:11
(v = FALSE iff 'not' v = TRUE) & (v = TRUE iff 'not' v = FALSE);
theorem :: MARGREL1:12
(v '&' w = TRUE iff v = TRUE & w = TRUE) & (v '&' w = FALSE iff v =
FALSE or w = FALSE);
theorem :: MARGREL1:13
FALSE '&' v = FALSE;
theorem :: MARGREL1:14
TRUE '&' v = v;
theorem :: MARGREL1:15
v '&' v = FALSE implies v = FALSE;
theorem :: MARGREL1:16
v '&' (w '&' u) = (v '&' w) '&' u;
definition
let X;
func ALL(X) -> set equals
:: MARGREL1:def 15
TRUE if not FALSE in X otherwise FALSE;
end;
registration
let X;
cluster ALL X -> boolean;
end;
definition
let X;
redefine func ALL X -> Element of BOOLEAN;
end;
theorem :: MARGREL1:17
(not FALSE in X iff ALL(X) = TRUE) & (FALSE in X iff ALL(X) = FALSE);
begin :: Addenda
:: from VALUAT_1, 2007.03.15, A.T.
definition
let f be Relation;
attr f is boolean-valued means
:: MARGREL1:def 16
rng f c= BOOLEAN;
end;
registration
cluster boolean-valued for Function;
end;
registration
let f be boolean-valued Function, x be object;
cluster f.x -> boolean;
end;
definition
let p be boolean-valued Function;
func 'not' p -> boolean-valued Function means
:: MARGREL1:def 17
dom it = dom p &
for x being object st x in dom p holds it.x = 'not'(p.x);
involutiveness;
let q be boolean-valued Function;
func p '&' q -> boolean-valued Function means
:: MARGREL1:def 18
dom it = dom p /\ dom
q & for x being object st x in dom it holds it.x = (p.x) '&' (q.x);
commutativity;
idempotence;
end;
registration
let A be set;
cluster -> boolean-valued for Function of A,BOOLEAN;
end;
definition
let A be non empty set;
let p be Function of A,BOOLEAN;
redefine func 'not' p -> Function of A,BOOLEAN means
:: MARGREL1:def 19
for x being Element of A holds it.x = 'not'(p.x);
let q be Function of A,BOOLEAN;
redefine func p '&' q -> Function of A,BOOLEAN means
:: MARGREL1:def 20
for x being Element of A holds it.x = (p.x) '&' (q.x);
end;
begin :: Moved from UNIALG_1, 2010.03.16, A.T.
reserve A,z for set,
x,y for FinSequence of A,
h for PartFunc of A*,A,
n,m for Nat;
definition
let IT be Relation;
attr IT is homogeneous means
:: MARGREL1:def 21
dom IT is with_common_domain;
end;
definition
let A;
let IT be PartFunc of A*,A;
attr IT is quasi_total means
:: MARGREL1:def 22
for x,y st len x = len y & x in dom IT holds y in dom IT;
end;
registration
let f be Relation;
let X be with_common_domain set;
cluster f|X -> homogeneous;
end;
registration
let A be non empty set, f be PartFunc of A*,A;
cluster dom f -> FinSequence-membered;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non empty for PartFunc of A*,A;
end;
registration
cluster homogeneous non empty for Function;
end;
registration let R be homogeneous Relation;
cluster dom R -> with_common_domain;
end;
theorem :: MARGREL1:18
for A being non empty set, a being Element of A holds <*>A .-->a
is homogeneous quasi_total non empty PartFunc of A*,A;
theorem :: MARGREL1:19
for A being non empty set, a being Element of A holds <*>A .-->a
is Element of PFuncs(A*,A);
definition
let A;
mode PFuncFinSequence of A is FinSequence of PFuncs(A*,A);
end;
definition
let A;
let IT be PFuncFinSequence of A;
attr IT is homogeneous means
:: MARGREL1:def 23
for n,h st n in dom IT & h = IT.n holds h is homogeneous;
end;
definition
let A;
let IT be PFuncFinSequence of A;
attr IT is quasi_total means
:: MARGREL1:def 24
for n,h st n in dom IT & h = IT.n holds h is quasi_total;
end;
definition
let A be non empty set;
let x be Element of PFuncs(A*,A);
redefine func <*x*> -> PFuncFinSequence of A;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non-empty for PFuncFinSequence of A;
end;
registration
let A be non empty set;
let f be homogeneous PFuncFinSequence of A;
let i be set;
cluster f.i -> homogeneous;
end;
reserve A for non empty set,
h for PartFunc of A*,A,
a for Element of A;
theorem :: MARGREL1:20
for x be Element of PFuncs(A*,A) st x = <*>A .--> a holds <*x*>
is homogeneous quasi_total non-empty;
definition
let f be homogeneous Relation;
func arity(f) -> Nat means
:: MARGREL1:def 25
for x being FinSequence st x in dom f holds it =
len x if ex x being FinSequence st x in dom f otherwise it = 0;
end;
definition
let f be homogeneous Function;
redefine func arity(f) -> Element of NAT;
end;
begin :: Moved from UNIALG_2, 2010.03.17, A.T.
theorem :: MARGREL1:21
for n be Nat, D be non empty set, D1 be non empty Subset of D
holds n-tuples_on D /\ n-tuples_on D1 = n-tuples_on D1;
theorem :: MARGREL1:22
for D being non empty set for h being homogeneous quasi_total non
empty PartFunc of D*,D holds dom h = (arity(h))-tuples_on D;
definition
let D be non empty set;
mode PFuncsDomHQN of D -> non empty set means
:: MARGREL1:def 26
for x be Element of it
holds x is homogeneous quasi_total non empty PartFunc of D*,D;
end;
definition
let D be non empty set, P be PFuncsDomHQN of D;
redefine mode Element of P -> homogeneous quasi_total non empty PartFunc of
D*,D;
end;