Package hardware-wire: Hardware wire devices
Information
| name | hardware-wire |
| version | 1.23 |
| description | Hardware wire devices |
| author | Joe Leslie-Hurd <joe@gilith.com> |
| license | MIT |
| checksum | cefd0f48eee39a598bed0d3ae5a66e7c31efbb56 |
| requires | base hardware-thm stream |
| show | Data.Bool Data.Stream Hardware Number.Natural |
Files
- Package tarball hardware-wire-1.23.tgz
- Theory source file hardware-wire.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. connect x x
⊦ ∀x. ∃y. connect x y
⊦ ∀x. ∃y. delay x y
⊦ ∀x. ∃y. not x y
⊦ ∀x. ∃y. pulse x y
⊦ ∀x y. ∃z. and2 x y z
⊦ ∀x y. ∃z. nor2 x y z
⊦ ∀x y. ∃z. or2 x y z
⊦ ∀x y. ∃z. xor2 x y z
⊦ ∀x. connect ground x ⇒ delay ground x
⊦ ∀x. connect ground x ⇒ not power x
⊦ ∀x. connect power x ⇒ delay power x
⊦ ∀x. connect power x ⇒ not ground x
⊦ ∀w x y. ∃z. and3 w x y z
⊦ ∀s x y. ∃z. case1 s x y z
⊦ ∀w x y. ∃z. majority3 w x y z
⊦ ∀w x y. ∃z. or3 w x y z
⊦ ∀w x y. ∃z. xor3 w x y z
⊦ ∀x y. connect ground y ⇒ and2 ground x y
⊦ ∀x y. connect ground y ⇒ and2 x ground y
⊦ ∀x y. connect ground y ⇒ xor2 x x y
⊦ ∀x y. connect power y ⇒ or2 power x y
⊦ ∀x y. connect power y ⇒ or2 x power y
⊦ ∀x y. connect x y ⇒ and2 power x y
⊦ ∀x y. connect x y ⇒ and2 x power y
⊦ ∀x y. connect x y ⇒ and2 x x y
⊦ ∀x y. connect x y ⇒ or2 ground x y
⊦ ∀x y. connect x y ⇒ or2 x ground y
⊦ ∀x y. connect x y ⇒ or2 x x y
⊦ ∀x y. connect x y ⇒ xor2 ground x y
⊦ ∀x y. connect x y ⇒ xor2 x ground y
⊦ ∀x y. not x y ⇒ xor2 power x y
⊦ ∀x y. not x y ⇒ xor2 x power y
⊦ ∀x y. connect x y ⇒ case1 x power ground y
⊦ ∀x y. not x y ⇒ case1 x ground power y
⊦ ∀x y z. connect x z ⇒ case1 power x y z
⊦ ∀x y z. connect y z ⇒ case1 ground x y z
⊦ ∀x y z. connect y z ⇒ case1 x y y z
⊦ ∀x y z. and2 x y z ⇒ case1 x y ground z
⊦ ∀x y z. and2 x y z ⇒ majority3 x y ground z
⊦ ∀x y z. or2 x y z ⇒ case1 x power y z
⊦ ∀x y z. or2 x y z ⇒ or3 x y ground z
⊦ ∀x y z. xor2 x y z ⇒ xor3 x y ground z
⊦ ∀x y t. connect x y ⇒ (signal y t ⇔ signal x t)
⊦ ∀x y. connect x y ⇔ ∀t. signal y t ⇔ signal x t
⊦ ∀x y t. not x y ⇒ (signal y t ⇔ ¬signal x t)
⊦ ∀x y. not x y ⇔ ∀t. signal y t ⇔ ¬signal x t
⊦ ∀x y t. pulse x y ∧ ¬signal x t ⇒ ¬signal y t
⊦ ∀x y t. delay x y ⇒ (signal y (t + 1) ⇔ 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 xn. not x xn ∧ and2 xn y z ⇒ case1 x ground y z
⊦ ∀x y z xn. not x xn ∧ or2 xn y z ⇒ case1 x y power z
⊦ ∀x y z t. and2 x y z ⇒ (signal z t ⇔ signal x t ∧ signal y t)
⊦ ∀x y z t. or2 x y z ⇒ (signal z t ⇔ signal x t ∨ signal y t)
⊦ ∀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 t. xor2 x y z ⇒ (signal z t ⇔ ¬(signal x t ⇔ signal y t))
⊦ ∀x y z. xor2 x y z ⇔ ∀t. signal z t ⇔ ¬(signal x t ⇔ signal y t)
⊦ ∀x y z t. nor2 x y z ⇒ (signal z t ⇔ ¬signal x t ∧ ¬signal y t)
⊦ ∀x y t. pulse x y ⇒ (signal y (t + 1) ⇔ ¬signal x t ∧ signal x (t + 1))
⊦ ∀s x y z t.
case1 s x y z ⇒
(signal z t ⇔ if signal s t then signal x t else 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
⊦ ∀w x y z t.
and3 w x y z ⇒ (signal z t ⇔ signal w t ∧ signal x t ∧ signal y t)
⊦ ∀w x y z t.
or3 w x y z ⇒ (signal z t ⇔ signal w t ∨ signal x t ∨ signal y t)
⊦ ∀w x y z t.
xor3 w x y z ⇒ (signal z t ⇔ signal w t ⇔ signal x t ⇔ 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
⊦ ∀w x y z t.
majority3 w x y z ⇒
(signal z t ⇔
signal w t ∧ signal x t ∨ signal w t ∧ signal y t ∨
signal x t ∧ signal y t)
⊦ ∀ld w x t k.
(∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧ sticky ld w x ⇒
(signal x (t + k) ⇔ ∃i. i ≤ k ∧ signal w (t + i))
External Type Operators
- →
- bool
- Data
- Stream
- stream
- Stream
- Hardware
- wire
- Number
- Natural
- natural
- Natural
External Constants
- =
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- Stream
- fromFunction
- nth
- Bool
- Hardware
- ground
- power
- signal
- wire
- Number
- Natural
- +
- -
- ≤
- bit0
- bit1
- suc
- zero
- Natural
Assumptions
⊦ ⊤
⊦ ¬⊥ ⇔ ⊤
⊦ ¬⊤ ⇔ ⊥
⊦ bit0 0 = 0
⊦ ∀t. t ⇒ t
⊦ ∀t. signal power t
⊦ ∀n. n ≤ n
⊦ ⊥ ⇔ ∀p. p
⊦ ∀t. t ∨ ¬t
⊦ ∀t. ¬signal ground t
⊦ ∀n. n ≤ suc n
⊦ (¬) = λp. p ⇒ ⊥
⊦ ∀t. (∀x. t) ⇔ t
⊦ (∀) = λp. p = λx. ⊤
⊦ ∀t. ¬¬t ⇔ t
⊦ ∀t. (⊤ ⇔ t) ⇔ t
⊦ ∀t. (t ⇔ ⊤) ⇔ t
⊦ ∀t. ⊥ ∧ t ⇔ ⊥
⊦ ∀t. ⊤ ∧ t ⇔ t
⊦ ∀t. t ∧ ⊥ ⇔ ⊥
⊦ ∀t. t ∧ ⊤ ⇔ t
⊦ ∀t. t ∧ t ⇔ t
⊦ ∀t. ⊥ ⇒ t ⇔ ⊤
⊦ ∀t. ⊤ ⇒ t ⇔ t
⊦ ∀t. t ⇒ ⊤ ⇔ ⊤
⊦ ∀t. ⊥ ∨ t ⇔ t
⊦ ∀t. ⊤ ∨ t ⇔ ⊤
⊦ ∀t. t ∨ ⊥ ⇔ t
⊦ ∀t. t ∨ ⊤ ⇔ ⊤
⊦ ∀t. t ∨ t ⇔ t
⊦ ∀n. ¬(suc n = 0)
⊦ ∀m. m + 0 = m
⊦ ∀f. nth (fromFunction f) = f
⊦ ∀t. (⊥ ⇔ t) ⇔ ¬t
⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t
⊦ ∀n. bit1 n = suc (bit0 n)
⊦ (⇒) = λp q. p ∧ q ⇔ p
⊦ ∀t. (t ⇔ ⊤) ∨ (t ⇔ ⊥)
⊦ ∀m. suc m = m + 1
⊦ ∀m. m ≤ 0 ⇔ m = 0
⊦ ∀t1 t2. (if ⊥ then t1 else t2) = t2
⊦ ∀t1 t2. (if ⊤ then t1 else t2) = t1
⊦ ∀b t. (if b then t else t) = t
⊦ ∀m n. m + n - n = m
⊦ ∀s t. signal (wire s) t ⇔ nth s t
⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤
⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q
⊦ ∀m n. m + suc n = suc (m + n)
⊦ ∀t1 t2. ¬(t1 ∨ t2) ⇔ ¬t1 ∧ ¬t2
⊦ ∀p a. (∃x. x = a ∧ p x) ⇔ p a
⊦ (∨) = λp q. ∀r. (p ⇒ r) ⇒ (q ⇒ r) ⇒ r
⊦ ∀t1 t2 t3. (t1 ∧ t2) ∧ t3 ⇔ t1 ∧ t2 ∧ t3
⊦ ∀t1 t2 t3. (t1 ∨ t2) ∨ t3 ⇔ t1 ∨ t2 ∨ t3
⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p
⊦ ∀m n. m ≤ suc n ⇔ m = suc n ∨ m ≤ n
⊦ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0
⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n
⊦ ∀p q r. (p ∨ q) ∧ r ⇔ p ∧ r ∨ q ∧ r
⊦ ∀p q. (∃x. p x ∨ q x) ⇔ (∃x. p x) ∨ ∃x. q x
⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)