Package hardware-def: Definition of the hardware model
Information
| name | hardware-def |
| version | 1.21 |
| description | Definition of the hardware model |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-11-01 |
| checksum | 57a720b860eec336c8df6a5b95175283225194bc |
| requires | base stream |
| show | Data.Bool Data.List Data.Stream Hardware Number.Natural |
Files
- Package tarball hardware-def-1.21.tgz
- Theory source file hardware-def.thy (included in the package tarball)
Defined Type Operators
- Hardware
- bus
- wire
Defined Constants
- 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
Theorems
⊦ Bus.nil = bus []
⊦ ground = wire (replicate ⊥)
⊦ power = wire (replicate ⊤)
⊦ ∀x. bus (Bus.wires x) = x
⊦ ∀w. wire (signals w) = w
⊦ ∀l. Bus.wires (bus l) = l
⊦ ∀s. signals (wire s) = s
⊦ ∀x. Bus.width x = length (Bus.wires x)
⊦ ∀w. signal w = nth (signals w)
⊦ ∀w. Bus.single w = bus (w :: [])
⊦ ∀n. Bus.ground n = bus (replicate ground n)
⊦ ∀n. Bus.power n = bus (replicate power n)
⊦ ∀x y. Bus.append x y = bus (Bus.wires x @ Bus.wires y)
⊦ ∀x t. Bus.signal x t = map (λw. signal w t) (Bus.wires x)
⊦ ∀x k n y.
Bus.sub x k n y ⇔
k + n ≤ Bus.width x ∧ y = bus (take n (drop k (Bus.wires x)))
External Type Operators
- →
- bool
- Data
- List
- list
- Stream
- stream
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ⊥
- ⊤
- List
- ::
- @
- []
- drop
- length
- map
- replicate
- take
- Stream
- nth
- replicate
- Bool
- Number
- Natural
- +
- ≤
- Natural
Assumptions
⊦ ⊤
⊦ (∃) = λp. p ((select) p)
⊦ ∀t. (∃x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤