latte-sets.ralgebra
The relation algebra operators.
dist-rinter-runion
(dist-rinter-runion [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq
(rinter R1 (runion R2 R3))
(runion (rinter R1 R2) (rinter R1 R3)))
Theorem: Distributivity of intersection over union.
dist-rinter-runion-sym
(dist-rinter-runion-sym [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq
(runion (rinter R1 R2) (rinter R1 R3))
(rinter R1 (runion R2 R3)))
Theorem: Symmetric case of dist-rinter-runion.
dist-runion-rinter
(dist-runion-rinter [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq
(runion R1 (rinter R2 R3))
(rinter (runion R1 R2) (runion R1 R3)))
Theorem: Distributivity of union over intersection.
dist-runion-rinter-sym
(dist-runion-rinter-sym [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq
(rinter (runion R1 R2) (runion R1 R3))
(runion R1 (rinter R2 R3)))
Theorem: Symmetric case of dist-runion-rinter.
rcomp-empty-full
(rcomp-empty-full [T :type] [U :type])(releq (rcomplement (emptyrel T U)) (fullrel T U))
Theorem:
rcomp-full-empty
(rcomp-full-empty [T :type] [U :type])(releq (rcomplement (fullrel T U)) (emptyrel T U))
Theorem:
rcomplement
(rcomplement [R (rel T U)])(lambda [x T] (lambda [y U] (not (R x y))))
Definition: The complement of relation R.
rdiff
(rdiff [R1 (rel T U)] [R2 (rel T U)])(lambda [x T] (lambda [y U] (and (R1 x y) (not (R2 x y)))))
Definition: Relational difference.
rdiff-cancel
(rdiff-cancel [R (rel T U)])(releq (rdiff R R) (emptyrel T U))
Theorem:
rdiff-empty-left
(rdiff-empty-left [R (rel T U)])(releq (rdiff (emptyrel T U) R) (emptyrel T U))
Theorem:
rdiff-empty-right
(rdiff-empty-right [R (rel T U)])(releq (rdiff R (emptyrel T U)) R)
Theorem:
restrict-dom
(restrict-dom [R (rel T U)] [s (set T)])(lambda [x T] (lambda [y U] (and (elem x s) (R x y))))
Definition: Restriction of domain of relation R to the subset s.
restrict-dom-dom
(restrict-dom-dom [R (rel T U)] [s (set T)])(seteq (dom (restrict-dom R s)) (inter s (dom R)))
Theorem:
restrict-ran
(restrict-ran [R (rel T U)] [s (set U)])(lambda [x T] (lambda [y U] (and (elem y s) (R x y))))
Definition: Restriction of range of relation R to the subset s.
rimage
(rimage [R (rel T U)] [s (set T)])(lambda [y U] (exists [x T] (and (elem x s) (R x y))))
Definition: Relational image of set s for relation R.
rinter
(rinter [R1 (rel T U)] [R2 (rel T U)])(lambda [x T] (lambda [y U] (and (R1 x y) (R2 x y))))
Definition: Relational intersection.
rinter-assoc
(rinter-assoc [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq (rinter R1 (rinter R2 R3)) (rinter (rinter R1 R2) R3))
Theorem:
rinter-assoc-sym
(rinter-assoc-sym [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq (rinter (rinter R1 R2) R3) (rinter R1 (rinter R2 R3)))
Theorem:
rinter-commute
(rinter-commute [R1 (rel T U)] [R2 (rel T U)])(releq (rinter R1 R2) (rinter R2 R1))
Theorem: Relation intersection commutes.
rinter-elim-left
(rinter-elim-left [R1 (rel T U)] [R2 (rel T U)] [x T] [y U])(==> ((rinter R1 R2) x y) (R1 x y))
Theorem: Elimination rule for intersection (left operand).
rinter-elim-right
(rinter-elim-right [R1 (rel T U)] [R2 (rel T U)] [x T] [y U])(==> ((rinter R1 R2) x y) (R2 x y))
Theorem: Elimination rule for intersection (right operand).
rinter-empty
(rinter-empty [R (rel T U)])(releq (rinter R (emptyrel T U)) (emptyrel T U))
Theorem:
rinter-idem
(rinter-idem [R (rel T U)])(releq (rinter R R) R)
Theorem:
rinverse
(rinverse [R (rel T U)])(lambda [y U] (lambda [x T] (R x y)))
Definition: The relational inverse of R.
rinverse-prop
(rinverse-prop [R (rel T U)] [x T] [y U])(==> (R x y) ((rinverse R) y x))
Theorem:
runion
(runion [R1 (rel T U)] [R2 (rel T U)])(lambda [x T] (lambda [y U] (or (R1 x y) (R2 x y))))
Definition: Relational union.
runion-assoc
(runion-assoc [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq (runion R1 (runion R2 R3)) (runion (runion R1 R2) R3))
Theorem:
runion-assoc-sym
(runion-assoc-sym [R1 (rel T U)] [R2 (rel T U)] [R3 (rel T U)])(releq (runion (runion R1 R2) R3) (runion R1 (runion R2 R3)))
Theorem:
runion-commute
(runion-commute [R1 (rel T U)] [R2 (rel T U)])(releq (runion R1 R2) (runion R2 R1))
Theorem: Relational union commutes.
runion-dom
(runion-dom [R1 (rel T U)] [R2 (rel T U)])(seteq (dom (runion R1 R2)) (set/union (dom R1) (dom R2)))
Theorem:
runion-empty
(runion-empty [R (rel T U)])(releq (runion R (emptyrel T U)) R)
Theorem:
runion-idem
(runion-idem [R (rel T U)])(releq (runion R R) R)
Theorem:
runion-ran
(runion-ran [R1 (rel T U)] [R2 (rel T U)])(seteq (ran (runion R1 R2)) (set/union (ran R1) (ran R2)))
Theorem:
subtract-dom
(subtract-dom [R (rel T U)] [s (set T)])(lambda [x T] (lambda [y U] (and (not (elem x s)) (R x y))))
Definition: Subtraction (or anti-restriction) of set s from the domain of relation R
subtract-ran
(subtract-ran [R (rel T U)] [s (set U)])(lambda [x T] (lambda [y U] (and (not (elem y s)) (R x y))))
Definition: Subtraction of set s from the range of relation R