• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
        • Ihs-theories
        • Ihs-init
        • Logops
          • Logops-lemmas
            • Logops-recursive-definitions-theory
              • Basic-logops-induction-schemes
              • Logops-recursive-helpers
              • Unsigned-byte-p*
              • Signed-byte-p*
              • Logxor*
              • Logtail*
              • Lognot*
              • Logmaskp*
              • Logior*
              • Loghead*
              • Logext*
              • Logbitp*
              • Logapp*
              • Logand*
              • Integer-length*
              • Ash*
            • Ihs/logbitp-lemmas
            • Ihs/logtail-lemmas
            • Ihs/loghead-lemmas
            • Ihs/logrpl-lemmas
            • Ihs/logand-lemmas
            • Ihs/logapp-lemmas
            • Ihs/logcar-lemmas
            • Ihs/integer-length-lemmas
            • Ihs/unsigned-byte-p-lemmas
            • Ihs/logcons-lemmas
            • Signed-byte-p-logops
            • Ihs/logxor-lemmas
            • Ihs/logior-lemmas
            • Ihs/logext-lemmas
            • Ihs/logextu-lemmas
            • Ihs/signed-byte-p-lemmas
            • Ihs/lognotu-lemmas
            • Ihs/lognot-lemmas
            • Ihs/logmaskp-lemmas
            • Ihs/ash-lemmas
            • Logops-lemmas-theory
            • Ihs/wrb-lemmas
            • Ihs/logite-lemmas
      • Rtl
    • Algebra
  • Testing-utilities

• Logops-recursive-definitions-theory

Basic-logops-induction-schemes

Some typical ways to induct when proving theorems about logical operations.

Definitions and Theorems

Function: logcdr-induction-1

(defun logcdr-induction-1 (i)
  (declare (xargs :guard (integerp i)))
  (cond ((zip i) t)
        ((equal i -1) t)
        (t (logcdr-induction-1 (logcdr i)))))

Function: logcdr-induction-2

(defun logcdr-induction-2 (i j)
  (declare (xargs :guard (and (integerp i) (integerp j))))
  (cond ((zip i) t)
        ((zip j) t)
        ((equal i -1) t)
        ((equal j -1) t)
        (t (logcdr-induction-2 (logcdr i)
                               (logcdr j)))))

Function: logcdr-induction-3

(defun logcdr-induction-3 (i j k)
  (declare (xargs :guard (and (integerp i)
                              (integerp j)
                              (integerp k))))
  (cond ((zip i) t)
        ((equal i -1) t)
        (t (logcdr-induction-3 (logcdr i)
                               (logcdr j)
                               (logcdr k)))))

Function: sub1-logcdr-induction-1

(defun sub1-logcdr-induction-1 (size i)
 "The elaborate base case is for the benefit of UNSIGNED-BYTE-P, which has no guards."
 (cond ((or (not (integerp size))
            (< size 0)
            (not (integerp i)))
        t)
       ((equal size 0) t)
       (t (sub1-logcdr-induction-1 (1- size)
                                   (logcdr i)))))

Function: sub1-logcdr-induction-2

(defun sub1-logcdr-induction-2 (size i j)
 "The elaborate base case is for the benefit of UNSIGNED-BYTE-P, which has no guards."
 (cond ((or (not (integerp size))
            (< size 0)
            (not (integerp i))
            (not (integerp j)))
        t)
       ((equal size 0) t)
       (t (sub1-logcdr-induction-2 (1- size)
                                   (logcdr i)
                                   (logcdr j)))))

Function: sub1-logcdr-induction-2-w/carry

(defun sub1-logcdr-induction-2-w/carry (size i j c)
 "The elaborate base case is for the benefit of SIGNED-BYTE-P, which has no guards."
 (cond ((or (not (integerp size))
            (<= size 0)
            (not (integerp i))
            (not (integerp j))
            (not (bitp c)))
        t)
       ((equal size 1) t)
       (t (sub1-logcdr-induction-2-w/carry (1- size)
                                           (logcdr i)
                                           (logcdr j)
                                           (b-and c (logcar i))))))

Function: sub1-logcdr-induction-3

(defun sub1-logcdr-induction-3 (size i j k)
 "The elaborate base case is for the benefit of SIGNED-BYTE-P, which has no guards."
 (cond ((or (not (integerp size))
            (<= size 0)
            (not (integerp i))
            (not (integerp j))
            (not (integerp k)))
        t)
       ((equal size 1) t)
       (t (sub1-logcdr-induction-3 (1- size)
                                   (logcdr i)
                                   (logcdr j)
                                   (logcdr k)))))