← 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/setbitn.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/setbitn.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(include-book "cat-def")
 
4
(local (include-book "setbitn-proofs"))
 
5
 
 
6
(defun natp (x)
 
7
  (declare (xargs :guard t))
 
8
  (and (integerp x)
 
9
       (<= 0 x)))
 
10
 
 
11
(defund bvecp (x k)
 
12
  (declare (xargs :guard (integerp k)))
 
13
  (and (integerp x)
 
14
       (<= 0 x)
 
15
       (< x (expt 2 k))))
 
16
 
 
17
(defund bitn (x n)
 
18
  (declare (xargs :guard (and (natp x)
 
19
                              (natp n))
 
20
                  :verify-guards nil))
 
21
  (mbe :logic (bits x n n)
 
22
       :exec  (if (evenp (ash x (- n))) 0 1)))
 
23
 
 
24
(defund setbits (x w i j y)
 
25
  (declare (xargs :guard (and (natp x)
 
26
                              (natp y)
 
27
                              (integerp i)
 
28
                              (integerp j)
 
29
                              (<= 0 j)
 
30
                              (<= j i)
 
31
                              (integerp w)
 
32
                              (< i w))
 
33
                  :verify-guards nil))
 
34
  (mbe :logic (cat (bits x (1- w) (1+ i))
 
35
                   (+ -1 w (- i))
 
36
                   (cat (bits y (+ i (- j)) 0)
 
37
                        (+ 1 i (- j))
 
38
                        (bits x (1- j) 0)
 
39
                        j)
 
40
                   (1+ i))
 
41
       :exec  (cond ((int= j 0)
 
42
                     (cond ((int= (1+ i) w)
 
43
                            (bits y (+ i (- j)) 0))
 
44
                           (t
 
45
                            (cat (bits x (1- w) (1+ i))
 
46
                                 (+ -1 w (- i))
 
47
                                 (bits y (+ i (- j)) 0)
 
48
                                 (1+ i)))))
 
49
                    ((int= (1+ i) w)
 
50
                     (cat (bits y (+ i (- j)) 0)
 
51
                          (+ 1 i (- j))
 
52
                          (bits x (1- j) 0)
 
53
                          j))
 
54
                    (t
 
55
                     (cat (bits x (1- w) (1+ i))
 
56
                          (+ -1 w (- i))
 
57
                          (cat (bits y (+ i (- j)) 0)
 
58
                               (+ 1 i (- j))
 
59
                               (bits x (1- j) 0)
 
60
                               j)
 
61
                          (1+ i))))))
 
62
 
 
63
(defund setbitn (x w n y)
 
64
  (declare (xargs :guard (and (natp x)
 
65
                              (natp y)
 
66
                              (integerp n)
 
67
                              (<= 0 n)
 
68
                              (integerp w)
 
69
                              (< n w))
 
70
                  :verify-guards nil))
 
71
  (setbits x w n n y))
 
72
 
 
73
(defthm setbitn-nonnegative-integer-type
 
74
  (and (integerp (setbitn x w n y))
 
75
       (<= 0 (setbitn x w n y)))
 
76
  :rule-classes (:type-prescription))
 
77
 
 
78
;this rule is no better than setbits-nonnegative-integer-type and might be worse:
 
79
(in-theory (disable (:type-prescription setbitn)))
 
80
 
 
81
(defthm setbitn-natp
 
82
  (natp (setbitn x w n y)))
 
83
 
 
84
;add setbitn-bvecp-simple?
 
85
 
 
86
(defthm setbitn-bvecp
 
87
  (implies (and (<= w k)
 
88
                (case-split (integerp k)))
 
89
           (bvecp (setbitn x w n y) k)))
 
90
 
 
91
(defthm setbitn-rewrite
 
92
  (implies (syntaxp (quotep n))
 
93
           (equal (setbitn x w n y)
 
94
                  (setbits x w n n y))))
 
95
 
 
96
;gen?
 
97
(defthm bitn-setbitn
 
98
  (implies (and (case-split (bvecp y 1))
 
99
                (case-split (< 0 w))
 
100
                (case-split (< n w))
 
101
                (case-split (< k w))
 
102
                (case-split (<= 0 k))
 
103
                (case-split (integerp w))
 
104
                (case-split (integerp n))
 
105
                (<= 0 n)
 
106
                (case-split (integerp k))
 
107
                )
 
108
           (equal (bitn (setbitn x w n y) k)
 
109
                  (if (equal n k)
 
110
                      y
 
111
                    (bitn x k)))))
 
112
 
 
113
(defthm setbitn-setbitn
 
114
  (implies (and (case-split (<= 0 n))
 
115
                (case-split (< n w))
 
116
                (case-split (integerp w))
 
117
                (case-split (integerp n))
 
118
                )
 
119
           (equal (setbitn (setbitn x w n y) w n y2)
 
120
                  (setbitn x w n y2))))
 
121
 
 
122
(defthm setbitn-does-nothing
 
123
  (implies (and (case-split (<= 0 n))
 
124
                (case-split (< n w))
 
125
                (case-split (integerp w))
 
126
                (case-split (integerp n))
 
127
                )
 
128
           (equal (setbitn x w n (bitn x n))
 
129
                  (bits x (1- w) 0))))
 
130