Package hardware-wire-def: Definition of hardware wire devices
Information
| name | hardware-wire-def |
| version | 1.8 |
| description | Definition of hardware wire devices |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| provenance | HOL Light theory extracted on 2014-04-14 |
| requires | bool hardware-thm |
| show | Data.Bool Hardware Number.Natural |
Files
- Package tarball hardware-wire-def-1.8.tgz
- Theory source file hardware-wire-def.thy (included in the package tarball)
Defined Constants
- Hardware
- and2
- and3
- case1
- connect
- delay
- majority3
- nor2
- not
- or2
- or3
- pulse
- sticky
- xor2
- xor3
Theorems
⊦ ∀x y. connect x y ⇔ ∀t. signal y t ⇔ signal x t
⊦ ∀x y. not x y ⇔ ∀t. signal y t ⇔ ¬signal x t
⊦ ∀x y. delay x y ⇔ ∀t. signal y (t + 1) ⇔ signal x t
⊦ ∀x y z. nor2 x y z ⇔ ∃zn. or2 x y zn ∧ not zn z
⊦ ∀x y z. and2 x y z ⇔ ∀t. signal z t ⇔ signal x t ∧ signal y t
⊦ ∀x y z. or2 x y z ⇔ ∀t. signal z t ⇔ signal x t ∨ signal y t
⊦ ∀x y. pulse x y ⇔ ∃xd xn. delay x xd ∧ not xd xn ∧ and2 x xn y
⊦ ∀w x y z. and3 w x y z ⇔ ∃wx. and2 w x wx ∧ and2 wx y z
⊦ ∀w x y z. or3 w x y z ⇔ ∃wx. or2 w x wx ∧ or2 wx y z
⊦ ∀w x y z. xor3 w x y z ⇔ ∃wx. xor2 w x wx ∧ xor2 wx y z
⊦ ∀x y z. xor2 x y z ⇔ ∀t. signal z t ⇔ ¬(signal x t ⇔ signal y t)
⊦ ∀s x y z.
case1 s x y z ⇔
∀t. signal z t ⇔ if signal s t then signal x t else signal y t
⊦ ∀ld w x.
sticky ld w x ⇔
∃p q r. case1 ld ground p q ∧ or2 w q r ∧ delay r p ∧ connect r x
⊦ ∀w x y z.
majority3 w x y z ⇔
∃wx wy xy. and2 w x wx ∧ and2 w y wy ∧ and2 x y xy ∧ or3 wx wy xy z
External Type Operators
- →
- bool
- Hardware
- wire
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ∃
- ∨
- ¬
- cond
- ⊤
- Bool
- Hardware
- ground
- signal
- Number
- Natural
- +
- bit1
- zero
- Natural
Assumptions
⊦ ⊤
⊦ (∀) = λp. p = λx. ⊤