• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
        • Builtin-defaxioms/defthms
          • Builtin-defthms
          • Builtin-defaxioms
          • Builtin-defaxioms/defthms-by-rule-classes
            • Builtin-defaxioms/defthms-without-rule-classes
            • Builtin-defaxioms/defthms-of-class-type-prescription
            • Builtin-defaxioms/defthms-of-class-rewrite
            • Builtin-defaxioms/defthms-of-class-forward-chaining
            • Builtin-defaxioms/defthms-of-class-definition
            • Builtin-defaxioms/defthms-of-class-congruence
            • Builtin-defaxioms/defthms-of-class-linear
            • Builtin-defaxioms/defthms-of-class-compound-recognizer
            • Builtin-defaxioms/defthms-of-class-tau-system
            • Builtin-defaxioms/defthms-of-class-equivalence
            • Builtin-defaxioms/defthms-of-class-elim
            • Builtin-defaxioms/defthms-of-class-well-founded-relation
            • Builtin-defaxioms/defthms-of-class-type-set-inverter
            • Builtin-defaxioms/defthms-of-class-rewrite-quoted-constant
            • Builtin-defaxioms/defthms-of-class-refinement
            • Builtin-defaxioms/defthms-of-class-generalize
            • Builtin-defaxioms/defthms-of-class-clause-processor
            • Builtin-defaxioms/defthms-of-class-built-in-clause
            • Builtin-defaxioms/defthms-of-class-meta
            • Builtin-defaxioms/defthms-of-class-induction
          • Builtin-defaxioms/defthms-by-types/functions
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Builtin-defaxioms/defthms-by-rule-classes

Builtin-defaxioms/defthms-without-rule-classes

Built-in axioms and theorems without rule classes.

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<=-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: 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: 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: completion-of-pkg-imports

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

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: nonzero-imagpart

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

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-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: closure

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

Theorem: apply$-userfn-takes-arity-args

(defthm apply$-userfn-takes-arity-args
 (implies
  (badge-userfn fn)
  (equal (apply$-userfn fn args)
         (apply$-userfn fn
                        (take (apply$-badge-arity (badge-userfn fn))
                              args))))
 :rule-classes nil)

Theorem: add-def-complex

(defthm add-def-complex
  (equal (+ x y)
         (complex (+ (realpart x) (realpart y))
                  (+ (imagpart x) (imagpart y))))
  :rule-classes nil)

Theorem: symbol-equality

(defthm symbol-equality
  (implies (and (or (symbolp s1) (symbolp s2))
                (equal (symbol-name s1)
                       (symbol-name s2))
                (equal (symbol-package-name s1)
                       (symbol-package-name s2)))
           (equal s1 s2))
  :rule-classes nil)

Theorem: all-boundp-preserves-assoc-equal

(defthm all-boundp-preserves-assoc-equal
  (implies (and (all-boundp tbl1 tbl2)
                (assoc-equal x tbl1))
           (assoc-equal x tbl2))
  :rule-classes nil)

Theorem: equal-char-code

(defthm equal-char-code
  (implies (and (characterp x) (characterp y))
           (implies (equal (char-code x) (char-code y))
                    (equal x y)))
  :rule-classes nil)

Theorem: doppelganger-apply$-userfn-takes-arity-args

(defthm doppelganger-apply$-userfn-takes-arity-args
  (implies (doppelganger-badge-userfn fn)
           (equal (doppelganger-apply$-userfn fn args)
                  (doppelganger-apply$-userfn
                       fn
                       (take (caddr (doppelganger-badge-userfn fn))
                             args))))
  :rule-classes nil)

Theorem: doppelganger-badge-userfn-type

(defthm doppelganger-badge-userfn-type
  (or (null (doppelganger-badge-userfn fn))
      (let ((x (doppelganger-badge-userfn fn)))
        (and (weak-apply$-badge-p x)
             (natp (access apply$-badge x :arity))
             (natp (access apply$-badge x :out-arity))
             (or (eq (access apply$-badge x :ilks) t)
                 (and (true-listp (access apply$-badge x :ilks))
                      (equal (len (access apply$-badge x :ilks))
                             (access apply$-badge x :arity))
                      (not (all-nils (access apply$-badge x :ilks)))
                      (subsetp (access apply$-badge x :ilks)
                               '(nil :fn :expr)))))))
  :rule-classes nil)

Theorem: function-symbolp-ev-fncall+-fns-strictp

(defthm function-symbolp-ev-fncall+-fns-strictp
  (let ((fn (ev-fncall+-fns fn args wrld big-n safe-mode gc-off t)))
    (and (symbolp fn)
         (or (null fn)
             (function-symbolp fn wrld))))
  :rule-classes nil)

Theorem: lower/upper-case-p-non-standard-disjointness

(defthm lower/upper-case-p-non-standard-disjointness
  (not (and (lower-case-p-non-standard x)
            (upper-case-p-non-standard x)))
  :rule-classes nil)