Package function-def: Definition of function operators and combinators
Information
| name | function-def |
| version | 1.10 |
| description | Definition of function operators and combinators |
| author | Joe Hurd <joe@gilith.com> |
| license | HOLLight |
| requires | bool |
| show | Data.Bool Function |
Files
- Package tarball function-def-1.10.tgz
- Theory file function-def.thy (included in the package tarball)
Defined Constants
- Function
- c
- id
- injective
- k
- ∘
- s
- surjective
- w
Theorems
⊦ id = λx. x
⊦ k = λx y. x
⊦ w = λf x. f x x
⊦ c = λf x y. f y x
⊦ s = λf g x. f x (g x)
⊦ ∀f g. f ∘ g = λx. f (g x)
⊦ ∀f. surjective f ⇔ ∀y. ∃x. y = f x
⊦ ∀f. injective f ⇔ ∀x1 x2. f x1 = f x2 ⇒ x1 = x2
Input Type Operators
- →
- bool
Input Constants
- =
- Data
- Bool
- ∀
- ⇒
- ∃
- T
- Bool
Assumptions
⊦ T
⊦ (∀) = λp. p = λx. T