Filtering...

verified-termination-and-guards

books/system/verified-termination-and-guards
other
(in-package "ACL2")
local
(local (in-theory (enable all-boundp-initial-global-table)))
other
(verify-termination collect-by-position)
local
(local (encapsulate nil
    (local (defun all-vars1/all-vars1-lst
        (flg lst ans)
        (if (eq flg 'all-vars1)
          (cond ((variablep lst) (add-to-set-eq lst ans))
            ((fquotep lst) ans)
            (t (all-vars1/all-vars1-lst 'all-vars-lst1 (cdr lst) ans)))
          (cond ((endp lst) ans)
            (t (all-vars1/all-vars1-lst 'all-vars-lst1
                (cdr lst)
                (all-vars1/all-vars1-lst 'all-vars1 (car lst) ans)))))))
    (local (defthm step-1-lemma
        (equal (all-vars1/all-vars1-lst flg lst ans)
          (if (equal flg 'all-vars1)
            (all-vars1 lst ans)
            (all-vars1-lst lst ans)))))
    (local (defthm step-2-lemma
        (implies (and (symbol-listp ans)
            (if (equal flg 'all-vars1)
              (pseudo-termp lst)
              (pseudo-term-listp lst)))
          (symbol-listp (all-vars1/all-vars1-lst flg lst ans)))))
    (defthm symbol-listp-all-vars1
      (implies (and (symbol-listp ans) (pseudo-termp lst))
        (symbol-listp (all-vars1 lst ans)))
      :hints (("Goal" :use (:instance step-2-lemma (flg 'all-vars1)))))))
other
(verify-termination make-lambda-application)
other
(verify-termination >=-len)
other
(verify-termination all->=-len)
other
(verify-termination strip-cadrs)
other
(verify-termination strip-caddrs)
other
(verify-termination alist-to-doublets)
other
(verify-termination ffnnamep)
other
(verify-termination world-evisceration-alist)
other
(verify-termination abbrev-evisc-tuple)
other
(verify-termination override-hints)
other
(verify-termination stobjp)
other
(verify-termination newline)
other
(verify-termination lambda-subtermp)
other
(verify-termination ens)
local
(local (defthm car-assoc-equal-cdr-type
    (implies (alistp x)
      (or (consp (assoc-equal-cdr key x))
        (equal (assoc-equal-cdr key x) nil)))
    :rule-classes :type-prescription))
other
(verify-termination runep)
other
(verify-termination write-for-read)
other
(verify-termination fnume)
other
(verify-termination translate-abbrev-rune)
other
(verify-termination logical-namep)
other
(verify-termination er-cmp-fn)
other
(verify-termination macro-args-er-cmp)
other
(verify-termination project-dir-prefix-entry)
other
(verify-termination filename-to-book-name-1)
other
(verify-termination filename-to-book-name)
other
(verify-termination include-book-dir)
other
(verify-termination strip-non-hidden-package-names)
other
(verify-termination enabled-structure-p)
other
(verify-termination enabled-numep)
enabled-runep-guard-helper-1theorem
(defthm enabled-runep-guard-helper-1
  (implies (and (assoc-equal-cdr r x) (nat-alistp x))
    (or (natp (car (assoc-equal-cdr r x)))
      (equal (car (assoc-equal-cdr r x)) nil)))
  :rule-classes :type-prescription)
enabled-runep-guard-helper-2theorem
(defthm enabled-runep-guard-helper-2
  (implies (and (car (assoc-equal-cdr r x)) (fixnat-alistp x))
    (<= (car (assoc-equal-cdr r x)) (fixnum-bound)))
  :rule-classes :linear)
other
(verify-termination enabled-runep)
other
(verify-termination disabledp-fn-lst)
symbolp-deref-macro-nametheorem
(defthm symbolp-deref-macro-name
  (implies (and (symbolp name)
      (symbol-alistp macro-aliases)
      (r-symbol-alistp macro-aliases))
    (symbolp (deref-macro-name name macro-aliases))))
other
(verify-termination (disabledp-fn (declare (xargs :guard-hints (("Goal" :in-theory (disable deref-macro-name)
           :do-not-induct t))))))
other
(verify-termination def-body)
other
(verify-termination access-command-tuple-number)
other
(verify-termination collect-non-x)
other
(verify-termination (silent-error (declare (xargs :verify-guards t))))
other
(verify-termination saved-output-token-p)
other
(verify-termination push-io-record)
other
(verify-termination scan-to-cltl-command)