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

Information

name	natural-bits-def
version	1.31
description	Definition of natural number to bit-list conversions
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2015-04-18
checksum	d3b322d91850c4c6fedf840cc18dcc7fb27aca1d
requires	base probability
show	Data.Bool Data.List Data.Pair Number.Natural Probability.Random

Files

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

Defined Constants

Number
- Natural
  - fromBool
  - Bits
    - Bits.and
    - Bits.append
    - Bits.bit
    - Bits.bound
    - Bits.compare
    - Bits.cons
    - Bits.fromList
    - Bits.head
    - Bits.normalList
    - Bits.or
    - Bits.shiftLeft
    - Bits.shiftRight
    - Bits.tail
    - Bits.toList
    - Bits.toVector
    - Bits.width
  - Uniform
    - Uniform.random
      - Uniform.random.loop

Theorems

⊦ ∀n. Bits.head n ⇔ odd n

⊦ ∀n. Bits.toVector n 0 = []

⊦ ∀l. Bits.fromList l = Bits.append l 0

⊦ ∀n. Bits.toList n = Bits.toVector n (Bits.width n)

⊦ ∀b. fromBool b = if b then 1 else 0

⊦ ∀n. Bits.tail n = n div 2

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

⊦ ∀n i. Bits.bit n i ⇔ Bits.head (Bits.shiftRight n i)

⊦ ∀l n. Bits.append l n = foldr Bits.cons n l

⊦ ∀n k. Bits.bound n k = n mod 2 ↑ k

⊦ ∀n k. Bits.shiftLeft n k = 2 ↑ k * n

⊦ ∀n k. Bits.shiftRight n k = n div 2 ↑ k

⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t

⊦ ∀n k.
Bits.toVector n (suc k) = Bits.head n :: Bits.toVector (Bits.tail n) k

⊦ ∀n r.
Uniform.random n r =
let w ← Bits.width (n - 1) in Uniform.random.loop n w r

⊦ ∀q m n. Bits.compare q m n ⇔ if q then m ≤ n else m < n

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

⊦ ∀m n.
    Bits.and m n =
    Bits.fromList
      (map (λi. Bits.bit m i ∧ Bits.bit n i)
         (interval 0 (min (Bits.width m) (Bits.width n))))

⊦ ∀m n.
    Bits.or m n =
    Bits.fromList
      (map (λi. Bits.bit m i ∨ Bits.bit n i)
         (interval 0 (max (Bits.width m) (Bits.width n))))

⊦ ∀n w r.
    Uniform.random.loop n w r =
    let (r₁, r₂) ← split r in
    let l ← bits w r₁ in
    let m ← Bits.fromList l in
    if m < n then m else Uniform.random.loop n w r₂

External Type Operators

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

External Constants

=
select
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∃!
  - ∨
  - ¬
  - cond
  - ⊥
  - ⊤
- List
  - ::
  - []
  - foldr
  - interval
  - last
  - map
  - null
- Pair
  - ,
Number
- Natural
  - *
  - +
  - -
  - <
  - ≤
  - ↑
  - bit0
  - bit1
  - div
  - log
  - max
  - min
  - mod
  - odd
  - suc
  - 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)

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

⊦ (∃!) = λp. (∃) p ∧ ∀x y. p x ∧ p y ⇒ x = y

⊦ ∀p g h. ∃f. ∀x. f x = if p x then f (g x) else h x

⊦ ∀e f. ∃!fn. fn 0 = e ∧ ∀n. fn (suc n) = f (fn n) n