		Search-engine friendly clone of the ACL2 documentation.

Pos-set

Pos-set-max

Maximum of a set of positive integers.

Signature
(pos-set-max set) → max
Arguments: set — Guard (pos-setp set).
Returns: max — Type (posp max).

If the set is empty, we return 1, which is the smallest positive integer.

Definitions and Theorems

Function: pos-set-max

(defun pos-set-max (set)
  (declare (xargs :guard (pos-setp set)))
  (let ((__function__ 'pos-set-max))
    (declare (ignorable __function__))
    (cond ((set::emptyp set) 1)
          (t (max (pos-fix (set::head set))
                  (pos-set-max (set::tail set)))))))

Theorem: posp-of-pos-set-max

(defthm posp-of-pos-set-max
  (b* ((max (pos-set-max set)))
    (posp max))
  :rule-classes :rewrite)

Theorem: pos-set-max->=-element

(defthm pos-set-max->=-element
  (implies (and (pos-setp set) (set::in elem set))
           (<= elem (pos-set-max set)))
  :rule-classes ((:linear :trigger-terms ((pos-set-max set)))))

Theorem: pos-set-max->=-subset

(defthm pos-set-max->=-subset
  (implies (and (pos-setp set2)
                (set::subset set1 set2))
           (<= (pos-set-max set1)
               (pos-set-max set2)))
  :rule-classes ((:linear :trigger-terms ((pos-set-max set1)
                                          (pos-set-max set2)))))

Theorem: pos-set-max-when-emptyp

(defthm pos-set-max-when-emptyp
  (implies (set::emptyp set)
           (equal (pos-set-max set) 1)))

Theorem: pos-set-max-of-singleton

(defthm pos-set-max-of-singleton
  (equal (pos-set-max (set::insert elem nil))
         (pos-fix elem)))