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