Filtering...

subcor-var

books/system/subcor-var

Included Books

sublis-var pseudo-termp-lemmas flag
other
(in-package "ACL2")
include-book
(include-book "sublis-var")
local
(local (include-book "pseudo-termp-lemmas"))
other
(verify-termination subcor-var1)
other
(verify-termination subcor-var
  (declare (xargs :verify-guards nil)))
local
(local (defun subcor-var-flg
    (flg vars terms x)
    (cond (flg (cond ((endp x) nil)
          (t (cons (subcor-var-flg nil vars terms (car x))
              (subcor-var-flg t vars terms (cdr x))))))
      (t (cond ((variablep x) (subcor-var1 vars terms x))
          ((fquotep x) x)
          (t (cons-term (ffn-symb x)
              (subcor-var-flg t vars terms (fargs x)))))))))
local
(local (defthmd subcor-var-flg-property
    (equal (subcor-var-flg flg vars term x)
      (if flg
        (subcor-var-lst vars term x)
        (subcor-var vars term x)))))
local
(local (defthm subcor-var-flg-preserves-len
    (implies flg
      (equal (len (subcor-var-flg flg vars terms x)) (len x)))))
local
(local (defthm pseudo-termp-subcor-var-flg
    (implies (and (symbol-listp vars)
        (pseudo-term-listp terms)
        (equal (len vars) (len terms))
        (if flg
          (pseudo-term-listp x)
          (pseudo-termp x)))
      (if flg
        (pseudo-term-listp (subcor-var-flg flg vars terms x))
        (pseudo-termp (subcor-var-flg flg vars terms x))))
    :rule-classes nil))
pseudo-term-listp-subcor-var-lsttheorem
(defthm pseudo-term-listp-subcor-var-lst
  (implies (and (symbol-listp vars)
      (pseudo-term-listp terms)
      (equal (len vars) (len terms))
      (pseudo-term-listp forms))
    (pseudo-term-listp (subcor-var-lst vars terms forms)))
  :hints (("Goal" :in-theory (enable subcor-var-flg-property)
     :use ((:instance pseudo-termp-subcor-var-flg (flg t) (x forms))))))
pseudo-term-listp-subcor-vartheorem
(defthm pseudo-term-listp-subcor-var
  (implies (and (symbol-listp vars)
      (pseudo-term-listp terms)
      (equal (len vars) (len terms))
      (pseudo-termp form))
    (pseudo-termp (subcor-var vars terms form)))
  :hints (("Goal" :in-theory (enable subcor-var-flg-property)
     :use ((:instance pseudo-termp-subcor-var-flg (flg nil) (x form))))))
other
(verify-guards subcor-var)
other
(verify-termination remove-lambdas1)
other
(verify-termination remove-lambdas)
local
(local (include-book "tools/flag" :dir :system))
local
(local (make-flag flag-remove-lambdas remove-lambdas1))
local
(local (defthm len-mv-nth-1-remove-lambdas-lst
    (equal (len (mv-nth 1 (remove-lambdas-lst x))) (len x))))
local
(local (defthm-flag-remove-lambdas (defthm pseudo-termp-mv-nth-1-remove-lambdas1
      (implies (pseudo-termp term)
        (pseudo-termp (mv-nth 1 (remove-lambdas1 term))))
      :flag remove-lambdas1)
    (defthm pseudo-term-listp-mv-nth-1-remove-lambdas-lst
      (implies (pseudo-term-listp termlist)
        (pseudo-term-listp (mv-nth 1 (remove-lambdas-lst termlist))))
      :flag remove-lambdas-lst)))
local
(local (defthm true-listp-mv-nth-1-remove-lambdas-lst
    (implies (force (true-listp lst))
      (true-listp (mv-nth 1 (remove-lambdas-lst lst))))
    :rule-classes :type-prescription))
other
(verify-guards remove-lambdas1)
other
(verify-guards remove-lambdas)