• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Real
    • ACL2-tutorial
    • Debugging
    • Miscellaneous
    • Prover-output
    • Built-in-theorems
      • Built-in-theorems-about-arithmetic
      • Built-in-theorems-about-symbols
      • Built-in-theorems-about-characters
      • Built-in-theorems-about-lists
      • Built-in-theorems-about-arrays
      • Built-in-theorems-about-strings
      • Built-in-theorems-about-alists
      • Built-in-theorems-about-total-order
      • Built-in-theorems-about-system-utilities
      • Built-in-theorems-about-cons-pairs
      • Built-in-theorems-for-tau
      • Built-in-theorems-about-bad-atoms
      • Built-in-theorems-about-logical-connectives
      • Built-in-theorems-about-booleans
      • Built-in-theorems-about-random$
      • Built-in-theorems-about-eqlables
    • Macros
    • Interfacing-tools
    • About-ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Built-in-theorems

Built-in-theorems-for-tau

Built-in theorems specifically for the tau system.

Theorem: basic-tau-rules

(defthm basic-tau-rules
        (and (implies (natp v) (not (minusp v)))
             (implies (natp v) (integerp v))
             (implies (posp v) (natp v))
             (implies (minusp v) (acl2-numberp v))
             (implies (integerp v) (rationalp v))
             (implies (rationalp v)
                      (not (complex-rationalp v)))
             (implies (rationalp v)
                      (not (characterp v)))
             (implies (rationalp v)
                      (not (stringp v)))
             (implies (rationalp v) (not (consp v)))
             (implies (rationalp v)
                      (not (symbolp v)))
             (implies (complex-rationalp v)
                      (not (characterp v)))
             (implies (complex-rationalp v)
                      (not (stringp v)))
             (implies (complex-rationalp v)
                      (not (consp v)))
             (implies (complex-rationalp v)
                      (not (symbolp v)))
             (implies (characterp v)
                      (not (stringp v)))
             (implies (characterp v) (not (consp v)))
             (implies (characterp v)
                      (not (symbolp v)))
             (implies (stringp v) (not (consp v)))
             (implies (stringp v) (not (symbolp v)))
             (implies (consp v) (not (symbolp v)))
             (implies (booleanp v) (symbolp v))
             (booleanp (equal x y))
             (booleanp (< x y)))
        :rule-classes :tau-system)

Theorem: bitp-as-inequality

(defthm bitp-as-inequality
        (implies (bitp x)
                 (and (natp x) (< x 2)))
        :rule-classes :tau-system)