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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/shft.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/shft.lisp

 

1

(in-package "ACL2")

 

2

 

 

3

(defun natp (x)

 

4

  (declare (xargs :guard t))

 

5

  (and (integerp x)

 

6

       (<= 0 x)))

 

7

 

 

8

(defund bvecp (x k)

 

9

  (declare (xargs :guard (integerp k)))

 

10

  (and (integerp x)

 

11

       (<= 0 x)

 

12

       (< x (expt 2 k))))

 

13

 

 

14

(defund fl (x)

 

15

  (declare (xargs :guard (real/rationalp x)))

 

16

  (floor x 1))

 

17

 

 

18

 

 

19

(local (include-book "../../arithmetic/top"))

 

20

 

 

21

(defund shft (x s l)

 

22

  (declare (xargs :guard (and (integerp s) (rationalp x))))

 

23

  (mod (fl (* (expt 2 s) x)) (expt 2 (nfix l))))

 

24

 

 

25

(defthm shft-nonnegative-integer-type

 

26

  (and (integerp (shft x s l))

 

27

       (<= 0 (shft x s l)))

 

28

  :rule-classes (:type-prescription))

 

29

 

 

30

;(:type-prescription shft) is no better than shft-nonnegative-integer-type and might be worse:

 

31

(in-theory (disable (:type-prescription shft)))

 

32

 

 

33

(defthm shft-natp

 

34

  (natp (shft x s n)))

 

35

 

 

36

(defthm shft-bvecp-simple

 

37

  (bvecp (shft x s n) n)

 

38

  :hints (("Goal" :in-theory (enable bvecp shft))))

 

39

 

 

40

(local (include-book "bvecp"))

 

41

 

 

42

(defthm shft-bvecp

 

43

  (implies (and (<= n k)

 

44

                (case-split (integerp k)))

 

45

           (bvecp (shft x s n) k))

 

46

  :hints (("Goal" :in-theory (disable shft-bvecp-simple)

 

47

           :use shft-bvecp-simple)))

 

48

 

 

49

 

 

50

 

• Older »

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