Package natural-fibonacci-thm: Properties of Fibonacci numbers

Information

namenatural-fibonacci-thm
version1.11
descriptionProperties of Fibonacci numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-03-26
requiresbase
natural-fibonacci-def
natural-fibonacci-exists
showData.Bool
Data.List
Number.Natural
Number.Natural.Fibonacci

Files

Theorems

decode [] = 0

n. zeckendorf (encode n)

n. decode (encode n) = n

n. k. n fibonacci k

fibonacci 2 = 1

k. fibonacci k = 0 k = 0

l. zeckendorf l encode (decode l) = l

h t. zeckendorf (h :: t) zeckendorf t

j k. j k fibonacci j fibonacci k

j k. fibonacci j < fibonacci k j < k

k. fibonacci (suc (suc k)) = fibonacci (suc k) + fibonacci k

j. ¬(j = 1) fibonacci j < fibonacci (suc j)

n. k. fibonacci k n n < fibonacci (k + 1)

l. ¬null l zeckendorf l fibonacci (length l + 1) decode l

l1 l2. zeckendorf (l1 @ l2) decode l1 < fibonacci (length l1 + 2)

l1 l2. zeckendorf l1 zeckendorf l2 decode l1 = decode l2 l1 = l2

l1 l2.
    zeckendorf l1 zeckendorf l2 length l1 < length l2
    decode l1 < decode l2

j k. ¬(j = 1 k = 2) j < k fibonacci j < fibonacci k

j k. ¬(j = 2 k = 1) fibonacci j fibonacci k j k

j k.
    fibonacci (j + (k + 1)) =
    fibonacci j * fibonacci k + fibonacci (j + 1) * fibonacci (k + 1)

p. p 0 p 1 (n. p n p (n + 1) p (n + 2)) n. p n

h.
    (f g n. (m. m + 1 = n m + 2 = n f m = g m) h f n = h g n)
    f. n. f n = h f n

Input Type Operators

Input Constants

Assumptions

null []

zeckendorf []

¬

¬

length [] = 0

bit0 0 = 0

fibonacci 0 = 0

t. t t

n. 0 n

n. n n

p. p

t. t ¬t

n. n suc n

(¬) = λp. p

t. (x. t) t

t. (x. t) t

() = λp. p = λx.

fibonacci 1 = 1

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

m. m < 0

n. 0 * n = 0

n. 0 + n = n

m. m + 0 = m

l. [] @ l = l

l. l @ [] = l

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m. 1 * m = m

l. null l l = []

h t. ¬null (h :: t)

m n. m m + n

m n. n m + n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. even (suc n) ¬even n

m. m 0 m = 0

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

h t. head (h :: t) = h

f p. decode.dest f p [] = 0

n. encode n = encode.find n 1 0

n. 0 < n ¬(n = 0)

n. bit0 (suc n) = suc (suc (bit0 n))

l. decode l = decode.dest 1 0 l

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

m n. m + n = n + m

m n. m + n - m = n

n. 2 * n = n + n

h t. length (h :: t) = suc (length t)

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. m < suc n m n

m n. suc m n m < n

m. m = 0 n. m = suc n

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

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

h t. (h :: []) @ t = h :: t

t1 t2. ¬t1 ¬t2 t2 t1

m n. m + suc n = suc (m + n)

m n. suc m + n = suc (m + n)

m n. m < m + n 0 < n

m n. n < m + n 0 < m

m n. suc m = suc n m = n

m n. suc m < suc n m < n

m n. suc m suc n m n

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. even (m * n) even m even n

m n. even (m + n) even m even n

l1 l2. length (l1 @ l2) = length l1 + length l2

m n. m n d. n = m + d

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

m n. m n m < n m = n

m n. m n n m m = n

m n. m < n d. n = m + suc d

p q r. p q r p q r

m n p. m + (n + p) = m + n + p

m n p. m + n = m + p n = p

m n p. m + p = n + p m = n

m n p. m + n < m + p n < p

m n p. n + m < p + m n < p

m n p. m + n m + p n p

m n p. m + p n + p m n

m n p. m < n n p m < p

m n p. m n n < p m < p

m n p. m n n p m p

l h t. (h :: t) @ l = h :: t @ l

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

m n. m suc n m = suc n m n

m n. m * n = 0 m = 0 n = 0

m n. m + n = 0 m = 0 n = 0

n. fibonacci (n + 2) = fibonacci (n + 1) + fibonacci n

P. P 0 (n. P n P (suc n)) n. P n

m n p. m * (n + p) = m * n + m * p

m n p. (m + n) * p = m * p + n * p

p. p [] (h t. p t p (h :: t)) l. p l

m n p. m * n = m * p m = 0 n = p

m n p. m * n m * p m = 0 n p

p. (n. p n) p ((minimal) p) m. m < (minimal) p ¬p m

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

m n p. m * n < m * p ¬(m = 0) n < p

h1 h2 t1 t2. h1 :: t1 = h2 :: t2 h1 = h2 t1 = t2

p c x y. p (if c then x else y) (c p x) (¬c p y)

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

p. p 0 p 1 (n. p n p (n + 1) p (n + 2)) n. p 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)

h.
    (f g n. (m. m + 1 = n m + 2 = n f m = g m) h f n = h g n)
    f. n. f n = h f n