• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
        • Builtin-defaxioms/defthms
          • Builtin-defthms
          • Builtin-defaxioms
          • Builtin-defaxioms/defthms-by-rule-classes
          • Builtin-defaxioms/defthms-by-types/functions
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Builtin-defaxioms/defthms

Builtin-defaxioms

All built-in axioms.

Definition: bad-atom<=-total

(defaxiom bad-atom<=-total
  (implies (and (bad-atom x) (bad-atom y))
           (or (bad-atom<= x y) (bad-atom<= y x)))
  :rule-classes nil)

Definition: bad-atom<=-transitive

(defaxiom bad-atom<=-transitive
  (implies (and (bad-atom<= x y)
                (bad-atom<= y z)
                (bad-atom x)
                (bad-atom y)
                (bad-atom z))
           (bad-atom<= x z))
  :rule-classes ((:rewrite :match-free :all)))

Definition: bad-atom<=-antisymmetric

(defaxiom bad-atom<=-antisymmetric
  (implies (and (bad-atom x)
                (bad-atom y)
                (bad-atom<= x y)
                (bad-atom<= y x))
           (equal x y))
  :rule-classes nil)

Definition: booleanp-bad-atom<=

(defaxiom booleanp-bad-atom<=
  (or (equal (bad-atom<= x y) t)
      (equal (bad-atom<= x y) nil))
  :rule-classes :type-prescription)

Definition: completion-of-realpart

(defaxiom completion-of-realpart
  (equal (realpart x)
         (if (acl2-numberp x) (realpart x) 0))
  :rule-classes nil)

Definition: completion-of-numerator

(defaxiom completion-of-numerator
  (equal (numerator x)
         (if (rationalp x) (numerator x) 0))
  :rule-classes nil)

Definition: completion-of-intern-in-package-of-symbol

(defaxiom completion-of-intern-in-package-of-symbol
  (equal (intern-in-package-of-symbol x y)
         (if (and (stringp x) (symbolp y))
             (intern-in-package-of-symbol x y)
           nil))
  :rule-classes nil)

Definition: completion-of-imagpart

(defaxiom completion-of-imagpart
  (equal (imagpart x)
         (if (acl2-numberp x) (imagpart x) 0))
  :rule-classes nil)

Definition: completion-of-denominator

(defaxiom completion-of-denominator
  (equal (denominator x)
         (if (rationalp x) (denominator x) 1))
  :rule-classes nil)

Definition: completion-of-coerce

(defaxiom completion-of-coerce
  (equal (coerce x y)
         (cond ((equal y 'list)
                (if (stringp x) (coerce x 'list) nil))
               (t (coerce (make-character-list x)
                          'string))))
  :rule-classes nil)

Definition: completion-of-complex

(defaxiom completion-of-complex
  (equal (complex x y)
         (complex (if (real/rationalp x) x 0)
                  (if (real/rationalp y) y 0)))
  :rule-classes nil)

Definition: completion-of-code-char

(defaxiom completion-of-code-char
  (equal (code-char x)
         (if (and (integerp x) (>= x 0) (< x 256))
             (code-char x)
           *null-char*))
  :rule-classes nil)

Definition: completion-of-char-code

(defaxiom completion-of-char-code
  (equal (char-code x)
         (if (characterp x) (char-code x) 0))
  :rule-classes nil)

Definition: completion-of-cdr

(defaxiom completion-of-cdr
  (equal (cdr x)
         (cond ((consp x) (cdr x)) (t nil)))
  :rule-classes nil)

Definition: completion-of-car

(defaxiom completion-of-car
  (equal (car x)
         (cond ((consp x) (car x)) (t nil)))
  :rule-classes nil)

Definition: completion-of-<

(defaxiom completion-of-<
  (equal (< x y)
         (if (and (real/rationalp x)
                  (real/rationalp y))
             (< x y)
           (let ((x1 (if (acl2-numberp x) x 0))
                 (y1 (if (acl2-numberp y) y 0)))
             (or (< (realpart x1) (realpart y1))
                 (and (equal (realpart x1) (realpart y1))
                      (< (imagpart x1) (imagpart y1)))))))
  :rule-classes nil)

Definition: completion-of-unary-/

(defaxiom completion-of-unary-/
  (equal (/ x)
         (if (and (acl2-numberp x) (not (equal x 0)))
             (/ x)
           0))
  :rule-classes nil)

Definition: completion-of-unary-minus

(defaxiom completion-of-unary-minus
  (equal (- x)
         (if (acl2-numberp x) (- x) 0))
  :rule-classes nil)

Definition: completion-of-*

(defaxiom completion-of-*
  (equal (* x y)
         (if (acl2-numberp x)
             (if (acl2-numberp y) (* x y) 0)
           0))
  :rule-classes nil)

Definition: completion-of-+

(defaxiom completion-of-+
  (equal (+ x y)
         (if (acl2-numberp x)
             (if (acl2-numberp y) (+ x y) x)
           (if (acl2-numberp y) y 0)))
  :rule-classes nil)

Definition: completion-of-symbol-package-name

(defaxiom completion-of-symbol-package-name
  (equal (symbol-package-name x)
         (if (symbolp x)
             (symbol-package-name x)
           ""))
  :rule-classes nil)

Definition: completion-of-symbol-name

(defaxiom completion-of-symbol-name
  (equal (symbol-name x)
         (if (symbolp x) (symbol-name x) ""))
  :rule-classes nil)

Definition: char-code-code-char-is-identity

(defaxiom char-code-code-char-is-identity
  (implies (and (integerp n) (<= 0 n) (< n 256))
           (equal (char-code (code-char n)) n)))

Definition: code-char-char-code-is-identity

(defaxiom code-char-char-code-is-identity
  (implies (characterp c)
           (equal (code-char (char-code c)) c)))

Definition: code-char-type

(defaxiom code-char-type
  (characterp (code-char n))
  :rule-classes :type-prescription)

Definition: char-code-linear

(defaxiom char-code-linear
  (< (char-code x) 256)
  :rule-classes :linear)

Definition: nil-is-not-circular

(defaxiom nil-is-not-circular
  (equal nil
         (intern-in-package-of-symbol
              (coerce (cons #\N (cons #\I (cons #\L 0)))
                      'string)
              'string))
  :rule-classes nil)

Definition: string-is-not-circular

(defaxiom string-is-not-circular
 (equal
  'string
  (intern-in-package-of-symbol
    (coerce (cons #\S
                  (cons #\T
                        (cons #\R
                              (cons #\I (cons #\N (cons #\G 0))))))
            (cons #\S
                  (cons #\T
                        (cons #\R
                              (cons #\I (cons #\N (cons #\G 0)))))))
    (intern-in-package-of-symbol 0 0)))
 :rule-classes nil)

Definition: keyword-package

(defaxiom keyword-package
  (equal (pkg-imports "KEYWORD") nil))

Definition: acl2-package

(defaxiom acl2-package
  (equal (pkg-imports "ACL2")
         *common-lisp-symbols-from-main-lisp-package*))

Definition: acl2-output-channel-package

(defaxiom acl2-output-channel-package
  (equal (pkg-imports "ACL2-OUTPUT-CHANNEL")
         nil))

Definition: acl2-input-channel-package

(defaxiom acl2-input-channel-package
  (equal (pkg-imports "ACL2-INPUT-CHANNEL")
         nil))

Definition: completion-of-pkg-imports

(defaxiom completion-of-pkg-imports
  (equal (pkg-imports x)
         (if (stringp x) (pkg-imports x) nil))
  :rule-classes nil)

Definition: no-duplicatesp-eq-pkg-imports

(defaxiom no-duplicatesp-eq-pkg-imports
  (no-duplicatesp-eq (pkg-imports pkg))
  :rule-classes :rewrite)

Definition: symbol-listp-pkg-imports

(defaxiom symbol-listp-pkg-imports
  (symbol-listp (pkg-imports pkg))
  :rule-classes
  ((:forward-chaining :trigger-terms ((pkg-imports pkg)))))

Definition: intern-in-package-of-symbol-is-identity

(defaxiom intern-in-package-of-symbol-is-identity
 (implies
  (and (stringp x)
       (symbolp y)
       (member-symbol-name x
                           (pkg-imports (symbol-package-name y))))
  (equal
   (intern-in-package-of-symbol x y)
   (car
      (member-symbol-name x
                          (pkg-imports (symbol-package-name y)))))))

Definition: symbol-package-name-intern-in-package-of-symbol

(defaxiom symbol-package-name-intern-in-package-of-symbol
 (implies
  (and
   (stringp x)
   (symbolp y)
   (not (member-symbol-name x
                            (pkg-imports (symbol-package-name y)))))
  (equal (symbol-package-name (intern-in-package-of-symbol x y))
         (symbol-package-name y))))

Definition: symbol-name-intern-in-package-of-symbol

(defaxiom symbol-name-intern-in-package-of-symbol
 (implies
     (and (stringp s) (symbolp any-symbol))
     (equal (symbol-name (intern-in-package-of-symbol s any-symbol))
            s)))

Definition: symbol-package-name-pkg-witness-name

(defaxiom symbol-package-name-pkg-witness-name
  (equal (symbol-package-name (pkg-witness pkg-name))
         (if (and (stringp pkg-name)
                  (not (equal pkg-name "")))
             pkg-name
           "ACL2")))

Definition: symbol-name-pkg-witness

(defaxiom symbol-name-pkg-witness
  (equal (symbol-name (pkg-witness pkg-name))
         *pkg-witness-name*))

Definition: intern-in-package-of-symbol-symbol-name

(defaxiom intern-in-package-of-symbol-symbol-name
  (implies (and (symbolp x)
                (equal (symbol-package-name x)
                       (symbol-package-name y)))
           (equal (intern-in-package-of-symbol (symbol-name x)
                                               y)
                  x)))

Definition: symbolp-pkg-witness

(defaxiom symbolp-pkg-witness
  (symbolp (pkg-witness x))
  :rule-classes :type-prescription)

Definition: symbolp-intern-in-package-of-symbol

(defaxiom symbolp-intern-in-package-of-symbol
  (symbolp (intern-in-package-of-symbol x y))
  :rule-classes :type-prescription)

Definition: stringp-symbol-package-name

(defaxiom stringp-symbol-package-name
  (stringp (symbol-package-name x))
  :rule-classes :type-prescription)

Definition: character-listp-coerce

(defaxiom character-listp-coerce
 (character-listp (coerce str 'list))
 :rule-classes
 (:rewrite (:forward-chaining :trigger-terms ((coerce str 'list)))))

Definition: coerce-inverse-2

(defaxiom coerce-inverse-2
  (implies (stringp x)
           (equal (coerce (coerce x 'list) 'string)
                  x)))

Definition: coerce-inverse-1

(defaxiom coerce-inverse-1
  (implies (character-listp x)
           (equal (coerce (coerce x 'string) 'list)
                  x)))

Definition: characterp-return

(defaxiom characterp-return
  (characterp #\Return)
  :rule-classes nil)

Definition: characterp-rubout

(defaxiom characterp-rubout
  (characterp #\Rubout)
  :rule-classes nil)

Definition: characterp-tab

(defaxiom characterp-tab
  (characterp #\Tab)
  :rule-classes nil)

Definition: characterp-page

(defaxiom characterp-page
  (characterp #\Page)
  :rule-classes nil)

Definition: booleanp-characterp

(defaxiom booleanp-characterp
  (booleanp (characterp x))
  :rule-classes nil)

Definition: lowest-terms

(defaxiom lowest-terms
  (implies (and (integerp n)
                (rationalp x)
                (integerp r)
                (integerp q)
                (< 0 n)
                (equal (numerator x) (* n r))
                (equal (denominator x) (* n q)))
           (equal n 1))
  :rule-classes nil)

Definition: integer-step

(defaxiom integer-step
  (implies (integerp x)
           (and (integerp (+ x 1))
                (integerp (+ x -1))))
  :rule-classes nil)

Definition: integer-1

(defaxiom integer-1
  (integerp 1)
  :rule-classes nil)

Definition: integer-0

(defaxiom integer-0
  (integerp 0)
  :rule-classes nil)

Definition: imagpart-complex

(defaxiom imagpart-complex
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (imagpart (complex x y)) y)))

Definition: realpart-complex

(defaxiom realpart-complex
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (realpart (complex x y)) x)))

Definition: realpart-imagpart-elim

(defaxiom realpart-imagpart-elim
  (implies (acl2-numberp x)
           (equal (complex (realpart x) (imagpart x))
                  x))
  :rule-classes (:rewrite :elim))

Definition: nonzero-imagpart

(defaxiom nonzero-imagpart
  (implies (complex/complex-rationalp x)
           (not (equal 0 (imagpart x))))
  :rule-classes nil)

Definition: complex-definition

(defaxiom complex-definition
  (implies (and (real/rationalp x)
                (real/rationalp y))
           (equal (complex x y) (+ x (* #C(0 1) y)))))

Definition: complex-implies1

(defaxiom complex-implies1
  (and (real/rationalp (realpart x))
       (real/rationalp (imagpart x)))
  :rule-classes nil)

Definition: integer-implies-rational

(defaxiom integer-implies-rational
  (implies (integerp x) (rationalp x))
  :rule-classes nil)

Definition: rational-implies2

(defaxiom rational-implies2
  (implies (rationalp x)
           (equal (* (/ (denominator x)) (numerator x))
                  x)))

Definition: rational-implies1

(defaxiom rational-implies1
  (implies (rationalp x)
           (and (integerp (denominator x))
                (integerp (numerator x))
                (< 0 (denominator x))))
  :rule-classes nil)

Definition: positive

(defaxiom positive
  (and (implies (and (< 0 x) (< 0 y))
                (< 0 (+ x y)))
       (implies (and (real/rationalp x)
                     (real/rationalp y)
                     (< 0 x)
                     (< 0 y))
                (< 0 (* x y))))
  :rule-classes nil)

Definition: trichotomy

(defaxiom trichotomy
  (and (implies (acl2-numberp x)
                (or (< 0 x) (equal x 0) (< 0 (- x))))
       (or (not (< 0 x)) (not (< 0 (- x)))))
  :rule-classes nil)

Definition: zero

(defaxiom zero
  (not (< 0 0))
  :rule-classes nil)

Definition: <-on-others

(defaxiom <-on-others
  (equal (< x y) (< (+ x (- y)) 0))
  :rule-classes nil)

Definition: distributivity

(defaxiom distributivity
  (equal (* x (+ y z))
         (+ (* x y) (* x z))))

Definition: inverse-of-*

(defaxiom inverse-of-*
  (implies (and (acl2-numberp x) (not (equal x 0)))
           (equal (* x (/ x)) 1)))

Definition: unicity-of-1

(defaxiom unicity-of-1
  (equal (* 1 x) (fix x)))

Definition: commutativity-of-*

(defaxiom commutativity-of-*
  (equal (* x y) (* y x)))

Definition: associativity-of-*

(defaxiom associativity-of-*
  (equal (* (* x y) z) (* x (* y z))))

Definition: inverse-of-+

(defaxiom inverse-of-+
  (equal (+ x (- x)) 0))

Definition: unicity-of-0

(defaxiom unicity-of-0
  (equal (+ 0 x) (fix x)))

Definition: commutativity-of-+

(defaxiom commutativity-of-+
  (equal (+ x y) (+ y x)))

Definition: associativity-of-+

(defaxiom associativity-of-+
  (equal (+ (+ x y) z) (+ x (+ y z))))

Definition: closure

(defaxiom closure
  (and (acl2-numberp (+ x y))
       (acl2-numberp (* x y))
       (acl2-numberp (- x))
       (acl2-numberp (/ x)))
  :rule-classes nil)

Definition: nonnegative-product

(defaxiom nonnegative-product
  (implies (real/rationalp x)
           (and (real/rationalp (* x x))
                (<= 0 (* x x))))
  :rule-classes ((:type-prescription :typed-term (* x x))))

Definition: cons-equal

(defaxiom cons-equal
  (equal (equal (cons x1 y1) (cons x2 y2))
         (and (equal x1 x2) (equal y1 y2))))

Definition: cdr-cons

(defaxiom cdr-cons
  (equal (cdr (cons x y)) y))

Definition: car-cons

(defaxiom car-cons
  (equal (car (cons x y)) x))

Definition: car-cdr-elim

(defaxiom car-cdr-elim
  (implies (consp x)
           (equal (cons (car x) (cdr x)) x))
  :rule-classes :elim)