		Search-engine friendly clone of the ACL2 documentation.

Value-expressions

Value-to-value-expr

Value expression that denotes a given value.

Signature
(value-to-value-expr val) → expr
Arguments: val — Guard (valuep val).
Returns: expr — Type (expression-resultp expr).

This is inverse of value-expr-to-value, as we plan to prove. More precisely, going from value to value expression and from there back to value yields the same value. Due to the non-uniqueness of expression values denoting values, the other inversion property does not hold in general.

We return nil if the group value is a non-finite point. This should never happen, so we plan to revise this code eventually, after perhaps the definition of group value is updated to require finite points.

Theorem: return-type-of-value-to-value-expr.expr

(defthm return-type-of-value-to-value-expr.expr
  (b* ((?expr (value-to-value-expr val)))
    (expression-resultp expr))
  :rule-classes :rewrite)

Theorem: return-type-of-value-list-to-value-expr-list.exprs

(defthm return-type-of-value-list-to-value-expr-list.exprs
  (b* ((?exprs (value-list-to-value-expr-list vals)))
    (expression-list-resultp exprs))
  :rule-classes :rewrite)

Theorem: return-type-of-name+value-to-value-struct-init.init

(defthm return-type-of-name+value-to-value-struct-init.init
  (b* ((?init (name+value-to-value-struct-init name val)))
    (struct-init-resultp init))
  :rule-classes :rewrite)

Theorem: return-type-of-value-map-to-value-struct-init-list.inits

(defthm return-type-of-value-map-to-value-struct-init-list.inits
  (b* ((?inits (value-map-to-value-struct-init-list valmap)))
    (struct-init-list-resultp inits))
  :rule-classes :rewrite)

Theorem: value-to-value-expr-of-value-fix-val

(defthm value-to-value-expr-of-value-fix-val
  (equal (value-to-value-expr (value-fix val))
         (value-to-value-expr val)))

Theorem: value-list-to-value-expr-list-of-value-list-fix-vals

(defthm value-list-to-value-expr-list-of-value-list-fix-vals
  (equal (value-list-to-value-expr-list (value-list-fix vals))
         (value-list-to-value-expr-list vals)))

Theorem: name+value-to-value-struct-init-of-identifier-fix-name

(defthm name+value-to-value-struct-init-of-identifier-fix-name
  (equal (name+value-to-value-struct-init (identifier-fix name)
                                          val)
         (name+value-to-value-struct-init name val)))

Theorem: name+value-to-value-struct-init-of-value-fix-val

(defthm name+value-to-value-struct-init-of-value-fix-val
  (equal (name+value-to-value-struct-init name (value-fix val))
         (name+value-to-value-struct-init name val)))

Theorem: value-map-to-value-struct-init-list-of-value-map-fix-valmap

(defthm value-map-to-value-struct-init-list-of-value-map-fix-valmap
 (equal (value-map-to-value-struct-init-list (value-map-fix valmap))
        (value-map-to-value-struct-init-list valmap)))

Theorem: value-to-value-expr-value-equiv-congruence-on-val

(defthm value-to-value-expr-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (value-to-value-expr val)
                  (value-to-value-expr val-equiv)))
  :rule-classes :congruence)

Theorem: value-list-to-value-expr-list-value-list-equiv-congruence-on-vals

(defthm
  value-list-to-value-expr-list-value-list-equiv-congruence-on-vals
  (implies (value-list-equiv vals vals-equiv)
           (equal (value-list-to-value-expr-list vals)
                  (value-list-to-value-expr-list vals-equiv)))
  :rule-classes :congruence)

Theorem: name+value-to-value-struct-init-identifier-equiv-congruence-on-name

(defthm
 name+value-to-value-struct-init-identifier-equiv-congruence-on-name
 (implies (identifier-equiv name name-equiv)
          (equal (name+value-to-value-struct-init name val)
                 (name+value-to-value-struct-init name-equiv val)))
 :rule-classes :congruence)

Theorem: name+value-to-value-struct-init-value-equiv-congruence-on-val

(defthm
      name+value-to-value-struct-init-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (name+value-to-value-struct-init name val)
                  (name+value-to-value-struct-init name val-equiv)))
  :rule-classes :congruence)

Theorem: value-map-to-value-struct-init-list-value-map-equiv-congruence-on-valmap

(defthm
 value-map-to-value-struct-init-list-value-map-equiv-congruence-on-valmap
 (implies
      (value-map-equiv valmap valmap-equiv)
      (equal (value-map-to-value-struct-init-list valmap)
             (value-map-to-value-struct-init-list valmap-equiv)))
 :rule-classes :congruence)

Theorem: expression-valuep-of-value-to-value-expr

(defthm expression-valuep-of-value-to-value-expr
  (b* ((?expr (value-to-value-expr val)))
    (implies (not (reserrp expr))
             (expression-valuep expr))))

Theorem: expression-list-valuep-of-value-list-to-value-expr-list

(defthm expression-list-valuep-of-value-list-to-value-expr-list
  (b* ((?exprs (value-list-to-value-expr-list vals)))
    (implies (not (reserrp exprs))
             (expression-list-valuep exprs))))

Theorem: struct-init-valuep-of-name+value-to-value-struct-init

(defthm struct-init-valuep-of-name+value-to-value-struct-init
  (b* ((?init (name+value-to-value-struct-init name val)))
    (implies (not (reserrp init))
             (struct-init-valuep init))))

Theorem: struct-init-list-valuep-of-value-map-to-value-struct-init-list

(defthm
     struct-init-list-valuep-of-value-map-to-value-struct-init-list
  (b* ((?inits (value-map-to-value-struct-init-list valmap)))
    (implies (not (reserrp inits))
             (struct-init-list-valuep inits))))

Subtopics

Value-map-to-value-struct-init-list
Name+value-to-value-struct-init
Value-list-to-value-expr-list