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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/badguys.lisp

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

books/rtl/rel6/support/support/badguys.lisp

 

1

; This file introduces definable Skolem functions that can be used in order to

 

2

; reduce theorems about all elements of a list to theorems about an arbitrary

 

3

; elements of a list.  Matt Kaufmann first learned of this trick from Ken

 

4

; Kunen.

 

5

 

 

6

(in-package "ACL2")

 

7

 

 

8

;;;**********************************************************************

 

9

;;;                       SUMBITS

 

10

;;;**********************************************************************

 

11

 

 

12

(include-book "merge") ; for badguy and lemmas about it

 

13

 

 

14

(defun sumbits-badguy (x y k)

 

15

  (if (zp k)

 

16

      0 ; arbitrary

 

17

    (if (not (equal (bitn x (1- k)) (bitn y (1- k))))

 

18

        (1- k)

 

19

      (sumbits-badguy x y (1- k)))))

 

20

 

 

21

(local

 

22

 (defthm sumbits-badguy-is-correct-lemma

 

23

   (implies (equal (bitn x (sumbits-badguy x y k))

 

24

                   (bitn y (sumbits-badguy x y k)))

 

25

            (equal (sumbits x k)

 

26

                   (sumbits y k)))

 

27

   :rule-classes nil))

 

28

 

 

29

(defthmd sumbits-badguy-is-correct

 

30

  (implies (and (bvecp x k)

 

31

                (bvecp y k)

 

32

                (equal (bitn x (sumbits-badguy x y k))

 

33

                       (bitn y (sumbits-badguy x y k)))

 

34

                (integerp k)

 

35

                (< 0 k))

 

36

           (equal (equal x y) t))

 

37

  :hints (("Goal"

 

38

           :use sumbits-badguy-is-correct-lemma

 

39

           :in-theory (enable sumbits-thm))))

 

40

 

 

41

(defthmd sumbits-badguy-bounds

 

42

  (implies (and (integerp k)

 

43

                (< 0 k))

 

44

           (let ((badguy (sumbits-badguy x y k)))

 

45

             (and (integerp badguy)

 

46

                  (<= 0 badguy)

 

47

                  (< badguy k)))))

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1