Package natural-fibonacci-def: Definition of Fibonacci numbers

Information

name	natural-fibonacci-def
version	1.17
description	Definition of Fibonacci numbers
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-06-10
requires	base natural-fibonacci-exists
show	Data.Bool Data.List Data.Pair Number.Natural Number.Natural.Fibonacci Probability.Random

Files

Package tarball natural-fibonacci-def-1.17.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
    - fromRandom
      - fromRandom.dest
    - zeckendorf

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 (r₁, r₂) ← split r in fromRandom.dest ⊥ 0 1 0 r₁ - 1, r₂

⊦ ∀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'

Input Type Operators

→
bool
Data
- List
  - list
- Pair
  - ×
Number
- Natural
  - natural
Probability
- Random
  - random

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - head
  - null
- Pair
  - ,
Number
- Natural
  - +
  - -
  - <
  - ≤
  - bit0
  - bit1
  - zero
Probability
- Random
  - bit
  - split

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 ⇔ ⊥)

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀p x. p x ⇒ p ((select) p)

⊦ ∀xy. ∃x y. xy = (x, y)

⊦ (∧) = λ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. ∀x y. fn (x, y) = f x y

⊦ ∀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

⊦ ∀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