:: Minimal Manysorted Signature for Partial Algebra
:: by Grzegorz Bancerek
::
:: Received October 1, 1995
:: Copyright (c) 1995-2016 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 FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, SETFAM_1, UNIALG_1,
FUNCT_2, PARTFUN1, SUBSET_1, NAT_1, STRUCT_0, CARD_3, MSUALG_1, UNIALG_2,
EQREL_1, ZFMISC_1, NUMBERS, FINSEQ_2, PBOOLE, CARD_1, ARYTM_3, INCPROJ,
ORDINAL4, RELAT_2, NEWTON, MCART_1, MARGREL1, PUA2MSS1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, SETFAM_1, RELAT_1, STRUCT_0, FUNCT_1, PBOOLE, RELSET_1,
PARTFUN1, MCART_1, FINSEQ_1, FINSEQ_2, FUNCT_2, RELAT_2, EQREL_1, CARD_3,
MARGREL1, MSUALG_1, UNIALG_1;
constructors NAT_1, EQREL_1, MSUALG_1, RELSET_1, DOMAIN_1, MARGREL1, XTUPLE_0,
NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1,
FINSEQ_1, EQREL_1, FINSEQ_2, CARD_3, STRUCT_0, UNIALG_1, MSUALG_1,
ORDINAL1, CARD_1, RELSET_1, PBOOLE, MARGREL1, XTUPLE_0, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin
registration
let X be with_non-empty_elements set;
cluster -> non-empty for FinSequence of X;
end;
registration
let A be non empty set;
cluster homogeneous quasi_total non-empty non empty for
PFuncFinSequence of A;
end;
registration
cluster non-empty -> non empty for UAStr;
end;
theorem :: PUA2MSS1:1
for f,g being non-empty Function st product f c= product g holds
dom f = dom g & for x being set st x in dom f holds f.x c= g.x;
theorem :: PUA2MSS1:2
for f,g being non-empty Function st product f = product g holds f = g;
definition
let A be non empty set;
let f be PFuncFinSequence of A;
redefine func rng f -> Subset of PFuncs(A*, A);
end;
definition
let A,B be non empty set;
let S be non empty Subset of PFuncs(A, B);
redefine mode Element of S -> PartFunc of A,B;
end;
definition
let A be non-empty UAStr;
mode OperSymbol of A is Element of dom the charact of A;
mode operation of A is Element of rng the charact of A;
end;
definition
let A be non-empty UAStr;
let o be OperSymbol of A;
func Den(o, A) -> operation of A equals
:: PUA2MSS1:def 1
(the charact of A).o;
end;
begin :: Partitions
::$CT
theorem :: PUA2MSS1:4
for X,Y being set st X is_finer_than Y
for p being FinSequence of X ex q being FinSequence of Y st
product p c= product q;
theorem :: PUA2MSS1:5
for X being set, P,Q being a_partition of X
for f being Function of P,Q st for a being set st a in P holds a c= f.a
for p being FinSequence of P, q being FinSequence of Q holds
product p c= product q iff f*p = q;
theorem :: PUA2MSS1:6
for P being set, f being Function st rng f c= union P
ex p being Function st dom p = dom f & rng p c= P & f in product p;
theorem :: PUA2MSS1:7
for X be set, P being a_partition of X, f being FinSequence of X
ex p being FinSequence of P st f in product p;
theorem :: PUA2MSS1:8
for X,Y being non empty set
for P being a_partition of X, Q being a_partition of Y holds
the set of all [:p,q:] where p is Element of P, q is Element of Q
is a_partition of [:X,Y:];
theorem :: PUA2MSS1:9
for X being non empty set for P being a_partition of X holds
the set of all product p where p is Element of P* is a_partition of X*;
theorem :: PUA2MSS1:10
for X being non empty set, n be Element of NAT
for P being a_partition of X holds
the set of all product p where p is Element of n-tuples_on P
is a_partition of n-tuples_on X;
theorem :: PUA2MSS1:11
for X being non empty set, Y be set st Y c= X
for P being a_partition of X holds
{a /\ Y where a is Element of P: a meets Y} is a_partition of Y;
theorem :: PUA2MSS1:12
for f being non empty Function, P being a_partition of dom f holds
the set of all f|a where a is Element of P is a_partition of f;
theorem :: PUA2MSS1:13
for X being set, p being FinSequence of SmallestPartition X
ex q being FinSequence of X st product p = {q};
definition
let X be set;
mode IndexedPartition of X -> Function means
:: PUA2MSS1:def 2
rng it is a_partition of X & it is one-to-one;
end;
definition
let X be set;
let P be IndexedPartition of X;
redefine func rng P -> a_partition of X;
end;
registration
let X be set;
cluster -> one-to-one non-empty for IndexedPartition of X;
end;
registration
let X be non empty set;
cluster -> non empty for IndexedPartition of X;
end;
definition
let X be set, P be a_partition of X;
redefine func id P -> IndexedPartition of X;
end;
definition
let X be set;
let P be IndexedPartition of X;
let x be object;
assume
x in X;
func P-index_of x -> set means
:: PUA2MSS1:def 3
it in dom P & x in P.it;
end;
theorem :: PUA2MSS1:14
for X being set, P being non-empty Function st Union P = X &
for x,y being set st x in dom P & y in dom P & x <> y holds P.x misses P.y
holds P is IndexedPartition of X;
theorem :: PUA2MSS1:15
for X,Y being non empty set, P being a_partition of Y
for f being Function of X, P st P c= rng f & f is one-to-one
holds f is IndexedPartition of Y;
begin :: Relations generated by operations of partial algebra
scheme :: PUA2MSS1:sch 1
IndRelationEx {A, B() -> non empty set, i() -> Nat,
R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}:
ex R being Relation of A(),B(), F being ManySortedSet of NAT st
R = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i);
scheme :: PUA2MSS1:sch 2
RelationUniq {A, B() -> non empty set, P[set,set]}:
for R1, R2 being Relation of A(), B() st
(for x being Element of A(), y being Element of B() holds
[x,y] in R1 iff P[x,y]) &
(for x being Element of A(), y being Element of B() holds
[x,y] in R2 iff P[x,y]) holds R1 = R2;
scheme :: PUA2MSS1:sch 3
IndRelationUniq {A, B() -> non empty set, i() -> Nat,
R0() -> (Relation of A(),B()), RR(set,set) -> Relation of A(),B()}:
for R1, R2 being Relation of A(),B() st (ex F being ManySortedSet of NAT st
R1 = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i)) & (ex F being ManySortedSet of NAT st
R2 = F.i() & F.0 = R0() &
for i being Nat, R being Relation of A(),B() st R = F.i
holds F.(i+1) = RR(R,i)) holds R1 = R2;
definition
let A be partial non-empty UAStr;
func DomRel A -> Relation of the carrier of A means
:: PUA2MSS1:def 4
for x,y being Element of A holds [x,y] in it iff
for f being operation of A, p,q being FinSequence holds
p^<*x*>^q in dom f iff p^<*y*>^q in dom f;
end;
registration
let A be partial non-empty UAStr;
cluster DomRel A -> total symmetric transitive;
end;
definition
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
func R|^A -> Relation of the carrier of A means
:: PUA2MSS1:def 5
for x,y being Element of A holds [x,y] in it iff [x,y] in R &
for f being operation of A for p,q being FinSequence
st p^<*x*>^q in dom f & p^<*y*>^q in dom f
holds [f.(p^<*x*>^q), f.(p^<*y*>^q)] in R;
end;
definition
let A be non-empty partial UAStr;
let R be Relation of the carrier of A;
let i be Nat;
func R|^(A,i) -> Relation of the carrier of A means
:: PUA2MSS1:def 6
ex F being ManySortedSet of NAT st it = F.i & F.0 = R &
for i being Nat, R being Relation of the carrier of A st R = F.i
holds F.(i+1) = R|^A;
end;
theorem :: PUA2MSS1:16
for A being non-empty partial UAStr, R being Relation of the carrier of A
holds R|^(A,0) = R & R|^(A,1) = R|^A;
theorem :: PUA2MSS1:17
for A being non-empty partial UAStr, i being Nat,
R being Relation of the carrier of A holds R|^(A,i+1) = R|^(A,i)|^A;
theorem :: PUA2MSS1:18
for A being non-empty partial UAStr, i,j being Element of NAT,
R being Relation of the carrier of A holds R|^(A,i+j) = R|^(A,i)|^(A,j);
theorem :: PUA2MSS1:19
for A being non-empty partial UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A
holds R|^A is total symmetric transitive;
theorem :: PUA2MSS1:20
for A being non-empty partial UAStr
for R being Relation of the carrier of A holds R|^A c= R;
theorem :: PUA2MSS1:21
for A being non-empty partial UAStr
for R being Equivalence_Relation of the carrier of A st R c= DomRel A
for i being Element of NAT holds R|^(A,i) is total symmetric transitive;
definition
let A be non-empty partial UAStr;
func LimDomRel A -> Relation of the carrier of A means
:: PUA2MSS1:def 7
for x,y being Element of A holds
[x,y] in it iff for i being Element of NAT holds [x,y] in (DomRel A)|^(A,i);
end;
theorem :: PUA2MSS1:22
for A being non-empty partial UAStr holds LimDomRel A c= DomRel A;
registration
let A be non-empty partial UAStr;
cluster LimDomRel A -> total symmetric transitive;
end;
begin :: Partitability
definition
let X be non empty set;
let f be PartFunc of X*, X;
let P be a_partition of X;
pred f is_partitable_wrt P means
:: PUA2MSS1:def 8
for p being FinSequence of P ex a being Element of P st f.:product p c= a;
end;
definition
let X be non empty set;
let f be PartFunc of X*, X;
let P be a_partition of X;
pred f is_exactly_partitable_wrt P means
:: PUA2MSS1:def 9
f is_partitable_wrt P &
for p being FinSequence of P st product p meets dom f holds
product p c= dom f;
end;
theorem :: PUA2MSS1:23
for A being non-empty partial UAStr for f being operation of A holds
f is_exactly_partitable_wrt SmallestPartition the carrier of A;
scheme :: PUA2MSS1:sch 4
FiniteTransitivity {x, y() -> FinSequence, P[set], R[set,set]}: P[y()]
provided
P[x()] and
len x() = len y() and
for p,q being FinSequence, z1,z2 being set
st P[p^<*z1*>^q] & R[z1,z2] holds P[p^<*z2*>^q] and
for i being Element of NAT st i in dom x() holds R[x().i, y().i];
theorem :: PUA2MSS1:24
for A being non-empty partial UAStr for f being operation of A holds
f is_exactly_partitable_wrt Class LimDomRel A;
definition
let A be partial non-empty UAStr;
mode a_partition of A -> a_partition of the carrier of A means
:: PUA2MSS1:def 10
for f being operation of A holds f is_exactly_partitable_wrt it;
end;
definition
let A be partial non-empty UAStr;
mode IndexedPartition of A -> IndexedPartition of the carrier of A means
:: PUA2MSS1:def 11
rng it is a_partition of A;
end;
definition
let A be partial non-empty UAStr;
let P be IndexedPartition of A;
redefine func rng P -> a_partition of A;
end;
theorem :: PUA2MSS1:25
for A being non-empty partial UAStr holds
Class LimDomRel A is a_partition of A;
theorem :: PUA2MSS1:26
for X being non empty set, P being a_partition of X
for p being FinSequence of P, q1,q2 being FinSequence, x,y being set
st q1^<*x*>^q2 in product p & ex a being Element of P st x in a & y in a
holds q1^<*y*>^q2 in product p;
theorem :: PUA2MSS1:27
for A being partial non-empty UAStr, P being a_partition of A holds
P is_finer_than Class LimDomRel A;
begin :: Morphisms between manysorted signatures
definition
let S1,S2 be ManySortedSign;
let f,g be Function;
pred f,g form_morphism_between S1,S2 means
:: PUA2MSS1:def 12
dom f = the carrier of S1 & dom g = the carrier' of S1 &
rng f c= the carrier of S2 & rng g c= the carrier' of S2 &
f*the ResultSort of S1 = (the ResultSort of S2)*g &
for o being set, p being Function
st o in the carrier' of S1 & p = (the Arity of S1).o
holds f*p = (the Arity of S2).(g.o);
end;
theorem :: PUA2MSS1:28
for S being non void non empty ManySortedSign holds
id the carrier of S, id the carrier' of S form_morphism_between S,S;
theorem :: PUA2MSS1:29
for S1,S2,S3 being ManySortedSign for f1,f2, g1,g2 being Function st
f1, g1 form_morphism_between S1,S2 & f2, g2 form_morphism_between S2,S3
holds f2*f1, g2*g1 form_morphism_between S1,S3;
definition
let S1,S2 be ManySortedSign;
pred S1 is_rougher_than S2 means
:: PUA2MSS1:def 13
ex f,g being Function st f,g form_morphism_between S2,S1 &
rng f = the carrier of S1 & rng g = the carrier' of S1;
end;
definition
let S1,S2 be non void non empty ManySortedSign;
redefine pred S1 is_rougher_than S2;
reflexivity;
end;
theorem :: PUA2MSS1:30
for S1,S2,S3 being ManySortedSign
st S1 is_rougher_than S2 & S2 is_rougher_than S3 holds S1 is_rougher_than S3;
begin :: Manysorted signature of partital algebra
definition
let A be partial non-empty UAStr;
let P be a_partition of A;
func MSSign(A,P) -> strict ManySortedSign means
:: PUA2MSS1:def 14
the carrier of it = P & the carrier' of it =
{[o,p] where o is OperSymbol of A, p is Element of P*:
product p meets dom Den(o,A)} &
for o being OperSymbol of A, p being Element of P*
st product p meets dom Den(o,A) holds (the Arity of it).[o,p] = p &
Den(o, A).:product p c= (the ResultSort of it).[o,p];
end;
registration
let A be partial non-empty UAStr;
let P be a_partition of A;
cluster MSSign(A,P) -> non empty non void;
end;
definition
let A be partial non-empty UAStr;
let P be a_partition of A;
let o be OperSymbol of MSSign(A,P);
redefine func o`1 -> OperSymbol of A;
redefine func o`2 -> Element of P*;
end;
definition
let A be partial non-empty UAStr;
let S be non void non empty ManySortedSign;
let G be MSAlgebra over S;
let P be IndexedPartition of the carrier' of S;
pred A can_be_characterized_by S,G,P means
:: PUA2MSS1:def 15
the Sorts of G is IndexedPartition of A &
dom P = dom the charact of A & for o being OperSymbol of A holds
(the Charact of G)|(P.o) is IndexedPartition of Den(o, A);
end;
definition
let A be partial non-empty UAStr;
let S be non void non empty ManySortedSign;
pred A can_be_characterized_by S means
:: PUA2MSS1:def 16
ex G being MSAlgebra over S, P being IndexedPartition of the carrier' of S st
A can_be_characterized_by S,G,P;
end;
theorem :: PUA2MSS1:31
for A being partial non-empty UAStr, P being a_partition of A
holds A can_be_characterized_by MSSign(A, P);
theorem :: PUA2MSS1:32
for A being partial non-empty UAStr
for S being non void non empty ManySortedSign for G being MSAlgebra over S
for Q being IndexedPartition of the carrier' of S
st A can_be_characterized_by S,G,Q
for o being OperSymbol of A, r being FinSequence of rng the Sorts of G
st product r c= dom Den(o,A) ex s being OperSymbol of S st
(the Sorts of G)*the_arity_of s = r & s in Q.o;
theorem :: PUA2MSS1:33
for A being partial non-empty UAStr, P being a_partition of A
st P = Class LimDomRel A
for S being non void non empty ManySortedSign st A can_be_characterized_by S
holds MSSign(A,P) is_rougher_than S;