all-fnnames

(in-package "ACL2")

(defsection std/system/all-fnnames
  :parents (std/system/term-queries)
  :short "Theorems about @(tsee all-fnnames)."
  :long (topstring (p "More precisely, these are theorems about @(tsee all-fnnames1),
     because @(tsee all-fnnames), as well as @(tsee all-fnnames-lst),
     is a macro that abbreviates @(tsee all-fnnames1).")
    (p "We also include the following theorem
     from @('system/all-fnnames.lisp'):")
    (@def "true-listp-all-fnnames"))
  (defthm true-listp-of-all-fnnames1-type
    (implies (true-listp acc)
      (true-listp (all-fnnames1 flg x acc)))
    :rule-classes :type-prescription)
  (defthm symbol-listp-of-all-fnnames1
    (implies (and (symbol-listp acc)
        (if flg
          (pseudo-term-listp x)
          (pseudo-termp x)))
      (symbol-listp (all-fnnames1 flg x acc))))
  (defthm all-fnnames1-includes-acc
    (subsetp-equal acc (all-fnnames1 flg x acc)))
  (local (defun-sk all-fnnames1-monotonic-acc-assertion
      (flg x)
      (forall (acc1 acc2)
        (implies (subsetp-equal acc1 acc2)
          (subsetp-equal (all-fnnames1 flg x acc1)
            (all-fnnames1 flg x acc2))))
      :rewrite :direct))
  (local (defthm all-fnnames1-monotonic-acc-lemma
      (all-fnnames1-monotonic-acc-assertion flg x)))
  (defthm all-fnnames1-monotonic-acc
    (implies (subsetp-equal acc1 acc2)
      (subsetp-equal (all-fnnames1 flg x acc1)
        (all-fnnames1 flg x acc2)))))