		Search-engine friendly clone of the ACL2 documentation.

Defflatsum-implementation

Defflatsum-theorem

Generate the theorem associated to a summand.

Signature
(defflatsum-theorem summand-predicate sum-predicate) → thm
Arguments: summand-predicate — Guard (symbolp summand-predicate).; sum-predicate — Guard (symbolp sum-predicate).
Returns: thm — A ACL2::pseudo-event-formp.

The theorem says that anything satisfying the summand also satisfies the sum. It is proved by enabling the definition of the sum recognizer.

Definitions and Theorems

Function: defflatsum-theorem

(defun defflatsum-theorem (summand-predicate sum-predicate)
 (declare (xargs :guard (and (symbolp summand-predicate)
                             (symbolp sum-predicate))))
 (let ((__function__ 'defflatsum-theorem))
  (declare (ignorable __function__))
  (b* ((thm-name (acl2::packn-pos (list sum-predicate '-when-
                                        summand-predicate)
                                  sum-predicate)))
   (cons
    'defthm
    (cons
     thm-name
     (cons
      (cons 'implies
            (cons (cons summand-predicate '(x))
                  (cons (cons sum-predicate '(x)) 'nil)))
      (cons
       ':hints
       (cons
        (cons
          (cons '"Goal"
                (cons ':in-theory
                      (cons (cons 'enable (cons sum-predicate 'nil))
                            'nil)))
          'nil)
        'nil))))))))