|
|
|---|
|
|
|
|---|
Lower a symbol value to an ACL2 symbol.
(lower-symbol symval) → 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
Function:
(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:
(defthm symbolp-of-lower-symbol (b* ((sym (lower-symbol symval))) (symbolp sym)) :rule-classes :rewrite)
Theorem:
(defthm lower-symbol-of-symbol-value-fix-symval (equal (lower-symbol (symbol-value-fix symval)) (lower-symbol symval)))
Theorem:
(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)