[acl2-books] r993 committed - Separate the more basic ihs-extensions stuff into a new book, and chan...
acl2-...@googlecode.com
Author: sswords
Date: Thu Mar 1 15:20:35 2012
Log: Separate the more basic ihs-extensions stuff into a new book, and
change rulesets so you don't have to specify them with (:ruleset name)
http://code.google.com/p/acl2-books/source/detail?r=993
Added:
/trunk/centaur/bitops/ihsext-basics.lisp
Modified:
/trunk/centaur/aig/base.lisp
/trunk/centaur/bitops/bitsets.lisp
/trunk/centaur/bitops/ihs-extensions.lisp
/trunk/tools/rulesets.lisp
=======================================
--- /dev/null
+++ /trunk/centaur/bitops/ihsext-basics.lisp Thu Mar 1 15:20:35 2012
@@ -0,0 +1,1215 @@
+
+(in-package "ACL2")
+
+(include-book "ihs/logops-definitions" :dir :system)
+(include-book "cutil/defsection" :dir :system)
+
+(include-book "tools/rulesets" :dir :system)
+
+(defconst *ihs-extensions-disables*
+ '(floor mod expt ash evenp oddp
+ logbitp logior logand lognot logxor
+ logcons logcar logcdr loghead
+ integer-length
+ logmaskp))
+
+(make-event
+ (prog2$ (cw "Note (from ihs-extensions): disabling ~&0.~%~%"
+ *ihs-extensions-disables*)
+ '(value-triple :invisible))
+ :check-expansion t)
+
+(in-theory (set-difference-theories (current-theory :here)
+ *ihs-extensions-disables*))
+
+(include-book "ihs/logops-lemmas" :dir :system)
+
+
+(local (include-book "arithmetic/top-with-meta" :dir :system))
+
+
+(def-ruleset! ihsext-basic-thms nil)
+(def-ruleset! ihsext-advanced-thms nil)
+(def-ruleset! ihsext-bad-type-thms nil)
+(def-ruleset! ihsext-redefs nil)
+(def-ruleset! ihsext-recursive-redefs nil)
+(def-ruleset! ihsext-inductions nil)
+(def-ruleset! ihsext-bounds-thms nil)
+(def-ruleset! ihsext-arithmetic nil)
+
+(defsection logcons-car-cdr
+
+ (local (in-theory (enable logcar logcons logcdr)))
+
+ (defthm logcons-when-zip
+ (implies (zip x)
+ (equal (logcons b x)
+ (bfix b))))
+
+ (defthm logcons-when-not-bit
+ (implies (not (bitp b))
+ (equal (logcons b x)
+ (logcons 0 x))))
+
+ (defthm logcar-when-zip
+ (implies (zip i)
+ (equal (logcar i) 0)))
+
+ (defthm logcdr-when-zip
+ (implies (zip i)
+ (equal (logcdr i) 0)))
+
+ (add-to-ruleset ihsext-bad-type-thms
+ '(logcons-when-zip
+ logcons-when-not-bit
+ logcar-when-zip
+ logcdr-when-zip))
+
+ ;; These are a special case since we don't produce definition rules
+ ;; for logcar/logcdr/logcons
+ (add-to-ruleset ihsext-basic-thms
+ '(logcons-when-zip
+ logcons-when-not-bit
+ logcar-when-zip
+ logcdr-when-zip))
+
+ (local (in-theory (enable* ihsext-bad-type-thms)))
+ (local (in-theory (disable logcar logcdr logcons)))
+
+ (defthm logcar-logcons-fix
+ (equal (logcar (logcons b x))
+ (bfix b))
+ :hints(("Goal" :cases ((integerp x)))
+ (and stable-under-simplificationp
+ '(:cases ((bitp b))))))
+
+ (defthm logcdr-logcons-fix
+ (equal (logcdr (logcons b x))
+ (ifix x))
+ :hints (("goal" :cases ((bitp b)))))
+
+
+ (defthm logcons-destruct
+ (equal (logcons (logcar x) (logcdr x))
+ (ifix x)))
+
+ (defthmd equal-logcons-strong
+ (equal (equal (logcons a b) i)
+ (and (integerp i)
+ (equal (logcar i) (bfix a))
+ (equal (logcdr i) (ifix b))))
+ :hints (("goal" :cases ((bitp a)))
+ (and stable-under-simplificationp
+ '(:cases ((integerp b))))))
+
+ (local (in-theory (enable equal-logcons-strong)))
+
+ (defthm equal-logcons-weak
+ (equal (equal (logcons a b) (logcons c d))
+ (and (equal (bfix a) (bfix c))
+ (equal (ifix b) (ifix d)))))
+
+ (defthm logcons-equal-constant
+ (implies (syntaxp (quotep i))
+ (equal (equal (logcons a b) i)
+ (and (integerp i)
+ (equal (logcar i) (bfix a))
+ (equal (logcdr i) (ifix b))))))
+
+ (add-to-ruleset ihsext-basic-thms
+ '(logcar-logcons-fix
+ logcdr-logcons-fix
+ logcons-destruct
+ equal-logcons-weak
+ logcons-equal-constant))
+
+ (add-to-ruleset ihsext-advanced-thms '(equal-logcons-strong))
+
+
+ (defthmd logcons-<-0-linear
+ (implies (and (integerp i) (< i 0))
+ (< (logcons b i) 0))
+ :rule-classes :linear)
+
+ (defthmd logcons->=-0-linear
+ (implies (or (not (integerp i))
+ (<= 0 i))
+ (<= 0 (logcons b i)))
+ :rule-classes :linear)
+
+ (defthmd logcdr-<-0-linear
+ (implies (and (integerp i) (< i 0))
+ (< (logcdr i) 0))
+ :rule-classes :linear)
+
+ (defthmd logcdr->=-0-linear
+ (implies (or (not (integerp i))
+ (<= 0 i))
+ (<= 0 (logcdr i)))
+ :rule-classes :linear)
+
+ ;; from logops-definitions
+ (add-to-ruleset ihsext-bounds-thms '(logcons-<-0
+ logcdr-<-0
+ logcons-<-0-linear
+ logcons->=-0-linear
+ logcdr-<-0-linear
+ logcdr->=-0-linear))
+
+ (defthmd logcons-<-n-strong
+ (implies (integerp j)
+ (equal (< (logcons b i) j)
+ (or (< (ifix i) (logcdr j))
+ (and (= (ifix i) (logcdr j))
+ (< (bfix b) (logcar j))))))
+ :hints(("Goal" :in-theory (enable logcons))))
+
+ (defthmd logcons->-n-strong
+ (implies (integerp j)
+ (equal (> (logcons b i) j)
+ (or (> (ifix i) (logcdr j))
+ (and (= (ifix i) (logcdr j))
+ (> (bfix b) (logcar j))))))
+ :hints(("Goal" :in-theory (enable logcons))))
+
+ (add-to-ruleset ihsext-advanced-thms '(logcons-<-n-strong
+ logcons->-n-strong))
+
+ (defthm logcons-<-constant
+ (implies (and (syntaxp (quotep j))
+ (integerp j))
+ (equal (< (logcons b i) j)
+ (or (< (ifix i) (logcdr j))
+ (and (= (ifix i) (logcdr j))
+ (< (bfix b) (logcar j))))))
+ :hints(("Goal" :in-theory (enable logcons-<-n-strong))))
+
+ (defthm logcons->-constant
+ (implies (and (syntaxp (quotep j))
+ (integerp j))
+ (equal (> (logcons b i) j)
+ (or (> (ifix i) (logcdr j))
+ (and (= (ifix i) (logcdr j))
+ (> (bfix b) (logcar j))))))
+ :hints(("Goal" :in-theory (enable logcons->-n-strong))))
+
+ (defthm logcons-<-logcons
+ (equal (< (logcons a i) (logcons b j))
+ (or (< (ifix i) (ifix j))
+ (and (= (ifix i) (ifix j))
+ (< (bfix a) (bfix b)))))
+ :hints(("Goal" :in-theory (enable logcons-<-n-strong))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcons-<-constant
+ logcons->-constant
+ logcons-<-logcons))
+
+ (defthm logcdr-<=-logcdr
+ (implies (<= (ifix a) (ifix b))
+ (<= (logcdr a) (logcdr b)))
+ :rule-classes (:rewrite :linear))
+
+ (add-to-ruleset ihsext-bounds-thms '(logcdr-<=-logcdr))
+
+ (defthm logcdr-<-const
+ (implies (and (syntaxp (quotep c))
+ (integerp c))
+ (equal (< (logcdr x) c)
+ (< (ifix x) (logcons 0 c))))
+ :hints(("Goal" :in-theory (enable logcons->-n-strong))))
+
+ (defthm logcdr->-const
+ (implies (and (syntaxp (quotep c))
+ (integerp c))
+ (equal (> (logcdr x) c)
+ (> (ifix x) (logcons 1 c))))
+ :hints(("Goal" :in-theory (enable logcons->-n-strong))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcdr-<-const logcdr->-const)))
+
+
+
+(local (in-theory (disable equal-logcons)))
+
+(defsection logbitp**
+
+ (local (in-theory (enable logbitp)))
+
+ (defthmd logbitp-when-not-natp
+ (implies (not (natp i))
+ (equal (logbitp i j)
+ (logbitp 0 j))))
+
+ (local (defthmd logbitp-when-not-integer
+ (implies (not (integerp j))
+ (equal (logbitp i j)
+ (logbitp i 0)))))
+
+ (defthmd logbitp-when-zip
+ (implies (zip j)
+ (equal (logbitp i j)
+ nil))
+ :hints(("Goal" :in-theory (enable logbitp-when-not-integer
+ floor zip))))
+
+ (add-to-ruleset ihsext-bad-type-thms
+ '(logbitp-when-not-natp
+ logbitp-when-zip))
+
+ (local (in-theory (enable logbitp-when-zip
+ logbitp-when-not-natp
+ logcar-when-zip
+ logcdr-when-zip)))
+ (local (in-theory (disable logbitp)))
+
+ (defthmd logbitp**
+ ;; This is a better replacement for logbitp* that doesn't have
unnecessary
+ ;; type restrictions.
+ (equal (logbitp pos i)
+ (cond ((zp pos)
+ (equal (logcar i) 1))
+ (t
+ (logbitp (1- pos) (logcdr i)))))
+ :hints(("Goal" :use ((:instance logbitp*
+ (pos (nfix pos)) (i (ifix i))))))
+ :rule-classes ((:definition :clique (logbitp)
+ :controller-alist ((logbitp t t)))))
+
+ (add-to-ruleset ihsext-redefs '(logbitp**))
+ (add-to-ruleset ihsext-recursive-redefs '(logbitp**))
+
+ (theory-invariant (not (active-runep '(:definition logbitp*)))
+ :key |Use LOGBITP** instead of LOGBITP*|)
+
+ (defun logbitp-ind (pos i)
+ (if (zp pos)
+ (= (logcar i) 1)
+ (logbitp-ind (1- pos) (logcdr i))))
+
+ (defthmd logbitp-induct
+ t
+ :rule-classes ((:induction
+ :pattern (logbitp pos i)
+ :scheme (logbitp-ind pos i))))
+
+ (add-to-ruleset ihsext-inductions '(logbitp-induct))
+
+ (local (in-theory (enable* ihsext-recursive-redefs)))
+
+ (defthm logbitp-of-logcons
+ (equal (logbitp pos (logcons b i))
+ (if (zp pos)
+ (= b 1)
+ (logbitp (1- pos) i)))
+ :hints (("goal" :expand ((logbitp pos (logcons b i)))))))
+
+(defsection integer-length*
+
+ (defthmd integer-length-when-zip
+ (implies (zip i)
+ (equal (integer-length i)
+ 0)))
+
+ (add-to-ruleset ihsext-bad-type-thms '(integer-length-when-zip))
+
+ ;; Integer-length* is already defined in logops-lemmas:
+ ;;(defthm integer-length*
+ ;; (equal (integer-length i)
+ ;; (cond ((zip i) 0)
+ ;; ((equal i -1) 0)
+ ;; (t (1+ (integer-length (logcdr i))))))
+ ;; :rule-classes
+ ;; ((:definition :clique (integer-length)
+ ;; :controller-alist ((integer-length t)))))
+
+
+
+ (add-to-ruleset ihsext-redefs '(integer-length*))
+ (add-to-ruleset ihsext-recursive-redefs '(integer-length*))
+
+ (local (in-theory (enable integer-length*)))
+
+ (defun integer-length-ind (i)
+ (declare (Xargs :measure (integer-length i)))
+ (cond ((zip i) 0)
+ ((= i -1) 0)
+ (t (+ 1 (integer-length-ind (logcdr i))))))
+
+ (defthmd integer-length-induct
+ t
+ :rule-classes ((:induction
+ :pattern (integer-length i)
+ :scheme (integer-length-ind i))))
+
+ (add-to-ruleset ihsext-inductions '(integer-length-induct)))
+
+(defsection logand**
+
+ (local (in-theory (enable logand)))
+
+ (defthmd logand-when-zip
+ (implies (or (zip i) (zip j))
+ (equal (logand i j) 0)))
+
+ (add-to-ruleset ihsext-bad-type-thms '(logand-when-zip))
+
+ (local (in-theory (enable* ihsext-bad-type-thms)))
+ (local (in-theory (disable logand)))
+
+ (defthmd logand**
+ ;; Better than logand* since there are no hyps.
+ (equal (logand i j)
+ (logcons (b-and (logcar i) (logcar j))
+ (logand (logcdr i) (logcdr j))))
+ :hints(("Goal" :use ((:instance logand*
+ (i (ifix i)) (j (ifix j))))))
+ :rule-classes
+ ((:definition :clique (binary-logand)
+ :controller-alist ((binary-logand t t)))))
+
+ (add-to-ruleset ihsext-redefs '(logand**))
+
+ (defthmd logand$
+ (equal (logand i j)
+ (cond ((or (zip i) (zip j)) 0)
+ ((= i -1) j)
+ ((= j -1) i)
+ (t (logcons (b-and (logcar i) (logcar j))
+ (logand (logcdr i) (logcdr j))))))
+ :hints (("goal" :in-theory (disable logcons logcar logcdr
+ logand* logand)
+ :use ((:instance logand*
+ (i (ifix i)) (j (ifix j))))))
+ :rule-classes ((:definition
+ :clique (binary-logand)
+ :controller-alist ((binary-logand t t)))))
+
+ (add-to-ruleset ihsext-recursive-redefs '(logand$))
+
+ (theory-invariant (not (active-runep '(:definition logand*)))
+ :key |Use LOGAND** or LOGAND$ instead of LOGAND*|)
+
+ (local (in-theory (enable integer-length*)))
+
+ (defun logand-ind (i j)
+ (declare (xargs :measure (integer-length i)))
+ (cond ((or (zip i) (zip j)) 0)
+ ((= i -1) j)
+ ((= j -1) i)
+ (t (logcons (b-and (logcar i) (logcar j))
+ (logand-ind (logcdr i) (logcdr j))))))
+
+ (defthmd logand-induct
+ t
+ :rule-classes ((:induction
+ :pattern (logand i j)
+ :scheme (logand-ind i j))))
+
+ (add-to-ruleset ihsext-inductions '(logand-induct))
+
+ (local (in-theory (enable* ihsext-recursive-redefs
+ ihsext-inductions)))
+
+ (defthm logcar-of-logand
+ (equal (logcar (logand x y))
+ (b-and (logcar x) (logcar y)))
+ :hints (("Goal" :expand (logand x y))))
+
+
+ (defthm logcdr-of-logand
+ (equal (logcdr (logand x y))
+ (logand (logcdr x) (logcdr y))))
+
+ (defthm logbitp-of-logand
+ (equal (logbitp a (logand x y))
+ (and (logbitp a x)
+ (logbitp a y))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcar-of-logand
+ logcdr-of-logand
+ logbitp-of-logand))
+
+ (defthmd logand-commutes
+ (equal (logand a b)
+ (logand b a)))
+
+ (add-to-ruleset ihsext-advanced-thms '(logand-commutes))
+
+ (defthm logand-<-0
+ (equal (< (logand x y) 0)
+ (and (< (ifix x) 0)
+ (< (ifix y) 0))))
+
+ (add-to-ruleset ihsext-bounds-thms '(logand-<-0)))
+
+
+
+(defsection lognot**
+
+ (defthmd lognot-when-zip
+ (implies (zip x)
+ (equal (lognot x) -1)))
+
+ (add-to-ruleset ihsext-bad-type-thms '(lognot-when-zip))
+
+ (local (in-theory (enable* ihsext-bad-type-thms)))
+
+ (defthmd lognot**
+ ;; Better than lognot* since there are no hyps.
+ (equal (lognot i)
+ (logcons (b-not (logcar i))
+ (lognot (logcdr i))))
+ :hints(("Goal"
+ :use ((:instance lognot*
+ (i (ifix i))))))
+ :rule-classes ((:definition :clique (lognot)
+ :controller-alist ((lognot t)))))
+
+ (add-to-ruleset ihsext-redefs '(lognot**))
+
+ (defthmd lognot$
+ (equal (lognot i)
+ (cond ((zip i) -1)
+ ((= i -1) 0)
+ (t (logcons (b-not (logcar i))
+ (lognot (logcdr i))))))
+ :hints (("goal" :use ((:instance lognot*
+ (i (ifix i))))
+ :in-theory (disable lognot lognot*)))
+ :rule-classes ((:definition
+ :clique (lognot)
+ :controller-alist ((lognot t)))))
+
+ (add-to-ruleset ihsext-recursive-redefs '(lognot$))
+
+ (theory-invariant (not (active-runep '(:definition lognot*)))
+ :key |Use LOGNOT** or LOGNOT$instead of LOGNOT*|)
+
+ (defthmd lognot-induct
+ t
+ :rule-classes ((:induction
+ :pattern (lognot i)
+ :scheme (integer-length-ind i))))
+
+ (add-to-ruleset ihsext-inductions '(lognot-induct))
+
+
+ (local (in-theory (enable* ihsext-recursive-redefs
+ ihsext-inductions)))
+
+ (defthm logcar-of-lognot
+ (equal (logcar (lognot x))
+ (b-not (logcar x))))
+
+ (defthm logcdr-of-lognot
+ (equal (logcdr (lognot x))
+ (lognot (logcdr x))))
+
+ (defthm logbitp-of-lognot
+ (equal (logbitp a (lognot x))
+ (not (logbitp a x))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcar-of-lognot
+ logcdr-of-lognot
+ logbitp-of-lognot))
+
+ (defthm lognot-<-0
+ (equal (< (lognot x) 0)
+ (not (< (ifix x) 0))))
+
+ (add-to-ruleset ihsext-bounds-thms '(lognot-<-0))
+
+ (defthm lognot-<-const
+ (implies (and (syntaxp (quotep j))
+ (integerp j))
+ (equal (< (lognot i) j)
+ (> (ifix i) (lognot j))))
+ :hints(("Goal" :in-theory (enable lognot)
+ :use ((:instance <-on-others
+ (x (lognot i)) (y j))
+ (:instance <-on-others
+ (x (lognot k)) (y (ifix i)))))))
+
+ (defthm lognot->-const
+ (implies (and (syntaxp (quotep j))
+ (integerp j))
+ (equal (> (lognot i) j)
+ (< (ifix i) (lognot j))))
+ :hints(("Goal" :in-theory (enable lognot)
+ :use ((:instance <-on-others
+ (y (lognot i)) (x j))
+ (:instance <-on-others
+ (y (lognot j)) (x (ifix i)))))))
+
+ (defthm lognot-equal-const
+ (implies (and (syntaxp (quotep j))
+ (integerp j))
+ (equal (equal (lognot i) j)
+ (equal (ifix i) (lognot j))))
+ :hints(("Goal" :in-theory (enable lognot))))
+
+ (add-to-ruleset ihsext-basic-thms '(lognot-<-const
+ lognot->-const
+ lognot-equal-const)))
+
+
+(defsection logior**
+
+ (local (in-theory (enable* logior
+ ihsext-recursive-redefs
+ ihsext-inductions
+ ihsext-advanced-thms)))
+
+ (defthmd logior**
+ ;; Better than logand* since there are no hyps.
+ (equal (logior i j)
+ (logcons (b-ior (logcar i) (logcar j))
+ (logior (logcdr i) (logcdr j))))
+ :rule-classes
+ ((:definition :clique (binary-logior)
+ :controller-alist ((binary-logior t t)))))
+
+ (add-to-ruleset ihsext-redefs '(logior**))
+
+ (defthmd logior$
+ (equal (logior i j)
+ (cond ((zip i) (ifix j))
+ ((zip j) i)
+ ((or (= j -1) (= i -1)) -1)
+ (t (logcons (b-ior (logcar i) (logcar j))
+ (logior (logcdr i) (logcdr j))))))
+ :rule-classes
+ ((:definition :clique (binary-logior)
+ :controller-alist ((binary-logior t t)))))
+
+ (add-to-ruleset ihsext-recursive-redefs '(logior$))
+
+ (theory-invariant (not (active-runep '(:definition logior*)))
+ :key |Use LOGIOR** or LOGIOR$ instead of LOGIOR*|)
+
+ ;; LOGAND-IND is the same induction scheme.
+ (defthmd logior-induct
+ t
+ :rule-classes ((:induction
+ :pattern (logior i j)
+ :scheme (logand-ind i j))))
+
+ (add-to-ruleset ihsext-inductions '(logior-induct))
+
+ (local (in-theory (enable* ihsext-bad-type-thms
+ logior-induct
+ logior$)))
+ (local (in-theory (disable logior)))
+
+ (defthm logcar-of-logior
+ (equal (logcar (logior x y))
+ (b-ior (logcar x) (logcar y)))
+ :hints (("goal" :expand (logior x y))))
+
+
+ (defthm logcdr-of-logior
+ (equal (logcdr (logior x y))
+ (logior (logcdr x) (logcdr y))))
+
+ (defthm logbitp-of-logior
+ (equal (logbitp a (logior x y))
+ (or (logbitp a x)
+ (logbitp a y))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcar-of-logior
+ logcdr-of-logior
+ logbitp-of-logior))
+
+ (defthmd logior-commutes
+ (equal (logior a b)
+ (logior b a)))
+
+ (add-to-ruleset ihsext-advanced-thms '(logior-commutes))
+
+ (defthm logior-<-0
+ (equal (< (logior x y) 0)
+ (or (< (ifix x) 0)
+ (< (ifix y) 0))))
+
+ (add-to-ruleset ihsext-bounds-thms '(logior-<-0))
+
+ (local (in-theory (disable logior-=-0)))
+
+ (defthm logior-equal-0
+ (equal (equal (logior i j) 0)
+ (and (equal (ifix i) 0)
+ (equal (ifix j) 0))))
+
+ (add-to-ruleset ihsext-basic-thms '(logior-equal-0)))
+
+
+(defsection logxor**
+
+ (local (in-theory (enable* logxor logeqv logorc1
+ ihsext-inductions
+ ihsext-advanced-thms)))
+
+ (defthmd logxor**
+ ;; Better than logxor* since there are no hyps.
+ (equal (logxor i j)
+ (logcons (b-xor (logcar i) (logcar j))
+ (logxor (logcdr i) (logcdr j))))
+ :rule-classes
+ ((:definition :clique (binary-logxor)
+ :controller-alist ((binary-logxor t t)))))
+
+ (add-to-ruleset ihsext-redefs '(logxor**))
+
+ (local (in-theory (enable* ihsext-recursive-redefs)))
+ (local (in-theory (disable bfix zbp)))
+
+ (defthmd logxor$
+ ;; Better than logxor* since there are no hyps.
+ (equal (logxor i j)
+ (cond ((zip i) (ifix j))
+ ((zip j) (ifix i))
+ ((= i -1) (lognot j))
+ ((= j -1) (lognot i))
+ (t (logcons (b-xor (logcar i) (logcar j))
+ (logxor (logcdr i) (logcdr j))))))
+ :rule-classes
+ ((:definition :clique (binary-logxor)
+ :controller-alist ((binary-logxor t t)))))
+
+ (add-to-ruleset ihsext-recursive-redefs '(logxor$))
+
+ (theory-invariant (not (active-runep '(:definition logxor*)))
+ :key |Use LOGXOR** or LOGXOR$ instead of LOGXOR*|)
+
+ (defthm logxor-induct
+ t
+ :rule-classes ((:induction
+ :pattern (logxor i j)
+ :scheme (logand-ind i j))))
+
+ (add-to-ruleset ihsext-inductions '(logxor-induct))
+
+ (local (in-theory (enable* ihsext-bad-type-thms
+ logxor-induct
+ logxor$)))
+ (local (in-theory (disable logxor)))
+
+ (defthm logcar-of-logxor
+ (equal (logcar (logxor x y))
+ (b-xor (logcar x) (logcar y)))
+ :hints (("goal" :expand (logxor x y))))
+
+
+ (defthm logcdr-of-logxor
+ (equal (logcdr (logxor x y))
+ (logxor (logcdr x) (logcdr y))))
+
+ (defthm logbitp-of-logxor
+ (equal (logbitp a (logxor x y))
+ (xor (logbitp a x)
+ (logbitp a y))))
+
+ (add-to-ruleset ihsext-basic-thms '(logcar-of-logxor
+ logcdr-of-logxor
+ logbitp-of-logxor))
+
+ (defthmd logxor-commutes
+ (equal (logxor a b)
+ (logxor b a)))
+
+ (add-to-ruleset ihsext-advanced-thms '(logxor-commutes))
+
+
+ (defthm logxor-<-0
+ (equal (< (logxor x y) 0)
+ (xor (< (ifix x) 0)
+ (< (ifix y) 0))))
+
+ (add-to-ruleset ihsext-bounds-thms '(logxor-<-0))
+
+ (defthm logxor-equal-0
+ (equal (equal (logxor x y) 0)
+ (equal (ifix x) (ifix y))))
+
+ (add-to-ruleset ihsext-basic-thms '(logxor-equal-0)))
+
+
+
+(defsection ash*
+ ;; Ash* is already defined in logops-lemmas.
+ ;;(defthmd ash*
+ ;; (equal (ash i count)
+ ;; (cond ((zip count) (ifix i))
+ ;; ((< count 0)
+ ;; (ash (logcdr i) (1+ count)))
+ ;; (t (logcons 0 (ash i (1- count))))))
+ ;; :rule-classes ((:definition :clique (ash)
+ ;; :controller-alist ((ash nil t)))))
+
+ (add-to-ruleset ihsext-recursive-redefs '(ash*))
+ (add-to-ruleset ihsext-redefs '(ash*))
+
+ (defun ash-ind (i count)
+ (declare (xargs :measure (abs (ifix count))))
+ (cond ((zip count) (ifix i))
+ ((< count 0)
+ (ash-ind (logcdr i) (1+ count)))
+ (t (logcons 0 (ash-ind i (1- count))))))
+
+ (defthmd ash-induct
+ t
+ :rule-classes ((:induction
+ :pattern (ash i count)
+ :scheme (ash-ind i count))))
+
+ (add-to-ruleset ihsext-inductions '(ash-induct))
+
+ (in-theory (disable ash))
+
+ (local (in-theory (enable* ihsext-inductions
+ ihsext-recursive-redefs)))
+
+ (defthmd ash-when-zip-i
+ (implies (zip i)
+ (equal (ash i count) 0)))
+
+ (add-to-ruleset ihsext-basic-thms '(ash-when-zip-i))
+
+ (defthmd ash-when-zip-count
+ (implies (zip count)
+ (equal (ash i count)
+ (ifix i))))
+
+ (add-to-ruleset ihsext-bad-type-thms '(ash-when-zip-count))
+
+ (defthmd logcar-of-ash
+ (equal (logcar (ash i count))
+ (if (<= (ifix count) 0)
+ (if (logbitp (- count) i) 1 0)
+ 0))
+ :hints (("goal" :induct t
+ :do-not-induct t
+ :expand ((logbitp (- count) i)))))
+
+ (add-to-ruleset ihsext-advanced-thms '(logcar-of-ash))
+
+ (local (in-theory (enable logcar-of-ash)))
+
+ (defthm logcdr-of-ash
+ (equal (logcdr (ash i count))
+ (ash i (1- (ifix count)))))
+
+ (defun logbitp-of-ash-ind (pos i count)
+ (declare (xargs :measure (abs (ifix count))))
+ (cond ((or (zp pos)
+ (zip count)) (list pos i))
+ ((< count 0)
+ (logbitp-of-ash-ind pos (logcdr i) (1+ count)))
+ (t (logbitp-of-ash-ind (1- pos) i (1- count)))))
+
+
+ (defthm logbitp-of-ash
+ (equal (logbitp pos (ash i count))
+ (and (<= (ifix count) (nfix pos))
+ (logbitp (- (nfix pos) (ifix count)) i)))
+ :hints (("goal" :induct (logbitp-of-ash-ind
+ pos i count)
+ :do-not-induct t)))
+
+ (add-to-ruleset ihsext-basic-thms '(logcdr-of-ash
+ logbitp-of-ash))
+
+
+ (defthm ash-<-0
+ (equal (< (ash i count) 0)
+ (< (ifix i) 0)))
+
+ (defthmd ash-<-0-linear
+ (implies (and (integerp i)
+ (< i 0))
+ (< (ash i count) 0))
+ :rule-classes :linear)
+
+ (defthmd ash->=-0-linear
+ (implies (or (not (integerp i))
+ (<= 0 i))
+ (<= 0 (ash i count)))
+ :rule-classes :linear)
+
+ (add-to-ruleset ihsext-bounds-thms '(ash-<-0
+ ash-<-0-linear
+ ash->=-0-linear)))
+
+(defsection expt
+
+ (defthmd expt-2-is-ash
+ (implies (natp n)
+ (equal (expt 2 n)
+ (ash 1 n)))
+ :hints(("Goal" :in-theory (enable ash floor))))
+
+ (add-to-ruleset ihsext-arithmetic '(expt-2-is-ash)))
+
+
+
+(defsection unsigned-byte-p**
+
+
+ (local (in-theory (enable* ihsext-recursive-redefs
+ ihsext-inductions)))
+
+ (local (in-theory (enable expt-2-is-ash)))
+
+ (defthmd unsigned-byte-p**
+ (equal (unsigned-byte-p bits x)
+ (and (integerp x)
+ (natp bits)
+ (cond ((= x 0) t)
+ ((or (= bits 0) (= x -1)) nil)
+ (t (unsigned-byte-p (1- bits) (logcdr x))))))
+ :rule-classes ((:definition
+ :clique (unsigned-byte-p)
+ :controller-alist ((unsigned-byte-p t t)))))
+
+ (local (in-theory (enable unsigned-byte-p**)))
+ (local (in-theory (disable unsigned-byte-p)))
+
+ (add-to-ruleset ihsext-recursive-redefs '(unsigned-byte-p**))
+
+ (defun unsigned-byte-p-ind (bits x)
+ (and (integerp x)
+ (natp bits)
+ (cond ((= x 0) t)
+ ((or (= bits 0) (= x -1)) nil)
+ (t (unsigned-byte-p-ind (1- bits) (logcdr x))))))
+
+ (defthm unsigned-byte-p-induct
+ t
+ :rule-classes ((:induction
+ :pattern (unsigned-byte-p bits x)
+ :scheme (unsigned-byte-p-ind bits x))))
+
+ (defthmd unsigned-byte-p-incr
+ (implies (and (unsigned-byte-p a x)
+ (natp b)
+ (<= a b))
+ (unsigned-byte-p b x)))
+
+ (local (in-theory (enable unsigned-byte-p-incr)))
+
+ (defthmd unsigned-byte-p-logcons
+ (implies (and (unsigned-byte-p a x)
+ (natp b)
+ (<= a (1- b)))
+ (unsigned-byte-p b (logcons bit x)))
+ :hints (("goal" :expand ((unsigned-byte-p b (logcons bit x))))))
+
+ (defthmd unsigned-byte-p-logcdr
+ (implies (and (unsigned-byte-p a x)
+ (natp b)
+ (<= a (1+ b)))
+ (unsigned-byte-p b (logcdr x))))
+
+ (add-to-ruleset ihsext-bounds-thms '(unsigned-byte-p-incr
+ unsigned-byte-p-logcons
+ unsigned-byte-p-logcdr))
+
+ (local (in-theory (disable unsigned-byte-p-logand
+ unsigned-byte-p-logior
+ logior-=-0)))
+
+ (defthmd unsigned-byte-p-logand-fix
+ (implies (or (unsigned-byte-p b x)
+ (unsigned-byte-p b y))
+ (unsigned-byte-p b (logand x y))))
+
+ (defun unsigned-byte-p-logior-ind (b x y)
+ (cond ((zp b) (list x y))
+ (t (unsigned-byte-p-logior-ind
+ (1- b) (logcdr x) (logcdr y)))))
+
+ (defthmd unsigned-byte-p-logior-fix
+ (equal (unsigned-byte-p b (logior x y))
+ (and (unsigned-byte-p b (ifix x))
+ (unsigned-byte-p b (ifix y))))
+ :hints (("goal" :induct (unsigned-byte-p-logior-ind b x y))))
+
+ (add-to-ruleset ihsext-basic-thms '(unsigned-byte-p-logand-fix
+ unsigned-byte-p-logior-fix)))
+
+
+(defsection signed-byte-p**
+
+ (local (in-theory (enable* ihsext-recursive-redefs
+ ihsext-inductions
+ ihsext-bounds-thms
+ ihsext-advanced-thms
+ ihsext-arithmetic
+ )))
+
+ (defthmd minus-to-lognot
+ (implies (integerp x)
+ (equal (- x)
+ (+ 1 (lognot x))))
+ :hints(("Goal" :in-theory (enable lognot)))
+ :rule-classes ((:rewrite :backchain-limit-lst (0))))
+
+ (defthmd elim-plus-one
+ (implies (and (integerp x)
+ (integerp y))
+ (equal (< x (+ 1 y))
+ (<= x y)))
+ :rule-classes ((:rewrite :backchain-limit-lst (0 0))))
+
+ (add-to-ruleset ihsext-advanced-thms '(minus-to-lognot
+ elim-plus-one))
+
+ (local (in-theory (enable minus-to-lognot elim-plus-one)))
+
+ (local (defthm ash-zero-fwd
+ (implies (and (equal (ash x bits) 0)
+ (not (zip x)))
+ (< bits 0))
+ :rule-classes :forward-chaining))
+
+
+ (defthmd signed-byte-p**
+ (equal (signed-byte-p bits x)
+ (and (integerp x)
+ (natp bits)
+ (cond ((= bits 0) nil)
+ ((or (= x 0) (= x -1)) t)
+ (t (signed-byte-p (1- bits) (logcdr x))))))
+ :rule-classes ((:definition
+ :clique (signed-byte-p)
+ :controller-alist ((signed-byte-p t t)))))
+
+ (local (in-theory (enable signed-byte-p**)))
+ (local (in-theory (disable signed-byte-p)))
+
+ (add-to-ruleset ihsext-recursive-redefs '(signed-byte-p**))
+
+ (defun signed-byte-p-ind (bits x)
+ (and (integerp x)
+ (natp bits)
+ (cond ((= bits 0) nil)
+ ((or (= x 0) (= x -1)) t)
+ (t (signed-byte-p-ind (1- bits) (logcdr x))))))
+
***The diff for this file has been truncated for email.***
=======================================
--- /trunk/centaur/aig/base.lisp Tue Feb 28 11:49:40 2012
+++ /trunk/centaur/aig/base.lisp Thu Mar 1 15:20:35 2012
@@ -216,6 +216,21 @@
(aig-env-lookup-missing-action :warn))
+;;(defsection aig-cases
+;; :parents (aig)
+;; :short "Control-flow macro to split into cases on what kind of AIG you
have
+;;encountered."
+;; :long "@(def aig-cases)"
+
+;; (defmacro aig-cases (x &key true false var inv and)
+;; `(let ((aig-cases-var ,x))
+;; (cond
+;; ((eq aig-cases-var t) ,true)
+;; ((eq aig-cases-var nil) ,false)
+;; ((atom aig-cases-var) ,var)
+;; ((eq (cdr aig-cases-var) nil) ,inv)
+;; (t ,and)))))
+
(defsection aig-cases
:parents (aig)
:short "Control-flow macro to split into cases on what kind of AIG you
have
=======================================
--- /trunk/centaur/bitops/bitsets.lisp Mon Feb 13 11:29:10 2012
+++ /trunk/centaur/bitops/bitsets.lisp Thu Mar 1 15:20:35 2012
@@ -415,7 +415,8 @@
(* 32 (+ 1 slice))
x))))
:hints(("Goal"
- :in-theory (disable bits-between-of-increment-right-index)))))
+ :in-theory (e/d (loghead)
+ (bits-between-of-increment-right-index))))))
@@ -533,6 +534,7 @@
(bignum-extract x slice)
acc))))
+ (local (in-theory (enable loghead)))
(defthm ttag-bitset-members-aux-redef
(implies (and (natp slice)
(integerp x))
=======================================
--- /trunk/centaur/bitops/ihs-extensions.lisp Mon Apr 18 06:40:23 2011
+++ /trunk/centaur/bitops/ihs-extensions.lisp Thu Mar 1 15:20:35 2012
@@ -27,30 +27,16 @@
; typically be only locally included since it makes various changes to the
; global theory such as disabling floor, mod, expt, etc.
-(include-book "ihs/logops-lemmas" :dir :system)
+(include-book "ihsext-basics")
(include-book "defaults")
(include-book "integer-length")
-(local (include-book "arithmetic-3/extra/top-ext" :dir :system))
+; (local (include-book "arithmetic-3/extra/top-ext" :dir :system))
(local (include-book "equal-by-logbitp"))
-(local (in-theory (disable expt-between-one-and-two)))
+; (local (in-theory (disable expt-between-one-and-two)))
-(defconst *ihs-extensions-disables*
- '(floor mod expt ash evenp oddp
- logbitp logior logand lognot logxor
- logcons logcar logcdr
- integer-length))
-
-(make-event
- (prog2$ (cw "Note (from ihs-extensions): disabling ~&0.~%~%"
- *ihs-extensions-disables*)
- '(value-triple :invisible))
- :check-expansion t)
-
-(in-theory (set-difference-theories (current-theory :here)
- *ihs-extensions-disables*))
(local (defun dec-induct (n)
@@ -86,7 +72,7 @@
(defthm ash-zero
(equal (ash x 0)
(ifix x))
- :hints(("Goal" :in-theory (enable ash))))
+ :hints(("Goal" :in-theory (enable ash* ash-induct))))
(defthm ash-1-removal
(equal (ash 1 n)
@@ -95,126 +81,39 @@
(expt 2 n)
0)
1))
- :hints(("Goal" :in-theory (enable ash))))
+ :hints(("Goal" :in-theory (enable expt-2-is-ash ash*))))
+
+(theory-invariant (not (and (active-runep '(:rewrite ash-1-removal))
+ (active-runep '(:rewrite expt-2-is-ash)))))
(defthm logcar-possibilities
(or (equal (logcar a) 0)
(equal (logcar a) 1))
:rule-classes ((:forward-chaining :trigger-terms ((logcar a))))
- :hints(("Goal" :in-theory (enable logcar))))
+ :hints(("Goal" :use logcar-type)))
(defthm |(logbitp 0 x)|
(equal (logbitp 0 x)
(equal (logcar x) 1))
- :hints(("Goal" :in-theory (enable logbitp logcar oddp evenp))))
+ :hints(("Goal" :in-theory (enable logbitp**))))
(encapsulate
()
;; The following theorems improve logbitp-0-minus-1 by eliminating
;; the unnecessary hyps.
- (local (defthm l0
- (implies (zp a)
- (not (logbitp a 0)))
- :hints(("Goal" :in-theory (enable logbitp)))))
-
- (local (defthm l1
- (implies (zp a)
- (logbitp a -1))
- :hints(("Goal" :in-theory (enable logbitp)))))
-
(defthm |(logbitp a 0)|
- (equal (logbitp a 0) nil)
- :hints(("Goal"
- :induct (dec-induct a)
- :in-theory (enable logbitp*))))
+ (equal (logbitp a 0) nil))
(defthm |(logbitp a -1)|
(equal (logbitp a -1) t)
:hints(("Goal"
:induct (dec-induct a)
- :in-theory (enable logbitp*))))
+ :in-theory (enable logbitp**))))
(in-theory (disable logbitp-0-minus-1)))
-(defthmd logbitp**
- ;; This is a better replacement for logbitp* that doesn't have
unnecessary
- ;; type restrictions.
- (equal (logbitp pos i)
- (cond ((zp pos)
- (equal (logcar i) 1))
- (t
- (logbitp (1- pos) (logcdr i)))))
- :rule-classes ((:definition :clique (logbitp) :controller-alist
((logbitp t t))))
- :hints(("Goal" :use ((:instance logbitp*)))))
-
-(theory-invariant (not (active-runep '(:definition logbitp*)))
- :key |Use LOGBITP** instead of LOGBITP*|)
-
-
-(defthmd logand**
- ;; Better than logand* since there are no hyps.
- (equal (logand i j)
- (logcons (b-and (logcar i) (logcar j))
- (logand (logcdr i) (logcdr j))))
- :rule-classes
- ((:definition :clique (binary-logand)
- :controller-alist ((binary-logand t t))))
- :hints(("Goal" :use ((:instance logand*)))))
-
-(theory-invariant (not (active-runep '(:definition logand*)))
- :key |Use LOGAND** instead of LOGAND*|)
-
-
-
-(defthmd logior**
- ;; Better than logand* since there are no hyps.
- (equal (logior i j)
- (logcons (b-ior (logcar i) (logcar j))
- (logior (logcdr i) (logcdr j))))
- :rule-classes
- ((:definition :clique (binary-logior)
- :controller-alist ((binary-logior t t))))
- :hints(("Goal" :use ((:instance logior*)))))
-
-(theory-invariant (not (active-runep '(:definition logior*)))
- :key |Use LOGIOR** instead of LOGIOR*|)
-
-
-
-(defthmd logxor**
- ;; Better than logxor* since there are no hyps.
- (equal (logxor i j)
- (logcons (b-xor (logcar i) (logcar j))
- (logxor (logcdr i) (logcdr j))))
- :rule-classes
- ((:definition :clique (binary-logxor)
- :controller-alist ((binary-logxor t t))))
- :hints(("Goal"
- :in-theory (e/d (logxor) (logmaskp))
- :use ((:instance logxor*)))))
-
-(theory-invariant (not (active-runep '(:definition logxor*)))
- :key |Use LOGXOR** instead of LOGXOR*|)
-
-
-(defthmd lognot**
- ;; Better than lognot* since there are no hyps.
- (equal (lognot i)
- (logcons (b-not (logcar i))
- (lognot (logcdr i))))
- :rule-classes ((:definition :clique (lognot)
- :controller-alist ((lognot t))))
- :hints(("Goal"
- :in-theory (enable lognot)
- :use ((:instance lognot*)))))
-
-(theory-invariant (not (active-runep '(:definition lognot*)))
- :key |Use LOGNOT** instead of LOGNOT*|)
-
-
-
(defthm logbitp-upper-bound
(implies (and (logbitp a x)
@@ -226,77 +125,45 @@
:induct (dec-logcdr-induct a x)
:in-theory (enable logbitp**))))
-(defthm logcar-of-logior
- (equal (logcar (logior x y))
- (if (or (= (logcar x) 1)
- (= (logcar y) 1))
- 1
- 0))
- :hints(("Goal"
- :expand (logior x y)
- :in-theory (enable logior**))))
-
-(defthm logbitp-of-logior
- (equal (logbitp a (logior x y))
- (or (logbitp a x)
- (logbitp a y)))
- :hints(("Goal"
- :induct (dec-logcdr-logcdr-induct a x y)
- :in-theory (enable logior** logbitp**))))
-
-(defthm logcar-of-logand
- (equal (logcar (logand x y))
- (if (and (= (logcar x) 1)
- (= (logcar y) 1))
- 1
- 0))
- :hints(("Goal"
- :expand (logand x y)
- :in-theory (enable logand**))))
-
-(defthm logbitp-of-logand
- (equal (logbitp a (logand x y))
- (and (logbitp a x)
- (logbitp a y)))
- :hints(("Goal"
- :induct (dec-logcdr-logcdr-induct a x y)
- :in-theory (enable logand** logbitp**))))
-
-(defthm logcar-of-lognot
- (equal (logcar (lognot x))
- (if (= (logcar x) 1)
- 0
- 1))
- :hints(("Goal" :in-theory (enable lognot**))))
-
-(defthm logbitp-of-lognot
- (equal (logbitp a (lognot x))
- (not (logbitp (nfix a) x)))
- :hints(("Goal"
- :induct (dec-logcdr-induct a x)
- :in-theory (enable lognot** logbitp**))))
-
-(defthm logcar-of-logxor
- (equal (logcar (logxor x y))
- (if (or (and (= (logcar x) 1)
- (= (logcar y) 1))
- (and (= (logcar x) 0)
- (= (logcar y) 0)))
- 0
- 1))
- :hints(("Goal"
- :expand (logxor x y)
- :in-theory (enable logxor**))))
-
-(defthm logbitp-of-logxor
- (equal (logbitp a (logxor x y))
- (xor (logbitp a x)
- (logbitp a y)))
- :hints(("Goal"
- :induct (dec-logcdr-logcdr-induct a x y)
- :in-theory (enable logxor** logbitp**))))
-
-
+;; This was slightly rephrased in ihsext-basics.lisp
+;;(defthm logcar-of-logior
+;; (equal (logcar (logior x y))
+;; (if (or (= (logcar x) 1)
+;; (= (logcar y) 1))
+;; 1
+;; 0))
+;; :hints(("Goal"
+;; :expand (logior x y)
+;; :in-theory (enable logior**))))
+
+;;(defthm logcar-of-logand
+;; (equal (logcar (logand x y))
+;; (if (and (= (logcar x) 1)
+;; (= (logcar y) 1))
+;; 1
+;; 0))
+;; :hints(("Goal"
+;; :expand (logand x y)
+;; :in-theory (enable logand**))))
+
+;;(defthm logcar-of-lognot
+;; (equal (logcar (lognot x))
+;; (if (= (logcar x) 1)
+;; 0
+;; 1))
+;; :hints(("Goal" :in-theory (enable lognot**))))
+
+;;(defthm logcar-of-logxor
+;; (equal (logcar (logxor x y))
+;; (if (or (and (= (logcar x) 1)
+;; (= (logcar y) 1))
+;; (and (= (logcar x) 0)
+;; (= (logcar y) 0)))
+;; 0
+;; 1))
+;; :hints(("Goal"
+;; :expand (logxor x y)
+;; :in-theory (enable logxor**))))
(defthm |(< (lognot a) 0)|
(equal (< (lognot a) 0)
@@ -453,135 +320,20 @@
-
-(defthm |(integerp (expt x n))|
- (implies (and (integerp n)
- (integerp x)
- (< 1 x))
- (equal (integerp (expt x n))
- (<= 0 n)))
- :hints(("Goal" :in-theory (enable expt))))
-
-
-(defthm |(logcdr (expt 2 n))|
- (equal (logcdr (expt 2 n))
- (if (posp n)
- (expt 2 (1- n))
- 0))
- :hints(("Goal" :in-theory (enable logcdr))))
-
-(defthm |(logcar (expt 2 n))|
- (equal (logcar (expt 2 n))
- (if (= (ifix n) 0)
- 1
- 0))
- :hints(("Goal" :in-theory (enable logcar))))
-
-(defthm logand-with-2^n-is-logbitp
- (implies (natp n)
- (equal (equal (logand x (expt 2 n)) 0)
- (not (logbitp n x))))
- :rule-classes ((:rewrite)
- (:rewrite :corollary
- (implies (natp n)
- (equal (equal (logand (expt 2 n) x) 0)
- (not (logbitp n x))))))
- :hints(("Goal"
- :in-theory (enable logand** logbitp**)
- :induct (dec-logcdr-induct n x))))
-
-
(encapsulate
()
- (local (in-theory (disable not-integerp-4a not-integerp-4b
- not-integerp-3a not-integerp-3b
- not-integerp-2a not-integerp-2b
- not-integerp-1a not-integerp-1b
- nintegerp-/
- (:type-prescription floor-zero . 1)
- (:type-prescription floor-zero . 2)
- (:type-prescription floor-zero . 3)
- (:rewrite floor-zero . 4)
- floor-non-negative-integerp-type-prescription
-
expt-type-prescription-nonpositive-base-odd-exponent
-
expt-type-prescription-negative-base-odd-exponent)))
- (local (defthm l0
- (implies (and (natp a)
- (integerp n)
- (< n 0))
- (equal (logbitp a (ash x n))
- (logbitp (- a n) x)))
- :hints(("Goal" :in-theory (enable logbitp ash)))))
-
- (local (defthm l1
- (implies (and (natp a)
- (natp n))
- (equal (logbitp a (ash x n))
- (if (< a n)
- nil
- (logbitp (- a n) x))))
- :hints(("Goal" :in-theory (enable logbitp ash oddp evenp)))))
-
- (defthm logbitp-of-ash
- (implies (natp a)
- (equal (logbitp a (ash x n))
- (cond ((or (not (integerp n))
- (= n 0))
- (logbitp a x))
- ((< n 0)
- (logbitp (- a n) x))
- ((< a n)
- nil)
- (t
- (logbitp (- a n) x)))))
- :hints(("Goal" :use ((:instance l0)
- (:instance l1))))))
-
-
-(encapsulate
- ()
- (local (defthm l0
- (implies (natp a)
- (equal (logbitp a (expt 2 a))
- t))
- :hints(("Goal"
- :induct (dec-induct a)
- :in-theory (enable logbitp**)))))
-
- (local (defthm l1
- (implies (and (not (equal a b))
- (natp a)
- (natp b))
- (not (logbitp a (expt2 b))))
- :hints(("Goal"
- :in-theory (enable logbitp**)
- :expand (logbitp a (expt 2 b))
- :induct (dec-dec-induct a b)))))
+
+ (local (in-theory (e/d* (ihsext-inductions
+ ihsext-recursive-redefs
+ expt-2-is-ash)
+ (ash-1-removal))))
(defthm logbitp-of-expt-2
(implies (natp b)
(equal (logbitp a (expt 2 b))
- (equal (nfix a) b)))
- :hints(("Goal" :use ((:instance l0)
- (:instance l1))))))
+ (equal (nfix a) b)))))
-
-
-(defthm |(mod a (expt 2 n)) < (expt 2 n)|
- (implies (integerp a)
- (< (mod a (expt 2 n))
- (expt 2 n)))
- :rule-classes ((:rewrite) (:linear)))
-
-(defthm expt-2-monotonic
- (implies (and (< a b)
- (integerp a)
- (integerp b))
- (< (expt 2 a)
- (expt 2 b)))
- :rule-classes ((:rewrite) (:linear)))
-
(defthm expt-2-lower-bound-by-logbitp
(implies (and (logbitp n x)
(natp n)
@@ -589,7 +341,11 @@
(<= (expt 2 n)
x))
:rule-classes ((:rewrite) (:linear))
- :hints(("Goal" :in-theory (enable logbitp evenp oddp))))
+ :hints(("Goal" :in-theory (e/d* (ihsext-arithmetic
+ ihsext-recursive-redefs
+ ihsext-inductions)
+ (ash-1-removal)))))
+
(defthmd logbitp-when-too-small
(implies (and (< a (expt 2 n))
@@ -601,24 +357,10 @@
(encapsulate
()
- (local (defthm l0
- (implies (and (< bit n)
- (natp bit)
- (integerp a)
- (natp n))
- (equal (logbitp bit (mod a (expt 2 n)))
- (logbitp bit a)))
- :hints(("Goal"
- :in-theory (enable logbitp evenp oddp)
- :nonlinearp t))))
-
- (local (defthm l1
- (implies (and (<= n bit)
- (natp bit)
- (integerp a)
- (natp n))
- (equal (logbitp bit (mod a (expt 2 n)))
- nil))))
+
+ (local (in-theory (e/d* (ihsext-arithmetic)
+ (ash-1-removal))))
+
(defthm |(logbitp bit (mod a (expt 2 n)))|
(implies (and (natp bit)
@@ -630,18 +372,6 @@
nil)))))
-(defthm |(logbitp n (+ (expt 2 n) a))|
- (implies (and (integerp a)
- (natp n))
- (equal (logbitp n (+ (expt 2 n) a))
- (not (logbitp n a))))
- :rule-classes ((:rewrite)
- (:rewrite :corollary
- (implies (and (integerp a)
- (natp n))
- (equal (logbitp n (+ a (expt 2 n)))
- (not (logbitp n a))))))
- :hints(("Goal" :in-theory (enable logbitp evenp oddp))))
(defthm normalize-logbitp-when-mods-equal
(implies (and (equal (mod a (expt 2 n))
@@ -660,6 +390,13 @@
(:instance |(logbitp bit (mod a (expt 2 n)))|
(a b))))))
+(defthmd integer-length-of-loghead
+ (<= (integer-length (loghead k a))
+ (nfix k))
+ :hints(("Goal" :in-theory (enable* ihsext-inductions
+ ihsext-recursive-redefs)))
+ :rule-classes :linear)
+
(defthm smaller-mods-are-still-the-same
(implies (and (equal (mod a (expt 2 n))
(mod b (expt 2 n)))
@@ -671,48 +408,93 @@
(equal (equal (mod a (expt 2 k))
(mod b (expt 2 k)))
t))
- :hints(("Goal"
- :in-theory (disable mod-force-equal-ext
- mod-zero cancel-mod-+
- mod-negative mod-positive
- mod-nonpositive
- mod-does-nothing)
- :use ((:functional-instance
- equal-by-logbitp
- (logbitp-hyp (lambda ()
- (and (equal (mod b (expt 2 n))
- (mod a (expt 2 n)))
- (< k n)
- (integerp a)
- (integerp b)
- (natp k)
- (natp n))))
- (logbitp-lhs (lambda () (mod b (expt 2 k))))
- (logbitp-rhs (lambda () (mod a (expt 2 k)))))))))
-
-(defthm |(2^n + a mod 2^n) when a < 2^n+1|
- (implies (and (case-split (< a (expt 2 (+ 1 n))))
- (natp a)
- (natp n))
- (equal (+ (expt 2 n) (mod a (expt 2 n)))
- (cond ((< a (expt 2 n))
- (+ (expt 2 n) a))
- ((< a (expt 2 (+ 1 n)))
- a))))
- :hints(("Goal" :nonlinearp t)))
-
-
-(defthm |(2^n + a mod 2^n) when 2^n+1 <= a, a[n] = 1|
- (implies (and (case-split (not (< a (expt 2 (+ 1 n)))))
- (logbitp n a)
- (natp a)
- (natp n))
- (equal (+ (expt 2 n) (mod a (expt 2 n)))
- (mod a (expt 2 (+ 1 n)))))
- :hints(("goal"
- :nonlinearp t
- :in-theory (e/d (logbitp oddp evenp)
- (nintegerp-expt)))))
+ :hints(("Goal" :in-theory (e/d* (ihsext-arithmetic
+ integer-length-of-loghead
+ ihsext-inductions
+ ihsext-recursive-redefs)
+ (ash-1-removal)))))
+
+(defthm +-of-logcons-with-cin
+ (implies (bitp cin)
+ (equal (+ cin
+ (logcons b1 r1)
+ (logcons b2 r2))
+ (logcons (b-xor cin (b-xor b1 b2))
+ (+ (b-ior (b-and cin b1)
+ (b-ior (b-and cin b2)
+ (b-and b1 b2)))
+ (ifix r1)
+ (ifix r2)))))
+ :hints(("Goal" :in-theory (enable logcons))))
+
+(defthm +-of-logcons
+ (equal (+ (logcons b1 r1)
+ (logcons b2 r2))
+ (logcons (b-xor b1 b2)
+ (+ (b-and b1 b2)
+ (ifix r1)
+ (ifix r2))))
+ :hints(("Goal" :in-theory (e/d (logcons) (equal-logcons)))))
+
+(encapsulate nil
+
+ ;;(local (include-book "arithmetic-3/extra/top-ext" :dir :system))
+ ;;(local (in-theory (disable expt-between-one-and-two
+ ;; exponents-add-for-nonneg-exponents)))
+
+ (local (include-book "arithmetic/top-with-meta" :dir :system))
+ (local (in-theory (e/d* (ihsext-arithmetic
+ ihsext-inductions
+ ihsext-recursive-redefs
+ logcons-<-n-strong
+ logcons->-n-strong)
+ (ash-1-removal
+ exponents-add-for-nonneg-exponents
+ expt))))
+
+ (defthm |(2^n + a mod 2^n) when a < 2^n+1|
+ (implies (and (case-split (< a (expt 2 (+ 1 n))))
+ (natp a)
+ (natp n))
+ (equal (+ (expt 2 n) (mod a (expt 2 n)))
+ (cond ((< a (expt 2 n))
+ (+ (expt 2 n) a))
+ ((< a (expt 2 (+ 1 n)))
+ a))))
+ :hints(("Goal" :induct (logbitp-ind n a)
+ :in-theory (disable ash*)
+ :do-not-induct t)
+ (and stable-under-simplificationp
+ '(:in-theory (enable ash*)))))
+
+ (defthm small-mods
+ (implies (integerp n)
+ (and (equal (mod n 1) 0)
+ (equal (mod n 2) (logcar n))))
+ :hints (("goal" :use ((:instance mod-to-loghead (n 0) (i n))
+ (:instance mod-to-loghead (n 1) (i n)))
+ :in-theory (disable mod-to-loghead))))
+
+ (theory-invariant (not (and (active-runep '(:rewrite small-mods))
+ (active-runep '(:definition logcar)))))
+
+ (defthm |(2^n + a mod 2^n) when 2^n+1 <= a, a[n] = 1|
+ (implies (and (case-split (not (< a (expt 2 (+ 1 n)))))
+ (logbitp n a)
+ (natp a)
+ (natp n))
+ (equal (+ (expt 2 n) (mod a (expt 2 n)))
+ (mod a (expt 2 (+ 1 n)))))
+ :hints(("Goal" :induct (logbitp-ind n a)
+ :in-theory (disable ash*)
+ :do-not-induct t)
+ (and stable-under-simplificationp
+ '(:in-theory (enable ash*))))))
+
+(in-theory (disable small-mods))
+(local (in-theory (enable small-mods)))
+
+
(defthm upper-bound-of-logior-for-naturals
(implies (and (< x (expt 2 n))
@@ -743,3 +525,121 @@
(i x)
(j y)
(size n))))))
+
+
+
+
+
+(encapsulate nil
+ (local (include-book "arithmetic-3/extra/top-ext" :dir :system))
+
+ (defthm |(integerp (expt x n))|
+ (implies (and (integerp x)
+ (< 1 x))
+ (equal (integerp (expt x n))
+ (<= 0 (ifix n))))
+ :hints(("Goal" :in-theory (enable expt)))))
+
+
+(defthm |(logcdr (expt 2 n))|
+ (equal (logcdr (expt 2 n))
+ (if (posp n)
+ (expt 2 (1- n))
+ 0))
+ :hints(("Goal" :in-theory (e/d* (ihsext-arithmetic)
+ (ash-1-removal))
+ :cases ((= 0 n)
+ (and (not (equal 0 n))
+ (integerp n))))))
+
+(defthm |(logcar (expt 2 n))|
+ (equal (logcar (expt 2 n))
+ (if (= (ifix n) 0)
+ 1
+ 0))
+ :hints(("Goal" :in-theory (e/d* (ihsext-arithmetic
+ logcar-of-ash)
+ (ash-1-removal))
+ :cases ((<= 0 n)
+ (and (< n 0)
+ (integerp n))))))
+
+
+(encapsulate
+ nil
+ (local (defthm expt->=-0
+ (implies (and (rationalp b)
+ (<= 0 b))
+ (<= 0 (expt b x)))
+ :hints(("Goal" :in-theory (enable expt)))
+ :rule-classes :linear))
+
+ (defthm logand-with-2^n-is-logbitp
+ (implies (natp n)
+ (equal (equal (logand x (expt 2 n)) 0)
+ (not (logbitp n x))))
+ :rule-classes ((:rewrite)
+ (:rewrite :corollary
+ (implies (natp n)
+ (equal (equal (logand (expt 2 n) x) 0)
+ (not (logbitp n x))))))
+ :hints(("Goal"
+ :in-theory (enable logand$ logbitp**)
+ :induct (dec-logcdr-induct n x)))))
+
+
+
+;; A variation on this is proved in ihsext-basics
+;;(defthm logbitp-of-ash
+;; (implies (natp a)
+;; (equal (logbitp a (ash x n))
+;; (cond ((or (not (integerp n))
+;; (= n 0))
+;; (logbitp a x))
+;; ((< n 0)
+;; (logbitp (- a n) x))
+;; ((< a n)
+;; nil)
+;; (t
+;; (logbitp (- a n) x))))))
+
+
+
+
+(encapsulate nil
+ (local (local (include-book "arithmetic-3/extra/top-ext" :dir :system)))
+
+ (defthm |(mod a (expt 2 n)) < (expt 2 n)|
+ (implies (integerp a)
+ (< (mod a (expt 2 n))
+ (expt 2 n)))
+ :rule-classes ((:rewrite) (:linear)))
+
+ (defthm expt-2-monotonic
+ (implies (and (< a b)
+ (integerp a)
+ (integerp b))
+ (< (expt 2 a)
+ (expt 2 b)))
+ :rule-classes ((:rewrite) (:linear))))
+
+
+
+
+
+(encapsulate nil
+ (local (local (include-book "arithmetic-3/extra/top-ext" :dir :system)))
+
+ (defthm |(logbitp n (+ (expt 2 n) a))|
+ (implies (and (integerp a)
+ (natp n))
+ (equal (logbitp n (+ (expt 2 n) a))
+ (not (logbitp n a))))
+ :rule-classes ((:rewrite)
+ (:rewrite :corollary
+ (implies (and (integerp a)
+ (natp n))
+ (equal (logbitp n (+ a (expt 2 n)))
+ (not (logbitp n a))))))
+ :hints(("Goal" :in-theory (enable logbitp evenp oddp)))))
+
=======================================
--- /trunk/tools/rulesets.lisp Thu Oct 8 16:42:35 2009
+++ /trunk/tools/rulesets.lisp Thu Mar 1 15:20:35 2012
@@ -17,9 +17,13 @@
(consp (assoc name ruleset-alist))))
(defun ruleset-designatorp (x world)
- (cond ((or (symbolp x)
- (and (consp x)
- (not (keywordp (car x)))))
+ (cond ((symbolp x)
+ (or (theoryp (list x) world)
+ (is-ruleset x world)
+ (cw "~
+**NOTE**:~%~x0 is not a rune, theory name, or ruleset name.~%" x)))
+ ((and (consp x)
+ (not (keywordp (car x))))
(theoryp! (list x) world))
((runep x world) t)
((and (consp x) (symbolp (car x)) (eq (cdr x) nil)) t)
@@ -120,27 +124,32 @@
(if (atom x)
nil
(let ((des (car x)))
- (if (or (atom des) (runep des world))
- (cons des (expand-ruleset1 (cdr x) world))
- (if (null (cdar x))
- (cons `(:executable-counterpart ,(caar x))
- (expand-ruleset1 (cdr x) world))
- (case (car des)
- (:ruleset
- (append (expand-ruleset1 (ruleset (cadr des)) world)
- (expand-ruleset1 (cdr x) world)))
- (:executable-counterpart-theory
- (append (executable-counterpart-theory (cadr des))
- (expand-ruleset1 (cdr x) world)))
- (:rules-of-class
- (append (rules-of-class (cadr des) (caddr des))
- (expand-ruleset1 (cdr x) world)))
- (:theory
- (append (theory (cadr des))
- (expand-ruleset1 (cdr x) world)))
- (:current-theory
- (append (executable-counterpart-theory (cadr des))
- (expand-ruleset1 (cdr x) world)))))))))
+ (cond ((atom des)
+ (if (theoryp (list des) world)
+ (cons des (expand-ruleset1 (cdr x) world))
+ (append (expand-ruleset1 (ruleset des) world)
+ (expand-ruleset1 (cdr x) world))))
+ ((runep des world)
+ (cons des (expand-ruleset1 (cdr x) world)))
+ ((null (cdar x))
+ (cons `(:executable-counterpart ,(caar x))
+ (expand-ruleset1 (cdr x) world)))
+ (t (case (car des)
+ (:ruleset
+ (append (expand-ruleset1 (ruleset (cadr des)) world)
+ (expand-ruleset1 (cdr x) world)))
+ (:executable-counterpart-theory
+ (append (executable-counterpart-theory (cadr des))
+ (expand-ruleset1 (cdr x) world)))
+ (:rules-of-class
+ (append (rules-of-class (cadr des) (caddr des))
+ (expand-ruleset1 (cdr x) world)))
+ (:theory
+ (append (theory (cadr des))
+ (expand-ruleset1 (cdr x) world)))
+ (:current-theory
+ (append (executable-counterpart-theory (cadr des))
+ (expand-ruleset1 (cdr x) world)))))))))
(defun expand-ruleset (x world)
(if (ruleset-designator-listp x world)