:: Technical Preliminaries to Algebraic Specifications
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2019 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 FUNCT_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_4, PARTFUN1, SUBSET_1,
PBOOLE, STRUCT_0, MSUALG_1, MARGREL1, CATALG_1, PUA2MSS1, TREES_1,
FINSEQ_1, INSTALG1, FUNCSDOM, MSUALG_6, PROB_2, CARD_3, ALGSPEC1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MSAFREE1, FINSEQ_1,
PBOOLE, RELSET_1, PARTFUN1, FINSEQ_2, FUNCT_4, LANG1, FUNCT_2, STRUCT_0,
CARD_3, MSUALG_1, PROB_2, PUA2MSS1, CIRCCOMB, MSUALG_6, INSTALG1,
CATALG_1;
constructors MSAFREE1, CIRCCOMB, PUA2MSS1, MSUALG_6, CATALG_1, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, PBOOLE, STRUCT_0, MSUALG_1,
MSUALG_2, CIRCCOMB, MSUALG_6, INSTALG1, CATALG_1, RELSET_1, FINSEQ_1,
FUNCT_4;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: ALGSPEC1:1
for f,g,h being Function st dom f /\ dom g c= dom h holds f+*g+*h = g+*f+*h;
theorem :: ALGSPEC1:2
for f,g,h being Function st f c= g & (rng h) /\ dom g c= dom f
holds g*h = f*h;
theorem :: ALGSPEC1:3
for f,g,h being Function st dom f misses rng h & g.:dom h misses
dom f holds f*(g+*h) = f*g;
theorem :: ALGSPEC1:4
for f1,f2,g1,g2 being Function st f1 tolerates f2 & g1 tolerates
g2 holds f1*g1 tolerates f2*g2;
theorem :: ALGSPEC1:5
for X1,Y1, X2,Y2 being non empty set for f being Function of X1,
X2, g being Function of Y1,Y2 st f c= g holds f* c= g*;
theorem :: ALGSPEC1:6
for X1,Y1, X2,Y2 be non empty set for f being Function of X1,X2,
g being Function of Y1,Y2 st f tolerates g holds f* tolerates g*;
definition
let X be set, f be Function;
func X-indexing(f) -> ManySortedSet of X equals
:: ALGSPEC1:def 1
(id X) +* (f|X);
end;
theorem :: ALGSPEC1:7
for X being set, f being Function holds rng (X-indexing f) = (X \
dom f) \/ f.:X;
theorem :: ALGSPEC1:8
for X being non empty set, f being Function, x being Element of X
holds (X-indexing f).x = ((id X) +* f).x;
theorem :: ALGSPEC1:9
for X,x being set, f being Function st x in X holds (x in dom f
implies (X-indexing f).x = f.x) & (not x in dom f implies (X-indexing f).x = x)
;
theorem :: ALGSPEC1:10
for X being set, f being Function st dom f = X holds X-indexing f = f;
theorem :: ALGSPEC1:11
for X being set, f being Function holds X-indexing (X-indexing f
) = X-indexing f;
theorem :: ALGSPEC1:12
for X being set, f being Function holds X-indexing ((id X)+*f) = X-indexing f
;
theorem :: ALGSPEC1:13
for X being set, f being Function st f c= id X holds X-indexing f = id X;
theorem :: ALGSPEC1:14
for X being set holds X-indexing {} = id X;
theorem :: ALGSPEC1:15
for X being set, f being Function st X c= dom f holds X-indexing f = f |X;
theorem :: ALGSPEC1:16
for f being Function holds {}-indexing f = {};
theorem :: ALGSPEC1:17
for X,Y being set, f being Function st X c= Y holds (Y-indexing
f)|X = X-indexing f;
theorem :: ALGSPEC1:18
for X,Y being set, f being Function holds (X \/ Y)-indexing f =
(X-indexing f) +* (Y-indexing f);
theorem :: ALGSPEC1:19
for X,Y being set, f being Function holds X-indexing f tolerates Y-indexing f
;
theorem :: ALGSPEC1:20
for X,Y being set, f being Function holds (X \/ Y)-indexing f =
(X-indexing f) \/ (Y-indexing f);
theorem :: ALGSPEC1:21
for X being non empty set, f,g being Function st rng g c= X
holds (X-indexing f)*g = ((id X) +* f)*g;
theorem :: ALGSPEC1:22
for f,g being Function st dom f misses dom g & rng g misses dom f for
X being set holds f*(X-indexing g) = f|X;
definition
let f be Function;
mode rng-retract of f -> Function means
:: ALGSPEC1:def 2
dom it = rng f & f*it = id rng f;
end;
theorem :: ALGSPEC1:23
for f being Function, g being rng-retract of f holds rng g c= dom f;
theorem :: ALGSPEC1:24
for f being Function, g being rng-retract of f for x being set
st x in rng f holds g.x in dom f & f.(g.x) = x;
theorem :: ALGSPEC1:25
for f being Function st f is one-to-one holds f" is rng-retract of f;
theorem :: ALGSPEC1:26
for f being Function st f is one-to-one for g being rng-retract of f
holds g = f";
theorem :: ALGSPEC1:27
for f1,f2 being Function st f1 tolerates f2 for g1 being
rng-retract of f1, g2 being rng-retract of f2 holds g1+*g2 is rng-retract of f1
+*f2;
theorem :: ALGSPEC1:28
for f1,f2 being Function st f1 c= f2 for g1 being rng-retract of f1 ex
g2 being rng-retract of f2 st g1 c= g2;
begin :: Replacement in signature
definition
let S be non empty non void ManySortedSign;
let f,g be Function;
pred f,g form_a_replacement_in S means
:: ALGSPEC1:def 3
for o1,o2 being OperSymbol of
S st ((id the carrier' of S) +* g).o1 = ((id the carrier' of S) +* g).o2 holds
((id the carrier of S) +* f)*the_arity_of o1 = ((id the carrier of S) +* f)*
the_arity_of o2 & ((id the carrier of S) +* f).the_result_sort_of o1 = ((id the
carrier of S) +* f).the_result_sort_of o2;
end;
theorem :: ALGSPEC1:29
for S being non empty non void ManySortedSign, f,g being
Function holds f,g form_a_replacement_in S iff for o1,o2 being OperSymbol of S
st ((the carrier' of S)-indexing g).o1 = ((the carrier' of S)-indexing g).o2
holds ((the carrier of S)-indexing f)*the_arity_of o1 = ((the carrier of S)
-indexing f)*the_arity_of o2 & ((the carrier of S)-indexing f).
the_result_sort_of o1 = ((the carrier of S)-indexing f).the_result_sort_of o2
;
theorem :: ALGSPEC1:30
for S being non empty non void ManySortedSign, f,g being
Function holds f,g form_a_replacement_in S iff (the carrier of S)-indexing f, (
the carrier' of S)-indexing g form_a_replacement_in S;
reserve S,S9 for non void Signature,
f,g for Function;
theorem :: ALGSPEC1:31
f,g form_morphism_between S,S9 implies f,g form_a_replacement_in S;
theorem :: ALGSPEC1:32
f, {} form_a_replacement_in S;
theorem :: ALGSPEC1:33
g is one-to-one & (the carrier' of S) /\ rng g c= dom g implies
f,g form_a_replacement_in S;
theorem :: ALGSPEC1:34
g is one-to-one & rng g misses the carrier' of S implies f,g
form_a_replacement_in S;
registration
let X be set, Y be non empty set;
let a be Function of Y, X*;
let r be Function of Y, X;
cluster ManySortedSign(#X, Y, a, r#) -> non void;
end;
definition
let S be non empty non void ManySortedSign;
let f,g be Function such that
f,g form_a_replacement_in S;
func S with-replacement (f,g) -> strict non empty non void ManySortedSign
means
:: ALGSPEC1:def 4
(the carrier of S)-indexing f, (the carrier' of S)-indexing g
form_morphism_between S, it & the carrier of it = rng ((the carrier of S)
-indexing f) & the carrier' of it = rng ((the carrier' of S)-indexing g);
end;
theorem :: ALGSPEC1:35
for S1,S2 being non void Signature for f being Function of the
carrier of S1, the carrier of S2 for g being Function st f,g
form_morphism_between S1,S2 holds f**the Arity of S1 = (the Arity of S2)*g;
theorem :: ALGSPEC1:36
f,g form_a_replacement_in S implies (the carrier of S)-indexing
f is Function of the carrier of S, the carrier of S with-replacement (f,g);
theorem :: ALGSPEC1:37
f,g form_a_replacement_in S implies for f9 being Function of the
carrier of S, the carrier of S with-replacement (f,g) st f9 = (the carrier of S
)-indexing f for g9 being rng-retract of (the carrier' of S)-indexing g holds
the Arity of S with-replacement (f,g) = f9* *(the Arity of S)*g9;
theorem :: ALGSPEC1:38
f,g form_a_replacement_in S implies for g9 being rng-retract of
(the carrier' of S)-indexing g holds the ResultSort of S with-replacement (f,g)
= ((the carrier of S)-indexing f)*(the ResultSort of S)*g9;
theorem :: ALGSPEC1:39
f,g form_morphism_between S,S9 implies S with-replacement (f,g)
is Subsignature of S9;
theorem :: ALGSPEC1:40
f,g form_a_replacement_in S iff (the carrier of S)-indexing f, (
the carrier' of S)-indexing g form_morphism_between S, S with-replacement (f,g)
;
theorem :: ALGSPEC1:41
dom f c= the carrier of S & dom g c= the carrier' of S & f,g
form_a_replacement_in S implies (id the carrier of S) +* f, (id the carrier' of
S) +* g form_morphism_between S, S with-replacement (f,g);
theorem :: ALGSPEC1:42
dom f = the carrier of S & dom g = the carrier' of S & f,g
form_a_replacement_in S implies f,g form_morphism_between S, S with-replacement
(f,g);
theorem :: ALGSPEC1:43
f,g form_a_replacement_in S implies S with-replacement ((the
carrier of S)-indexing f, g) = S with-replacement (f,g);
theorem :: ALGSPEC1:44
f,g form_a_replacement_in S implies S with-replacement (f, (the
carrier' of S)-indexing g) = S with-replacement (f,g);
begin :: Signature extensions
definition
let S be Signature;
mode Extension of S -> Signature means
:: ALGSPEC1:def 5
S is Subsignature of it;
end;
theorem :: ALGSPEC1:45
for S being Signature holds S is Extension of S;
theorem :: ALGSPEC1:46
for S1 being Signature, S2 being Extension of S1, S3 being
Extension of S2 holds S3 is Extension of S1;
theorem :: ALGSPEC1:47
for S1,S2 being non empty Signature st S1 tolerates S2 holds S1
+*S2 is Extension of S1;
theorem :: ALGSPEC1:48
for S1, S2 being non empty Signature holds S1+*S2 is Extension of S2;
theorem :: ALGSPEC1:49
for S1,S2,S being non empty ManySortedSign for f1,g1, f2,g2
being Function st f1 tolerates f2 & f1, g1 form_morphism_between S1, S & f2, g2
form_morphism_between S2, S holds f1+*f2, g1+*g2 form_morphism_between S1+*S2,
S;
theorem :: ALGSPEC1:50
for S1,S2,E being non empty Signature holds E is Extension of S1 & E
is Extension of S2 iff S1 tolerates S2 & E is Extension of S1+*S2;
registration
let S be non empty Signature;
cluster -> non empty for Extension of S;
end;
registration
let S be non void Signature;
cluster -> non void for Extension of S;
end;
theorem :: ALGSPEC1:51
for S,T being Signature st S is empty holds T is Extension of S;
registration
let S be Signature;
cluster non empty non void strict for Extension of S;
end;
theorem :: ALGSPEC1:52
for S being non void Signature, E being Extension of S st
f,g form_a_replacement_in E holds f,g form_a_replacement_in S;
theorem :: ALGSPEC1:53
for S being non void Signature, E being Extension of S st f,g
form_a_replacement_in E holds E with-replacement(f,g) is Extension of S
with-replacement(f,g);
theorem :: ALGSPEC1:54
for S1,S2 being non void Signature st S1 tolerates S2 for f,g being
Function st f,g form_a_replacement_in S1+*S2 holds (S1+*S2) with-replacement (f
,g) = (S1 with-replacement (f,g))+*(S2 with-replacement (f,g));
begin :: Algebras
definition
mode Algebra -> object means
:: ALGSPEC1:def 6
ex S being non void Signature st it is feasible MSAlgebra over S;
end;
definition
let S be Signature;
mode Algebra of S -> Algebra means
:: ALGSPEC1:def 7
ex E being non void Extension of S st it is feasible MSAlgebra over E;
end;
theorem :: ALGSPEC1:55
for S being non void Signature, A being feasible MSAlgebra over S
holds A is Algebra of S;
theorem :: ALGSPEC1:56
for S being Signature, E being Extension of S, A being Algebra of E
holds A is Algebra of S;
theorem :: ALGSPEC1:57
for S being Signature, E being non empty Signature, A being
MSAlgebra over E st A is Algebra of S holds the carrier of S c= the carrier of
E & the carrier' of S c= the carrier' of E;
theorem :: ALGSPEC1:58
for S being non void Signature, E being non empty Signature for
A being MSAlgebra over E st A is Algebra of S for o being OperSymbol of S holds
(the Charact of A).o is Function of (the Sorts of A)#.the_arity_of o, (the
Sorts of A).the_result_sort_of o;
theorem :: ALGSPEC1:59
for S being non empty Signature, A being Algebra of S for E being non
empty ManySortedSign st A is MSAlgebra over E holds A is MSAlgebra over E+*S;
theorem :: ALGSPEC1:60
for S1,S2 being non empty Signature for A being MSAlgebra over
S1 st A is MSAlgebra over S2 holds the carrier of S1 = the carrier of S2 & the
carrier' of S1 = the carrier' of S2;
registration
let S be non void Signature, A be non-empty disjoint_valued MSAlgebra over S;
cluster the Sorts of A -> one-to-one;
end;
theorem :: ALGSPEC1:61
for S being non void Signature for A being disjoint_valued
MSAlgebra over S for C1,C2 being Component of the Sorts of A holds C1 = C2 or
C1 misses C2;
theorem :: ALGSPEC1:62
for S,S9 being non void Signature for A being non-empty
disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds the
ManySortedSign of S = the ManySortedSign of S9;
theorem :: ALGSPEC1:63
for S9 being non void Signature for A being non-empty disjoint_valued
MSAlgebra over S st A is Algebra of S9 holds S is Extension of S9;