Package relation-def: Definition of relation operators
Information
| name | relation-def |
| version | 1.8 |
| description | Definition of relation operators |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-02-07 |
| requires | bool |
| show | Data.Bool Data.Pair Relation |
Files
- Package tarball relation-def-1.8.tgz
- Theory 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 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
- →
- bool
- Data
- Pair
- ×
- Pair
- Set
- Set.set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ¬
- ⊤
- Pair
- ,
- Bool
- Set
- Set.∅
- Set.bigIntersect
- Set.bigUnion
- Set.fromPredicate
- Set.image
- Set.∩
- Set.∈
- Set.⊆
- Set.∪
- Set.universe
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤