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