:: A Scheme for Extensions of Homomorphisms of Manysorted Algebras
:: by Andrzej Trybulec
::
:: Received December 13, 1994
:: Copyright (c) 1994-2018 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, CARD_3, RELAT_1, TARSKI, XBOOLE_0, LANG1, SUBSET_1,
DTCONSTR, TREES_4, FINSEQ_1, TDGROUP, TREES_3, TREES_2, STRUCT_0,
MSUALG_1, PBOOLE, MSAFREE, ZFMISC_1, MARGREL1, PROB_2, NAT_1, PARTFUN1,
MCART_1, MSUALG_3, MSAFREE1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_2, STRUCT_0, XTUPLE_0, MCART_1,
FINSEQ_1, MULTOP_1, PROB_2, CARD_3, TREES_2, TREES_3, TREES_4, LANG1,
DTCONSTR, PBOOLE, MSUALG_1, MSAFREE, MSUALG_3;
constructors MULTOP_1, PROB_2, MSUALG_3, MSAFREE, RELSET_1, CAT_3, FINSEQ_2,
XTUPLE_0;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FINSEQ_1, RELAT_1, TREES_3,
STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, MSAFREE, ORDINAL1, PBOOLE,
XTUPLE_0;
requirements BOOLE, SUBSET;
begin
theorem :: MSAFREE1:1
for f,g being Function st g in product f holds rng g c= Union f;
scheme :: MSAFREE1:sch 1
DTConstrUniq{DT()->non empty DTConstrStr, D()->non empty set, G(set) ->
Element of D(), H(set, set, set) -> Element of D(), f1, f2() -> Function of TS(
DT()), D() }: f1() = f2()
provided
for t being Symbol of DT() st t in Terminals DT()
holds f1().(root-tree t) = G(t) and
for nt being Symbol of DT(), ts being Element of (TS DT())*
st nt ==> roots ts
for x being Element of D()* st x = f1() * ts
holds f1().(nt-tree ts) = H(nt, ts, x) and
for t being Symbol of DT() st t in Terminals DT()
holds f2().(root-tree t) = G(t) and
for nt being Symbol of DT(), ts being Element of (TS DT())*
st nt ==> roots ts
for x being Element of D()* st x = f2() * ts
holds f2().(nt-tree ts) = H(nt, ts, x);
theorem :: MSAFREE1:2 :: MSAFREE:5
for S being non void non empty ManySortedSign, X being
ManySortedSet of the carrier of S
for o,b being object st [o,b] in REL(X) holds o
in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the
carrier of S}:] \/ Union coprod X)*;
theorem :: MSAFREE1:3 :: MSAFREE:5
for S being non void non empty ManySortedSign, X being ManySortedSet
of the carrier of S for o being OperSymbol of S, b being FinSequence st [[o,the
carrier of S],b] in REL(X) holds len b = len (the_arity_of o) & for x be set st
x in dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for
o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of
o1 = (the_arity_of o).x) & (b.x in Union(coprod X) implies b.x in coprod((
the_arity_of o).x,X));
registration
let I be non empty set, M be ManySortedSet of I;
cluster rng M -> non empty;
end;
registration
let I be set;
cluster empty-yielding -> disjoint_valued for ManySortedSet of I;
end;
registration
let I be set;
cluster disjoint_valued for ManySortedSet of I;
end;
definition
let I be non empty set;
let X be disjoint_valued ManySortedSet of I;
let D be non-empty ManySortedSet of I;
let F be ManySortedFunction of X,D;
func Flatten F -> Function of Union X, Union D means
:: MSAFREE1:def 1
for i being Element of I, x being set st x in X.i holds it.x = F.i.x;
end;
theorem :: MSAFREE1:4
for I being non empty set, X being disjoint_valued ManySortedSet
of I, D being non-empty ManySortedSet of I for F1,F2 be ManySortedFunction of X
,D st Flatten F1 = Flatten F2 holds F1 = F2;
definition
let S be non empty ManySortedSign;
let A be MSAlgebra over S;
attr A is disjoint_valued means
:: MSAFREE1:def 2
the Sorts of A is disjoint_valued;
end;
definition
let S be non empty ManySortedSign;
func SingleAlg S -> strict MSAlgebra over S means
:: MSAFREE1:def 3
for i being set st i in the carrier of S holds (the Sorts of it).i = {i};
end;
registration
let S be non empty ManySortedSign;
cluster non-empty disjoint_valued for MSAlgebra over S;
end;
registration
let S be non empty ManySortedSign;
cluster SingleAlg S -> non-empty disjoint_valued;
end;
registration
let S be non empty ManySortedSign;
let A be disjoint_valued MSAlgebra over S;
cluster the Sorts of A -> disjoint_valued;
end;
theorem :: MSAFREE1:5
for S being non void non empty ManySortedSign, o being OperSymbol
of S, A1 be non-empty disjoint_valued MSAlgebra over S, A2 be non-empty
MSAlgebra over S, f be ManySortedFunction of A1,A2, a be Element of Args(o,A1)
holds (Flatten f)*a = f#a;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeSort X -> disjoint_valued;
end;
scheme :: MSAFREE1:sch 2
FreeSortUniq{ S() -> non void non empty ManySortedSign,
X,D() -> non-empty ManySortedSet of the carrier of S(),
G(set) -> Element of Union D(),
H(object, object, object) -> Element of Union D(),
f1, f2() -> ManySortedFunction of FreeSort X(),D() }:
f1() = f2()
provided
for o being OperSymbol of S(), ts being Element of Args(o,FreeMSA X())
for x being Element of (Union D())* st x = (Flatten f1()) * ts holds
f1().(the_result_sort_of o).(Den(o,FreeMSA X()).ts) = H(o, ts, x) and
for s being SortSymbol of S(), y be set st y in FreeGen(s,X())
holds f1().s.y = G(y) and
for o being OperSymbol of S(), ts being Element of Args(o,FreeMSA X())
for x being Element of (Union D())* st x = (Flatten f2()) * ts holds
f2().(the_result_sort_of o).(Den(o,FreeMSA X()).ts) = H(o, ts, x) and
for s being SortSymbol of S(), y be set st y in FreeGen(s,X())
holds f2().s.y = G(y);
registration
let S be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of S;
cluster FreeMSA X -> non-empty;
end;
registration
let S be non void non empty ManySortedSign;
let o be OperSymbol of S;
let A be non-empty MSAlgebra over S;
cluster Args(o,A) -> non empty;
cluster Result(o,A) -> non empty;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster the Sorts of FreeMSA X -> disjoint_valued;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeMSA X -> disjoint_valued;
end;
scheme :: MSAFREE1:sch 3
ExtFreeGen{ S() -> non void non empty ManySortedSign, X() -> non-empty
ManySortedSet of the carrier of S(), MSA() -> non-empty MSAlgebra over S(),
P[object,object,object],
IT1, IT2() -> ManySortedFunction of FreeMSA X(), MSA() }:
IT1() = IT2()
provided
IT1() is_homomorphism FreeMSA X(), MSA() and
for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X())
holds IT1().s.y = x iff P[s,x,y] and
IT2() is_homomorphism FreeMSA X(), MSA() and
for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X())
holds IT2().s.y = x iff P[s,x,y];