/*
 * Exercise A.1.4 on page 232 of
 * Software Abstractions, by Daniel Jackson
 *
 * When writing "navigation expressions," you may notice repeated
 * subexpressions that can be factored out, making the overall expression more
 * succinct. For example the expression (p.mother.brother + p.father.brother),
 * denoting p's uncles, can be written instead as p.(mother + father).brother.
 * Simplifications like this rely on the assumption that certain algebraic
 * identities hold, such as
 *
 * a) distributivity of join over union: s.(p + q) = s.p + s.q
 *
 * b) distributivity of join over difference: s.(p - q) = s.p - s.q
 *
 * c) distributivity of join over intersection: s.(p & q) = s.p & s.q
 *
 * for a given set s and binary relations p and q.
 *
 * For each putative identity, say whether it holds, and if not, give a
 * counterexample. The commands below tell the analyzer to find
 * counterexample withint a universe of 4 elements. When you find that a
 * property does not hold, try and obtain the smallest counterexample you can,
 * by reducing the scope (for example, replacing "for 4" by "for 2").
 */
module examples/tutorial/distribution

assert union {
  all s: set univ, p, q: univ -> univ | s.(p + q) = s.p + s.q
}

assert difference {
  all s: set univ, p, q: univ -> univ | s.(p - q) = s.p - s.q
}

assert intersection {
  all s: set univ, p, q: univ -> univ | s.(p & q) = s.p & s.q
}

check union for 4
check difference for 4
check intersection for 4