other
(in-package "STD")
other
(include-book "xdoc/top" :dir :system)
other
(defsection defthm-natp :parents (std/util) :short "Prove rules about a term yielding values in @(tsee natp)." :long "<p> Use the macro @('defthm-natp') to prove a @('rewrite') rule saying that some term yields a @('natp'), a @('type-prescription') corollary saying that the term yields a @('natp'), and a @('linear') corollary saying that the term yields a value greater than or equal to zero. </p> <p> Usage: </p> @({ (defthm-natp <theorem-name> :hyp <hypotheses> :concl <conclusion> :hints <usual ACL2 hints for the main theorem>) :gen-rewrite <t or nil> ;; Make main theorem a :rewrite rule :gen-type <t or nil> ;; Generate :type-prescription corollary :gen-linear <t or nil> ;; Generate :linear corollary :hyp-t <hypotheses for the :type-prescription corollary> :hyp-l <hypotheses for the :linear corollary> :hints-t <usual ACL2 hints for the :type-prescription corollary> :hints-l <usual ACL2 hints for the :linear corollary> :otf-flg <t or nil>) }) <p> The above form produces a theorem of the following form (if both @(':gen-type') and @(':gen-linear') are @('t') and @(':gen-rewrite') is @('t') or unsupplied): </p> @({ (defthm <theorem-name> (implies <hypotheses> (natp <conclusion>)) :hints <usual ACL2 hints> :otf-flg <t or nil> :rule-classes (:rewrite (:type-prescription :corollary (implies <hypotheses> (natp <conclusion>)) :hints <usual ACL2 hints for the :type-prescription corollary>) (:linear :corollary (implies <hypotheses> (<= 0 <conclusion>)) :hints <usual ACL2 hints for the :linear corollary>))) }) <p> If @(':hints-t') is not supplied, hints to prove the type prescription corollary are generated automatically. In this case, the hypotheses for the type prescription corollary must trivially subsume the ones for the main theorem specified by @(':hyp'); in particular, they may have additional conjuncts or additional calls to @(tsee force). Analogous remarks apply to @(':hints-l'). </p> <p> Also see the related macros @(tsee defthm-unsigned-byte-p) and @(tsee defthm-signed-byte-p). </p>")
defthm-natpmacro
(defmacro defthm-natp (name &key (hyp 't) concl (gen-rewrite 't) gen-type gen-linear hints hyp-t hyp-l hints-t hints-l otf-flg) (if concl (let ((hyp-t (or hyp-t hyp)) (hyp-l (or hyp-l hyp)) (hints-t (or hints-t '(("Goal" :in-theory nil)))) (hints-l (or hints-l '(("Goal" :in-theory '(natp)))))) `(defthm ,STD::NAME ,(IF (EQ STD::HYP T) `(STD::NATP ,STD::CONCL) `(STD::IMPLIES ,STD::HYP (STD::NATP ,STD::CONCL))) ,@(AND STD::HINTS `(:HINTS ,STD::HINTS)) ,@(AND STD::OTF-FLG `(:OTF-FLG T)) :rule-classes (,@(IF STD::GEN-REWRITE '(:REWRITE) NIL) ,@(AND STD::GEN-TYPE `((:TYPE-PRESCRIPTION :COROLLARY ,(IF (EQ STD::HYP-T T) `(STD::NATP ,STD::CONCL) `(STD::IMPLIES ,STD::HYP-T (STD::NATP ,STD::CONCL))) :HINTS ,STD::HINTS-T))) ,@(AND STD::GEN-LINEAR `((:LINEAR :COROLLARY ,(IF (EQ STD::HYP-L T) `(<= 0 ,STD::CONCL) `(STD::IMPLIES ,STD::HYP-L (<= 0 ,STD::CONCL))) :HINTS ,STD::HINTS-L)))))) nil))
other
(defsection defthm-unsigned-byte-p :parents (std/util) :short "Prove rules about a term yielding values in @(tsee unsigned-byte-p)." :long "<p> Use the macro @('defthm-unsigned-byte-p') to prove a @('rewrite') rule saying that some term yields an @('unsigned-byte-p'), a @('type-prescription') corollary saying that the term yields a @('natp') (or, if @('bound') is 1, a @('bitp')), and a @('linear') corollary saying that the term yields a value greater than or equal to 0 and less than <tt>(expt 2 bound)</tt>. </p> <p> Usage: </p> @({ (defthm-unsigned-byte-p <theorem-name> :hyp <hypotheses> :bound <n> :concl <conclusion> :hints <usual ACL2 hints for the main theorem> :gen-rewrite <t or nil> ;; Make main theorem a :rewrite rule :gen-type <t or nil> ;; Generate :type-prescription corollary :gen-linear <t or nil> ;; Generate :linear corollary :hyp-t <hypotheses for the :type-prescription corollary> :hyp-l <hypotheses for the :linear corollary> :hints-t <usual ACL2 hints for the :type-prescription corollary> :hints-l <usual ACL2 hints for the :linear corollary> :otf-flg <t or nil>) }) <p> In the most common case (both @(':gen-type') and @(':gen-linear') are @('t'), @(':gen-rewrite') is @('t') or unsupplied, and @('bound') is not the special value 1 which would cause a tighter @(':type-prescription') rule), the theorem produced is of the following form: </p> @({ (defthm <theorem-name> (implies <hypotheses> (unsigned-byte-p <n> <conclusion>)) :hints <usual ACL2 hints for the main theorem> :otf-flg <t or nil> :rule-classes (:rewrite (:type-prescription :corollary (implies <hypotheses for the :type-prescription corollary> (natp <conclusion>)) :hints <usual ACL2 hints for the :type-prescription corollary>) (:linear :corollary (implies <hypotheses for the :linear corollary> (and (<= 0 <conclusion>) (< <conclusion> (expt 2 <n>)))) :hints <usual ACL2 hints for the :linear corollary>))) }) <p> If @(':hints-t') is not supplied, hints to prove the type prescription corollary are generated automatically. In this case, the hypotheses for the type prescription corollary must trivially subsume the ones for the main theorem specified by @(':hyp'); in particular, they may have additional conjuncts or additional calls to @(tsee force). Analogous remarks apply to @(':hints-l'). </p> <p> Also see the related macros @(tsee defthm-natp) and @(tsee defthm-signed-byte-p). </p>")
defthm-unsigned-byte-pmacro
(defmacro defthm-unsigned-byte-p (name &key (hyp 't) bound concl (gen-rewrite 't) gen-type gen-linear hyp-t hyp-l hints hints-t hints-l otf-flg) (if (and concl bound) (let* ((hyp-t (or hyp-t hyp)) (hyp-l (or hyp-l hyp)) (bitp (equal 1 bound)) (hints-t (or hints-t `(("Goal" :in-theory '(unsigned-byte-p integer-range-p natp ,@(AND STD::BITP '(STD::BITP (:E EXPT)))))))) (hints-l (or hints-l '(("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))) (2^bound (if (natp bound) (expt 2 bound) `(expt 2 ,STD::BOUND)))) `(defthm ,STD::NAME ,(IF (EQ STD::HYP T) `(STD::UNSIGNED-BYTE-P ,STD::BOUND ,STD::CONCL) `(STD::IMPLIES ,STD::HYP (STD::UNSIGNED-BYTE-P ,STD::BOUND ,STD::CONCL))) ,@(AND STD::HINTS `(:HINTS ,STD::HINTS)) ,@(AND STD::OTF-FLG `(:OTF-FLG T)) :rule-classes (,@(IF STD::GEN-REWRITE '(:REWRITE) NIL) ,@(AND STD::GEN-TYPE `((:TYPE-PRESCRIPTION :COROLLARY ,(LET ((STD::CONCLUSION (IF STD::BITP `(STD::BITP ,STD::CONCL) `(STD::NATP ,STD::CONCL)))) (IF (EQ STD::HYP-T T) STD::CONCLUSION `(STD::IMPLIES ,STD::HYP-T ,STD::CONCLUSION))) :HINTS ,STD::HINTS-T))) ,@(AND STD::GEN-LINEAR `((:LINEAR :COROLLARY ,(IF (EQ STD::HYP-L T) `(AND (<= 0 ,STD::CONCL) (< ,STD::CONCL ,STD::2^BOUND)) `(STD::IMPLIES ,STD::HYP-L (AND (<= 0 ,STD::CONCL) (< ,STD::CONCL ,STD::2^BOUND)))) :HINTS ,STD::HINTS-L)))))) nil))
other
(defsection defthm-signed-byte-p :parents (std/util) :short "Prove rules about a term yielding values in @(tsee signed-byte-p)." :long "<p> Use the macro @('defthm-signed-byte-p') to prove a @('rewrite') rule saying that some term yields a @('signed-byte-p'), a @('type-prescription') corollary saying that the term yields an @('integerp'), and a @('linear') corollary saying that the term yields a value greater than or equal to <tt>(- (expt 2 (1- bound)))</tt> and less than <tt>(expt 2 (1- bound))</tt>. </p> <p> Usage: </p> @({ (defthm-signed-byte-p <theorem-name> :hyp <hypotheses> :bound <n> :concl <conclusion> :hints <usual ACL2 hints for the main theorem> :gen-rewrite <t or nil> ;; Make main theorem a :rewrite rule :gen-type <t or nil> ;; Generate :type-prescription corollary :gen-linear <t or nil> ;; Generate :linear corollary :hyp-t <hypotheses for the :type-prescription corollary> :hyp-l <hypotheses for the :linear corollary> :hints-t <usual ACL2 hints for the :type-prescription corollary> :hints-l <usual ACL2 hints for the :linear corollary> :otf-flg <t or nil>) }) <p> The above form produces a theorem of the following form (if both @(':gen-type') and @(':gen-linear') are @('t') and @(':gen-rewrite') is @('t') or unsupplied): </p> @({ (defthm <theorem-name> (implies <hypotheses> (signed-byte-p <n> <conclusion>)) :hints <usual ACL2 hints for the main theorem> :otf-flg <t or nil> :rule-classes (:rewrite (:type-prescription :corollary (implies <hypotheses for the :type-prescription corollary> (integerp <conclusion>)) :hints <usual ACL2 hints for the :type-prescription corollary>) (:linear :corollary (implies <hypotheses for the :linear corollary> (and (<= (- (expt 2 (1- <n>)) <conclusion>)) (< <conclusion> (expt 2 (1- <n>))))) :hints <usual ACL2 hints for the :linear corollary>))) }) <p> If @(':hints-t') is not supplied, hints to prove the type prescription corollary are generated automatically. In this case, the hypotheses for the type prescription corollary must trivially subsume the ones for the main theorem specified by @(':hyp'); in particular, they may have additional conjuncts or additional calls to @(tsee force). Analogous remarks apply to @(':hints-l'). </p> <p> Also see the related macros @(tsee defthm-natp) and @(tsee defthm-unsigned-byte-p). </p>")
defthm-signed-byte-pmacro
(defmacro defthm-signed-byte-p (name &key (hyp 't) bound concl (gen-rewrite 't) gen-type gen-linear hyp-t hyp-l hints hints-t hints-l otf-flg) (if (and concl bound) (let* ((hyp-t (or hyp-t hyp)) (hyp-l (or hyp-l hyp)) (hints-t (or hints-t '(("Goal" :in-theory '(signed-byte-p integer-range-p))))) (hints-l (or hints-l '(("Goal" :in-theory '(signed-byte-p integer-range-p (:e expt)))))) (2^bound-1 (if (natp bound) (expt 2 (1- bound)) `(expt 2 (1- ,STD::BOUND)))) (low-2^bound-1 (if (natp bound) (- 2^bound-1) `(- (expt 2 (1- ,STD::BOUND)))))) `(defthm ,STD::NAME ,(IF (EQ STD::HYP T) `(STD::SIGNED-BYTE-P ,STD::BOUND ,STD::CONCL) `(STD::IMPLIES ,STD::HYP (STD::SIGNED-BYTE-P ,STD::BOUND ,STD::CONCL))) ,@(AND STD::HINTS `(:HINTS ,STD::HINTS)) ,@(AND STD::OTF-FLG `(:OTF-FLG T)) :rule-classes (,@(IF STD::GEN-REWRITE '(:REWRITE) NIL) ,@(AND STD::GEN-TYPE `((:TYPE-PRESCRIPTION :COROLLARY ,(IF (EQ STD::HYP-T T) `(INTEGERP ,STD::CONCL) `(STD::IMPLIES ,STD::HYP-T (INTEGERP ,STD::CONCL))) :HINTS ,STD::HINTS-T))) ,@(AND STD::GEN-LINEAR `((:LINEAR :COROLLARY ,(IF (EQ STD::HYP-L T) `(AND (<= ,STD::LOW-2^BOUND-1 ,STD::CONCL) (< ,STD::CONCL ,STD::2^BOUND-1)) `(STD::IMPLIES ,STD::HYP-L (AND (<= ,STD::LOW-2^BOUND-1 ,STD::CONCL) (< ,STD::CONCL ,STD::2^BOUND-1)))) :HINTS ,STD::HINTS-L)))))) nil))