Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Order Sorted Algebras

**by****Josef Urban**- Received September 19, 2002
- MML identifier: OSALG_1

- [ Mizar article, MML identifier index ]

environ vocabulary ZF_REFLE, PBOOLE, BOOLE, RELAT_1, RELAT_2, EQREL_1, FUNCT_1, PRALG_1, TDGROUP, SEQM_3, NATTRA_1, CARD_3, FINSEQ_1, FUNCOP_1, AMI_1, QC_LANG1, CARD_5, CARD_LAR, SETFAM_1, MSUALG_1, ORDERS_1, OSALG_1; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, STRUCT_0, FUNCT_2, EQREL_1, SETFAM_1, PARTFUN1, FINSEQ_1, FINSEQ_2, CARD_3, PBOOLE, ORDERS_1, MSUALG_1, ORDERS_3, YELLOW18; constructors ORDERS_3, EQREL_1, YELLOW18; clusters FUNCT_1, RELSET_1, STRUCT_0, SUBSET_1, ARYTM_3, MSUALG_1, FILTER_1, ORDERS_3, WAYBEL_7, MSAFREE, PARTFUN1, XBOOLE_0; requirements BOOLE, SUBSET; begin :: Preliminaries :: TODO: constant ManySortedSet, constant OrderSortedSet, :: constant -> order-sorted ManySortedSet of R definition 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 OperSymbols of S; end; definition let S be non void non empty ManySortedSign; let o be OperSymbol of S; canceled; redefine func the_result_sort_of o -> Element of S; end; :::::::::::::: Some structures ::::::::::::::::::: :: overloaded MSALGEBRA is modelled using an Equivalence_Relation :: on OperSymbols ... partially hack enforced by previous articles, :: partially can give more general treatment than the usual definition definition struct(ManySortedSign) OverloadedMSSign (# carrier -> set, OperSymbols -> set, Overloading -> Equivalence_Relation of the OperSymbols, Arity -> Function of the OperSymbols, the carrier*, ResultSort -> Function of the OperSymbols, the carrier #); end; :: Order Sorted Signatures definition struct(ManySortedSign,RelStr) RelSortedSign (# carrier -> set, InternalRel -> (Relation of the carrier), OperSymbols -> set, Arity -> Function of the OperSymbols, the carrier*, ResultSort -> Function of the OperSymbols, the carrier #); end; definition struct(OverloadedMSSign,RelSortedSign) OverloadedRSSign (# carrier -> set, InternalRel -> (Relation of the carrier), OperSymbols -> set, Overloading -> Equivalence_Relation of the OperSymbols, Arity -> Function of the OperSymbols, the carrier*, ResultSort -> Function of the OperSymbols, 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; definition 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 2 S is reflexive transitive antisymmetric; end; definition cluster order-sorted -> reflexive transitive antisymmetric OverloadedRSSign; cluster strict non empty non void order-sorted OverloadedRSSign; end; definition cluster non empty non void 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 3 [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 4 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 5 the Overloading of S = id (the OperSymbols 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 6 the carrier of S0 = the carrier of it & id the carrier of S0 = the InternalRel of it & the OperSymbols of S0 = the OperSymbols of it & id the OperSymbols 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; definition cluster discrete op-discrete discernable (strict non empty non void order-sorted OverloadedRSSign); end; definition cluster op-discrete -> discernable (non empty non void OverloadedRSSign); end; ::FIXME: the order of this and the previous clusters cannot be exchanged!! definition 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 7 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 8 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 9 for o being OperSymbol of S holds o is monotone; end; theorem :: OSALG_1:9 S is op-discrete implies S is monotone; definition cluster monotone OrderSortedSign; end; definition let S be monotone OrderSortedSign; cluster monotone OperSymbol of S; end; definition let S be monotone OrderSortedSign; cluster -> monotone OperSymbol of S; end; definition cluster op-discrete -> monotone OrderSortedSign; end; :: constants not overloaded if monotone theorem :: OSALG_1:10 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 10 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 11 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 12 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 13 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 14 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; definition cluster regular (monotone OrderSortedSign); end; definition cluster op-discrete -> regular (monotone OrderSortedSign); end; definition let SR be regular (monotone OrderSortedSign); cluster -> regular OperSymbol of SR; end; reserve SR for regular (monotone OrderSortedSign), o,o1,o2,o3,o4 for OperSymbol of SR, w1 for Element of (the carrier of SR)*; theorem :: OSALG_1:13 ( w1 <= the_arity_of o & 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 15 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 16 (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; canceled; attr M is order-sorted means :: OSALG_1:def 18 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; definition let R; cluster order-sorted ManySortedSet of R; end; ::FIXME: functor clusters for redefined funcs do not work, definition let R,z; redefine func ConstOSSet(R,z) -> order-sorted ManySortedSet of R; end; :: OrderSortedSet respects the ordering definition let R be non empty Poset; mode OrderSortedSet of R is order-sorted ManySortedSet of R; end; definition let R be non empty Poset; cluster non-empty OrderSortedSet of R; end; :::::::::::::::::::::::::::::::::::::::::::::::::::::: :: order-sorted MSAlgebra, OSAlgebra, ConstOSA, OSAlg of a MSAlgebra :::::::::::::::::::::::::::::::::::::::::::::::::::::: 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 19 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 20 the Sorts of it = ConstOSSet(S,z) & the Charact of it = CH; end; theorem :: OSALG_1:18 ConstOSA(S,z,CH) is order-sorted; definition let S; cluster strict non-empty order-sorted MSAlgebra over S; end; definition 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; definition let S be discrete OrderSortedSign; cluster -> order-sorted 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 21 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 22 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 23 for o1,o2 st o1 <= o2 holds Den(o2,A)|Args(o1,A) = Den(o1,A); end; :: REVISE:: WELLFND1:1 should be generalised to Relation and moved to RELAT_1 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 24 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; definition let S; cluster monotone strict non-empty OSAlgebra of S; end; definition 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 OperSymbols of S) equals :: OSALG_1:def 25 Class the Overloading of S; end; definition let S; cluster -> non empty 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 26 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 & len the_arity_of op1 = len the_arity_of 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 27 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;

Back to top