Package relation-thm: Properties of relation operators
Information
| name | relation-thm |
| version | 1.2 |
| description | Properties of relation operators |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2011-11-15 |
| requires | bool pair set relation-def |
| show | Data.Bool Data.Pair Relation |
Files
- Package tarball relation-thm-1.2.tgz
- Theory file relation-thm.thy (included in the package tarball)
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. Set.∈ (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. Set.∈ 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. Set.∈ r s ⇒ r x y
⊦ ∀s x y. bigUnion s x y ⇔ ∃r. Set.∈ 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
Input Type Operators
- →
- bool
- Data
- Pair
- ×
- Pair
- Set
- Set.set
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- F
- T
- Pair
- ,
- Bool
- Relation
- bigIntersect
- bigUnion
- empty
- fromSet
- intersect
- irreflexive
- reflexive
- subrelation
- toSet
- transitive
- transitiveClosure
- union
- universe
- Set
- Set.∅
- Set.bigIntersect
- Set.bigUnion
- Set.fromPredicate
- Set.image
- Set.∩
- Set.∈
- Set.⊆
- Set.∪
- Set.universe
Assumptions
⊦ T
⊦ empty = fromSet Set.∅
⊦ universe = fromSet Set.universe
⊦ ¬F ⇔ T
⊦ ∀x. Set.∈ x Set.universe
⊦ ∀t. t ⇒ t
⊦ F ⇔ ∀p. p
⊦ ∀x. ¬Set.∈ x Set.∅
⊦ (¬) = λp. p ⇒ F
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. T
⊦ ∀t. F ∧ t ⇔ F
⊦ ∀t. T ∧ t ⇔ t
⊦ ∀t. t ∧ T ⇔ t
⊦ ∀t. F ⇒ t ⇔ T
⊦ ∀t. T ⇒ t ⇔ t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀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))
⊦ ∀x y. x = y ⇔ y = x
⊦ ∀p x. Set.∈ x (Set.fromPredicate p) ⇔ p x
⊦ ∀r. irreflexive r ⇔ ∀x. ¬r x x
⊦ (∧) = λp q. (λf. f p q) = λf. f T T
⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q
⊦ ∀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))
⊦ ∀P. (∀p. P p) ⇔ ∀p1 p2. P (p1, p2)
⊦ ∀f g. (∀x. f x = g x) ⇔ f = g
⊦ ∀s t. Set.⊆ s t ∧ Set.⊆ t s ⇒ s = t
⊦ ∀s x y. fromSet s x y ⇔ Set.∈ (x, y) s
⊦ ∀p q r. p ⇒ q ⇒ r ⇔ p ∧ q ⇒ r
⊦ ∀s t u. Set.⊆ s t ∧ Set.⊆ t u ⇒ Set.⊆ s u
⊦ ∀s t. Set.⊆ s t ⇔ ∀x. Set.∈ x s ⇒ Set.∈ x t
⊦ ∀s t. (∀x. Set.∈ x s ⇔ Set.∈ x t) ⇒ s = t
⊦ ∀t f. Set.⊆ t (Set.bigIntersect f) ⇔ ∀s. Set.∈ s f ⇒ Set.⊆ t s
⊦ ∀s x. Set.∈ x (Set.bigIntersect s) ⇔ ∀t. Set.∈ t s ⇒ Set.∈ x t
⊦ ∀s x. Set.∈ x (Set.bigUnion s) ⇔ ∃t. Set.∈ t s ∧ Set.∈ x t
⊦ ∀p x. Set.∈ x { y. y | p y } ⇔ p x
⊦ ∀s t x. Set.∈ x (Set.∩ s t) ⇔ Set.∈ x s ∧ Set.∈ x t
⊦ ∀s t x. Set.∈ x (Set.∪ s t) ⇔ Set.∈ x s ∨ Set.∈ 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. Set.∈ y (Set.image f s) ⇔ ∃x. y = f x ∧ Set.∈ x s
⊦ ∀r. transitive r ⇔ ∀x y z. r x y ∧ r y z ⇒ r x z
⊦ ∀x y a b. (x, y) = (a, b) ⇔ x = a ∧ y = b
⊦ ∀P f s. (∀y. Set.∈ y (Set.image f s) ⇒ P y) ⇔ ∀x. Set.∈ x s ⇒ P (f x)