Package natural-funpow-thm: Properties of function power
Information
| name | natural-funpow-thm |
| version | 1.3 |
| description | Properties of function power |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-06-15 |
| requires | bool function natural-add natural-def natural-funpow-def natural-mult natural-numeral |
| show | Data.Bool Function Number.Natural |
Files
- Package tarball natural-funpow-thm-1.3.tgz
- Theory file natural-funpow-thm.thy (included in the package tarball)
Theorems
⊦ ∀n. id ↑ n = id
⊦ ∀f. f ↑ 1 = f
⊦ ∀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
Input Type Operators
- →
- bool
- Number
- Natural
- natural
- Natural
Input Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ⊤
- Bool
- Function
- ↑
- id
- ∘
- Number
- Natural
- *
- +
- bit0
- bit1
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ bit0 0 = 0
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀m. m * 0 = 0
⊦ ∀m. m + 0 = m
⊦ ∀f. f ↑ 0 = id
⊦ ∀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 ⊤ ⊤
⊦ ∀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 n. f ↑ suc n = f ∘ f ↑ n
⊦ ∀f g h. f ∘ g ∘ h = f ∘ (g ∘ h)
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n