Filtering...

all-vars

books/std/system/all-vars

Included Books

flag constructors
other
(in-package "ACL2")
include-book
(include-book "tools/flag" :dir :system)
include-book
(include-book "xdoc/constructors" :dir :system)
other
(defxdoc std/system/all-vars
  :parents (std/system/term-queries)
  :short "Theorems about @(tsee all-vars)."
  :long (topstring (p "See the file for lemmas about @('all-vars1').")
    (@def "symbol-listp-of-all-vars")
    (@def "true-listp-of-all-vars")))
other
(make-flag all-vars1)
other
(defthm-flag-all-vars1 (defthm true-listp-of-all-vars1
    (equal (true-listp (all-vars1 term ans)) (true-listp ans))
    :flag all-vars1)
  (defthm true-listp-of-all-vars1-lst
    (equal (true-listp (all-vars1-lst lst ans))
      (true-listp ans))
    :flag all-vars1-lst))
true-listp-of-all-vars1-typetheorem
(defthm true-listp-of-all-vars1-type
  (implies (true-listp ans) (true-listp (all-vars1 term ans)))
  :rule-classes :type-prescription)
true-listp-of-all-vars1-lst-typetheorem
(defthm true-listp-of-all-vars1-lst-type
  (implies (true-listp ans)
    (true-listp (all-vars1-lst term ans)))
  :rule-classes :type-prescription)
other
(defthm-flag-all-vars1 (defthm symbol-listp-of-all-vars1
    (implies (pseudo-termp term)
      (equal (symbol-listp (all-vars1 term ans))
        (symbol-listp ans)))
    :flag all-vars1)
  (defthm symbol-listp-of-all-vars1-lst
    (implies (pseudo-term-listp lst)
      (equal (symbol-listp (all-vars1-lst lst ans))
        (symbol-listp ans)))
    :flag all-vars1-lst))
symbol-listp-of-all-varstheorem
(defthm symbol-listp-of-all-vars
  (implies (pseudo-termp term) (symbol-listp (all-vars term))))
true-listp-of-all-varstheorem
(defthm true-listp-of-all-vars
  (true-listp (all-vars term))
  :rule-classes (:rewrite :type-prescription))