Package natural-funpow: Function power
Information
| name | natural-funpow |
| version | 1.12 |
| description | Function power |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| requires | bool function natural-add natural-def natural-mult natural-numeral natural-thm |
| show | Data.Bool Function Number.Natural |
Files
- Package tarball natural-funpow-1.12.tgz
- Theory source file natural-funpow.thy (included in the package tarball)
Defined Constant
- Function
- ↑
Theorems
⊦ ∀n. id ↑ n = id
⊦ ∀f. f ↑ 0 = id
⊦ ∀f. f ↑ 1 = f
⊦ ∀f n. f ↑ suc n = f ∘ f ↑ n
⊦ ∀f n. f ↑ suc n = f ↑ n ∘ f
⊦ ∀f n x. (f ↑ suc n) x = f ((f ↑ n) x)
⊦ ∀f n x. (f ↑ suc n) x = (f ↑ n) (f x)
⊦ ∀f m n. f ↑ (m * n) = (f ↑ m) ↑ n
⊦ ∀f m n. f ↑ (m + n) = f ↑ m ∘ f ↑ n
External Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∃!
- ⊤
- Bool
- Function
- id
- ∘
- Number
- Natural
- *
- +
- bit0
- bit1
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ bit0 0 = 0
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀m. m * 0 = 0
⊦ ∀m. m + 0 = m
⊦ ∀f. f ∘ id = f
⊦ ∀f. id ∘ f = f
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀f g x. (f ∘ g) x = f (g x)
⊦ ∀m n. m * suc n = m + m * n
⊦ ∀f g h. f ∘ g ∘ h = f ∘ (g ∘ h)
⊦ ∀r. (∀x. ∃y. r x y) ⇔ ∃f. ∀x. r x (f x)
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y
⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n