c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder% Algebraic hierarchy
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig RightDistrib = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag1 : Magma %open * %as +.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag2 : Magma %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder dist : |- forall [x] (forall [y] (forall [z] ((x + y) * z == (x * z) + (y * z)))).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Distrib = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag1 : Magma.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag2 : Magma.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct rdis : RightDistrib = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag1 := mag1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag2 := mag2.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct ldis : RightDistrib = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag1 := mag1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag2 := OppositeMagma rdis.mag2.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit add : GroupAbelian %open + 0 -.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mult : Semigroup %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %infix none 110 *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct dis : Distrib = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag1 := add.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag2 := mult.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig RingCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit r : Ring %open + 0 - *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : MagmaCommut = {%struct mag := r.mult.}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig RingUnit = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit r : Ring %open + 0 - *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mon : Monoid = {%struct sg := r.mult.} %open e %as 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig RingUnitCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit ru : RingUnit %open + 0 - * 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : MagmaCommut = {%struct mag := Ring..mult.}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig IntegralDomain = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit ru : RingUnit %open + 0 - * 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder noZeroDiv : |- forall [x] forall [y] (x != 0 and y != 0 => x * y != 0).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig RingDivision = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit ru : RingUnit %open + 0 - * 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder inv : i -> i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder invLeft : |- forall [x] (x != 0 => x * (inv x) == 1).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder invRight : |- forall [x] (x != 0 => (inv x) * x == 1).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Field = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit rd : RingDivision.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : RingCommut = {%struct r := rd.}.