Concepts from Algebra

spec
     Semigroup =
     sort
          Elem
     op
           __ + __: Elem * Elem -> Elem,
                    assoc
end

spec
     Monoid =
     SemiGroup with sort Elem, op __ + __
then
     op
           0:Elem;
           __ + __: Elem * Elem -> Elem,
                    unit 0
end

spec
     CommutativeMonoid =
     Monoid with sort Elem, op 0, __ + __
then
     op
           __ + __: Elem * Elem -> Elem,
                    comm
end

spec
     DefineGroup =
     Monoid with sort Elem, op 0, __ + __
then
     var
          x:Elem
     .          exists x': Elem . x + x' = 0 /\ x' + x = 0
end

spec
     Group [DefineGroup with sort Elem, op 0, __ + __ ] =
%%def
     ops
           inv: Elem -> Elem;
           __ - __: Elem * Elem -> Elem;
     vars
          x,y: Elem
     %%          inv(x)
     .          x + inv(x) = 0
     .          inv(x) + x = 0
     %%          x - y
     .          x - y = x + inv(y)
end

spec
     DefineCommutativeGroup =
     DefineGroup with sort Elem, op 0, __ + __
then
     op
           __ + __: Elem * Elem -> Elem,
                    comm
end

spec
     CommutativeGroup
     [DefineCommutativeGroup with sort Elem, op 0, __ + __ ] =
%%def
     Group [DefineGroup] with ops inv, __ - __
end

spec
     DefineRing =
     DefineCommutativeGroup with sort Elem, ops 0, __ + __
then
     Monoid
     with
          ops  0 |-> 1,
           __+__ |-> __*__
     then
     %%prec          __ + __ < __ * __
     vars
          x,y,z:Elem
     %%          distributive laws:
     .          (x+y)*z = (x * z) + (y * z)
     .          z * ( x + y ) = (z * x) + (z * y)
end

spec
     Ring [DefineRing with sort Elem, ops 0, 1, __+__, __ * __ ] =
%%def
     CommutativeGroup [DefineCommutativeGroup]
     with ops inv, __ - __
%%prec
     __ - __ < __ * __
then
     %%def
     sort
          RUnit = { x: Elem . exists x': Elem . x * x' = 1 /\ x' * x = 1 }
end

spec
     DefineIntegralDomain =
     DefineRing with sort Elem, ops 0, 1, __+__, __ * __
then
     axiom
          not (1 = 0)
     op
           __ * __: Elem * Elem -> Elem,
                    comm
     vars
          x, y :Elem
     %%          without zero divisors:
     .          x=0 \/ y=0 if x * y = 0
end

spec
     IntegralDomain
     [DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __ ] =
%%def
     Ring [DefineRing] with sort RUnit, ops inv, __ - __
then
     %%def
     sort
           Irred= { x: Elem .                  not (x in RUnit) /\
                  ( forall y, z: Elem . x = y * z => (y in RUnit \/ z in
                  RUnit ) ) }
end

%% the definition of a factorial ring depends on the sorts
%% Unit and Irred, which both have to be interpreted
%% in a structure that shall be seen as a factorial ring
%% therefore we do not split the specification into two parts
%% as we did for the above algebraic structures

spec
     FactorialRing
     [DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __ ] =
     IntegralDomain [DefineIntegralDomain]
     with sorts RUnit, Irred, ops inv, __ - __
     and
     FiniteSet [sort Irred]
      with preds __  elemOf __,__ isSubsetOf __,
           ops __ union __, __ intersection __, add, __ without __, __ -
           __, __ symmDiff __
then
     preds
           equiv: Irred * Irred;
           equiv: FinSet[Irred] * FinSet[Irred]
     op
          prod: FinSet[Irred] -> Elem
     vars
          x: Elem; u,v: RUnit; i,j: Irred; S,T :FinSet[Irred]
     %%          product of a finite set of irreducible elements:
     .          prod({}) = 1
     .          prod(set(i)) = i
     .          prod(S union T) = prod(S) * prod(T)
     %%          equivalence of irreducible elements:
     .          equiv(i,j) <=> exists u: RUnit . i= u * j
     %%          equivalence of finite sets of irreducible elements:
     .           equiv(S,T) <=> ( S={} /\ T={} ) \/
                          (exists s,t: Irred . s  elemOf S /\ t  elemOf T
                          /\
                          equiv(s,t) /\ equiv(S without s, T without t) )
     %%          any element of the ring is the product of irreducible elements:
     .          exists S:FinSet[Irred] . exists u:RUnit . x = u * prod(S)
     %%          the product is "unique":
     .           equiv(S,T) if x=u * prod(S) /\ x=v * prod(T)
end

spec
     ConstructField =
     DefineRing with sort Elem, ops 0, 1, __+__, __ * __
then
     axiom
          0 =/= 1
     sort
          NonZeroElements = { x: Elem . x =/= 0 }
then
     DefineGroup
     with
          sorts Elem |-> NonZeroElements,
           ops 0 |-> 1,
           __+__ |-> __*__
end

%% an obvious view which helps to write the specification Field:

view
     MultiplicativeGroup_in_Field:
     DefineGroup to ConstructField =
     sort
          Elem |-> NonZeroElements,
     ops
           0 |-> 1,
           __+__ |-> __*__
end

spec
     DefineField=
     ConstructField
      hide sort NonZeroElements
      with sort Elem, ops 0, 1, __+__, __ * __
end

spec
     Field [DefineField with sort Elem, ops 0, 1, __+__, __ * __ ] =
%%def
     Ring [DefineRing] with sort RUnit, ops inv, __ - __
then
     %%def
     Group [view MultiplicativeGroup_in_Field]
     with
     ops
           __ - __ |-> __ / __,
           inv |-> multInv
     %%prec
          __+ __, __ - __ < __ / __
then
     op
          __ / __: Elem × Elem ->? Elem
     vars
          x,y: Elem
     .          def x/y <=> not y = 0  %%changed
     .          0/x = 0 if def 0/x
end

spec
     DefineCommutativeField=
     DefineField with sort Elem, ops 0, 1, __+__, __ * __
then
     op
           __ * __ : Elem × Elem -> Elem,
                     comm
end

spec
     CommutativeField
     [DefineCommutativeField with
      sort Elem,
      ops 0, 1, __+__, __ * __
     ] =
%%def
     Field [DefineField]
end