c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder% Algebraic hierarchy
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../logics/first-order/proof_theory/derived.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Magma = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder * : i -> i -> i. %infix none 100 *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppositeMagma : Magma -> Magma = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder * := [x][y] y * x.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MagmaCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mag : Magma %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder commut : |- forall [x] forall [y] (x * y == y * x).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppositeMagmaCommut : MagmaCommut -> MagmaCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag := OppositeMagma mag.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder commut := forallI [x] forallI [y] (forall2E commut y x).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Semigroup = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mag : Magma %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder assoc : |- forall [x] forall [y] forall [z] ((x * y) * z == x * (y * z)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppositeSemigroup : Semigroup -> Semigroup = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag := OppositeMagma mag.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder assoc := forallI [z] forallI [y] forallI [x] (sym (forall3E assoc x y z)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig SemigroupCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit sg : Semigroup.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : MagmaCommut = {%struct mag := sg.}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view OppositeSemigroupCommut : SemigroupCommut -> SemigroupCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct sg := OppositeSemigroup sg.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc := OppositeMagmaCommut mc.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MagmaIdempotent = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open |- forall ==.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mag : Magma %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder idem : |- forall [x] (x * x == x).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit sg : Semigroup.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct midem : MagmaIdempotent = {%struct mag := sg.}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MagmaRightIden = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open i |- forall ==.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mag : Magma %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder iden : |- forall [x] (x * e == x).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MagmaIdentity = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit rid : MagmaRightIden %open * e.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct lid : MagmaRightIden = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mag := OppositeMagma rid.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Monoid = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit sg : Semigroup %open *.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct miden : MagmaIdentity = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct rid.mag := sg.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MonoidCommut = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open |- forall ==.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mon : Monoid.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : MagmaCommut = {%struct mag := mon.}.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig MagmaRightInv = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt %open i |- forall ==.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit id : MagmaIdentity %open * e.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder inv : i -> i.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder inverse : |- forall [x] (x * (inv x) == e).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Group = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit mon : Monoid %open * e.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct minv : MagmaRightInv = {%struct id := mon.miden.} %open inv.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig GroupAbelian = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FOLEQPFExt.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct %implicit g : Group %open * %as + e %as 0 inv %as -.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %struct mc : MagmaCommut = {%struct mag := g.}.