:: Order Sorted Algebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2016 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 PBOOLE, FINSEQ_1, RELAT_1, TARSKI, XBOOLE_0, MSUALG_1, SUBSET_1,
STRUCT_0, EQREL_1, FUNCT_1, ORDERS_2, ORDERS_1, RELAT_2, NATTRA_1,
MARGREL1, XXREAL_0, SEQM_3, CARD_5, CARD_LAR, FUNCOP_1, CARD_3, SETFAM_1,
OSALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1,
ORDERS_1, FUNCT_2, EQREL_1, SETFAM_1, PARTFUN1, FINSEQ_1, FUNCOP_1,
FINSEQ_2, CARD_3, PBOOLE, ORDERS_2, STRUCT_0, MSUALG_1, ORDERS_3;
constructors EQREL_1, ORDERS_3, RELSET_1, MSAFREE;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, EQREL_1,
STRUCT_0, MSUALG_1, ORDERS_3, ORDINAL1, RELAT_1, PBOOLE, FINSEQ_1;
requirements BOOLE, SUBSET;
begin :: Preliminaries
:: TODO: constant ManySortedSet, constant OrderSortedSet,
:: constant -> order-sorted ManySortedSet of R
registration
let I be set, f be ManySortedSet of I, p be FinSequence of I;
cluster f * p -> FinSequence-like;
end;
definition
let S be non empty ManySortedSign;
mode SortSymbol of S is Element of S;
end;
definition
let S be non empty ManySortedSign;
mode OperSymbol of S is Element of the carrier' of S;
end;
:: Some structures
:: overloaded MSALGEBRA is modelled using an Equivalence_Relation
:: on carrier' ... partially hack enforced by previous articles,
:: partially can give more general treatment than the usual definition
definition
struct(ManySortedSign) OverloadedMSSign (# carrier -> set, carrier' -> set,
Overloading -> Equivalence_Relation of the carrier', Arity -> Function of the
carrier', the carrier*, ResultSort -> Function of the carrier', the carrier #);
end;
:: Order Sorted Signatures
definition
struct(ManySortedSign,RelStr) RelSortedSign (# carrier -> set, InternalRel
-> (Relation of the carrier), carrier' -> set, Arity -> Function of the
carrier', the carrier*, ResultSort -> Function of the carrier', the carrier #);
end;
definition
struct(OverloadedMSSign,RelSortedSign) OverloadedRSSign (# carrier -> set,
InternalRel -> (Relation of the carrier), carrier' -> set, Overloading ->
Equivalence_Relation of the carrier', Arity -> Function of the carrier', the
carrier*, ResultSort -> Function of the carrier', the carrier #);
end;
:: The inheritance for structures should be much improved, much of the
:: following is very bad hacking
reserve A,O for non empty set,
R for Order of A,
Ol for Equivalence_Relation of O,
f for Function of O,A*,
g for Function of O,A;
:: following should be possible, but isn't:
:: set RS0 = RelSortedSign(#A,R,O,f,g #);
:: inheritance of attributes for structures does not work!!! :
:: RelStr(#A,R#) is reflexive does not imply that for RelSortedSign(...)
theorem :: OSALG_1:1
OverloadedRSSign(#A,R,O,Ol,f,g #) is non empty non void reflexive
transitive antisymmetric;
registration
let A,R,O,Ol,f,g;
cluster OverloadedRSSign(#A,R,O,Ol,f,g #) -> strict non empty reflexive
transitive antisymmetric;
end;
begin
:: order-sorted, ~=, discernable, op-discrete
reserve S for OverloadedRSSign;
:: should be stated for nonoverloaded, but the inheritance is bad
definition
let S;
attr S is order-sorted means
:: OSALG_1:def 1
S is reflexive transitive antisymmetric;
end;
registration
cluster order-sorted -> reflexive transitive antisymmetric for
OverloadedRSSign;
cluster strict non empty non void order-sorted for OverloadedRSSign;
end;
registration
cluster non empty non void for OverloadedMSSign;
end;
definition
let S be non empty non void OverloadedMSSign;
let x,y be OperSymbol of S;
pred x ~= y means
:: OSALG_1:def 2
[x,y] in the Overloading of S;
symmetry;
reflexivity;
end;
:: remove when transitivity implemented
theorem :: OSALG_1:2
for S being non empty non void OverloadedMSSign, o,o1,o2 being
OperSymbol of S holds o ~= o1 & o1 ~= o2 implies o ~= o2;
:: with previous definition, equivalent funcs with same rank could exist
definition
let S be non empty non void OverloadedMSSign;
attr S is discernable means
:: OSALG_1:def 3
for x,y be OperSymbol of S st x ~= y &
the_arity_of x = the_arity_of y & the_result_sort_of x = the_result_sort_of y
holds x = y;
attr S is op-discrete means
:: OSALG_1:def 4
the Overloading of S = id (the carrier' of S);
end;
theorem :: OSALG_1:3
for S being non empty non void OverloadedMSSign holds S is
op-discrete iff for x,y be OperSymbol of S st x ~= y holds x = y;
theorem :: OSALG_1:4
for S being non empty non void OverloadedMSSign holds S is
op-discrete implies S is discernable;
begin
:: OSSign of ManySortedSign, OrderSortedSign
reserve S0 for non empty non void ManySortedSign;
:: we require strictness here for simplicity, more interesting is whether
:: we could do a nonstrict version, keeping the remaining fields of S0;
definition
let S0;
func OSSign S0 -> strict non empty non void order-sorted OverloadedRSSign
means
:: OSALG_1:def 5
the carrier of S0 = the carrier of it & id the carrier of S0 = the
InternalRel of it & the carrier' of S0 = the carrier' of it & id the carrier'
of S0 = the Overloading of it & the Arity of S0 = the Arity of it & the
ResultSort of S0 = the ResultSort of it;
end;
theorem :: OSALG_1:5
OSSign S0 is discrete op-discrete;
registration
cluster discrete op-discrete discernable for strict non empty non void
order-sorted OverloadedRSSign;
end;
registration
cluster op-discrete -> discernable for non empty non void OverloadedRSSign;
end;
::FIXME: the order of this and the previous clusters cannot be exchanged!!
registration
let S0;
cluster OSSign S0 -> discrete op-discrete;
end;
definition
mode OrderSortedSign is discernable non empty non void order-sorted
OverloadedRSSign;
end;
:: monotonicity of OrderSortedSign
:: monotone overloaded signature means monotonicity for equivalent
:: operations
:: a stronger property of the Overloading should be stated ...
:: o1 ~= o2 implies len (the_arity_of o2) = len (the_arity_of o1)
:: ... probably not, unnecessary
reserve S for non empty Poset;
reserve s1,s2 for Element of S;
reserve w1,w2 for Element of (the carrier of S)*;
:: this is mostly done in YELLOW_1, but getting the constructors work
:: could be major effort; I don't care now
definition
let S;
let w1,w2 be Element of (the carrier of S)*;
pred w1 <= w2 means
:: OSALG_1:def 6
len w1 = len w2 & for i being set st i in dom w1
for s1,s2 st s1 = w1.i & s2 = w2.i holds s1 <= s2;
reflexivity;
end;
theorem :: OSALG_1:6
for w1,w2 being Element of (the carrier of S)* holds w1 <= w2 &
w2 <= w1 implies w1 = w2;
theorem :: OSALG_1:7
S is discrete & w1 <= w2 implies w1 = w2;
reserve S for OrderSortedSign;
reserve o,o1,o2 for OperSymbol of S;
reserve w1 for Element of (the carrier of S)*;
theorem :: OSALG_1:8
S is discrete & o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2)
& the_result_sort_of o1 <= the_result_sort_of o2 implies o1 = o2;
:: monotonicity of the signature
:: this doesnot extend to Overloading!
definition
let S;
let o;
attr o is monotone means
:: OSALG_1:def 7
for o2 st o ~= o2 & (the_arity_of o) <= (
the_arity_of o2) holds the_result_sort_of o <= the_result_sort_of o2;
end;
definition
let S;
attr S is monotone means
:: OSALG_1:def 8
for o being OperSymbol of S holds o is monotone;
end;
theorem :: OSALG_1:9
S is op-discrete implies S is monotone;
registration
cluster monotone for OrderSortedSign;
end;
registration
let S be monotone OrderSortedSign;
cluster monotone for OperSymbol of S;
end;
registration
let S be monotone OrderSortedSign;
cluster -> monotone for OperSymbol of S;
end;
registration
cluster op-discrete -> monotone for OrderSortedSign;
end;
theorem :: OSALG_1:10 :: constants not overloaded if monotone
S is monotone & the_arity_of o1 = {} & o1 ~= o2 & the_arity_of o2 = {}
implies o1=o2;
:: least args,sort,rank,regularity for OperSymbol and
:: monotone OrderSortedSign
:: least bound for arguments
definition
let S,o,o1,w1;
pred o1 has_least_args_for o,w1 means
:: OSALG_1:def 9
o ~= o1 & w1 <= the_arity_of
o1 & for o2 st o ~= o2 & w1 <= the_arity_of o2 holds the_arity_of o1 <=
the_arity_of o2;
pred o1 has_least_sort_for o,w1 means
:: OSALG_1:def 10
o ~= o1 & w1 <= the_arity_of
o1 & for o2 st o ~= o2 & w1 <= the_arity_of o2 holds the_result_sort_of o1 <=
the_result_sort_of o2;
end;
definition
let S,o,o1,w1;
pred o1 has_least_rank_for o,w1 means
:: OSALG_1:def 11
o1 has_least_args_for o,w1 & o1 has_least_sort_for o,w1;
end;
definition
let S,o;
attr o is regular means
:: OSALG_1:def 12
o is monotone & for w1 st w1 <= the_arity_of
o ex o1 st o1 has_least_args_for o,w1;
end;
definition
let SM be monotone OrderSortedSign;
attr SM is regular means
:: OSALG_1:def 13
for om being OperSymbol of SM holds om is regular;
end;
reserve SM for monotone OrderSortedSign,
o,o1,o2 for OperSymbol of SM,
w1 for Element of (the carrier of SM)*;
theorem :: OSALG_1:11
SM is regular iff for o,w1 st w1 <= the_arity_of o ex o1 st o1
has_least_rank_for o,w1;
theorem :: OSALG_1:12
for SM being monotone OrderSortedSign holds SM is op-discrete
implies SM is regular;
registration
cluster regular for monotone OrderSortedSign;
end;
registration
cluster op-discrete -> regular for monotone OrderSortedSign;
end;
registration
let SR be regular monotone OrderSortedSign;
cluster -> regular for OperSymbol of SR;
end;
reserve SR for regular monotone OrderSortedSign,
o,o1,o3,o4 for OperSymbol of SR,
w1 for Element of (the carrier of SR)*;
theorem :: OSALG_1:13
o3 has_least_args_for o,w1 & o4 has_least_args_for o,w1 implies o3 = o4;
definition
let SR,o,w1;
assume
w1 <= the_arity_of o;
func LBound(o,w1) -> OperSymbol of SR means
:: OSALG_1:def 14
it has_least_args_for o, w1;
end;
theorem :: OSALG_1:14
for w1 st w1 <= the_arity_of o holds LBound(o,w1) has_least_rank_for o,w1;
:: ConstOSSet of Poset, OrderSortedSets
reserve R for non empty Poset;
reserve z for non empty set;
:: just to avoid on-the-spot casting in the examples
definition
let R,z;
func ConstOSSet(R,z) -> ManySortedSet of the carrier of R equals
:: OSALG_1:def 15
(the
carrier of R) --> z;
end;
theorem :: OSALG_1:15
ConstOSSet(R,z) is non-empty & for s1,s2 being Element of R st
s1 <= s2 holds ConstOSSet(R,z).s1 c= ConstOSSet(R,z).s2;
definition
let R;
let M be ManySortedSet of R;
attr M is order-sorted means
:: OSALG_1:def 16
for s1,s2 being Element of R st s1 <= s2 holds M.s1 c= M.s2;
end;
theorem :: OSALG_1:16
ConstOSSet(R,z) is order-sorted;
registration
let R;
cluster order-sorted for ManySortedSet of R;
end;
registration
let R,z;
cluster ConstOSSet(R,z) -> order-sorted;
end;
definition
let R be non empty Poset;
mode OrderSortedSet of R is order-sorted ManySortedSet of R;
end;
registration
let R be non empty Poset;
cluster non-empty for OrderSortedSet of R;
end;
reserve s1,s2 for SortSymbol of S,
o,o1,o2,o3 for OperSymbol of S,
w1,w2 for Element of (the carrier of S)*;
definition
let S;
let M be MSAlgebra over S;
attr M is order-sorted means
:: OSALG_1:def 17
for s1,s2 st s1 <= s2 holds (the Sorts of M).s1 c= (the Sorts of M).s2;
end;
theorem :: OSALG_1:17
for M being MSAlgebra over S holds M is order-sorted iff the
Sorts of M is OrderSortedSet of S;
reserve CH for ManySortedFunction of ConstOSSet(S,z)# * the Arity of S,
ConstOSSet(S,z) * the ResultSort of S;
definition
let S,z,CH;
func ConstOSA(S,z,CH) -> strict non-empty MSAlgebra over S means
:: OSALG_1:def 18
the Sorts of it = ConstOSSet(S,z) & the Charact of it = CH;
end;
theorem :: OSALG_1:18
ConstOSA(S,z,CH) is order-sorted;
registration
let S;
cluster strict non-empty order-sorted for MSAlgebra over S;
end;
registration
let S,z,CH;
cluster ConstOSA(S,z,CH) -> order-sorted;
end;
definition
let S;
mode OSAlgebra of S is order-sorted MSAlgebra over S;
end;
theorem :: OSALG_1:19
for S being discrete OrderSortedSign, M being MSAlgebra over S
holds M is order-sorted;
registration
let S be discrete OrderSortedSign;
cluster -> order-sorted for MSAlgebra over S;
end;
reserve A for OSAlgebra of S;
theorem :: OSALG_1:20
w1 <= w2 implies (the Sorts of A)#.w1 c= (the Sorts of A)#.w2;
reserve M for MSAlgebra over S0;
:: canonical OSAlgebra for MSAlgebra
definition
let S0,M;
func OSAlg M -> strict OSAlgebra of OSSign S0 means
:: OSALG_1:def 19
the Sorts of it = the Sorts of M & the Charact of it = the Charact of M;
end;
:: monotone OSAlgebra
reserve A for OSAlgebra of S;
:: Element of A should mean Element of Union the Sorts of A here ...
:: MSAFREE3:def 1; Element of A,s is defined in MSUALG_6
theorem :: OSALG_1:21
for w1,w2,w3 being Element of (the carrier of S)* holds w1 <= w2
& w2 <= w3 implies w1 <= w3;
definition
let S,o1,o2;
pred o1 <= o2 means
:: OSALG_1:def 20
o1 ~= o2 & (the_arity_of o1) <= (the_arity_of o2
) & the_result_sort_of o1 <= the_result_sort_of o2;
reflexivity;
end;
theorem :: OSALG_1:22
o1 <= o2 & o2 <= o1 implies o1 = o2;
theorem :: OSALG_1:23
o1 <= o2 & o2 <= o3 implies o1 <= o3;
theorem :: OSALG_1:24
the_result_sort_of o1 <= the_result_sort_of o2 implies Result(o1
,A) c= Result(o2,A);
theorem :: OSALG_1:25
the_arity_of o1 <= the_arity_of o2 implies Args(o1,A) c= Args(o2 ,A);
theorem :: OSALG_1:26
o1 <= o2 implies Args(o1,A) c= Args(o2,A) & Result(o1,A) c= Result(o2, A );
:: OSAlgebra is monotone iff the interpretation of the same symbol on
:: widening sorts coincides
:: the definition would be nicer as function inclusion (see TEqMon)
:: without the restriction to Args(o1,A), but the permissiveness
:: of FUNCT_2:def 1 spoils that
definition
let S,A;
attr A is monotone means
:: OSALG_1:def 21
for o1,o2 st o1 <= o2 holds Den(o2,A)|Args( o1,A) = Den(o1,A);
end;
theorem :: OSALG_1:27
for A being non-empty OSAlgebra of S holds A is monotone iff for
o1,o2 st o1 <= o2 holds Den(o1,A) c= Den(o2,A);
theorem :: OSALG_1:28
(S is discrete or S is op-discrete) implies A is monotone;
:: TrivialOSA(S,z,z1) interprets all funcs as one constant
definition
let S,z;
let z1 be Element of z;
func TrivialOSA(S,z,z1) -> strict OSAlgebra of S means
:: OSALG_1:def 22
the Sorts of
it = ConstOSSet(S,z) & for o holds Den(o,it) = Args(o,it) --> z1;
end;
theorem :: OSALG_1:29
for z1 being Element of z holds TrivialOSA(S,z,z1) is non-empty
& TrivialOSA(S,z,z1) is monotone;
registration
let S;
cluster monotone strict non-empty for OSAlgebra of S;
end;
registration
let S,z;
let z1 be Element of z;
cluster TrivialOSA(S,z,z1) -> monotone non-empty;
end;
:: OperNames, OperName, Name
reserve op1,op2 for OperSymbol of S;
definition
let S;
func OperNames S -> non empty (Subset-Family of the carrier' of S) equals
:: OSALG_1:def 23
Class the Overloading of S;
end;
registration
let S;
cluster -> non empty for Element of OperNames S;
end;
definition
let S;
mode OperName of S is Element of OperNames S;
end;
definition
let S,op1;
func Name op1 -> OperName of S equals
:: OSALG_1:def 24
Class(the Overloading of S,op1);
end;
theorem :: OSALG_1:30
op1 ~= op2 iff op2 in Class(the Overloading of S,op1);
theorem :: OSALG_1:31
op1 ~= op2 iff Name op1 = Name op2;
theorem :: OSALG_1:32
for X being set holds X is OperName of S iff ex op1 st X = Name op1;
definition
let S;
let o be OperName of S;
redefine mode Element of o -> OperSymbol of S;
end;
theorem :: OSALG_1:33
for on being OperName of S, op being OperSymbol of S holds op is
Element of on iff Name op = on;
theorem :: OSALG_1:34
for SR being regular monotone OrderSortedSign, op1,op2 being
OperSymbol of SR, w being Element of (the carrier of SR)* st op1 ~= op2 & w <=
the_arity_of op1 & w <= the_arity_of op2 holds LBound(op1,w) = LBound(op2,w);
definition
let SR be regular monotone OrderSortedSign, on be OperName of SR, w be
Element of (the carrier of SR)*;
assume
ex op being Element of on st w <= the_arity_of op;
func LBound(on,w) -> Element of on means
:: OSALG_1:def 25
for op being Element of on st w <= the_arity_of op holds it = LBound(op,w);
end;
theorem :: OSALG_1:35
for S being regular monotone OrderSortedSign, o being OperSymbol of
S, w1 being Element of (the carrier of S)* st w1 <= the_arity_of o holds LBound
(o,w1) <= o;