Package natural-fibonacci-def: Definition of Fibonacci numbers
Information
| name | natural-fibonacci-def |
| version | 1.2 |
| description | Definition of Fibonacci numbers |
| author | Joe Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2012-03-08 |
| requires | base natural-fibonacci-exists |
| show | Data.Bool Data.List Data.Pair Number.Natural Number.Natural.Fibonacci |
Files
- Package tarball natural-fibonacci-def-1.2.tgz
- Theory file natural-fibonacci-def.thy (included in the package tarball)
Defined Constants
- Number
- Natural
- fibonacci
- Fibonacci
- decode
- decode.dest
- encode
- encode.find
- encode.mk
- decode
- Natural
Theorems
⊦ fibonacci 0 = 0
⊦ fibonacci 1 = 1
⊦ ∀f p. decode.dest f p [] = 0
⊦ ∀n. encode n = encode.find n 1 0
⊦ ∀l. decode l = decode.dest 1 0 l
⊦ ∀n. fibonacci (n + 2) = fibonacci (n + 1) + fibonacci n
⊦ ∀n f p.
encode.find n f p =
let s ← f + p in
if n < s then encode.mk [] n f p else encode.find n s f
⊦ ∀f p h t.
decode.dest f p (h :: t) =
let s ← f + p in let n ← decode.dest s f t in if h then s + n else n
⊦ ∀l n f p.
encode.mk l n f p =
if p = 0 then l
else if f ≤ n then encode.mk (⊤ :: l) (n - f) p (f - p)
else encode.mk (⊥ :: l) n p (f - p)
Input Type Operators
- →
- bool
- Data
- List
- list
- Pair
- ×
- List
- Number
- Natural
- natural
- Natural
Input Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- []
- Pair
- ,
- Bool
- Number
- Natural
- +
- -
- <
- ≤
- bit0
- bit1
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (λx. t x) = t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀p x. p x ⇒ p ((select) p)
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀PAIR'. ∃fn. ∀a0 a1. fn (a0, a1) = PAIR' a0 a1
⊦ ∀p. (∀x. ∃y. p x y) ⇔ ∃y. ∀x. p x (y x)
⊦ ∀b f x y. f (if b then x else y) = if b then f x else f y
⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x
⊦ ∀NIL' CONS'.
∃fn. fn [] = NIL' ∧ ∀a0 a1. fn (a0 :: a1) = CONS' a0 a1 (fn a1)
⊦ ∃f. f 0 = 0 ∧ f 1 = 1 ∧ ∀n. f (n + 2) = f (n + 1) + f n