Filtering...

termp

books/system/termp

Included Books

legal-variablep
other
(in-package "ACL2")
include-book
(include-book "legal-variablep")
plist-worldp-with-formals-forward-to-plist-worldptheorem
(defthm plist-worldp-with-formals-forward-to-plist-worldp
  (implies (plist-worldp-with-formals wrld)
    (plist-worldp wrld))
  :rule-classes :forward-chaining)
other
(verify-termination arity
  (declare (xargs :guard (and (or (and (consp fn) (consp (cdr fn)) (true-listp (cadr fn)))
          (symbolp fn))
        (plist-worldp-with-formals w)))))
other
(verify-termination (termp (declare (xargs :guard (plist-worldp-with-formals w)
        :guard-hints (("Goal" :in-theory (disable member-eq)))
        :verify-guards nil)))
  (term-listp (declare (xargs :guard (plist-worldp-with-formals w)
        :guard-hints (("Goal" :in-theory (disable member-eq)))
        :verify-guards nil))))
in-theory
(in-theory (disable legal-variable-or-constant-namep))
termp-implies-pseudo-termpencapsulate
(encapsulate nil
  (local (defun pseudo-termp/pseudo-term-listp
      (flg x)
      (if (eq flg 'pseudo-termp)
        (cond ((atom x) (symbolp x))
          ((eq (car x) 'quote) (and (consp (cdr x)) (null (cdr (cdr x)))))
          ((not (true-listp x)) nil)
          ((not (pseudo-termp/pseudo-term-listp 'pseudo-term-listp (cdr x))) nil)
          (t (or (symbolp (car x))
              (and (true-listp (car x))
                (equal (length (car x)) 3)
                (eq (car (car x)) 'lambda)
                (symbol-listp (cadr (car x)))
                (pseudo-termp/pseudo-term-listp 'pseudo-termp
                  (caddr (car x)))
                (equal (length (cadr (car x))) (length (cdr x)))))))
        (cond ((atom x) (equal x nil))
          (t (and (pseudo-termp/pseudo-term-listp 'pseudo-termp (car x))
              (pseudo-termp/pseudo-term-listp 'pseudo-term-listp (cdr x))))))))
  (local (defthm term-listp-implies-true-listp
      (implies (term-listp x w) (true-listp x))
      :rule-classes :forward-chaining))
  (local (defthm arglistp1-implies-symbol-listp
      (implies (arglistp1 x) (symbol-listp x))
      :hints (("Goal" :in-theory (enable arglistp1)))
      :rule-classes :forward-chaining))
  (local (defthm step-1-lemma
      (equal (pseudo-termp/pseudo-term-listp flg x)
        (if (eq flg 'pseudo-termp)
          (pseudo-termp x)
          (pseudo-term-listp x)))))
  (local (defthm step-2-lemma
      (implies (if (eq flg 'pseudo-termp)
          (termp x w)
          (term-listp x w))
        (pseudo-termp/pseudo-term-listp flg x))
      :hints (("Goal" :in-theory (enable arglistp)) ("Subgoal *1/4''" :expand (termp x w)))))
  (defthm termp-implies-pseudo-termp
    (implies (termp x w) (pseudo-termp x))
    :hints (("Goal" :use ((:instance step-2-lemma (flg 'pseudo-termp)))))
    :rule-classes (:rewrite :forward-chaining))
  (defthm term-listp-implies-pseudo-term-listp
    (implies (term-listp x w) (pseudo-term-listp x))
    :hints (("Goal" :use ((:instance step-2-lemma (flg 'pseudo-term-listp)))))
    :rule-classes (:rewrite :forward-chaining)))
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)))))))
local
(local (defthm symbol-listp-implies-true-listp
    (implies (symbol-listp x) (true-listp x))))
local
(local (defthm arglistp1-implies-true-listp
    (implies (arglistp1 x) (true-listp x))
    :hints (("Goal" :in-theory (enable arglistp1)))))
other
(verify-guards termp)
other
(verify-termination term-list-listp)
other
(verify-termination arities-okp)
arities-okp-implies-aritytheorem
(defthm arities-okp-implies-arity
  (implies (and (arities-okp user-table w) (assoc fn user-table))
    (equal (arity fn w) (cdr (assoc fn user-table)))))
arities-okp-implies-logicptheorem
(defthm arities-okp-implies-logicp
  (implies (and (arities-okp user-table w) (assoc fn user-table))
    (logicp fn w)))
in-theory
(in-theory (disable arity arities-okp))
other
(verify-termination logic-fnsp)
other
(verify-termination logic-termp)
other
(verify-termination logic-term-listp)
other
(verify-termination logic-fns-list-listp)
other
(verify-termination logic-term-list-listp)
other
(verify-termination theory-invariant-table-guard)