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