		Search-engine friendly clone of the ACL2 documentation.

Values

Lower-symbol

Lower a symbol value to an ACL2 symbol.

Signature
(lower-symbol symval) → sym
Arguments: symval — Guard (symbol-valuep symval).
Returns: sym — Type (symbolp sym).

This is the opposite of lift-symbol. It lowers a symbol value from the meta level.

This must be used with care, because at the meta level a symbol is any pair of a package (name) and a (symbol) name, but (i) the package name may not exist in the current ACL2 environment and (ii) the package may exist but import a symbol with that name from another package. In the first case, the call of pkg-witness causes an error. In the second case, the resulting ACL2 symbol may have a different symbol-package-name.

Nonetheless, if this function is judiciously called on a meta-level symbol that corresponds to an ACL2 symbol in the current ACL2 environment (e.g. on a result of lift-symbol), then the result will be the expected ACL2 symbol.

We construct the symbol via intern-in-package-of-symbol, using the package witness of the package name. Since the guard of pkg-witness requires the package name to be non-empty, we need at least to check that here. If it is empty, we use the "ACL2" package just to make this function total.

Definitions and Theorems

Function: lower-symbol

(defun
 lower-symbol (symval)
 (declare (xargs :guard (symbol-valuep symval)))
 (let
     ((__function__ 'lower-symbol))
     (declare (ignorable __function__))
     (b* ((package (symbol-value->package symval))
          (name (symbol-value->name symval))
          (package (if (equal package "") "ACL2" package)))
         (intern-in-package-of-symbol name (pkg-witness package)))))

Theorem: symbolp-of-lower-symbol

(defthm symbolp-of-lower-symbol
        (b* ((sym (lower-symbol symval)))
            (symbolp sym))
        :rule-classes :rewrite)

Theorem: lower-symbol-of-symbol-value-fix-symval

(defthm lower-symbol-of-symbol-value-fix-symval
        (equal (lower-symbol (symbol-value-fix symval))
               (lower-symbol symval)))

Theorem: lower-symbol-symbol-value-equiv-congruence-on-symval

(defthm lower-symbol-symbol-value-equiv-congruence-on-symval
        (implies (symbol-value-equiv symval symval-equiv)
                 (equal (lower-symbol symval)
                        (lower-symbol symval-equiv)))
        :rule-classes :congruence)