Package natural-fibonacci-def: Definition of Fibonacci numbers

Information

namenatural-fibonacci-def
version1.39
descriptionDefinition of Fibonacci numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-06-12
requiresbase
natural-fibonacci-exists
probability
showData.Bool
Data.List
Data.Pair
Number.Natural
Number.Natural.Fibonacci
Probability.Random

Files

Defined Constants

Theorems

zeckendorf []

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

h t.
    zeckendorf (h :: t)
    if null t then h else ¬(h head t) zeckendorf t

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

r.
    fromRandom r =
    let (r1, r2) split r in (fromRandom.dest 0 1 0 r1 - 1, r2)

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)

b n f p r.
    fromRandom.dest b n f p r =
    let (b', r') bit r in
    if b' b then n
    else
      let s f + p in fromRandom.dest b' (if b' then s + n else n) s f r'

External Type Operators

External Constants

Assumptions

¬

¬

() = λp. p ((select) p)

t. (λx. t x) = t

() = λp. p = λx.

t. (t ) t

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)

x. a b. x = (a, b)

() = λp q. (λf. f p q) = λf. f

() = λp. q. (x. p x q) q

() = λp q. r. (p r) (q r) r

f. fn. a b. fn (a, b) = f a b

r. (x. y. r x y) f. x. r x (f 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

b f. fn. fn [] = b h t. fn (h :: t) = f h t (fn t)

f. f 0 = 0 f 1 = 1 n. f (n + 2) = f (n + 1) + f n