← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/lib1/bvecp-helpers.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/lib1/bvecp-helpers.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
(include-book "rtl")
 
6
(include-book "rtlarr")
 
7
(local (include-book "../support/bvecp-helpers"))
 
8
 
 
9
(defthm bv-arrp-implies-nonnegative-integerp
 
10
  (implies (bv-arrp obj size)
 
11
           (and (integerp (ag index obj))
 
12
                (<= 0 (ag index obj))))
 
13
  :rule-classes (:rewrite :type-prescription)
 
14
  )
 
15
 
 
16
; The two events following the next local include-book were added by Matt
 
17
; K. June 2004: Some proofs require calls of expt to be evaluated, but some
 
18
; calls are just too large (2^2^n for large n).  So we use the following hack,
 
19
; which allows calls of 2^n for n<130 to be evaluated even when the
 
20
; executable-counterpart of expt is disabled.  The use of 130 is somewhat
 
21
; arbitrary, chosen in the hope that it suffices for relieving of hyps related
 
22
; to widths of bit vectors
 
23
 
 
24
(local (include-book "../../arithmetic/basic"))
 
25
 
 
26
(defun expt-exec (r i)
 
27
  (declare (xargs :guard
 
28
                  (and (acl2-numberp r)
 
29
                       (integerp i)
 
30
                       (not (and (eql r 0) (< i 0))))))
 
31
  (mbe :logic (hide (expt r i)) ; hide may avoid potential loop
 
32
       :exec (expt r i)))
 
33
 
 
34
(defthm expt-2-evaluator
 
35
  (implies (syntaxp (and (quotep n)
 
36
                         (natp (cadr n))
 
37
                         (< (cadr n) 130)
 
38
                         ))
 
39
           (equal (expt 2 n)
 
40
                  (expt-exec 2 n))))
 
41