• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
      • Lispfloat
        • Er-double-expt
        • Er-float+
        • Er-float-expt
        • Er-double/
        • Er-double+
        • Er-double*
        • Er-double-
        • Er-float/
        • Er-float*
        • Er-float-
        • Er-float-tan
        • Er-float-sqrt
        • Er-float-sin
        • Er-float-e^x
        • Er-float-cos
        • Er-double-tan
        • Er-double-sqrt
        • Er-double-sin
        • Er-double-e^x
        • Er-double-cos
      • Arithmetic-1
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Include-an-arithmetic-book
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra
  • Testing-utilities

• Lispfloat

Er-float+

(Single-precision) floating point addition.

(er-float+ a b) is a lispfloat wrapper function.

In the logic this function does not have a definition, but its ACL2::constraints say it returns (mv errmsg ans), where:

• errmsg is either a string that indicates an error has occurred (e.g., a rounding error when converting rationals to floats, an overflow, etc.)
• ans is a rational.

Definitions and Theorems

Basic Type Theorems

Theorem: er-float+-mvtypes-0

(defthm er-float+-mvtypes-0
  (maybe-stringp (mv-nth 0 (er-float+ a b)))
  :rule-classes :type-prescription)

Theorem: er-float+-mvtypes-1

(defthm er-float+-mvtypes-1
  (rationalp (mv-nth 1 (er-float+ a b)))
  :rule-classes :type-prescription)

Rational-Equiv Congruence Rules

Theorem: er-float+-of-rfix-a

(defthm er-float+-of-rfix-a
  (equal (er-float+ (rfix a) b)
         (er-float+ a b)))

Theorem: er-float+-rational-equiv-congruence-on-a

(defthm er-float+-rational-equiv-congruence-on-a
  (implies (acl2::rational-equiv a a-equiv)
           (equal (er-float+ a b)
                  (er-float+ a-equiv b)))
  :rule-classes :congruence)

Theorem: er-float+-of-rfix-b

(defthm er-float+-of-rfix-b
  (equal (er-float+ a (rfix b))
         (er-float+ a b)))

Theorem: er-float+-rational-equiv-congruence-on-b

(defthm er-float+-rational-equiv-congruence-on-b
  (implies (acl2::rational-equiv b b-equiv)
           (equal (er-float+ a b)
                  (er-float+ a b-equiv)))
  :rule-classes :congruence)