Package word16-bytes-def: word16-bytes-def

Information

name	word16-bytes-def
version	1.1
description	word16-bytes-def
author	Joe Hurd <joe@gilith.com>
license	MIT
provenance	HOL Light theory extracted on 2011-03-17
show	Data.Bool

Files

Package tarball word16-bytes-def-1.1.tgz
Theory file word16-bytes-def.thy (included in the package tarball)

Defined Constants

Data
- Word16
  - Data.Word16.fromBytes
  - Data.Word16.toBytes

Theorems

⊦ ∀b1 b2.
    Data.Word16.fromBytes b1 b2 =
    Data.Word16.or
      (Data.Word16.shiftLeft
         (Data.Word16.fromNatural (Data.Byte.toNatural b1))
         (Number.Numeral.bit0
            (Number.Numeral.bit0
               (Number.Numeral.bit0
                  (Number.Numeral.bit1 Number.Numeral.zero)))))
      (Data.Word16.fromNatural (Data.Byte.toNatural b2))

⊦ ∀w.
    Data.Word16.toBytes w =
    Data.Pair.,
      (Data.Byte.fromNatural
         (Data.Word16.toNatural
            (Data.Word16.shiftRight w
               (Number.Numeral.bit0
                  (Number.Numeral.bit0
                     (Number.Numeral.bit0
                        (Number.Numeral.bit1 Number.Numeral.zero)))))))
      (Data.Byte.fromNatural
         (Data.Word16.toNatural
            (Data.Word16.and w
               (Data.Word16.fromNatural
                  (Number.Numeral.bit1
                     (Number.Numeral.bit1
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          Number.Numeral.zero))))))))))))

Input Type Operators

→
bool
Data
- Byte
  - Data.Byte.byte
- Pair
  - Data.Pair.*
- Word16
  - Data.Word16.word16
Number
- Natural
  - Number.Natural.natural

Input Constants

=
Data
- Bool
  - ∀
  - T
- Byte
  - Data.Byte.fromNatural
  - Data.Byte.toNatural
- Pair
  - Data.Pair.,
- Word16
  - Data.Word16.and
  - Data.Word16.fromNatural
  - Data.Word16.or
  - Data.Word16.shiftLeft
  - Data.Word16.shiftRight
  - Data.Word16.toNatural
Number
- Numeral
  - Number.Numeral.bit0
  - Number.Numeral.bit1
  - Number.Numeral.zero

Assumptions

⊦ T

⊦ (∀) = λP. P = λx. T