1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
(in-package "ACL2")
(include-book "bitn")
(include-book "bits")
(defun sumbits (x n)
(if (zp n)
0
(+ (* (expt 2 (1- n)) (bitn x (1- n)))
(sumbits x (1- n)))))
(defthmd sumbits-bits
(implies (and (natp x)
(natp n)
(> n 0))
(equal (sumbits x n)
(bits x (1- n) 0)))
:hints (("Goal" :in-theory (enable bits-n-n-rewrite) ;yuck?
:induct (sumbits x n))
("Subgoal *1/2" :use ((:instance bitn-plus-bits (n (1- n)) (m 0))))))
(defthmd sumbits-thm
(implies (and (bvecp x n)
(natp n)
(> n 0))
(equal (sumbits x n)
x))
:hints (("Goal" :in-theory (enable sumbits-bits bvecp))))
(defun sumbits-badguy (x y k)
(if (zp k)
0 ; arbitrary
(if (not (equal (bitn x (1- k)) (bitn y (1- k))))
(1- k)
(sumbits-badguy x y (1- k)))))
(local
(defthm sumbits-badguy-is-correct-lemma
(implies (equal (bitn x (sumbits-badguy x y k))
(bitn y (sumbits-badguy x y k)))
(equal (sumbits x k)
(sumbits y k)))
:rule-classes nil))
(defthmd sumbits-badguy-is-correct
(implies (and (bvecp x k)
(bvecp y k)
(equal (bitn x (sumbits-badguy x y k))
(bitn y (sumbits-badguy x y k)))
(integerp k)
(< 0 k))
(equal (equal x y) t))
:hints (("Goal"
:use sumbits-badguy-is-correct-lemma
:in-theory (enable sumbits-thm))))
(defthmd sumbits-badguy-bounds
(implies (and (integerp k)
(< 0 k))
(let ((badguy (sumbits-badguy x y k)))
(and (integerp badguy)
(<= 0 badguy)
(< badguy k)))))
|
