MARGREL1: Many-Argument Relations

:: Many-Argument Relations
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let B be non empty set ;
let A be set ;
let b be Element of B;
:: original: -->
redefine func A --> b -> Function of A,B;
coherence

proof end;

end;

definition

let IT be FinSequence-membered set ;

redefine attr IT is with_common_domain means :Def1: :: MARGREL1:def 1
for a, b being FinSequence st a in IT & b in IT holds
len a = len b;

proof end;

end;

:: deftheorem Def1 defines with_common_domain MARGREL1:def 1 :

registration

cluster FinSequence-membered with_common_domain for set ;

proof end;

end;

definition

mode relation is FinSequence-membered with_common_domain set ;

end;

theorem :: MARGREL1:1

for X being set
for p being relation st X c= p holds
X is relation ;

theorem :: MARGREL1:2

for a being FinSequence holds {a} is relation

proof end;

scheme :: MARGREL1:sch 1
relexist{ F₁() -> set , P₁[ FinSequence] } :

ex r being relation st
for a being FinSequence holds
( a in r iff ( a in F₁() & P₁[a] ) )

provided

A1: for a, b being FinSequence st P₁[a] & P₁[b] holds
len a = len b

proof end;

definition

let p, r be relation;

redefine pred p = r means :: MARGREL1:def 2
for a being FinSequence holds
( a in p iff a in r );

proof end;

end;

:: deftheorem defines = MARGREL1:def 2 :

registration

cluster empty -> with_common_domain for set ;

proof end;

end;

theorem Th3: :: MARGREL1:3

for p being relation st ( for a being FinSequence holds not a in p ) holds
p = {}

proof end;

definition

let p be relation;
assume A1: p <> {} ;

func the_arity_of p -> Element of NAT means :: MARGREL1:def 3
for a being FinSequence st a in p holds
it = len a;

proof end;

proof end;

end;

:: deftheorem defines the_arity_of MARGREL1:def 3 :

definition

let k be Element of NAT ;

mode relation_length of k -> relation means :: MARGREL1:def 4
for a being FinSequence st a in it holds
len a = k;

proof end;

end;

:: deftheorem defines relation_length MARGREL1:def 4 :

definition

let X be set ;

mode relation of X -> relation means :: MARGREL1:def 5
for a being FinSequence st a in it holds
rng a c= X;

proof end;

end;

:: deftheorem defines relation MARGREL1:def 5 :

theorem Th4: :: MARGREL1:4

for X being set holds {} is relation of X

proof end;

theorem Th5: :: MARGREL1:5

for k being Element of NAT holds {} is relation_length of k

proof end;

definition

let X be set ;
let k be Element of NAT ;

mode relation of X,k -> relation means :: MARGREL1:def 6
( it is relation of X & it is relation_length of k );

proof end;

end;

:: deftheorem defines relation MARGREL1:def 6 :

definition

let D be non empty set ;

func relations_on D -> set means :Def7: :: MARGREL1:def 7
for X being set 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 ) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines relations_on MARGREL1:def 7 :

registration

let D be non empty set ;

cluster relations_on D -> non empty ;

proof end;

end;

definition

let D be non empty set ;
mode relation of D is Element of relations_on D;

end;

theorem :: MARGREL1:6

for D being non empty set
for X being set
for r being Element of relations_on D st X c= r holds
X is Element of relations_on D

proof end;

theorem :: MARGREL1:7

for D being non empty set
for a being FinSequence of D holds {a} is Element of relations_on D

proof end;

theorem :: MARGREL1:8

for D being non empty set
for x, y being Element of D holds {<*x,y*>} is Element of relations_on D

proof end;

definition

let D be non empty set ;
let p, r be Element of relations_on D;

:: original: =
redefine pred p = r means :Def8: :: MARGREL1:def 8
for a being FinSequence of D holds
( a in p iff a in r );

proof end;

end;

:: deftheorem Def8 defines = MARGREL1:def 8 :

scheme :: MARGREL1:sch 2
relDexist{ F₁() -> non empty set , P₁[ FinSequence of F₁()] } :

ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() holds
( a in r iff P₁[a] )

provided

A1: for a, b being FinSequence of F₁() st P₁[a] & P₁[b] holds
len a = len b

proof end;

definition

let D be non empty set ;

func empty_rel D -> Element of relations_on D means :Def9: :: MARGREL1:def 9
for a being FinSequence of D holds not a in it;

proof end;

proof end;

end;

:: deftheorem Def9 defines empty_rel MARGREL1:def 9 :

theorem :: MARGREL1:9

for D being non empty set holds empty_rel D = {}

proof end;

definition

let D be non empty set ;
let p be Element of relations_on D;
assume A1: p <> empty_rel D ;

func the_arity_of p -> Element of NAT means :: MARGREL1:def 10
for a being FinSequence of D st a in p holds
it = len a;

proof end;

proof end;

end;

:: deftheorem defines the_arity_of MARGREL1:def 10 :

scheme :: MARGREL1:sch 3
relDexist2{ F₁() -> non empty set , F₂() -> Element of NAT , P₁[ FinSequence of F₁()] } :

ex r being Element of relations_on F₁() st
for a being FinSequence of F₁() st len a = F₂() holds
( a in r iff P₁[a] )

proof end;

definition

func BOOLEAN -> set equals :: MARGREL1:def 11
{0,1};

end;

:: deftheorem defines BOOLEAN MARGREL1:def 11 :

registration

cluster BOOLEAN -> non empty ;

end;

definition

:: original: FALSE
redefine func FALSE -> Element of BOOLEAN ;
coherence by TARSKI:def 2;
:: original: TRUE
redefine func TRUE -> Element of BOOLEAN ;
coherence by TARSKI:def 2;

end;

definition

let x be set ;

redefine attr x is boolean means :Def12: :: MARGREL1:def 12
x in BOOLEAN ;

proof end;

end;

:: deftheorem Def12 defines boolean MARGREL1:def 12 :

registration

cluster -> boolean for Element of BOOLEAN ;

coherence by Def12;

end;

definition

let v be boolean set ;

redefine func 'not' v equals :: MARGREL1:def 13
TRUE if v = FALSE
otherwise FALSE ;

proof end;

consistency ;
let w be boolean set ;

redefine func v '&' w equals :: MARGREL1:def 14
TRUE if ( v = TRUE & w = TRUE )
otherwise FALSE ;

proof end;

end;

:: deftheorem defines 'not' MARGREL1:def 13 :

:: deftheorem defines '&' MARGREL1:def 14 :

definition

let v be Element of BOOLEAN ;
:: original: 'not'
redefine func 'not' v -> Element of BOOLEAN ;
correctness by Def12;
let w be Element of BOOLEAN ;
:: original: '&'
redefine func v '&' w -> Element of BOOLEAN ;
correctness by Def12;

end;

theorem :: MARGREL1:10

canceled;

theorem :: MARGREL1:11

for v being boolean set holds
( ( v = FALSE implies 'not' v = TRUE ) & ( 'not' v = TRUE implies v = FALSE ) & ( v = TRUE implies 'not' v = FALSE ) & ( 'not' v = FALSE implies v = TRUE ) ) ;

theorem :: MARGREL1:12

for v, w being boolean set holds
( ( v '&' w = TRUE implies ( v = TRUE & w = TRUE ) ) & ( v = TRUE & w = TRUE implies v '&' w = TRUE ) & ( not v '&' w = FALSE or v = FALSE or w = FALSE ) & ( ( v = FALSE or w = FALSE ) implies v '&' w = FALSE ) ) by XBOOLEAN:101, XBOOLEAN:140;

theorem :: MARGREL1:13

for v being boolean set holds FALSE '&' v = FALSE ;

theorem :: MARGREL1:14

for v being boolean set holds TRUE '&' v = v ;

theorem :: MARGREL1:15

for v being boolean set st v '&' v = FALSE holds
v = FALSE ;

theorem :: MARGREL1:16

for v, w, u being boolean set holds v '&' (w '&' u) = (v '&' w) '&' u ;

definition

let X be set ;

func ALL X -> set equals :Def15: :: MARGREL1:def 15
TRUE if not FALSE in X
otherwise FALSE ;

end;

:: deftheorem Def15 defines ALL MARGREL1:def 15 :

registration

let X be set ;

cluster ALL X -> boolean ;

correctness by Def15;

end;

definition

let X be set ;
:: original: ALL
redefine func ALL X -> Element of BOOLEAN ;
correctness by Def12;

end;

theorem :: MARGREL1:17

for X being set holds
( ( not FALSE in X implies ALL X = TRUE ) & ( ALL X = TRUE implies not FALSE in X ) & ( FALSE in X implies ALL X = FALSE ) & ( ALL X = FALSE implies FALSE in X ) ) by Def15;

begin

:: from VALUAT_1, 2007.03.15, A.T.

definition

let f be Relation;

attr f is boolean-valued means :Def16: :: MARGREL1:def 16
rng f c= BOOLEAN ;

end;

:: deftheorem Def16 defines boolean-valued MARGREL1:def 16 :

registration

cluster Relation-like Function-like boolean-valued for set ;

proof end;

end;

registration

let f be boolean-valued Function;
let x be set ;

cluster f . x -> boolean ;

proof end;

end;

definition

let p be boolean-valued Function;

func 'not' p -> boolean-valued Function means :Def17: :: MARGREL1:def 17
( dom it = dom p & ( for x being set st x in dom p holds
it . x = 'not' (p . x) ) );

proof end;

proof end;

proof end;

let q be boolean-valued Function;

func p '&' q -> boolean-valued Function means :Def18: :: MARGREL1:def 18
( dom it = (dom p) /\ (dom q) & ( for x being set st x in dom it holds
it . x = (p . x) '&' (q . x) ) );

proof end;

proof end;

commutativity ;
idempotence ;

end;

:: deftheorem Def17 defines 'not' MARGREL1:def 17 :

:: deftheorem Def18 defines '&' MARGREL1:def 18 :

registration

let A be set ;

cluster Function-like quasi_total -> boolean-valued for Element of bool [:A,BOOLEAN:];

proof end;

end;

definition

let A be non empty set ;
let p be Function of A,BOOLEAN;

:: original: 'not'
redefine func 'not' p -> Function of A,BOOLEAN means :: MARGREL1:def 19
for x being Element of A holds it . x = 'not' (p . x);

proof end;

proof end;

let q be Function of A,BOOLEAN;

:: original: '&'
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);

proof end;

proof end;

end;

:: deftheorem defines 'not' MARGREL1:def 19 :

:: deftheorem defines '&' MARGREL1:def 20 :

begin

definition

let IT be Relation;

attr IT is homogeneous means :Def21: :: MARGREL1:def 21
dom IT is with_common_domain ;

end;

:: deftheorem Def21 defines homogeneous MARGREL1:def 21 :

definition

let A be set ;
let IT be PartFunc of (A *),A;

attr IT is quasi_total means :Def22: :: MARGREL1:def 22
for x, y being FinSequence of A st len x = len y & x in dom IT holds
y in dom IT;

end;

:: deftheorem Def22 defines quasi_total MARGREL1:def 22 :

registration

let f be Relation;
let X be with_common_domain set ;

cluster f | X -> homogeneous ;

proof end;

end;

registration

let A be non empty set ;
let f be PartFunc of (A *),A;

cluster dom f -> FinSequence-membered ;

proof end;

end;

registration

let A be non empty set ;

cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total for Element of bool [:(A *),A:];

proof end;

end;

registration

cluster Relation-like Function-like non empty homogeneous for set ;

proof end;

end;

registration

let R be homogeneous Relation;

cluster dom R -> with_common_domain ;

coherence by Def21;

end;

theorem Th18: :: MARGREL1:18

for A being non empty set
for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A *),A

proof end;

theorem :: MARGREL1:19

for A being non empty set
for a being Element of A holds (<*> A) .--> a is Element of PFuncs ((A *),A)

proof end;

definition

let A be set ;
mode PFuncFinSequence of A is FinSequence of PFuncs ((A *),A);

end;

definition

let A be set ;
let IT be PFuncFinSequence of A;

attr IT is homogeneous means :Def23: :: MARGREL1:def 23
for n being Nat
for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds
h is homogeneous ;

end;

:: deftheorem Def23 defines homogeneous MARGREL1:def 23 :

definition

let A be set ;
let IT be PFuncFinSequence of A;

attr IT is quasi_total means :Def24: :: MARGREL1:def 24
for n being Nat
for h being PartFunc of (A *),A st n in dom IT & h = IT . n holds
h is quasi_total ;

end;

:: deftheorem Def24 defines quasi_total MARGREL1:def 24 :

definition

let A be non empty set ;
let x be Element of PFuncs ((A *),A);
:: original: <*
redefine func <*x*> -> PFuncFinSequence of A;
coherence

proof end;

end;

registration

let A be non empty set ;

cluster Relation-like non-empty NAT -defined PFuncs ((A *),A) -valued Function-like Function-yielding V22() V31() FinSequence-like FinSubsequence-like countable homogeneous quasi_total for FinSequence of PFuncs ((A *),A);

proof end;

end;

registration

let A be non empty set ;
let f be homogeneous PFuncFinSequence of A;
let i be set ;

cluster f . i -> homogeneous ;

proof end;

end;

theorem :: MARGREL1:20

for A being non empty set
for a being Element of A
for x being Element of PFuncs ((A *),A) st x = (<*> A) .--> a holds
( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty )

proof end;

definition

let f be homogeneous Relation;

func arity f -> Nat means :Def25: :: 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 ;

consistency ;
existence

proof end;

proof end;

end;

:: deftheorem Def25 defines arity MARGREL1:def 25 :

definition

let f be homogeneous Function;
:: original: arity
redefine func arity f -> Element of NAT ;
coherence by ORDINAL1:def 12;

end;

begin

theorem :: MARGREL1:21

for n being Nat
for D being non empty set
for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1

proof end;

theorem :: MARGREL1:22

for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D

proof end;

definition

let D be non empty set ;

mode PFuncsDomHQN of D -> non empty set means :Def26: :: MARGREL1:def 26
for x being Element of it holds x is non empty homogeneous quasi_total PartFunc of (D *),D;

proof end;

end;

:: deftheorem Def26 defines PFuncsDomHQN MARGREL1:def 26 :

definition

let D be non empty set ;
let P be PFuncsDomHQN of D;
:: original: Element
redefine mode Element of P -> non empty homogeneous quasi_total PartFunc of (D *),D;
coherence by Def26;

end;