		Search-engine friendly clone of the ACL2 documentation.

Smtlink-hint-syntax

Smtlink-option-syntax-p

Recoginizer for smtlink-option-syntax.

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

Definitions and Theorems

Function: smtlink-option-syntax-p

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

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

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

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

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

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

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

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

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

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

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

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

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