% Algebraic hierarchy

%sig Magma = {
  %include FOL %open i.
  * : i -> i -> i.    %infix none 10 *.
}.

%view OppositeMagma : Magma -> Magma = {
  * := [x][y] y * x.
}.

%sig MagmaCommut = {
  %include FOL %open ded forall ==.
  %struct mag : Magma %open *. 
  commut : ded forall [x] forall [y] (x * y == y * x).
}.

%view OppositeMagmaCommut : MagmaCommut -> MagmaCommut = {
  %struct mag := OppositeMagma mag.
  commut := FOL..forallI [x] FOL..forallI [y] (FOL..forallE x (FOL..forallE y commut)).
}.

%sig Semigroup = {
  %include FOL %open ded forall ==.
  %struct mag : Magma %open *.
  assoc : ded forall [x] forall [y] forall [z] ((x * y) * z == x * (y * z)).
}.

%view OppositeSemigroup : Semigroup -> Semigroup = {
  %struct mag := OppositeMagma mag.
  assoc := FOL..forallI [z] FOL..forallI [y] FOL..forallI [x] (FOL..eqsym (FOL..forallE z (FOL..forallE y (FOL..forallE x assoc)))).
}.

%sig SemigroupCommut = {
  %include FOL.
  %struct sg : Semigroup.
  %struct mc : MagmaCommut = {%struct mag := sg.mag.}.
}.

%% This view can be found by purely module level reasoning, this can be automatized efficiently.
%view OppositeSemigroupCommut : SemigroupCommut -> SemigroupCommut = {
  %struct sg := OppositeSemigroup sg.
  %struct mc := OppositeMagmaCommut mc.
}.

%sig MagmaIdempotent = {
  %include FOL %open ded forall ==.
  %struct mag : Magma %open *. 
  idem : ded forall [x] (x * x == x). 
}.

%sig RightIdentity = {
  %include FOL %open ded forall ==.
  %struct mag : Magma %open *. 
  e : FOL..i.
  iden : ded forall [x] (x * e == x).
}.

%sig Monoid = {
  %include FOL %open ded forall ==.
  %struct sg : Semigroup.
  %struct rid : RightIdentity = {%struct mag := sg.mag.} %open * e.
  %struct lid : RightIdentity = {%struct mag := OppositeMagma sg.mag. e := e.}.
}.

%sig MonoidCommut = {
  %include FOL %open ded forall ==.
  %struct mon : Monoid.
  %struct mc : MagmaCommut = {%struct mag := mon.sg.mag.}.
}.

%sig RightInverse = {
  %include FOL %open i ded forall ==.
  %struct rid : RightIdentity  %open * e.
  inv : i -> i.
  inverse : ded forall [x] (x * (inv x) == e).
}. 

%sig Group = {
  %include FOL %open ded forall ==.
  %struct mon : Monoid %open * e.
  %struct minv : RightInverse = {%struct rid := mon.rid.}.
  inv = minv.inv.
}.

%sig GroupAbelian = {
  %include FOL.
  %struct g : Group %open * e inv.
  %struct mc : MagmaCommut = {%struct mag := g.mon.sg.mag.}.
  + = [x][y] x * y.    %infix none 5 +.  
  0 = e.
  - = inv.  
}.

%sig MagmaDistrib = {
  %include FOL %open ded forall ==.
  %struct mag1 : Magma.
  %struct mag2 : Magma.
  + = [x] [y] x mag1.* y.
  * = [x] [y] x mag2.* y.
  %infix none 5 +.
  %infix none 10 *.    
  dist : ded forall [x] (forall [y] (forall [z] ((x + y) * z == x * z + y * z))).
}.

%sig Ring = {
  %include FOL.
  %struct ga : GroupAbelian %open + 0 -.
  %struct sg : Semigroup %open *.
  %struct md : MagmaDistrib = {%struct mag1 := ga.g.mon.sg.mag. %struct mag2 := sg.mag.}.
}.

%sig RingCommut = {
  %include FOL.
  %struct r : Ring %open + 0 - *.
  %struct mc : MagmaCommut = {%struct mag := r.sg.mag.}.
}.

%sig RingUnit = {
  %include FOL.
  %struct r : Ring %open + 0 - *.
  %struct mon : Monoid = {%struct sg := r.sg.} %open e.
  1 = e.
}.

%sig RingUnitCommut = {
  %include FOL.
  %struct ru : RingUnit %open + 0 - * 1.
  %struct mc : MagmaCommut = {%struct mag := ru.mon.sg.mag.}.
}.

%sig IntegralDomain = {
  %include FOL %open ded forall != and =>.
  %struct ru : RingUnit %open + 0 - * 1.
  noZeroDiv : ded forall [x] forall [y] (x != 0  and  y != 0  => x * y != 0).
}.  

%sig RingDivision = {
  %include FOL %open ded i forall != == =>.
  %struct ru : RingUnit %open + 0 - * 1.
  inv : i -> i.
  invLeft : ded forall [x] (x != 0  =>  x * (inv x) == 1). 
  invRight : ded forall [x] (x != 0  => (inv x) * x == 1).
}.

%sig Field = {
  %include FOL.
  %struct rd : RingDivision.
  %struct mc : MagmaCommut = {%struct mag := rd.ru.mon.sg.mag.}.
}.