Package relation-thm: Properties of relation operators

Information

namerelation-thm
version1.15
descriptionProperties of relation operators
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-11-17
checksumd7008776d55f6c2701e81a162a7f24486e8db96a
requiresbool
pair
relation-def
set
showData.Bool
Data.Pair
Relation
Set

Files

Theorems

irreflexive empty

reflexive universe

transitive empty

transitive universe

r. transitive (transitiveClosure r)

r. subrelation r r

r. subrelation r (transitiveClosure r)

x y. universe x y

s. toSet (fromSet s) = s

r. fromSet (toSet r) = r

x y. ¬empty x y

r x. reflexive r r x x

r x. irreflexive r ¬r x x

r s. toSet r = toSet s r = s

r s.
    subrelation r s transitive s subrelation (transitiveClosure r) s

r s. subrelation r s subrelation s r r = s

r x y. (x, y) toSet r r x y

r s t. subrelation r s subrelation s t subrelation r t

r s. subrelation r (bigIntersect s) t. t s subrelation r t

r s. subrelation r s x y. r x y s x y

r s. (x y. r x y s x y) r = s

s x y. bigIntersect s x y r. r s r x y

s x y. bigUnion s x y r. r s r x y

r s x y. intersect r s x y r x y s x y

r s x y. union r s x y r x y s x y

External Type Operators

External Constants

Assumptions

empty = fromSet

universe = fromSet universe

¬

x. x universe

t. t t

p. p

x. ¬(x )

(¬) = λp. p

t. (x. t) t

() = λp. p = λx.

t. t

t. t t

t. t t

t. t

t. t t

() = λp q. p q p

r. reflexive r x. r x x

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

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

x y. x = y y = x

p x. x fromPredicate p p x

r. irreflexive r x. ¬r x x

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

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)

p. (x. p x) a b. p (a, b)

f g. (x. f x = g x) f = g

s t. s t t s s = t

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

p q r. p q r p q r

s t u. s t t u s u

s t. s t x. x s x t

s t. (x. x s x t) s = t

t u. t bigIntersect u s. s u t s

s x. x bigIntersect s t. t s x t

s x. x bigUnion s t. t s x t

p x. x { y. y | p y } p x

s t x. x s t x s x t

s t x. x s t x s x t

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

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

y s f. y image f s x. y = f x x s

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

a b a' b'. (a, b) = (a', b') a = a' b = b'

p f s. (y. y image f s p y) x. x s p (f x)