Package hardware-thm: Properties of the hardware model

Information

name	hardware-thm
version	1.30
description	Properties of the hardware model
author	Joe Leslie-Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2014-11-01
checksum	f7df20db276cdf89bc70160c34bd8f17cb8bdd71
requires	bool hardware-def list natural natural-bits stream
show	Data.Bool Data.List Data.Stream Hardware Number.Natural

Files

Package tarball hardware-thm-1.30.tgz
Theory source file hardware-thm.thy (included in the package tarball)

Theorems

⊦ Bus.ground 0 = Bus.nil

⊦ Bus.power 0 = Bus.nil

⊦ Bus.width Bus.nil = 0

⊦ ∀t. signal power t

⊦ ∀t. ¬signal ground t

⊦ Bus.ground 1 = Bus.single ground

⊦ Bus.power 1 = Bus.single power

⊦ ∀x. Bus.append Bus.nil x = x

⊦ ∀x. Bus.append x Bus.nil = x

⊦ ∀n. Bus.width (Bus.ground n) = n

⊦ ∀n. Bus.width (Bus.power n) = n

⊦ ∀t. Bus.signal Bus.nil t = []

⊦ ∀w. Bus.width (Bus.single w) = 1

⊦ ∀t. fromBool (signal ground t) = 0

⊦ ∀t. Bits.toNatural (Bus.signal Bus.nil t) = 0

⊦ ∀t. fromBool (signal power t) = 1

⊦ ∀x. Bus.width x = 0 ⇔ x = Bus.nil

⊦ ∀x t. length (Bus.signal x t) = Bus.width x

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.ground n) t) = 0

⊦ ∀n. Bus.ground (suc n) = Bus.append (Bus.single ground) (Bus.ground n)

⊦ ∀n. Bus.power (suc n) = Bus.append (Bus.single power) (Bus.power n)

⊦ ∀n t. Bus.signal (Bus.ground n) t = replicate ⊥ n

⊦ ∀n t. Bus.signal (Bus.power n) t = replicate ⊤ n

⊦ ∀s t. signal (wire s) t ⇔ nth s t

⊦ ∀w x. Bus.width (Bus.append (Bus.single w) x) = suc (Bus.width x)

⊦ ∀w₁ w₂. Bus.single w₁ = Bus.single w₂ ⇔ w₁ = w₂

⊦ ∀w₁ w₂. Bus.single w₁ = Bus.single w₂ ⇒ w₁ = w₂

⊦ ∀x y. Bus.width (Bus.append x y) = Bus.width x + Bus.width y

⊦ ∀x y. Bus.sub x 0 (Bus.width x) y ⇔ y = x

⊦ ∀x. Bus.width x = 1 ⇔ ∃w. x = Bus.single w

⊦ ∀w t. Bus.signal (Bus.single w) t = signal w t :: []

⊦ ∀w t.
Bits.toNatural (Bus.signal (Bus.single w) t) = fromBool (signal w t)

⊦ ∀m n. Bus.ground (m + n) = Bus.append (Bus.ground m) (Bus.ground n)

⊦ ∀m n. Bus.power (m + n) = Bus.append (Bus.power m) (Bus.power n)

⊦ ∀x y z. Bus.append (Bus.append x y) z = Bus.append x (Bus.append y z)

⊦ ∀w₁ w₂. (∀t. signal w₁ t ⇔ signal w₂ t) ⇔ w₁ = w₂

⊦ ∀w₁ w₂. (∀t. signal w₁ t ⇔ signal w₂ t) ⇒ w₁ = w₂

⊦ ∀x k n y. Bus.sub x k n y ⇒ Bus.width y = n

⊦ ∀x y z. Bus.sub (Bus.append x y) 0 (Bus.width x) z ⇔ z = x

⊦ ∀n t. Bits.toNatural (Bus.signal (Bus.power n) t) = 2 ↑ n - 1

⊦ ∀x y z. Bus.sub (Bus.append x y) (Bus.width x) (Bus.width y) z ⇔ z = y

⊦ ∀x y t. Bus.signal (Bus.append x y) t = Bus.signal x t @ Bus.signal y t

⊦ ∀x k n y. Bus.sub x k n y ⇒ k + n ≤ Bus.width x

⊦ ∀x k n. k + n ≤ Bus.width x ⇒ ∃y. Bus.sub x k n y

⊦ ∀x y k. Bus.sub x k 0 y ⇔ k ≤ Bus.width x ∧ y = Bus.nil

⊦ ∀w x t.
Bus.signal (Bus.append (Bus.single w) x) t =
signal w t :: Bus.signal x t

⊦ ∀k n x. Bus.sub Bus.nil k n x ⇔ k = 0 ∧ n = 0 ∧ x = Bus.nil

⊦ ∀x k n y z. Bus.sub x k n y ∧ Bus.sub x k n z ⇒ y = z

⊦ ∀w₁ w₂ x₁ x₂.
Bus.append (Bus.single w₁) x₁ = Bus.append (Bus.single w₂) x₂ ⇔
w₁ = w₂ ∧ x₁ = x₂

⊦ ∀n x.
Bus.width x = suc n ⇔
∃w y. x = Bus.append (Bus.single w) y ∧ Bus.width y = n

⊦ ∀n i k x. Bus.sub (Bus.ground n) i k x ⇔ i + k ≤ n ∧ x = Bus.ground k

⊦ ∀n i k x. Bus.sub (Bus.power n) i k x ⇔ i + k ≤ n ∧ x = Bus.power k

⊦ ∀x y k n z.
Bus.sub (Bus.append x y) (Bus.width x + k) n z ⇔ Bus.sub y k n z

⊦ ∀x y t.
    Bits.toNatural (Bus.signal (Bus.append x y) t) =
    Bits.toNatural (Bus.signal x t) +
    Bits.shiftLeft (Bits.toNatural (Bus.signal y t)) (Bus.width x)

⊦ ∀x y n z.
Bus.sub (Bus.append x y) 0 (Bus.width x + n) (Bus.append x z) ⇔
Bus.sub y 0 n z

⊦ ∀w x n y.
Bus.sub (Bus.append (Bus.single w) x) 0 (suc n)
(Bus.append (Bus.single w) y) ⇔ Bus.sub x 0 n y

⊦ ∀x k n y t.
    Bus.sub x k n y ⇒
    Bits.shiftLeft (Bits.toNatural (Bus.signal y t)) k ≤
    Bits.toNatural (Bus.signal x t)

⊦ ∀x k n y t.
    Bus.sub x k n y ⇒
    Bits.toNatural (Bus.signal y t) =
    Bits.bound (Bits.shiftRight (Bits.toNatural (Bus.signal x t)) k) n

⊦ ∀x y k n z.
k + n ≤ Bus.width x ⇒
(Bus.sub (Bus.append x y) k n z ⇔ Bus.sub x k n z)

⊦ ∀x j m y k n z. Bus.sub x j m y ∧ Bus.sub y k n z ⇒ Bus.sub x (j + k) n z

⊦ ∀x y z k m n.
Bus.sub x k m y ∧ Bus.sub x (k + m) n z ⇒
Bus.sub x k (m + n) (Bus.append y z)

⊦ ∀x j m y k n z.
Bus.sub x j m y ⇒ (Bus.sub y k n z ⇔ k + n ≤ m ∧ Bus.sub x (j + k) n z)

⊦ ∀x y k n xs ys xt yt.
Bus.sub x k n xs ∧ Bus.sub y k n ys ∧
Bus.signal x xt = Bus.signal y yt ⇒ Bus.signal xs xt = Bus.signal ys yt

⊦ ∀x k n y.
    Bus.sub x k n y ⇒
    ∃d p q.
      Bus.width x = k + (n + d) ∧ Bus.sub x 0 k p ∧ Bus.sub x (k + n) d q ∧
      x = Bus.append p (Bus.append y q)

External Type Operators

→
bool
Data
- List
  - list
- Stream
  - stream
Hardware
- bus
- wire
Number
- Natural
  - natural

External Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ¬
  - ⊥
  - ⊤
- List
  - ::
  - @
  - []
  - drop
  - length
  - map
  - replicate
  - take
- Stream
  - nth
  - replicate
Hardware
- bus
- ground
- power
- signal
- signals
- wire
- Bus
  - Bus.append
  - Bus.ground
  - Bus.nil
  - Bus.power
  - Bus.signal
  - Bus.single
  - Bus.sub
  - Bus.width
  - Bus.wires
Number
- Natural
  - +
  - -
  - ≤
  - ↑
  - bit0
  - bit1
  - fromBool
  - suc
  - zero
  - Bits
    - Bits.bound
    - Bits.shiftLeft
    - Bits.shiftRight
    - Bits.toNatural
    - Bits.width

Assumptions

⊦ ⊤

⊦ Bus.nil = bus []

⊦ ¬⊥ ⇔ ⊤

⊦ length [] = 0

⊦ bit0 0 = 0

⊦ fromBool ⊥ = 0

⊦ Bits.toNatural [] = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ ground = wire (replicate ⊥)

⊦ power = wire (replicate ⊤)

⊦ fromBool ⊤ = 1

⊦ ∀t. t ∨ ¬t

⊦ (¬) = λp. p ⇒ ⊥

⊦ ∀t. (∀x. t) ⇔ t

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

⊦ ∀x. replicate x 0 = []

⊦ ∀t. (⊤ ⇔ t) ⇔ t

⊦ ∀t. ⊥ ∧ t ⇔ ⊥

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊥ ⇔ ⊥

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀x. bus (Bus.wires x) = x

⊦ ∀w. wire (signals w) = w

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀l. [] @ l = l

⊦ ∀l. l @ [] = l

⊦ ∀l. drop 0 l = l

⊦ ∀l. take 0 l = []

⊦ ∀l. Bus.wires (bus l) = l

⊦ ∀s. signals (wire s) = s

⊦ ∀f. map f [] = []

⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t

⊦ ∀x. Bus.width x = length (Bus.wires x)

⊦ ∀w. signal w = nth (signals w)

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀k. Bits.toNatural (replicate ⊥ k) = 0

⊦ ∀l. take (length l) l = l

⊦ ∀l. Bits.width (Bits.toNatural l) ≤ length l

⊦ ∀m n. m ≤ m + n

⊦ ∀m n. n ≤ m + n

⊦ ∀n k. Bits.bound n k ≤ n

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀b. Bits.toNatural (b :: []) = fromBool b

⊦ ∀w. Bus.single w = bus (w :: [])

⊦ ∀n. Bus.ground n = bus (replicate ground n)

⊦ ∀n. Bus.power n = bus (replicate power n)

⊦ ∀m. suc m = m + 1

⊦ ∀m. m ≤ 0 ⇔ m = 0

⊦ ∀a n. nth (replicate a) n = a

⊦ ∀x n. length (replicate x n) = n

⊦ ∀l. length l = 0 ⇔ l = []

⊦ ∀x y. x = y ⇒ y = x

⊦ ∀m n. m + n = n + m

⊦ ∀n k. Bits.bound (Bits.shiftLeft n k) k = 0

⊦ ∀f l. length (map f l) = length l

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

⊦ ∀l₁ l₂. drop (length l₁) (l₁ @ l₂) = l₂

⊦ ∀l₁ l₂. take (length l₁) (l₁ @ l₂) = l₁

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

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

⊦ ∀n k. Bits.bound (Bits.bound n k) k = Bits.bound n k

⊦ ∀x n. replicate x (suc n) = x :: replicate x n

⊦ ∀x y. Bus.append x y = bus (Bus.wires x @ Bus.wires y)

⊦ ∀n k. Bits.bound n k = n ⇔ Bits.width n ≤ k

⊦ ∀n k. Bits.shiftRight n k = 0 ⇔ Bits.width n ≤ k

⊦ ∀l₁ l₂. length (l₁ @ l₂) = length l₁ + length l₂

⊦ ∀x t. Bus.signal x t = map (λw. signal w t) (Bus.wires x)

⊦ ∀m n. m ≤ n ⇔ ∃d. n = m + d

⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r

⊦ ∀n k. Bits.bound n k + Bits.shiftLeft (Bits.shiftRight n k) k = n

⊦ ∀n l. n ≤ length l ⇒ length (take n l) = n

⊦ ∀k. Bits.toNatural (replicate ⊤ k) = 2 ↑ k - 1

⊦ ∀f x n. map f (replicate x n) = replicate (f x) n

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

⊦ ∀m n p. m + n = m + p ⇔ n = p

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀l₁ l₂ l₃. l₁ @ l₂ @ l₃ = (l₁ @ l₂) @ l₃

⊦ ∀l l₁ l₂. l @ l₁ = l @ l₂ ⇔ l₁ = l₂

⊦ ∀s₁ s₂. (∀n. nth s₁ n = nth s₂ n) ⇔ s₁ = s₂

⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

⊦ ∀l₁ l₂.
Bits.toNatural (l₁ @ l₂) =
Bits.toNatural l₁ + Bits.shiftLeft (Bits.toNatural l₂) (length l₁)

⊦ ∀f h t. map f (h :: t) = f h :: map f t

⊦ ∀n l. n ≤ length l ⇒ n + length (drop n l) = length l

⊦ ∀x m n. replicate x (m + n) = replicate x m @ replicate x n

⊦ ∀n j k.
Bits.bound (Bits.shiftLeft n k) (j + k) =
Bits.shiftLeft (Bits.bound n j) k

⊦ ∀n₁ n₂ k.
Bits.shiftRight (n₁ + Bits.shiftLeft n₂ k) k =
Bits.shiftRight n₁ k + n₂

⊦ ∀f l₁ l₂. map f (l₁ @ l₂) = map f l₁ @ map f l₂

⊦ ∀m n k.
Bits.bound (Bits.bound m k + Bits.bound n k) k = Bits.bound (m + n) k

⊦ ∀h₁ h₂ t₁ t₂. h₁ :: t₁ = h₂ :: t₂ ⇔ h₁ = h₂ ∧ t₁ = t₂

⊦ ∀l n. length l = suc n ⇔ ∃h t. l = h :: t ∧ length t = n

⊦ ∀m n l. m + n ≤ length l ⇒ drop (m + n) l = drop m (drop n l)

⊦ ∀l₁ l1' l₂ l2'. length l₁ = length l1' ∧ l₁ @ l₂ = l1' @ l2' ⇒ l₁ = l1'

⊦ ∀l₁ l1' l₂ l2'. length l₂ = length l2' ∧ l₁ @ l₂ = l1' @ l2' ⇒ l₂ = l2'

⊦ ∀m n l. m + n ≤ length l ⇒ take (m + n) l = take m l @ take n (drop m l)

⊦ ∀x k n y.
Bus.sub x k n y ⇔
k + n ≤ Bus.width x ∧ y = bus (take n (drop k (Bus.wires x)))