• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
        • Yul
        • Zcash
        • ACL2-programming-language
          • Primitive-functions
          • Translated-terms
          • Values
            • Value
            • Symbol-value
            • Lower-symbol
            • Lift-symbol-list
              • Symbol-value-option
              • Value-option
              • Lift-value
              • Lift-symbol
              • Value-rational->get
              • Value-integer->get
              • Value-case-rational
              • Value-case-integer
              • Value-symbol-list
              • Lower-value
              • Value-list-of
              • Value-list
              • Symbol-value-list
              • Symbol-value-set
              • Value-t
              • Value-nil
            • Evaluation
            • Program-equivalence
            • Functions
            • Packages
            • Programs
            • Interpreter
            • Evaluation-states
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Values

    Lift-symbol-list

    Lift lift-symbol to lists.

    Signature
    (lift-symbol-list x) → symvals
    Returns
    symvals — Type (symbol-value-listp symvals).

    This is an ordinary std::defprojection.

    Definitions and Theorems

    Function: lift-symbol-list-exec

    (defun lift-symbol-list-exec (x acc)
      (declare (xargs :guard (symbol-listp x)))
      (let ((__function__ 'lift-symbol-list-exec))
        (declare (ignorable __function__))
        (if (consp x)
            (lift-symbol-list-exec (cdr x)
                                   (cons (lift-symbol (car x)) acc))
          acc)))

    Function: lift-symbol-list-nrev

    (defun lift-symbol-list-nrev (x acl2::nrev)
      (declare (xargs :stobjs (acl2::nrev)))
      (declare (xargs :guard (symbol-listp x)))
      (let ((__function__ 'lift-symbol-list-nrev))
        (declare (ignorable __function__))
        (if (atom x)
            (acl2::nrev-fix acl2::nrev)
          (let ((acl2::nrev (acl2::nrev-push (lift-symbol (car x))
                                             acl2::nrev)))
            (lift-symbol-list-nrev (cdr x)
                                   acl2::nrev)))))

    Function: lift-symbol-list

    (defun lift-symbol-list (x)
     (declare (xargs :guard (symbol-listp x)))
     (let ((__function__ 'lift-symbol-list))
      (declare (ignorable __function__))
      (mbe
       :logic
       (if (consp x)
           (cons (lift-symbol (car x))
                 (lift-symbol-list (cdr x)))
         nil)
       :exec
       (if (atom x)
           nil
        (acl2::with-local-nrev (lift-symbol-list-nrev x acl2::nrev))))))

    Theorem: symbol-value-listp-of-lift-symbol-list

    (defthm symbol-value-listp-of-lift-symbol-list
      (b* ((symvals (lift-symbol-list x)))
        (symbol-value-listp symvals))
      :rule-classes :rewrite)

    Theorem: lift-symbol-list-nrev-removal

    (defthm lift-symbol-list-nrev-removal
      (equal (lift-symbol-list-nrev acl2::x acl2::nrev)
             (append acl2::nrev (lift-symbol-list acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-exec-removal

    (defthm lift-symbol-list-exec-removal
      (equal (lift-symbol-list-exec acl2::x acl2::acc)
             (revappend (lift-symbol-list acl2::x)
                        acl2::acc))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-of-rev

    (defthm lift-symbol-list-of-rev
      (equal (lift-symbol-list (rev acl2::x))
             (rev (lift-symbol-list acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-of-list-fix

    (defthm lift-symbol-list-of-list-fix
      (equal (lift-symbol-list (list-fix acl2::x))
             (lift-symbol-list acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-of-append

    (defthm lift-symbol-list-of-append
      (equal (lift-symbol-list (append acl2::a acl2::b))
             (append (lift-symbol-list acl2::a)
                     (lift-symbol-list acl2::b)))
      :rule-classes ((:rewrite)))

    Theorem: cdr-of-lift-symbol-list

    (defthm cdr-of-lift-symbol-list
      (equal (cdr (lift-symbol-list acl2::x))
             (lift-symbol-list (cdr acl2::x)))
      :rule-classes ((:rewrite)))

    Theorem: car-of-lift-symbol-list

    (defthm car-of-lift-symbol-list
      (equal (car (lift-symbol-list acl2::x))
             (and (consp acl2::x)
                  (lift-symbol (car acl2::x))))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-under-iff

    (defthm lift-symbol-list-under-iff
      (iff (lift-symbol-list acl2::x)
           (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: consp-of-lift-symbol-list

    (defthm consp-of-lift-symbol-list
      (equal (consp (lift-symbol-list acl2::x))
             (consp acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: len-of-lift-symbol-list

    (defthm len-of-lift-symbol-list
      (equal (len (lift-symbol-list acl2::x))
             (len acl2::x))
      :rule-classes ((:rewrite)))

    Theorem: true-listp-of-lift-symbol-list

    (defthm true-listp-of-lift-symbol-list
      (true-listp (lift-symbol-list acl2::x))
      :rule-classes :type-prescription)

    Theorem: lift-symbol-list-when-not-consp

    (defthm lift-symbol-list-when-not-consp
      (implies (not (consp acl2::x))
               (equal (lift-symbol-list acl2::x) nil))
      :rule-classes ((:rewrite)))

    Theorem: lift-symbol-list-of-cons

    (defthm lift-symbol-list-of-cons
      (equal (lift-symbol-list (cons acl2::a acl2::b))
             (cons (lift-symbol acl2::a)
                   (lift-symbol-list acl2::b)))
      :rule-classes ((:rewrite)))