LinearDistributivity.als

sig E {
  join, meet : E -> one E
}
one sig top, bot in E {}

fact {
  all x, y, z : E {
    -- commutativity
    x.join[y] = y.join[x]
    x.meet[y] = y.meet[x]

    -- associativity
    (x.join[y]).join[z] = x.join[y.join[z]]
    (x.meet[y]).meet[z] = x.meet[y.meet[z]]

    -- unit laws
    x.meet[top] = x
    x.join[bot] = x

    -- idempotence
    x.join[x] = x
    x.meet[x] = x

    -- asborption
    x.meet[x.join[y]] = x
    x.join[x.meet[y]] = x
  }
}

pred show {}

run show for 5 E

assert wellDefinedOrdering {
  all x, y : E {
    x.join[y]=x <=> x.meet[y]=y
  }
}

check wellDefinedOrdering for 7 E

pred distributivity {
  all x, y, z : E | x.meet[y.join[z]] = (x.meet[y]).join[x.meet[z]]
}

run distributivity for 5 E

assert linearDistributivityAsEquality {
  distributivity =>
    all x, y, z : E | x.meet[y.join[z]] = x.meet[y].join[z]
}

check linearDistributivityAsEquality for 7 E

pred le[x : E, y : E] {
  x.join[y] = y
}

assert linearDistributivityAsInequality {
  distributivity =>
    all x, y, z : E | le[x.meet[y.join[z]], x.meet[y].join[z]]
}

check linearDistributivityAsInequality  for 7 E