		Search-engine friendly clone of the ACL2 documentation.

Real-operations

Ge-real-values

Apply >= to real values [C17:6.5.8/3] [C17:6.5.8/6].

Signature
(ge-real-values val1 val2) → resval
Arguments: val1 — Guard (valuep val1).; val2 — Guard (valuep val2).
Returns: resval — Type (valuep resval).

We perform the usual arithmetic conversions and then we apply the operation on the integers. In our current formalization, integers are the only real values. This ACL2 function will be extended with more cases if/when we extend our model with non-integer real values.

Definitions and Theorems

Function: ge-real-values

(defun ge-real-values (val1 val2)
  (declare (xargs :guard (and (valuep val1) (valuep val2))))
  (declare (xargs :guard (and (value-realp val1)
                              (value-realp val2))))
  (let ((__function__ 'ge-real-values))
    (declare (ignorable __function__))
    (b* (((mv val1 val2)
          (uaconvert-values val1 val2)))
      (ge-integer-values val1 val2))))

Theorem: valuep-of-ge-real-values

(defthm valuep-of-ge-real-values
  (b* ((resval (ge-real-values val1 val2)))
    (valuep resval))
  :rule-classes :rewrite)

Theorem: ge-real-values-of-value-fix-val1

(defthm ge-real-values-of-value-fix-val1
  (equal (ge-real-values (value-fix val1) val2)
         (ge-real-values val1 val2)))

Theorem: ge-real-values-value-equiv-congruence-on-val1

(defthm ge-real-values-value-equiv-congruence-on-val1
  (implies (value-equiv val1 val1-equiv)
           (equal (ge-real-values val1 val2)
                  (ge-real-values val1-equiv val2)))
  :rule-classes :congruence)

Theorem: ge-real-values-of-value-fix-val2

(defthm ge-real-values-of-value-fix-val2
  (equal (ge-real-values val1 (value-fix val2))
         (ge-real-values val1 val2)))

Theorem: ge-real-values-value-equiv-congruence-on-val2

(defthm ge-real-values-value-equiv-congruence-on-val2
  (implies (value-equiv val2 val2-equiv)
           (equal (ge-real-values val1 val2)
                  (ge-real-values val1 val2-equiv)))
  :rule-classes :congruence)