fsubcor-var - ACL2 Book

Included Books

top flag

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

local

(local (include-book "tools/flag" :dir :system))

local

(local (defthm pseudo-termp-of-subcor-var1
    (implies (and (pseudo-term-listp terms) (symbolp var))
      (pseudo-termp (subcor-var1 vars terms var)))))

local

(local (make-flag flag fsubcor-var))

local

(local (defthm len-of-fsubcor-var-lst
    (equal (len (fsubcor-var-lst vars terms forms)) (len forms))))

local

(local (defthm-flag (defthm theorem-for-fsubcor-var
      (implies (and (pseudo-term-listp terms) (pseudo-termp form))
        (pseudo-termp (fsubcor-var vars terms form)))
      :flag fsubcor-var)
    (defthm theorem-for-fsubcor-var-lst
      (implies (and (pseudo-term-listp terms) (pseudo-term-listp forms))
        (pseudo-term-listp (fsubcor-var-lst vars terms forms)))
      :flag fsubcor-var-lst)
    :hints (("Goal" :expand (:free (a b) (pseudo-termp (cons a b)))))))

other

(defsection std/system/fsubcor-var
  :parents (std/system/term-transformations)
  :short "Theorems about @(tsee fsubcor-var)."
  (defthm pseudo-termp-of-fsubcor-var
    (implies (and (pseudo-term-listp terms) (pseudo-termp form))
      (pseudo-termp (fsubcor-var vars terms form))))
  (defthm pseudo-term-listp-of-fsubcor-var-lst
    (implies (and (pseudo-term-listp terms) (pseudo-term-listp forms))
      (pseudo-term-listp (fsubcor-var-lst vars terms forms))))
  (defthm len-of-fsubcor-var-lst
    (equal (len (fsubcor-var-lst vars terms forms)) (len forms))))

in-theory

(in-theory (disable fsubcor-var fsubcor-var-lst))