Package relation-def: Definition of relation operators
Information
| name | relation-def |
| version | 1.25 |
| description | Definition of relation operators |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-10-30 |
| checksum | 9f7a83d975e6e78994a4c5cbf2a328f27bc1d513 |
| requires | bool set |
| show | Data.Bool Data.Pair Relation Set |
Files
- Package tarball relation-def-1.25.tgz
- Theory source file relation-def.thy (included in the package tarball)
Defined Constants
- Relation
- bigIntersect
- bigUnion
- empty
- fromSet
- intersect
- irreflexive
- reflexive
- subrelation
- toSet
- transitive
- transitiveClosure
- union
- universe
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
- →
- bool
- Data
- Pair
- ×
- Pair
- Set
- set
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- ⊤
- Pair
- ,
- Bool
- Set
- ∅
- bigIntersect
- bigUnion
- fromPredicate
- image
- ∩
- ∈
- ⊆
- ∪
- universe
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤