← 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/bias.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/bias.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(local (include-book "bias-proofs"))
 
4
 
 
5
(defund bvecp (x k)
 
6
  (declare (xargs :guard (integerp k)))
 
7
  (and (integerp x)
 
8
       (<= 0 x)
 
9
       (< x (expt 2 k))))
 
10
 
 
11
; bias of a q bit exponent field is 2^(q-1)-1 
 
12
(defund bias (q) (- (expt 2 (- q 1)) 1) )
 
13
 
 
14
(defthm bias-non-negative-integerp-type-prescription
 
15
  (implies (and (case-split (integerp q))
 
16
                (case-split (< 0 q))
 
17
                )
 
18
           (and (integerp (bias q))
 
19
                (<= 0 (bias q))))
 
20
  :rule-classes :TYPE-PRESCRIPTION)
 
21
 
 
22
;BOZO rename q2 to k?
 
23
(defthm bias-bvecp
 
24
   (implies (and (<= (1- q) q2)
 
25
                 (case-split (< 0 q))
 
26
                 (case-split (integerp q))
 
27
                 (case-split (integerp q2))
 
28
                 )
 
29
            (bvecp (bias q) q2)))
 
30
 
 
31
(defthm bias-integerp-rewrite
 
32
  (equal (integerp (bias q))
 
33
         (or (and (acl2-numberp q) (not (integerp q)))
 
34
             (<= 1 q))))
 
35
 
 
36
;where's bias-integerp?
 
37
(defthm bias-integerp
 
38
  (implies (case-split (< 0 k))
 
39
           (integerp (bias k))))
 
40
 
 
41
(defthm bias-with-q-an-acl2-number-but-not-an-integer
 
42
  (implies (and (not (integerp q))
 
43
                (case-split (acl2-numberp q)))
 
44
           (equal (bias q)
 
45
                  0)))
 
46
 
 
47
(defthm bias-with-q-not-an-acl2-number
 
48
  (implies (not (acl2-numberp q))
 
49
           (equal (bias q)
 
50
                  -1/2)))
 
 
b'\\ No newline at end of file'