Package relation-def: Definition of relation operators

Information

namerelation-def
version1.23
descriptionDefinition of relation operators
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-12-02
requiresbool
set
showData.Bool
Data.Pair
Relation
Set

Files

Defined Constants

Theorems

empty = fromSet

universe = fromSet universe

r. reflexive r x. r x x

s. bigIntersect s = fromSet (bigIntersect (image toSet s))

s. bigUnion s = fromSet (bigUnion (image toSet s))

r. irreflexive r x. ¬r x x

r s. subrelation r s toSet r toSet s

r s. intersect r s = fromSet (toSet r toSet s)

r s. union r s = fromSet (toSet r toSet s)

s x y. fromSet s x y (x, y) s

r. toSet r = { x y. (x, y) | r x y }

r.
    transitiveClosure r =
    bigIntersect { s. s | subrelation r s transitive s }

r. transitive r x y z. r x y r y z r x z

External Type Operators

External Constants

Assumptions

() = λp. p = λx.