		Search-engine friendly clone of the ACL2 documentation.

Defbyte

Defbyte-ihs-theorems

Introduce some theorems about a defbyte instance and functions in the IHS library.

Introduction

Since unsigned-byte-p and signed-byte-p have certain formal relations with functions in IHS, similar relations can be proved for instances of defbyte.

This macro automates this process, by including the IHS basic definitions and by generating theorems. For now this macro generates just one theorem; more will be added in the future as needed.

The reason for not having defbyte itself generate these theorems is to avoid always including IHS when using defbyte. Having a separate macro leads to greater modularity.

General Form

(defbyte-ihs-theorems type)

Inputs

type

A symbol that names a fixtype previously introduced via defbyte. This specifies the defbyte instance for which the theorems are generated.

Generated Events

bytep-of-loghead-of-size

One of the following
If the defbyte instance is unsigned, a rewrite rule saying that (loghead size ...), where size is the byte size, satisfies the recognizer of the bytes.
If the defbyte instance is signed, a rewrite rule saying that (logext size ...), where size is the byte size, satisfies the recognizer of the bytes.

Subtopics

Defbyte-ihs-theorems-implementation: Implementation of defbyte-ihs-theorems.