Package relation-def: Definition of relation operators

Information

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

Files

Defined Constants

Theorems

empty = fromSet Set.∅

universe = fromSet Set.universe

r. reflexive r x. r x x

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

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

r. irreflexive r x. ¬r x x

r s. subrelation r s Set.⊆ (toSet r) (toSet s)

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

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

s x y. fromSet s x y Set.∈ (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

Input Type Operators

Input Constants

Assumptions

T

() = λp. p = λx. T