Logops-recursive-definitions-theory
Recursive equivalents of logical operations.
The logical operations on numbers, e.g., loghead, logapp, etc., are defined in terms of modular arithmetic. It is often useful,
however, to consider these functions as if they were recursive in terms of
logcar and logcdr. This theory provides that alternate view of
the functions. When this theory is enabled, lemmas are enabled that
rewrite all of the logical operations listed above into an equivalent recursive
form. It is then possible to do inductive proofs using these definitions.
Note, however, that you will have to explicitly select an induction scheme.
Note that this theory is disabled by default. It should only be
enabled during proofs about logical operations where their recursive
counterparts are to be used.
Subtopics
- Basic-logops-induction-schemes
- Some typical ways to induct when proving theorems about logical
operations.
- Logops-recursive-helpers
- Some additional lemmas that are included in logops-recursive-definitions-theory to help with inducting over the
definitions of logical operations.
- Unsigned-byte-p*
- Recursive definition of unsigned-byte-p.
- Signed-byte-p*
- Recursive definition of signed-byte-p.
- Logxor*
- Recursive definition of logxor.
- Logtail*
- Recursive definition of logtail.
- Lognot*
- Recursive definition of lognot.
- Logmaskp*
- Recursive definition of logmaskp.
- Logior*
- Recursive definition of logior.
- Loghead*
- Recursive definition of loghead.
- Logext*
- Recursive definition of logext.
- Logbitp*
- Recursive definition of logbitp.
- Logapp*
- Recursive definition of logapp.
- Logand*
- Recursive definition of logand.
- Integer-length*
- Recursive definition of integer-length.
- Ash*
- Recursive definition of ash.
