Package natural-bits-def: Definition of natural number to bit-list conversions

Information

name	natural-bits-def
version	1.13
description	Definition of natural number to bit-list conversions
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2012-11-10
requires	bool list natural pair probability relation
show	Data.Bool Data.List Data.Pair Number.Natural Probability.Random

Files

Package tarball natural-bits-def-1.13.tgz
Theory file natural-bits-def.thy (included in the package tarball)

Defined Constants

Number
- Natural
  - Bits
    - Bits.bit
    - Bits.fromNatural
    - Bits.normal
    - Bits.toNatural
    - Bits.width
  - Uniform
    - Uniform.fromRandom
      - Uniform.fromRandom.loop

Theorems

⊦ Bits.toNatural [] = 0

⊦ ∀l. Bits.normal l ⇔ null l ∨ last l

⊦ ∀n. Bits.fromNatural n = map (Bits.bit n) (interval 0 (Bits.width n))

⊦ ∀n i. Bits.bit n i ⇔ odd (n div 2 ↑ i)

⊦ ∀n. Bits.width n = if n = 0 then 0 else log 2 n + 1

⊦ ∀h t. Bits.toNatural (h :: t) = 2 * Bits.toNatural t + if h then 1 else 0

⊦ ∀n r.
    Uniform.fromRandom n r =
    let w ← Bits.width (n - 1) in
    let (r₁, r₂) ← split r in
    (Uniform.fromRandom.loop n w r₁ mod n, r₂)

⊦ ∀n w r.
    Uniform.fromRandom.loop n w r =
    let (l, r') ← bits w r in
    let m ← Bits.toNatural l in
    if m < n then m else Uniform.fromRandom.loop n w r'

Input Type Operators

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

Input Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - interval
  - last
  - map
  - null
- Pair
  - ,
Number
- Natural
  - *
  - +
  - -
  - <
  - ↑
  - bit0
  - bit1
  - div
  - log
  - mod
  - odd
  - zero
Probability
- Random
  - bits
  - split

Assumptions

⊦ ⊤

⊦ ¬⊥ ⇔ ⊤

⊦ ¬⊤ ⇔ ⊥

⊦ (∃) = λp. p ((select) p)

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λp. p = λx. ⊤

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

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