library Nat
%% authors: M.Roggenbach, T.Mossakowski, L.Schröder
%% copyright: 12.12.00

%% RelationsAndOrders

spec
     Relation =
     sort
          Elem
     pred
          __ ~ __: Elem * Elem
end

spec
     ReflexiveRelation =
     Relation
then
     var
          x:Elem
     .
          %[refl] x ~ x
end

spec
     SymmetricRelation =
     Relation
then
     vars
          x,y:Elem
     .
          %[sym] x ~ y if y ~ x
end

spec
     TransitiveRelation =
     Relation
then
     vars
          x,y,z:Elem
     .
          %[trans] x ~ z if x ~ y /\ y ~ z
end

spec
     SimilarityRelation =
     ReflexiveRelation and SymmetricRelation
end

spec
     PartialEquivalenceRelation =
     SymmetricRelation and TransitiveRelation
end

spec
     EquivalenceRelation =
     ReflexiveRelation and PartialEquivalenceRelation
end

spec
     SigOrder[sort Elem] =
     preds
           __ <= __, __ < __,
           __ >= __, __ > __: Elem * Elem;
     vars
          x,y:Elem
     .
          %[SigOrder_geq_def] x >= y <=> y <= x
     .
          %[SigOrder_less_def] x < y <=> (x <= y /\ not (x=y))
     .
          %[SigOrder_greater_def] x > y <=> y < x
end

spec
     PreOrder =
     {ReflexiveRelation and TransitiveRelation}
     with pred __ ~ __ |-> __ <= __
end

spec
     PartialOrder =
     PreOrder
then
     vars
          x,y:Elem
     .
          %[POrder_antisym] x = y if x <= y /\ y <= x
end

spec
     ExtPartialOrder  [PartialOrder]
=
     %def
     SigOrder [sort Elem]
and
{
          ops
                inf,sup : Elem × Elem ->? Elem
          vars
               x,y,z: Elem
          .
               %[inf_def] inf(x,y) = z <=>
                z <= x /\ z <= y /\ (forall t: Elem . t <= x /\ t <= y => t
                <= z)
          .
               %[sup_def] sup(x,y) = z <=>
                x <= z /\ y <= z /\ (forall t: Elem . x <= t /\ y <= t => z
                <= t)
     then
          %implies
          ops
               inf,sup : Elem × Elem ->? Elem, comm
}
end

spec
     TotalOrder =
     PartialOrder
then
     vars
          x,y:Elem
     .
          %[TOrder_comparability] x <= y \/ y <= x
end

spec
     ExtTotalOrder  [TotalOrder]
=
     %def
     ExtPartialOrder [PartialOrder]
and
{
          ops
               min, max: Elem × Elem -> Elem
          vars
               x,y: Elem
          .
               %[min_def] min(x,y) = x when x <= y else y
          .
               %[max_def] max(x,y) = y when x <= y else x
     then
          %implies
          ops
                min, max: Elem × Elem -> Elem,
                          comm, assoc
}
then
     %implies
     vars
          x,y: Elem
     .
          %[min_inf_relation] min(x,y)=inf(x,y)
     .
          %[max_sup_relation] max(x,y)=sup(x,y)
end

spec
     BooleanAlgebra =
     sort
          Elem
     ops
           0,1:       Elem;
           __ cap __: Elem * Elem -> Elem, assoc, comm, unit 1;
           __ cup __: Elem * Elem -> Elem, assoc, comm, unit 0;
     %prec
          { __ cup __ } < { __ cap __}
     vars
          x,y,z:Elem
     .
          %[absorption_def1] x cap ( x cup y) = x
     .
          %[absorption_def2] x cup ( x cap y) = x
     .
          %[zeroAndCap] x cap 0 = 0
     .
          %[oneAndCup] x cup 1 = 1
     .
          %[BA_distr_def1] x cap ( y cup z) = (x cap y) cup ( x cap z)
     .
          %[BA_distr_def2] x cup ( y cap z) = (x cup y) cap ( x cup z)
     .
          %[BA_inverse_def]
          exists x': Elem . x cup x' = 1 /\ x cap x' = 0
then
     %implies
     op
          __ cup __, __ cap __ : Elem * Elem -> Elem , idem
     var
          x: Elem
     .
          %[BA_uniqueComplement] exists! x': Elem . x cup x' = 1 /\ x cap
          x' = 0
end

spec
     ExtBooleanAlgebra  [BooleanAlgebra]
=
     %def
     {
          SigOrder [sort Elem]
          then vars x,y:Elem
          . %[BA_po_def] x <= y <=> x cap y = x
     }
     and
     {
          op compl: Elem -> Elem
          vars x,y:Elem
          . %[BA_compl_def] compl(x)=y <=> x cup y = 1 /\ x cap y = 0
     }
then
     %implies
     vars
          x,y: Elem
     .
          %[de_Morgan1] compl(x cap y) = compl(x) cup compl(y)
     .
          %[de_Morgan2] compl(x cup y) = compl(x) cap compl(y)
     .
          %[BA_involution_compl] compl(compl(x)) = x
end

view
     PartialOrder_in_ExtBooleanAlgebra  [BooleanAlgebra]:
     PartialOrder to ExtBooleanAlgebra[BooleanAlgebra]
end


%% PreNumbers

spec SigPreNumbers [sort Elem] =
     SigOrder [sort Elem]
then ops   0: Elem;
           __ + __, __ * __: Elem × Elem -> Elem %left assoc;
     %prec { __ + __ } < { __ * __ }
end

spec GenerateNat =
  free type Nat ::= 0 | suc(pre:? Nat)
end

spec PreNat =
  GenerateNat and SigPreNumbers [sort Nat]
then
     vars m,n: Nat
     . %[Nat_leq_def1] 0 <= n
     . %[Nat_leq_def2] not (suc(n) <= 0)
     . %[Nat_leq_def3] suc(m) <= suc(n) <=> m <= n
   
     . %[Nat_add__0] 0 + m = m
     . %[Nat_add_suc] suc(n) + m = suc(n + m)

     . %[Nat_mult_0] 0 * m = 0
     . %[Nat_mult_suc] suc(n) * m = (n * m) + m

then %def
     sort Pos = { p: Nat . p > 0 }
     op    %[PreNat_1_def] 1: Pos = suc(0) as Pos;
           1 : Nat;
           __*__: Pos × Pos -> Pos;
           __+__: Pos × Nat -> Pos;
           __+__: Nat × Pos -> Pos;
end

view TotalOrder_in_PreNat: TotalOrder to PreNat =
     sort Elem |-> Nat
end

%% Algebra_I

spec 
     BinAlg =
     sort
          Elem
     op
          __ * __: Elem * Elem -> Elem
end

spec
     SemiGroup =
     BinAlg
then
     op
          __ * __: Elem * Elem -> Elem, assoc
end

view
     SemiGroup_in_Totalorder_max  :
     SemiGroup to ExtTotalOrder[TotalOrder] =
op
     __ * __ |-> max
end

view
     SemiGroup_in_Totalorder_min  :
     SemiGroup to ExtTotalOrder[TotalOrder] =
op
     __*__ |-> min
end

spec
     SigPowerBinAlg [sort Exponent] =
     BinAlg
then    
     op __ ^ __: Elem * Exponent -> Elem
     %prec {__*__} < {__^ __}
end

spec 
     PowerTheorems [sort Exponent;
                    ops __ + __, __ * __: Exponent * Exponent -> Exponent] =
     SigPowerBinAlg [sort Exponent]
then
     vars x: Elem; n,m: Exponent
     .    %[Power_add] x ^ (n + m)=x ^ n * x ^ m
     .    %[Power_mult] x ^ (n * m)=(x ^ n) ^ m
end

        
spec
     ExtSemiGroup[SemiGroup] given PreNat =
%def
     SigPowerBinAlg [sort Pos]
then
     vars
          x: Elem; n: Pos
     .
          %[SemiGroup_power_1] x ^ 1 = x
     .
          %[SemiGroup_power_suc] x ^ (suc(n) as Pos) = x * x ^ n
then
     %implies
     PowerTheorems [PreNat fit sort Exponent |-> Pos]
end

spec 
     CommutativeSemiGroup =
     SemiGroup
then
     op __*__: Elem * Elem -> Elem, comm
end

spec
     PowerTheoremsComm [sort Exponent;
                ops __ + __, __ * __: Exponent * Exponent -> Exponent] =
     SigPowerBinAlg [sort Exponent]
then
     vars x,y: Elem; n: Exponent
     .
          %[Power_basemult] x^ n * y^ n=(x*y)^ n
end

spec 
     ExtCommutativeSemiGroup [CommutativeSemiGroup] given PreNat =
%def
     ExtSemiGroup [SemiGroup]
then
     %implies
     PowerTheoremsComm [PreNat fit sort Exponent |-> Pos]
end

spec
     Monoid =
     SemiGroup
then
     ops
           e:      Elem;
           __ * __:Elem * Elem -> Elem, unit e
end

spec
     ExtMonoid  [Monoid] given PreNat =
%def
{
     ExtSemiGroup [SemiGroup]
then 
     SigPowerBinAlg [sort Nat]
then
     var
          x: Elem
     .
          %[Monoid_power_0] x ^ 0 = e
} hide __^__: Elem * Pos -> Elem
then
     %implies
     {vars
          x: Elem; n,m: Nat
     .    
          %[Monoid_power_unit] e ^ n = e
     then
          PowerTheorems [PreNat fit sort Exponent |-> Nat] 
     }
end

spec
     CommutativeMonoid =
     Monoid
and
     CommutativeSemiGroup
end

view
     CommutativeMonoid_in_PreNat_Add:
     CommutativeMonoid to PreNat
=
     sort
          Elem |-> Nat,
     ops
           e |-> 0,
           __ * __ |-> __ + __
end

view
     CommutativeMonoid_in_PreNat_Mult:
     CommutativeMonoid to PreNat
=
     sort
          Elem |-> Nat,
     ops
          e |-> 1,
          __ * __ |-> __ * __
end

spec
     ExtCommutativeMonoid  [CommutativeMonoid]
     given PreNat =
%def
     ExtMonoid [Monoid]
then
     %implies
     PowerTheoremsComm [PreNat fit sort Exponent |-> Nat] 
end

spec
     Group =
     Monoid
then
     var x: Elem
     .
        exists x': Elem . x' * x = e
end


%% Numbers:

spec SigNumbers[sort Elem][sort Exponent] =
     SigPreNumbers[sort Elem]
then SigPowerBinAlg[sort Exponent]
then %def
     op  +__: Elem -> Elem
     %prec {+__} <> {__ ^ __}
     var   x: Elem
     . %[plus_def] + x = x
then op abs: Elem -> Elem
end

spec Nat =
     ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Mult]
     with
      sorts Nat, Pos,
      preds __ <= __, __ >= __, __ < __, __ > __,
      ops  0, 1, suc, pre, __+__, __*__, __ ^ __
and
     ExtCommutativeMonoid [view CommutativeMonoid_in_PreNat_Add]
     with op  __ ^ __ |-> __ * __
and
     ExtTotalOrder [PreNat reveal sort Nat, pred __ <= __ ]
     with ops min, max
and
     SigNumbers[sort Nat][sort Nat]
then
     preds odd, even: Nat

     ops   __! :    Nat -> Nat;
           __ -?__: Nat × Nat ->? Nat;
           __ /? __: Nat × Nat ->? Nat;
           __ div __, __ mod __ , __ quot __, __ rem __ :Nat × Nat ->? Nat;

     %prec { __ -? __ , __ + __ } < 
           { __*__, __ /? __, __div__, __mod__, __ quot __, __rem__ }
     %prec { __*__, __ /? __, __div__, __mod__, __ quot __, __rem__ }
           < { __ ^ __}

     vars m,n,r,s: Nat; p: Pos
     .    %[Nat_abs] abs(n) = n

     .    %[Nat_odd_def] odd(m) <=> not even(m)
     .    %[Nat_even_zero] even(0)
     .    %[Nat_even_suc] even(suc(m)) <=> odd(m)

     .    %[Nat_factorial_zero] 0! = 1
     .    %[Nat_factorial_suc] suc(n)! =suc(n)*n!

     .    %[Nat_sub_def] m -? n = r <=> m = r + n

     .    %[Nat_divide_0] not def(m /? 0)
     .    %[Nat_divide_Pos] ( m /? n = r <=> m = r * n ) if n>0

     .    %[Nat_div]
           m div n = r <=> (exists s: Nat . m = n*r + s /\ s < n)
     .    %[Nat_mod]
           m mod n = s <=> (exists r: Nat . m = n*r + s /\ s < n)
     .    %[Nat_quot] m quot n = m div n
     .    %[Nat_rem] m rem n = m mod n

     %%   Operations to represent natural numbers with digits:
     ops   1,2,3,4,5,6,7,8,9: Nat;
           __ @@ __ :         Nat × Nat -> Nat %left assoc
     %number __@@__
     vars m,n: Nat
     .    %[Nat_1_def] 1 = suc (0)
     .    %[Nat_2_def] 2 = suc (1)
     .    %[Nat_3_def] 3 = suc (2)
     .    %[Nat_4_def] 4 = suc (3)
     .    %[Nat_5_def] 5 = suc (4)
     .    %[Nat_6_def] 6 = suc (5)
     .    %[Nat_7_def] 7 = suc (6)
     .    %[Nat_8_def] 8 = suc (7)
     .    %[Nat_9_def] 9 = suc (8)
     .    %[Nat_decimal_def] m @@ n = (m * suc(9)) + n

then %implies
     vars m,n,r,s,t: Nat; p: Pos
     .    %[Nat_sub_dom] def(m-?n) <=> m >= n
     .    %[Nat_divide_dom] def(m /? n) <=> m mod n = 0
     .    %[Nat_div_dom] def ( m div n ) <=> not (n=0)
     .    %[Nat_mod_dom] def ( m mod n ) <=> not (n=0)
     .    %[Nat_quot_dom] def ( m quot n ) <=> not (n=0)
     .    %[Nat_rem_dom] def ( m rem n ) <=> not (n=0)
     .    %[Nat_max_unit] max(m,0) = m
     .    %[Nat_distr] (r + s) * t = (r * t) + (s * t)
end