• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
        • Deftagsum
        • Defprod
        • Defflexsum
        • Defbitstruct
        • Deflist
        • Defalist
        • Defbyte
        • Deffixequiv
        • Defresult
        • Deffixtype
        • Defoption
        • Fty-discipline
        • Fold
        • Fty-extensions
          • Defbyte
          • Defresult
          • Fold
          • Defsubtype
          • Defset
          • Specific-types
          • Defflatsum
          • Deflist-of-len
          • Pos-list
          • Defbytelist
          • Defomap
          • Defbyte-standard-instances
          • Deffixtype-alias
          • Defbytelist-standard-instances
          • Defunit
          • Byte-list
          • Byte
          • Database
          • Pos-option
          • Nibble
          • Nat-option
          • String-option
          • Byte-list20
          • Byte-list32
          • Byte-list64
          • Pseudo-event-form
          • Natoption/natoptionlist
          • Nati
          • Character-list
          • Nat/natlist
          • Maybe-string
          • Nibble-list
          • Natoption/natoptionlist-result
          • Nat/natlist-result
          • Nat-option-list-result
          • Set
          • String-result
          • String-list-result
          • Nat-result
          • Nat-option-result
          • Nat-list-result
          • Maybe-string-result
          • Integer-result
          • Character-result
          • Character-list-result
          • Boolean-result
          • Map
          • Bag
          • Pos-set
            • Pos-sfix
            • Pos-setp
            • Pos-set->=-pos
            • Pos-set-max
              • Pos-sequiv
            • Hex-digit-char-list
            • Dec-digit-char-list
            • Pseudo-event-form-list
            • Nat-option-list
            • Symbol-set
            • String-set
            • Nat-set
            • Oct-digit-char-list
            • Bin-digit-char-list
            • Bit-list
          • Defsubtype
          • Defset
          • Deftypes
          • Specific-types
          • Defflatsum
          • Deflist-of-len
          • Defbytelist
          • Fty::basetypes
          • Defomap
          • Defvisitors
          • Deffixtype-alias
          • Deffixequiv-sk
          • Defunit
          • Multicase
          • Deffixequiv-mutual
          • Fty::baselists
          • Def-enumcase
          • Defmap
        • Apt
        • Std/util
        • Defdata
        • Defrstobj
        • Seq
        • Match-tree
        • Defrstobj
        • With-supporters
        • Def-partial-measure
        • Template-subst
        • Soft
        • Defthm-domain
        • Event-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • 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)))