:: Many-Argument Relations :: by Edmund Woronowicz :: :: Received June 1, 1990 :: Copyright (c) 1990-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 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, PARTFUN1, FUNCT_2, XBOOLEAN, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1; 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;