:: Technical Preliminaries to Algebraic Specifications
:: by Grzegorz Bancerek
::
:: Received September 7, 1999
:: Copyright (c) 1999-2011 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 Th13: :: 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 by Th13, XBOOLE_1:2;

theorem :: ALGSPEC1:15

canceled;

theorem :: ALGSPEC1:16

for X being set
for f being Function st X c= dom f holds
X -indexing f = f | X

proof end;

theorem :: ALGSPEC1:17

for f being Function holds {} -indexing f = {} ;

theorem Th18: :: ALGSPEC1:18

for X, Y being set
for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f

proof end;

theorem Th19: :: ALGSPEC1:19

for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)

proof end;

theorem Th20: :: ALGSPEC1:20

for X, Y being set
for f being Function holds X -indexing f tolerates Y -indexing f

proof end;

theorem Th21: :: ALGSPEC1:21

for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)

proof end;

theorem Th22: :: ALGSPEC1:22

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:23

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 b₁ being Function st
( dom b₁ = rng f & f * b₁ = id (rng f) )

proof end;

end;

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

theorem Th24: :: ALGSPEC1:24

for f being Function
for g being rng-retract of f holds rng g c= dom f

proof end;

theorem Th25: :: ALGSPEC1:25

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:26

for f being Function st f is one-to-one holds
f " is rng-retract of f

proof end;

theorem :: ALGSPEC1:27

for f being Function st f is one-to-one holds
for g being rng-retract of f holds g = f "

proof end;

theorem Th28: :: ALGSPEC1:28

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:29

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 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 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 Th31: :: ALGSPEC1:31

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 Th32: :: ALGSPEC1:32

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:33

for S being non void Signature
for f being Function holds f, {} form_a_replacement_in S

proof end;

theorem Th34: :: ALGSPEC1:34

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:35

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 A1: 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 b₁, b₂ being non empty non void strict ManySortedSign st the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b₁ & the carrier of b₁ = rng ( the carrier of S -indexing f) & the carrier' of b₁ = rng ( the carrier' of S -indexing g) & the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b₂ & the carrier of b₂ = rng ( the carrier of S -indexing f) & the carrier' of b₂ = rng ( the carrier' of S -indexing g) holds
b₁ = b₂

proof end;

existence
ex b₁ being non empty non void strict ManySortedSign st
( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b₁ & the carrier of b₁ = rng ( the carrier of S -indexing f) & the carrier' of b₁ = 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 b₄ being non empty non void strict ManySortedSign holds
( b₄ = S with-replacement (f,g) iff ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b₄ & the carrier of b₄ = rng ( the carrier of S -indexing f) & the carrier' of b₄ = rng ( the carrier' of S -indexing g) ) );

theorem Th36: :: ALGSPEC1:36

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 Th37: :: ALGSPEC1:37

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 Th38: :: ALGSPEC1:38

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 Th39: :: ALGSPEC1:39

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 Th40: :: ALGSPEC1:40

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 Th41: :: ALGSPEC1:41

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 Th42: :: ALGSPEC1:42

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:43

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 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 (( the carrier of S -indexing f),g) = S with-replacement (f,g)

proof end;

theorem Th45: :: ALGSPEC1:45

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 b₁ being Signature st S is Subsignature of b₁

proof end;

end;

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

theorem :: ALGSPEC1:46

canceled;

theorem Th47: :: ALGSPEC1:47

for S being Signature holds S is Extension of S

proof end;

theorem Th48: :: ALGSPEC1:48

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 Th49: :: ALGSPEC1:49

for S1, S2 being non empty Signature st S1 tolerates S2 holds
S1 +* S2 is Extension of S1

proof end;

theorem Th50: :: ALGSPEC1:50

for S1, S2 being non empty Signature holds S1 +* S2 is Extension of S2

proof end;

theorem Th51: :: ALGSPEC1:51

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:52

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 Extension of S;
coherence
for b₁ being Extension of S holds not b₁ is empty

proof end;

end;

registration

let S be non void Signature;
cluster -> non void Extension of S;
coherence
for b₁ being Extension of S holds not b₁ is void

proof end;

end;

theorem Th53: :: ALGSPEC1:53

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 Extension of S;
existence
ex b₁ being Extension of S st
( not b₁ is empty & not b₁ is void & b₁ is strict )

proof end;

end;

theorem Th54: :: ALGSPEC1:54

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:55

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:56

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 of S;
existence
ex b₁ being set ex S being non void Signature st b₁ is feasible MSAlgebra of S

proof end;

end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :
for b₁ being set holds
( b₁ is Algebra iff ex S being non void Signature st b₁ is feasible MSAlgebra of 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 of E;
existence
ex b₁ being Algebra ex E being non void Extension of S st b₁ is feasible MSAlgebra of E

proof end;

end;

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

theorem :: ALGSPEC1:57

for S being non void Signature
for A being feasible MSAlgebra of S holds A is Algebra of S

proof end;

theorem :: ALGSPEC1:58

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 Th59: :: ALGSPEC1:59

for S being Signature
for E being non empty Signature
for A being MSAlgebra of 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 Th60: :: ALGSPEC1:60

for S being non void Signature
for E being non empty Signature
for A being MSAlgebra of 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:61

for S being non empty Signature
for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra of E holds
A is MSAlgebra of E +* S

proof end;

theorem Th62: :: ALGSPEC1:62

for S1, S2 being non empty Signature
for A being MSAlgebra of S1 st A is MSAlgebra of S2 holds
( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )

proof end;

theorem :: ALGSPEC1:63

canceled;

registration

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

proof end;

end;

theorem Th64: :: ALGSPEC1:64

for S being non void Signature
for A being disjoint_valued MSAlgebra of S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )

proof end;

theorem Th65: :: ALGSPEC1:65

for S, S9 being non void Signature
for A being non-empty disjoint_valued MSAlgebra of S st A is MSAlgebra of 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:66

for S, S9 being non void Signature
for A being non-empty disjoint_valued MSAlgebra of S st A is Algebra of S9 holds
S is Extension of S9

proof end;