		Search-engine friendly clone of the ACL2 documentation.

Self-bounds-for-ash

Lemmas for the bounds of (ash a b) versus a.

These are lemmas for:

(< (ASH A B) A)
(= A (ASH A B))
(< A (ASH A B))

BOZO these only address when A is positive. We should extend these to negative numbers.

Definitions and Theorems

Theorem: (< a (ash a b)) when (posp a)

(defthm
 |(< a (ash a b)) when (posp a)|
 (implies (posp a)
          (equal (< a (ash a b)) (posp b)))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp a) (posp b))
                                             (< a (ash a b))))))

Theorem: (= a (ash a b)) when (posp a)

(defthm |(= a (ash a b)) when (posp a)|
        (implies (posp a)
                 (equal (equal a (ash a b)) (zip b))))

Theorem: (< (ash a b) a) when (posp a)

(defthm
 |(< (ash a b) a) when (posp a)|
 (implies (posp a)
          (equal (< (ash a b) a) (negp b)))
 :rule-classes ((:rewrite)
                (:linear :corollary (implies (and (posp a) (negp b))
                                             (< (ash a b) a)))))