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;