The abstract of the Mizar article:

Technical Preliminaries to Algebraic Specifications

by

Grzegorz Bancerek

Received September 7, 1999

MML identifier: ALGSPEC1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCT_4, PARTFUN1, PBOOLE, AMI_1,
      MSUALG_1, QC_LANG1, CATALG_1, PUA2MSS1, TREES_1, FINSEQ_1, INSTALG1,
      FUNCSDOM, MSUALG_6, TDGROUP, PRALG_1, ZF_REFLE, PROB_2, CARD_3, ALGSPEC1;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, MSAFREE1, FINSEQ_1,
      RELSET_1, PARTFUN1, FINSEQ_2, FUNCT_4, PBOOLE, LANG1, FUNCT_2, STRUCT_0,
      CARD_3, MSUALG_1, PROB_2, PUA2MSS1, CIRCCOMB, MSUALG_6, INSTALG1,
      CATALG_1;
 constructors MSAFREE1, PUA2MSS1, CIRCCOMB, MSUALG_6, CATALG_1;
 clusters RELAT_1, FUNCT_1, PRALG_1, RELSET_1, STRUCT_0, MSUALG_1, MSUALG_2,
      MSAFREE, PRE_CIRC, CIRCCOMB, MSUALG_6, INSTALG1, CATALG_1, XBOOLE_0;
 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 c= rng g & 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 holds X-indexing (f|X) = X-indexing f;

theorem :: ALGSPEC1:16
 for X being set, f being Function st X c= dom f holds X-indexing f = f|X;

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

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

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

theorem :: ALGSPEC1:20
 for X,Y being set, f being Function holds X-indexing f tolerates Y-indexing f;

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

theorem :: ALGSPEC1:22
 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:23
   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:24
 for f being Function, g being rng-retract of f holds rng g c= dom f;

theorem :: ALGSPEC1:25
 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:26
   for f being Function st f is one-to-one holds f" is rng-retract of f;

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

theorem :: ALGSPEC1:28
 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:29
   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 OperSymbols of S) +* g).o1 = ((id the OperSymbols 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:30
 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 OperSymbols of S)-indexing g).o1
       = ((the OperSymbols 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:31
 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 OperSymbols of S)-indexing g
      form_a_replacement_in S;

reserve S,S' for non void Signature, f,g for Function;

theorem :: ALGSPEC1:32
 f,g form_morphism_between S,S' implies f,g form_a_replacement_in S;


theorem :: ALGSPEC1:33
   f, {} form_a_replacement_in S;

theorem :: ALGSPEC1:34
 g is one-to-one & (the OperSymbols of S) /\ rng g c= dom g
   implies f,g form_a_replacement_in S;


theorem :: ALGSPEC1:35
   g is one-to-one & rng g misses the OperSymbols of S
   implies f,g form_a_replacement_in S;


definition
 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 OperSymbols of S)-indexing g
     form_morphism_between S, it &
    the carrier of it = rng ((the carrier of S)-indexing f) &
    the OperSymbols of it = rng ((the OperSymbols of S)-indexing g);
end;

theorem :: 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;

theorem :: ALGSPEC1:37
 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:38
 f,g form_a_replacement_in S implies
 for f' being Function of the carrier of S,
                          the carrier of S with-replacement (f,g)
  st f' = (the carrier of S)-indexing f
 for g' being rng-retract of (the OperSymbols of S)-indexing g holds
  the Arity of S with-replacement (f,g) = f'* *(the Arity of S)*g';

theorem :: ALGSPEC1:39
 f,g form_a_replacement_in S implies
 for g' being rng-retract of (the OperSymbols of S)-indexing g holds
  the ResultSort of S with-replacement (f,g)
     = ((the carrier of S)-indexing f)*(the ResultSort of S)*g';

theorem :: ALGSPEC1:40
 f,g form_morphism_between S,S' implies
  S with-replacement (f,g) is Subsignature of S';

theorem :: ALGSPEC1:41
 f,g form_a_replacement_in S iff
   (the carrier of S)-indexing f, (the OperSymbols of S)-indexing g
             form_morphism_between S, S with-replacement (f,g);

theorem :: ALGSPEC1:42
 dom f c= the carrier of S & dom g c= the OperSymbols of S &
   f,g form_a_replacement_in S
  implies (id the carrier of S) +* f, (id the OperSymbols of S) +* g
             form_morphism_between S, S with-replacement (f,g);

theorem :: ALGSPEC1:43
   dom f = the carrier of S & dom g = the OperSymbols of S &
   f,g form_a_replacement_in S
  implies f,g form_morphism_between S, S with-replacement (f,g);

theorem :: ALGSPEC1:44
 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:45
 f,g form_a_replacement_in S implies
  S with-replacement (f, (the OperSymbols 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;

canceled;

theorem :: ALGSPEC1:47
 for S being Signature holds S is Extension of S;

theorem :: ALGSPEC1:48
 for S1 being Signature, S2 being Extension of S1, S3 being Extension of S2
  holds S3 is Extension of S1;

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

theorem :: ALGSPEC1:50
 for S1, S2 being non empty Signature
  holds S1+*S2 is Extension of S2;

theorem :: 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;

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;

definition
 let S be non empty Signature;
 cluster -> non empty Extension of S;
end;

definition
 let S be non void Signature;
 cluster -> non void Extension of S;
end;

theorem :: ALGSPEC1:53
 for S,T being Signature st S is empty
   holds T is Extension of S;

definition
 let S be Signature;
 cluster non empty non void strict Extension of S;
end;

theorem :: ALGSPEC1:54
 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:55
   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:56
   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 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:57
   for S being non void Signature, A being feasible MSAlgebra over S
   holds A is Algebra of S;

theorem :: ALGSPEC1:58
   for S being Signature, E being Extension of S, A being Algebra of E
  holds A is Algebra of S;

theorem :: ALGSPEC1:59
 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 OperSymbols of S c= the OperSymbols of E;

theorem :: ALGSPEC1:60
 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:61
   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:62
 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 OperSymbols of S1 = the OperSymbols of S2;

theorem :: ALGSPEC1:63
 for S being non void Signature
 for A being non-empty disjoint_valued MSAlgebra over S
  holds the Sorts of A is one-to-one;

theorem :: ALGSPEC1:64
 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:65
 for S,S' being non void Signature
 for A being non-empty disjoint_valued MSAlgebra over S
  st A is MSAlgebra over S'
  holds the ManySortedSign of S = the ManySortedSign of S';

theorem :: ALGSPEC1:66
   for S' being non void Signature
 for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S'
  holds S is Extension of S';