:: Technical Preliminaries to Algebraic Specifications
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem Th1: :: ALGSPEC1:1
for f, g, h being Function st (dom f) /\ (dom g) c= dom h holds
(f +* g) +* h = (g +* f) +* h
proof end;

theorem Th2: :: ALGSPEC1:2
for f, g, h being Function st f c= g & (rng h) /\ (dom g) c= dom f holds
g * h = f * h
proof end;

theorem Th3: :: 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
proof end;

theorem Th4: :: ALGSPEC1:4
for f1, f2, g1, g2 being Function st f1 tolerates f2 & g1 tolerates g2 holds
f1 * g1 tolerates f2 * g2
proof end;

theorem Th5: :: ALGSPEC1:5
for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *
proof end;

theorem Th6: :: ALGSPEC1:6
for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *
proof end;

definition
let X be set ;
let f be Function;
func X -indexing f -> ManySortedSet of X equals :: ALGSPEC1:def 1
(id X) +* (f | X);
coherence
(id X) +* (f | X) is ManySortedSet of X
proof end;
end;

:: deftheorem defines -indexing ALGSPEC1:def 1 :
for X being set
for f being Function holds X -indexing f = (id X) +* (f | X);

theorem Th7: :: ALGSPEC1:7
for X being set
for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)
proof end;

theorem Th8: :: ALGSPEC1:8
for X being non empty set
for f being Function
for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x
proof end;

theorem Th9: :: ALGSPEC1:9
for X, x being set
for 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 ) )
proof end;

theorem Th10: :: ALGSPEC1:10
for X being set
for f being Function st dom f = X holds
X -indexing f = f
proof end;

theorem Th11: :: ALGSPEC1:11
for X being set
for f being Function holds X -indexing (X -indexing f) = X -indexing f
proof end;

theorem Th12: :: ALGSPEC1:12
for X being set
for f being Function holds X -indexing ((id X) +* f) = X -indexing f
proof end;

theorem :: ALGSPEC1:13
for X being set
for f being Function st f c= id X holds
X -indexing f = id X
proof end;

theorem :: ALGSPEC1:14
for X being set holds X -indexing {} = id X ;

theorem :: ALGSPEC1:15
for X being set
for f being Function st X c= dom f holds
X -indexing f = f | X
proof end;

theorem :: ALGSPEC1:16
for f being Function holds {} -indexing f = {} ;

theorem Th17: :: ALGSPEC1:17
for X, Y being set
for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f
proof end;

theorem Th18: :: ALGSPEC1:18
for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)
proof end;

theorem Th19: :: ALGSPEC1:19
for X, Y being set
for f being Function holds X -indexing f tolerates Y -indexing f
proof end;

theorem Th20: :: ALGSPEC1:20
for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)
proof end;

theorem Th21: :: ALGSPEC1:21
for X being non empty set
for f, g being Function st rng g c= X holds
(X -indexing f) * g = ((id X) +* f) * g
proof end;

theorem :: ALGSPEC1:22
for f, g being Function st dom f misses dom g & rng g misses dom f holds
for X being set holds f * (X -indexing g) = f | X
proof end;

definition
let f be Function;
mode rng-retract of f -> Function means :Def2: :: ALGSPEC1:def 2
( dom it = rng f & f * it = id (rng f) );
existence
ex b1 being Function st
( dom b1 = rng f & f * b1 = id (rng f) )
proof end;
end;

:: deftheorem Def2 defines rng-retract ALGSPEC1:def 2 :
for f, b2 being Function holds
( b2 is rng-retract of f iff ( dom b2 = rng f & f * b2 = id (rng f) ) );

theorem Th23: :: ALGSPEC1:23
for f being Function
for g being rng-retract of f holds rng g c= dom f
proof end;

theorem Th24: :: ALGSPEC1:24
for f being Function
for 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 )
proof end;

theorem :: ALGSPEC1:25
for f being Function st f is one-to-one holds
f " is rng-retract of f
proof end;

theorem :: ALGSPEC1:26
for f being Function st f is one-to-one holds
for g being rng-retract of f holds g = f "
proof end;

theorem Th27: :: ALGSPEC1:27
for f1, f2 being Function st f1 tolerates f2 holds
for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2
proof end;

theorem :: ALGSPEC1:28
for f1, f2 being Function st f1 c= f2 holds
for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2
proof end;

begin

definition
let S be non empty non void ManySortedSign ;
let f, g be Function;
pred f,g form_a_replacement_in S means :Def3: :: 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;

:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def 3 :
for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff 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) ) );

theorem Th29: :: ALGSPEC1:29
for S being non empty non void ManySortedSign
for 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) ) )
proof end;

theorem Th30: :: ALGSPEC1:30
for S being non empty non void ManySortedSign
for 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 )
proof end;

theorem Th31: :: ALGSPEC1:31
for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
f,g form_a_replacement_in S
proof end;

theorem :: ALGSPEC1:32
for S being non void Signature
for f being Function holds f, {} form_a_replacement_in S
proof end;

theorem Th33: :: ALGSPEC1:33
for S being non void Signature
for g, f being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds
f,g form_a_replacement_in S
proof end;

theorem :: ALGSPEC1:34
for S being non void Signature
for g, f being Function st g is one-to-one & rng g misses the carrier' of S holds
f,g form_a_replacement_in S
proof end;

registration
let X be set ;
let 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 ;
coherence
not ManySortedSign(# X,Y,a,r #) is void ;
end;

definition
let S be non empty non void ManySortedSign ;
let f, g be Function;
assume X1: f,g form_a_replacement_in S ;
func S with-replacement (f,g) -> non empty non void strict ManySortedSign means :Def4: :: 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) );
uniqueness
for b1, b2 being non empty non void strict ManySortedSign st the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng ( the carrier of S -indexing f) & the carrier' of b1 = rng ( the carrier' of S -indexing g) & the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b2 & the carrier of b2 = rng ( the carrier of S -indexing f) & the carrier' of b2 = rng ( the carrier' of S -indexing g) holds
b1 = b2
proof end;
existence
ex b1 being non empty non void strict ManySortedSign st
( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng ( the carrier of S -indexing f) & the carrier' of b1 = rng ( the carrier' of S -indexing g) )
proof end;
end;

:: deftheorem Def4 defines with-replacement ALGSPEC1:def 4 :
for S being non empty non void ManySortedSign
for f, g being Function st f,g form_a_replacement_in S holds
for b4 being non empty non void strict ManySortedSign holds
( b4 = S with-replacement (f,g) iff ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b4 & the carrier of b4 = rng ( the carrier of S -indexing f) & the carrier' of b4 = rng ( the carrier' of S -indexing g) ) );

theorem Th35: :: 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
proof end;

theorem Th36: :: ALGSPEC1:36
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))
proof end;

theorem Th37: :: ALGSPEC1:37
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
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 holds
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
proof end;

theorem Th38: :: ALGSPEC1:38
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
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
proof end;

theorem Th39: :: ALGSPEC1:39
for S, S9 being non void Signature
for f, g being Function st f,g form_morphism_between S,S9 holds
S with-replacement (f,g) is Subsignature of S9
proof end;

theorem Th40: :: ALGSPEC1:40
for S being non void Signature
for 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_morphism_between S,S with-replacement (f,g) )
proof end;

theorem Th41: :: ALGSPEC1:41
for S being non void Signature
for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)
proof end;

theorem :: ALGSPEC1:42
for S being non void Signature
for f, g being Function st dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S holds
f,g form_morphism_between S,S with-replacement (f,g)
proof end;

theorem Th43: :: ALGSPEC1:43
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)
proof end;

theorem Th44: :: ALGSPEC1:44
for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)
proof end;

begin

definition
let S be Signature;
mode Extension of S -> Signature means :Def5: :: ALGSPEC1:def 5
S is Subsignature of it;
existence
ex b1 being Signature st S is Subsignature of b1
proof end;
end;

:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :
for S, b2 being Signature holds
( b2 is Extension of S iff S is Subsignature of b2 );

theorem Th45: :: ALGSPEC1:45
for S being Signature holds S is Extension of S
proof end;

theorem Th46: :: ALGSPEC1:46
for S1 being Signature
for S2 being Extension of S1
for S3 being Extension of S2 holds S3 is Extension of S1
proof end;

theorem Th47: :: ALGSPEC1:47
for S1, S2 being non empty Signature st S1 tolerates S2 holds
S1 +* S2 is Extension of S1
proof end;

theorem Th48: :: ALGSPEC1:48
for S1, S2 being non empty Signature holds S1 +* S2 is Extension of S2
proof end;

theorem Th49: :: 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
proof end;

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 ) )
proof end;

registration
let S be non empty Signature;
cluster -> non empty for Extension of S;
coherence
for b1 being Extension of S holds not b1 is empty
proof end;
end;

registration
let S be non void Signature;
cluster -> non void for Extension of S;
coherence
for b1 being Extension of S holds not b1 is void
proof end;
end;

theorem Th51: :: ALGSPEC1:51
for S, T being Signature st S is empty holds
T is Extension of S
proof end;

registration
let S be Signature;
cluster non empty non void strict feasible for Extension of S;
existence
ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict )
proof end;
end;

theorem Th52: :: ALGSPEC1:52
for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S
proof end;

theorem :: ALGSPEC1:53
for f, g being Function
for S being non void Signature
for 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)
proof end;

theorem :: ALGSPEC1:54
for S1, S2 being non void Signature st S1 tolerates S2 holds
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))
proof end;

begin

definition
mode Algebra -> set means :Def6: :: ALGSPEC1:def 6
 ex S being non void Signature st it is feasible MSAlgebra over S;
existence
ex b1 being set ex S being non void Signature st b1 is feasible MSAlgebra over S
proof end;
end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :
for b1 being set holds
( b1 is Algebra iff ex S being non void Signature st b1 is feasible MSAlgebra over S );

definition
let S be Signature;
mode Algebra of S -> Algebra means :Def7: :: ALGSPEC1:def 7
 ex E being non void Extension of S st it is feasible MSAlgebra over E;
existence
ex b1 being Algebra ex E being non void Extension of S st b1 is feasible MSAlgebra over E
proof end;
end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :
for S being Signature
for b2 being Algebra holds
( b2 is Algebra of S iff ex E being non void Extension of S st b2 is feasible MSAlgebra over E );

theorem :: ALGSPEC1:55
for S being non void Signature
for A being feasible MSAlgebra over S holds A is Algebra of S
proof end;

theorem :: ALGSPEC1:56
for S being Signature
for E being Extension of S
for A being Algebra of E holds A is Algebra of S
proof end;

theorem Th57: :: ALGSPEC1:57
for S being Signature
for E being non empty Signature
for 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 )
proof end;

theorem Th58: :: ALGSPEC1:58
for S being non void Signature
for E being non empty Signature
for A being MSAlgebra over E st A is Algebra of S holds
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))
proof end;

theorem :: ALGSPEC1:59
for S being non empty Signature
for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra over E holds
A is MSAlgebra over E +* S
proof end;

theorem Th60: :: 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 )
proof end;

registration
let S be non void Signature;
let A be non-empty disjoint_valued MSAlgebra over S;
cluster the Sorts of A -> one-to-one ;
coherence
the Sorts of A is one-to-one
proof end;
end;

theorem Th61: :: 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 )
proof end;

theorem Th62: :: 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
ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of S9, the carrier' of S9, the Arity of S9, the ResultSort of S9 #)
proof end;

theorem :: ALGSPEC1:63
for S, 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
proof end;