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

Information

Files

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

Defined Constants

• Number
  • Natural
    • fromBool
    • Bits
      • Bits.append
      • Bits.bit
      • Bits.bound
      • Bits.cons
      • Bits.fromNatural
      • Bits.head
      • Bits.normal
      • Bits.shiftLeft
      • Bits.shiftRight
      • Bits.tail
      • Bits.toNatural
      • Bits.width
    • Uniform
      • Uniform.fromRandom
        • Uniform.fromRandom.loop

Theorems

⊦ ∀n. Bits.head n ⇔ odd n

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

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

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

⊦ ∀l. Bits.normal 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. Bits.fromNatural n = map (Bits.bit n) (interval 0 (Bits.width n))

⊦ ∀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. Bits.width n = if n = 0 then 0 else log 2 n + 1

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

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
    • 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)

⊦ ∀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 g h. ∃f. ∀x. f x = if p x then f (g x) else h x

OpenTheory package document generated by opentheory 1.2 (release 20140322)