		Search-engine friendly clone of the ACL2 documentation.

Function-syntax

Function-option-syntax-p

Recoginizer for function-option-syntax.

Signature
(function-option-syntax-p term used) → (mv ok new-used)
Arguments: used — Guard (function-option-name-lst-p used).
Returns: ok — Type (booleanp ok).; new-used — Type (function-option-name-lst-p new-used).

Definitions and Theorems

Function: function-option-syntax-p

(defun function-option-syntax-p (term used)
 (declare (xargs :guard (function-option-name-lst-p used)))
 (let ((acl2::__function__ 'function-option-syntax-p))
  (declare (ignorable acl2::__function__))
  (b* ((used (function-option-name-lst-fix used))
       ((unless (true-listp term))
        (mv nil used))
       ((unless (consp term)) (mv t used))
       ((unless (and (car term)
                     (cdr term)
                     (not (cddr term))))
        (mv nil used))
       ((cons option body-lst) term)
       ((unless (function-option-name-p option))
        (mv nil used))
       (option-type (cdr (assoc-equal option *function-options*))))
    (mv (and (not (member-equal option used))
             (eval-function-option-type option-type (car body-lst)))
        (cons option used)))))

Theorem: booleanp-of-function-option-syntax-p.ok

(defthm booleanp-of-function-option-syntax-p.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (booleanp ok))
  :rule-classes :rewrite)

Theorem: function-option-name-lst-p-of-function-option-syntax-p.new-used

(defthm
    function-option-name-lst-p-of-function-option-syntax-p.new-used
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (function-option-name-lst-p new-used))
  :rule-classes :rewrite)

Theorem: function-option-syntax-p--monotonicity.ok

(defthm function-option-syntax-p--monotonicity.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (and (subsetp used-1 used :test 'equal)
                  ok)
             (mv-nth 0
                     (function-option-syntax-p term used-1))))
  :rule-classes :rewrite)

Theorem: function-option-syntax-p--ok-congruence.ok

(defthm function-option-syntax-p--ok-congruence.ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (acl2::set-equiv used-1 used)
             (equal (mv-nth 0
                            (function-option-syntax-p term used-1))
                    ok)))
  :rule-classes (:congruence))

Theorem: function-option-syntax-p--monotonicity.new-used

(defthm function-option-syntax-p--monotonicity.new-used
 (b* (((mv ?ok ?new-used)
       (function-option-syntax-p term used)))
   (implies (and (subsetp used-1 used :test 'equal)
                 ok)
            (subsetp (mv-nth 1
                             (function-option-syntax-p term used-1))
                     new-used
                     :test 'equal)))
 :rule-classes :rewrite)

Theorem: function-option-syntax-p--new-used-when-ok

(defthm function-option-syntax-p--new-used-when-ok
  (b* (((mv ?ok ?new-used)
        (function-option-syntax-p term used)))
    (implies (and term ok)
             (equal new-used
                    (cons (car term)
                          (function-option-name-lst-fix used)))))
  :rule-classes :rewrite)