Package hardware-bus-def: Definition of hardware bus devices

Information

namehardware-bus-def
version1.25
descriptionDefinition of hardware bus devices
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2014-10-30
checksumd4921f168ad7d633de4d5e08f48adf7f0232fc1a
requiresbool
hardware-thm
hardware-wire
natural
showData.Bool
Hardware
Number.Natural

Files

Defined Constants

Theorems

⊦ Bus.connect = Bus.lift2 connect

⊦ Bus.delay = Bus.lift2 delay

⊦ Bus.not = Bus.lift2 not

⊦ Bus.and2 = Bus.lift3 and2

⊦ Bus.or2 = Bus.lift3 or2

⊦ Bus.xor2 = Bus.lift3 xor2

⊦ ∀s. Bus.case1 s = Bus.lift3 (case1 s)

⊦ ∀x i w. Bus.wire x i w ⇔ Bus.sub x i 1 (Bus.single w)

⊦ ∀w x y z. Bus.and3 w x y z ⇔ ∃wx. Bus.and2 w x wx ∧ Bus.and2 wx y z

⊦ ∀w x y z. Bus.or3 w x y z ⇔ ∃wx. Bus.or2 w x wx ∧ Bus.or2 wx y z

⊦ ∀w x y z. Bus.xor3 w x y z ⇔ ∃wx. Bus.xor2 w x wx ∧ Bus.xor2 wx y z

⊦ ∀w x y z.
    Bus.majority3 w x y z ⇔
    ∃wx wy xy.
      Bus.and2 w x wx ∧ Bus.and2 w y wy ∧ Bus.and2 x y xy ∧
      Bus.or3 wx wy xy z

⊦ ∀r x y.
    Bus.lift2 r x y ⇔
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧
      ∀i xi yi. Bus.wire x i xi ∧ Bus.wire y i yi ⇒ r xi yi

⊦ ∀x y.
    Bus.reverse x y ⇔
    Bus.width x = Bus.width y ∧
    ∀i j xi yj.
      i + (j + 1) = Bus.width x ∧ Bus.wire x i xi ∧ Bus.wire y j yj ⇒
      xi = yj

⊦ ∀r x y z.
    Bus.lift3 r x y z ⇔
    ∃n.
      Bus.width x = n ∧ Bus.width y = n ∧ Bus.width z = n ∧
      ∀i xi yi zi.
        Bus.wire x i xi ∧ Bus.wire y i yi ∧ Bus.wire z i zi ⇒ r xi yi zi

External Type Operators

External Constants

Assumptions

⊦ ⊤

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