:: Free Universal Algebra Construction
::  by Beata Perkowska
::
:: Received October 20, 1993
:: Copyright (c) 1993-2021 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 NUMBERS, SUBSET_1, XBOOLE_0, ARYTM_1, CARD_1, RELAT_1, FINSEQ_1,
      QUANTAL1, UNIALG_1, UNIALG_2, FUNCT_1, MSAFREE, TARSKI, STRUCT_0,
      FINSEQ_2, PRELAMB, CQC_SIM1, MSUALG_3, FUNCOP_1, PARTFUN1, FUNCT_2,
      NAT_1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, CARD_3, TREES_2,
      QC_LANG1, FREEALG;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1,
      RELSET_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, FUNCOP_1, FINSEQ_2,
      TREES_2, TREES_3, TREES_4, MARGREL1, STRUCT_0, UNIALG_1, UNIALG_2, LANG1,
      DTCONSTR, PRE_POLY, ALG_1;
 constructors DOMAIN_1, FINSEQOP, DTCONSTR, ALG_1, RELSET_1, PRE_POLY;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, PARTFUN1, XREAL_0,
      FINSEQ_1, FINSEQ_2, TREES_3, STRUCT_0, UNIALG_2, DTCONSTR, CARD_1,
      RELSET_1, MARGREL1, FUNCT_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

::
:: Preliminaries
::

reserve x,y for set,
  n for Nat;

definition
  let IT be set;
  attr IT is disjoint_with_NAT means
:: FREEALG:def 1

  IT misses NAT;
end;

registration
  cluster non empty disjoint_with_NAT for set;
end;

notation
  let IT be Relation;
  antonym IT is with_zero for IT is non-empty;
  synonym IT is without_zero for IT is non-empty;
end;

definition
  let IT be Relation;
  redefine attr IT is with_zero means
:: FREEALG:def 2

  0 in rng IT;
end;

registration
  cluster non empty with_zero for FinSequence of NAT;
  cluster non empty without_zero for FinSequence of NAT;
end;

begin

::
:: Free Universal Algebra - General Notions
::

definition
  let U1 be Universal_Algebra, n be Nat;
  assume
 n in dom (the charact of U1);

  func oper(n,U1) -> operation of U1 equals
:: FREEALG:def 3

  (the charact of U1).n;
end;

definition
  let U0 be Universal_Algebra;
  mode GeneratorSet of U0 -> Subset of U0 means
:: FREEALG:def 4
    for A being Subset of U0 st A
    is opers_closed & it c= A holds A = the carrier of U0;
end;

definition
  let U0 be Universal_Algebra;
  let IT be GeneratorSet of U0;
  attr IT is free means
:: FREEALG:def 5

  for U1 be Universal_Algebra st U0,U1
are_similar holds for f be Function of IT,the carrier of U1 ex h be Function of
  U0,U1 st h is_homomorphism & h|IT = f;
end;

definition
  let IT be Universal_Algebra;
  attr IT is free means
:: FREEALG:def 6

  ex G being GeneratorSet of IT st G is free;
end;

registration
  cluster free strict for Universal_Algebra;
end;

registration
  let U0 be free Universal_Algebra;
  cluster free for GeneratorSet of U0;
end;

theorem :: FREEALG:1
  for U0 be strict Universal_Algebra,A be Subset of U0 st Constants U0
  <> {} or A <> {} holds A is GeneratorSet of U0 iff GenUnivAlg(A) = U0;

begin

::
:: Construction of a Decorated Tree Structure for Free Universal Algebra
::

definition
  let f be non empty FinSequence of NAT, X be set;
  func REL(f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X)*) means
:: FREEALG:def 7

  for a be Element of (dom f) \/ X, b be Element of ((dom f) \/ X)* holds [a,b]
  in it iff a in dom f & f.a = len b;
end;

definition
  let f be non empty FinSequence of NAT, X be set;
  func DTConUA(f,X) -> strict DTConstrStr equals
:: FREEALG:def 8
  DTConstrStr (# (dom f) \/ X,
    REL(f,X) #);
end;

registration
  let f be non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> non empty;
end;

theorem :: FREEALG:2
  for f be non empty FinSequence of NAT, X be set holds (Terminals
  (DTConUA(f,X))) c= X & NonTerminals(DTConUA(f,X)) = dom f;

theorem :: FREEALG:3
  for f be non empty FinSequence of NAT, X be disjoint_with_NAT set
  holds (Terminals (DTConUA(f,X))) = X;

registration
  let f be non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> with_nonterminals;
end;

registration
  let f be with_zero non empty FinSequence of NAT, X be set;
  cluster DTConUA(f,X) -> with_nonterminals with_useful_nonterminals;
end;

registration
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  cluster DTConUA(f,D) -> with_terminals with_nonterminals
    with_useful_nonterminals;
end;

definition
  let f be non empty FinSequence of NAT, X be set, n be Nat;
  assume
 n in dom f;
  func Sym(n,f,X) -> Symbol of DTConUA(f,X) equals
:: FREEALG:def 9

  n;
end;

begin

::
:: Construction of Free Universal Algebra for Non Empty Set of Generators and
::                           Given Signature

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set,
  n be Nat;
  assume
 n in dom f;
  func FreeOpNSG(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
  DTConUA(f,D))*, TS(DTConUA(f,D)) means
:: FREEALG:def 10

  dom it = (f/.n)-tuples_on TS(
  DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
  it.p = Sym(n,f,D)-tree(p);
end;

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  func FreeOpSeqNSG(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
:: FREEALG:def 11

  len it = len f & for n st n in dom it holds it.n = FreeOpNSG(n,f,D);
end;

definition
  let f be non empty FinSequence of NAT, D be disjoint_with_NAT non empty set;
  func FreeUnivAlgNSG(f,D) -> strict Universal_Algebra equals
:: FREEALG:def 12
  UAStr (# TS(
    DTConUA(f,D)), FreeOpSeqNSG(f,D)#);
end;

theorem :: FREEALG:4
  for f be non empty FinSequence of NAT, D be disjoint_with_NAT non
  empty set holds signature (FreeUnivAlgNSG(f,D)) = f;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  func FreeGenSetNSG(f,D) -> Subset of FreeUnivAlgNSG(f,D) equals
:: FREEALG:def 13
  {root-tree s
  where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
end;

theorem :: FREEALG:5
  for f be non empty FinSequence of NAT,D be non empty
  disjoint_with_NAT set holds FreeGenSetNSG(f,D) is non empty;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  redefine func FreeGenSetNSG(f,D) -> GeneratorSet of FreeUnivAlgNSG(f,D);
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set,
  C be non empty set, s be Symbol of (DTConUA(f,D)), F be Function of
  FreeGenSetNSG(f,D),C;
  assume
 s in Terminals (DTConUA(f,D));
  func pi(F,s) -> Element of C equals
:: FREEALG:def 14

  F.(root-tree s);
end;

definition
  let f be non empty FinSequence of NAT, D be set, s be Symbol of (DTConUA(f,D
  ));
  given p be FinSequence such that
 s ==> p;
  func @s -> Nat equals
:: FREEALG:def 15

  s;
end;

theorem :: FREEALG:6
  for f be non empty FinSequence of NAT,D be non empty
  disjoint_with_NAT set holds FreeGenSetNSG(f,D) is free;

registration
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  cluster FreeUnivAlgNSG(f,D) -> free;
end;

definition
  let f be non empty FinSequence of NAT, D be non empty disjoint_with_NAT set;
  redefine func FreeGenSetNSG(f,D) -> free GeneratorSet of FreeUnivAlgNSG(f,D);
end;

begin

::
:: Construction of Free Universal Algebra for Given Signature
::  (with at Last One Zero Argument Operation) and Set of Generators
::

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
  n be Nat;
  assume
 n in dom f;
  func FreeOpZAO(n,f,D) -> homogeneous quasi_total non empty PartFunc of (TS
  DTConUA(f,D))*, TS(DTConUA(f,D)) means
:: FREEALG:def 16

  dom it = (f/.n)-tuples_on TS(
  DTConUA(f,D)) & for p be FinSequence of TS(DTConUA(f,D)) st p in dom it holds
  it.p = Sym(n,f,D)-tree(p);
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeOpSeqZAO(f,D) -> PFuncFinSequence of TS DTConUA(f,D) means
:: FREEALG:def 17

  len it = len f & for n st n in dom it holds it.n = FreeOpZAO(n,f,D);
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeUnivAlgZAO(f,D) -> strict Universal_Algebra equals
:: FREEALG:def 18
  UAStr (# TS(
    DTConUA(f,D)), FreeOpSeqZAO(f,D)#);
end;

theorem :: FREEALG:7
  for f be with_zero non empty FinSequence of NAT, D be
  disjoint_with_NAT set holds signature (FreeUnivAlgZAO(f,D)) = f;

theorem :: FREEALG:8
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds FreeUnivAlgZAO(f,D) is with_const_op;

theorem :: FREEALG:9
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds Constants(FreeUnivAlgZAO(f,D)) <> {};

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  func FreeGenSetZAO(f,D) -> Subset of FreeUnivAlgZAO(f,D) equals
:: FREEALG:def 19
  {root-tree s
  where s is Symbol of DTConUA(f,D): s in Terminals DTConUA(f,D)};
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  redefine func FreeGenSetZAO(f,D) -> GeneratorSet of FreeUnivAlgZAO(f,D);
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set,
  C be non empty set, s be Symbol of (DTConUA(f,D)), F be Function of (
  FreeGenSetZAO(f,D)),C;
  assume
 s in Terminals (DTConUA(f,D));
  func pi(F,s) -> Element of C equals
:: FREEALG:def 20

  F.(root-tree s);
end;

theorem :: FREEALG:10
  for f be with_zero non empty FinSequence of NAT,D be
  disjoint_with_NAT set holds FreeGenSetZAO(f,D) is free;

registration
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  cluster FreeUnivAlgZAO(f,D) -> free;
end;

definition
  let f be with_zero non empty FinSequence of NAT, D be disjoint_with_NAT set;
  redefine func FreeGenSetZAO(f,D) -> free GeneratorSet of FreeUnivAlgZAO(f,D);
end;

registration
  cluster strict free with_const_op for Universal_Algebra;
end;