← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/user/bvecp.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/user/bvecp.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(defun natp (x)
 
4
  (declare (xargs :guard t))
 
5
  (and (integerp x)
 
6
       (<= 0 x)))
 
7
 
 
8
(local (include-book "../support/support/bvecp"))
 
9
 
 
10
;; New stuff:
 
11
 
 
12
(defund bvecp (x k)
 
13
  (declare (xargs :guard (integerp k)))
 
14
  (and (integerp x)
 
15
       (<= 0 x)
 
16
       (< x (expt 2 k))))
 
17
 
 
18
(defthm bvecp-with-n-not-a-positive-integer
 
19
  (implies (or (not (integerp k))
 
20
               (<= k 0))
 
21
           (equal (bvecp x k)
 
22
                  (equal 0 x))))
 
23
 
 
24
(defthm bvecp-0
 
25
  (bvecp 0 k))
 
26
 
 
27
;drop?
 
28
;just a special case of bvecp-with-n-not-a-positive-integer
 
29
(defthm bvecp-0-thm
 
30
  (equal (bvecp x 0)
 
31
         (equal x 0)))
 
32
 
 
33
(defthm bvecp-ones
 
34
  (implies (case-split (<= 0 k))
 
35
           (bvecp (+ -1 (expt 2 k)) k)))
 
36
 
 
37
;k1 is a free var
 
38
(defthm bvecp-longer
 
39
   (implies (and (bvecp x k1)
 
40
                 (<= k1 k2)
 
41
                 (case-split (integerp k2))
 
42
                 )
 
43
            (bvecp x k2))
 
44
   :rule-classes ((:rewrite :match-free :all)))
 
45
 
 
46
;expensive and so disabled
 
47
;no free var
 
48
(defthmd bvecp-one-longer
 
49
  (implies (and (integerp k)
 
50
                (bvecp x (- k 1)))
 
51
           (bvecp x k))
 
52
  :rule-classes ((:rewrite :backchain-limit-lst (nil 2))))
 
53
 
 
54
 
 
55
(defthm bvecp-of-non-integer
 
56
  (implies (not (integerp x))
 
57
           (not (bvecp x k))))
 
58
 
 
59
;gen (replace n+1 with an arbitrary integer > n)?
 
60
(defthm bvecp-expt-2-n
 
61
  (implies (and (case-split (integerp n))
 
62
                (case-split (<= 0 n))
 
63
                )
 
64
           (bvecp (expt 2 n) (+ 1 n))))
 
65
 
 
66
; The following lemma can be critical during backchaining.  Imagine that ACL2
 
67
; backchains to (bvecp (if test x y) k) and we know (bvecp x k) and (bvecp y
 
68
; k). ACL2 may fail to relieve the hyp because it is merely rewriting; there is
 
69
; no case splitting.  So we need a rule about bvecp applied to an if
 
70
; expression.
 
71
(defthm bvecp-if
 
72
  (equal (bvecp (if test x y) k)
 
73
         (if test (bvecp x k) (bvecp y k))))
 
74
 
 
75
 
 
76
; The following are analogous to mk-bvarr etc. in rtlarr.lisp.
 
77
 
 
78
;better name?
 
79
(defund mk-bvec (r k)
 
80
  (declare (xargs :guard (integerp k)))
 
81
  (if (bvecp r k) r 0))
 
82
 
 
83
(defthm mk-bvec-is-bvecp
 
84
  (bvecp (mk-bvec r k) k))
 
85
 
 
86
(defthm mk-bvec-identity
 
87
  (implies (bvecp r k)
 
88
           (equal (mk-bvec r k) r)))
 
89
 
 
90
;BOZO make a version to shift by a constant!
 
91
(defthm bvecp-shift
 
92
  (implies (and (integerp x) ;note!
 
93
                (<= 0 m)
 
94
                (case-split (integerp m))
 
95
                (case-split (integerp n))
 
96
                )
 
97
           (equal (bvecp (* x (expt 2 m)) n)
 
98
                  (bvecp x (- n m)))))
 
99
 
 
100
(defthm bvecp-shift-alt
 
101
  (implies (and (integerp x) ;note!
 
102
                (<= 0 m)
 
103
                (case-split (integerp m))
 
104
                (case-split (integerp n))
 
105
                )
 
106
           (equal (bvecp (* (expt 2 m) x) n)
 
107
                  (bvecp x (- n m)))))
 
108
 
 
109
;gen this!
 
110
;BOZO will this unify (* 2 x) with 0??
 
111
(defthm bvecp-shift-by-2
 
112
  (implies (and (syntaxp (not (quotep x))) ;prevents loops...
 
113
                (integerp x)
 
114
                (<= 0 m) ;gen?
 
115
                (case-split (integerp m))
 
116
                (case-split (integerp n))
 
117
                )
 
118
           (equal (bvecp (* 2 x) n)
 
119
                  (bvecp x (- n 1)))))
 
120
 
 
121
 
 
122
;gen?
 
123
;in general, rewrite (bvecp k n) where k is a constant to a fact about n
 
124
(defthm bvecp-1
 
125
  (implies (and (<= 1 n)
 
126
                (integerp n))
 
127
           (bvecp 1 n)))
 
128
 
 
129
;n is a free variable
 
130
;Disabled since may cause expensive backchaining.
 
131
(defthmd natp-bvecp
 
132
  (implies (bvecp x n)
 
133
           (natp x))
 
134
  :rule-classes ((:rewrite :match-free :once)))
 
135
 
 
136
(defthmd bvecp-forward
 
137
  (implies (bvecp x k)
 
138
           (and (integerp x)
 
139
                (<= 0 x)
 
140
                (< x (expt 2 k)))) ;tigher-bound?
 
141
  :rule-classes :forward-chaining)
 
142
 
 
143
(defthm bvecp-product
 
144
  (implies (and (bvecp x m)
 
145
                (bvecp y n)
 
146
                )
 
147
           (bvecp (* x y) (+ m n)))
 
148
  :rule-classes ())
 
149
 
 
150
(defthmd bvecp-1-rewrite
 
151
  (equal (bvecp x 1)
 
152
         (or (equal x 0) (equal x 1))))
 
153
 
 
154
;make another for not-equal-0 implies equal-1?
 
155
(defthm bvecp-1-0
 
156
    (implies (and (bvecp x 1)
 
157
                  (not (equal x 1)))
 
158
             (equal x 0))
 
159
  :rule-classes :forward-chaining)
 
160
 
 
161
(defthm bvecp+1
 
162
  (implies (and (natp n)
 
163
                (bvecp x n))
 
164
           (bvecp x (+ 1 n))))
 
165
 
 
166
;same as bvecp-longer.decide which param names to use.  j and k??
 
167
(defthmd bvecp-monotone
 
168
    (implies (and (bvecp x n)
 
169
                  (<= n m)
 
170
                  (case-split (integerp m))
 
171
                  )               
 
172
             (bvecp x m)))
 
173
 
 
174
 
 
175
;This bounds the amount of carry out that we can have from the sum.
 
176
(defthm bvecp-sum-of-bvecps
 
177
  (implies (and (bvecp x (+ -1 k))
 
178
                (bvecp y (+ -1 k))
 
179
                (case-split (integerp k)))
 
180
           (bvecp (+ x y) k)))
 
181
 
 
182
 
 
183
;add rule that (not (natp x)) implies (not (bvecp x k)) ??
 
184
 
 
185
;exported in lib/
 
186
(defthmd bvecp-0-1
 
187
  (implies (and (bvecp x 1)
 
188
                (not (equal x 0)))
 
189
           (equal x 1))
 
190
  :rule-classes :forward-chaining)
 
 
b'\\ No newline at end of file'