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

« back to all changes in this revision

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

 

1

(in-package "ACL2")

 

2

 

 

3

(set-enforce-redundancy t)

 

4

 

 

5

(local (include-book "../support/rom-helpers"))

 

6

 

 

7

(defund bvecp (x k)

 

8

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

 

9

  (and (integerp x)

 

10

       (<= 0 x)

 

11

       (< x (expt 2 k))))

 

12

(local (in-theory (enable bvecp)))

 

13

 

 

14

(defun natp (x)

 

15

  (declare (xargs :guard t))

 

16

  (and (integerp x)

 

17

       (<= 0 x)))

 

18

 

 

19

(defun check-array (name a dim1 dim2)

 

20

  (if (zp dim1)

 

21

      t

 

22

    (and (bvecp (aref1 name a (1- dim1)) dim2)

 

23

         (check-array name a (1- dim1) dim2))))

 

24

 

 

25

(defthm check-array-lemma-1

 

26

    (implies (and (not (zp dim1))

 

27

                  (check-array name a dim1 dim2)

 

28

                  (natp i)

 

29

                  (< i dim1))

 

30

             (bvecp (aref1 name a i) dim2))

 

31

  :rule-classes ())

 

32

 

 

33

(defthm check-array-lemma

 

34

    (implies (and (bvecp i n)

 

35

                  (not (zp (expt 2 n)))

 

36

                  (check-array name a (expt 2 n) dim2))           

 

37

             (bvecp (aref1 name a i) dim2))

 

38

  :rule-classes ())

 

39

 

 

40

 

• Older »

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