← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/ereps.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/support/ereps.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
; Eric Smith, David Russinoff, with contributions and suggestions by Matt Kaufmann
 
4
; AMD, June 2001 
 
5
;this file was previously called repsproofs.lisp
 
6
 
 
7
(include-book "rtl")
 
8
(include-book "float") ;to get the defns...
 
9
 
 
10
(local (include-book "ereps-proofs"))
 
11
 
 
12
(set-inhibit-warnings "theory") ; avoid warning in the next event
 
13
(local (in-theory nil))
 
14
;(set-inhibit-warnings) ; restore theory warnings (optional)
 
15
 
 
16
 
 
17
; bias of a q bit exponent field is 2^(q-1)-1 
 
18
(defund bias (q) (- (expt 2 (- q 1)) 1) )
 
19
 
 
20
;;Encoding of floating-point numbers with explicit leading one:
 
21
;;bit vectors of length p+q+1, consisting of 1-bit sign field, 
 
22
;;q-bit exponent field (bias = 2**(q-1)-1), and p-bit significand field.
 
23
 
 
24
(defund esgnf  (x p q) (bitn x (+ p q)))
 
25
(defund eexpof (x p q) (bits x (1- (+ p q)) p)) 
 
26
(defund esigf  (x p)   (bits x (1- p) 0))
 
27
 
 
28
;;;**********************************************************************
 
29
;;;                       REPRESENTABLE NUMBERS
 
30
;;;**********************************************************************
 
31
 
 
32
(defund erepp (x p q)
 
33
  (and (rationalp x)
 
34
       (not (= x 0))
 
35
       (bvecp (+ (expo x) (bias q)) q)
 
36
       (exactp x p)))
 
37
 
 
38
 
 
39
;;;**********************************************************************
 
40
;;;                      VALID ENCODINGS
 
41
;;;**********************************************************************
 
42
 
 
43
(defund eencodingp (x p q)
 
44
  (and (bvecp x (+ p q 1))
 
45
       (= (bitn x (- p 1)) 1)))
 
46
 
 
47
 
 
48
;;;**********************************************************************
 
49
;;;                       EENCODE
 
50
;;;**********************************************************************
 
51
 
 
52
 
 
53
 
 
54
; sig, expo, and sgn are defined in float.lisp
 
55
 
 
56
 
 
57
;bozo disable!
 
58
(defund eencode (x p q)
 
59
  (cat (cat (if (= (sgn x) 1) 0 1)
 
60
            1
 
61
            (+ (expo x) (bias q))
 
62
            q)
 
63
       (1+ q)
 
64
       (* (sig x) (expt 2 (- p 1)))
 
65
       p) )
 
66
 
 
67
 
 
68
 
 
69
 
 
70
;;;**********************************************************************
 
71
;;;                       EDECODE
 
72
;;;**********************************************************************
 
73
 
 
74
 
 
75
(defund edecode (x p q)
 
76
  (* (if (= (esgnf x p q) 0) 1 -1)
 
77
     (esigf x p)
 
78
     (expt 2 (+ 1 (- p) (eexpof x p q) (- (bias q))))))
 
79
 
 
80
 
 
81
 
 
82
;;;**********************************************************************
 
83
;;;                      Encoding and Decoding are Inverses
 
84
;;;**********************************************************************
 
85
 
 
86
(defthm erepp-edecode
 
87
  (implies (and (eencodingp x p q)
 
88
                (integerp p)
 
89
                (> p 0)
 
90
                (integerp q)
 
91
                (> q 0))
 
92
           (erepp (edecode x p q) p q)))
 
93
 
 
94
 
 
95
(defthm eencodingp-eencode
 
96
  (implies (and (erepp x p q)
 
97
                (integerp p)
 
98
                (> p 0)
 
99
                (integerp q)
 
100
                (> q 0))
 
101
           (eencodingp (eencode x p q) p q) ))
 
102
 
 
103
(defthm edecode-eencode
 
104
  (implies (and (erepp x p q)
 
105
                (integerp p)
 
106
;                (> p 0)
 
107
                (integerp q)
 
108
 ;               (> q 0)
 
109
                )
 
110
           (equal (edecode (eencode x p q) p q)
 
111
                  x )))
 
112
 
 
113
(defthm eencode-edecode
 
114
  (implies (and (eencodingp x p q)
 
115
                (integerp p)
 
116
                (>= p 0)
 
117
                (integerp q)
 
118
                (> q 0))
 
119
           (equal (eencode (edecode x p q) p q)
 
120
                  x )))
 
121
 
 
122
(defthm expo-edecode
 
123
  (implies (and (eencodingp x p q)
 
124
                (integerp p)
 
125
                (> p 0)
 
126
                (integerp q)
 
127
                (> q 0))  
 
128
           (equal (expo (edecode x p q))
 
129
                  (- (eexpof x p q) (bias q))
 
130
                  )))
 
131
 
 
132
(defthm sgn-edecode
 
133
  (implies (and (eencodingp x p q)
 
134
                (integerp p)
 
135
                (> p 0)
 
136
                (integerp q)
 
137
                (> q 0))
 
138
           (equal (sgn (edecode  x p q))
 
139
                  (if (= (esgnf x p q) 0) 1 -1))))
 
140
 
 
141
(defthm sig-edecode
 
142
  (implies (and (eencodingp  x p q)
 
143
                (integerp p)
 
144
                (> p 0)
 
145
                (integerp q)
 
146
                (> q 0))
 
147
           (equal (sig (edecode  x p q))
 
148
                  (/ (esigf x p) (expt 2 (- p 1))))))
 
149
 
 
150
(defthm eencodingp-not-zero
 
151
  (implies (and (eencodingp x p q)
 
152
                (integerp p)
 
153
                (> p 0)
 
154
                (integerp q)
 
155
                (> q 0))
 
156
           (not (equal (edecode x p q) 0))))
 
157
 
 
158
(defund rebias-expo (expo old new)
 
159
  (+ expo (- (bias new) (bias old))))
 
160
 
 
161
;;I actually needed all four of the following lemmas, although I would have thought
 
162
;;that the two bvecp lemmas would be enough.
 
163
 
 
164
(defthm natp-rebias-up
 
165
    (implies (and (natp n)
 
166
                  (natp m)
 
167
                  (< 0 m)
 
168
                  (<= m n)
 
169
                  (bvecp x m))
 
170
             (natp (rebias-expo x m n)))
 
171
    :hints (("goal" :in-theory (e/d ( expt-split rebias-expo bvecp natp bias
 
172
                                                  ) (expt-compare))
 
173
                  :use (:instance expt-weak-monotone (n m) (m n)))))
 
174
 
 
175
(defthm natp-rebias-down
 
176
    (implies (and (natp n)
 
177
                  (natp m)
 
178
                  (< 0 m)
 
179
                  (<= m n)
 
180
                  (bvecp x n)
 
181
                  (< x (+ (expt 2 (1- n)) (expt 2 (1- m))))
 
182
                  (>= x (- (expt 2 (1- n)) (expt 2 (1- m)))))
 
183
             (natp (rebias-expo x n m)))
 
184
    :hints (("goal" :in-theory (enable rebias-expo bvecp natp bias))))
 
185
 
 
186
(defthm bvecp-rebias-up
 
187
    (implies (and (natp n)
 
188
                  (natp m)
 
189
                  (< 0 m)
 
190
                  (<= m n)
 
191
                  (bvecp x m))
 
192
             (bvecp (rebias-expo x m n) n)))
 
193
 
 
194
(defthm bvecp-rebias-down
 
195
    (implies (and (natp n)
 
196
                  (natp m)
 
197
                  (< 0 m)
 
198
                  (<= m n)
 
199
                  (bvecp x n)
 
200
                  (< x (+ (expt 2 (1- n)) (expt 2 (1- m))))
 
201
                  (>= x (- (expt 2 (1- n)) (expt 2 (1- m)))))
 
202
             (bvecp (rebias-expo x n m) m)))
 
203
 
 
204
(defthm rebias-up
 
205
    (implies (and (natp n)
 
206
                  (natp m)
 
207
                  (> n m)
 
208
                  (> m 1)
 
209
                  (bvecp x m))
 
210
             (equal (rebias-expo x m n)
 
211
                    (cat (cat (bitn x (1- m))
 
212
                              1
 
213
                              (mulcat 1 (- n m) (lnot (bitn x (1- m)) 1))
 
214
                              (- n m))
 
215
                         (1+ (- n m))
 
216
                         (bits x (- m 2) 0)
 
217
                         (1- m))))
 
218
  :rule-classes ())
 
219
 
 
220
(defthm rebias-down
 
221
    (implies (and (natp n)
 
222
                  (natp m)
 
223
                  (> n m)
 
224
                  (> m 1)
 
225
                  (bvecp x n)
 
226
                  (< x (+ (expt 2 (1- n)) (expt 2 (1- m))))
 
227
                  (>= x (- (expt 2 (1- n)) (expt 2 (1- m)))))
 
228
             (equal (rebias-expo x n m)
 
229
                    (cat (bitn x (1- n))
 
230
                         1
 
231
                         (bits x (- m 2) 0)
 
232
                         (1- m))))
 
233
  :rule-classes ())
 
234