Recoginizer for smtlink-option-syntax.
(smtlink-option-syntax-p term used) → (mv ok new-used)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)