[PostScript]
RelationOps: trait
  % Useful non-primitive operators on relations.
  assumes RelationBasics
  includes 
    DerivedOrders (R, \subseteq for <=, \supseteq for >=, 
                   \subset for <, \supset for >)
  introduces
    __ \in __, __ \notin __: E, R -> Bool
    set, dom, range, __\superplus, __\superstar: R -> R
    __ \I __, __ \circ __, __ - __, __ \times __: R, R -> R
    domRestrict, rangeRestrict, image: R, R -> R
    skolem: E, R, R, E -> E
  asserts
    forall e, e1, e2, e3: E, r, r1, r2: R
      e \in r == e \langle r \rangle e;
      e \notin r == ~(e \in r);
      set(r) == r \I I;
      dom(r) == set(r \circ \top);
      range(r) == set(\top \circ r);
      e1 \langle r1 \I r2 \rangle e2 == e1 \langle r1 \rangle e2 /\ e1 \langle r2 \rangle e2;
      (e1 \langle r1 \rangle e2 /\ e2 \langle r2 \rangle e3)
        => e1 \langle r1 \circ r2 \rangle e3;
      e1 \langle r1 \circ r2 \rangle e2
        => (e1 \langle r1 \rangle skolem(e1, r1, r2, e2) 
          /\ skolem(e1, r1, r2, e2) \langle r2 \rangle e2);
      r\superplus == r \circ (r\superstar);
      r\superstar == I \U (r\superplus);
      (r1 = I \U r2 /\ r2 = r \circ r1) => 
        ((r\superstar) \subseteq r1 /\ (r\superplus) \subseteq r2);
      r1 - r2 == r1 \I (-r2);
      r1 \times r2 == set(r1) \circ \top \circ set(r2);
      r1 \subseteq r2 == r1 - r2 = \bot;
      domRestrict(r1, r2) == r1 \I (r2 \circ \top);
      image(r1, r2) == set(r1) \circ r2;
      rangeRestrict(r1, r2) == r1 \I (\top \circ r2)
  implies
    AbelianMonoid (\top for unit, \I for \circ, R for T),
    Distributive (\U for +, \I for *, R for T),
    Distributive (\I for +, \U for *, R for T),
    Idempotent (set, R),
    Monoid (I for unit, R for T),
    Lattice (R for T, \U for \lub, \I for \glb,
      \subseteq for <=, \supseteq for >=, \subset for <, \supset for >),
    PartialOrder (R, \subseteq for <=, \supseteq for >=, \subset for <, 
      \supset for >)
    forall e: E, r, r1, r2: R
      e \in r == e \in set(r);
      -(r1 \U r2) == (-r1) \I (-r2);
      -(r1 \I r2) == (-r1) \U (-r2);
      (r1 \circ r2)\inv == (r2\inv) \circ (r1\inv)
    converts
      \in, \notin, set, dom, range, __\superplus, __\superstar, __-__, \times,
      \U, \I, \circ, -:R->R, \inv, \subseteq, \supseteq, \subset, \supset, 
      domRestrict, image, rangeRestrict
[Table of Contents] [Index]