		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-rules

Some rules used by the lifter.

The lifter generates proofs that make use of certain rules about omaps and about some built-ins. To avoid a dependency on the libraries that contain those rules, here we create versions of these rules that are part of the lifter and that are used in proofs generated by the lifter.

Definitions and Theorems

Theorem: lift-rule-omap-in-to-in-of-keys

(defthm lift-rule-omap-in-to-in-of-keys
  (iff (omap::assoc key map)
       (in key (omap::keys map))))

Theorem: lift-rule-omap-consp-of-assoc-iff-assoc

(defthm lift-rule-omap-consp-of-assoc-iff-assoc
  (iff (consp (omap::assoc key map))
       (omap::assoc key map)))

Theorem: lift-rule-natp-of-mod

(defthm lift-rule-natp-of-mod
  (implies (and (integerp a) (posp b))
           (natp (mod a b))))

Theorem: lift-rule-nfix-when-natp

(defthm lift-rule-nfix-when-natp
  (implies (natp x) (equal (nfix x) x)))