/usr/share/acl2-7.2dfsg/books/misc/enumerate.lisp is in acl2-books-source 7.2dfsg-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 64 65 66 67 68 69 70 71 72 73 74 75 | ; A Little Proof Hack: Enumerating the Values of a Term
; J Strother Moore
; November, 2013
; (certify-book "enumerate")
; If you attach the hint
; :use ((:instance enumerate (term x) (i -2) (j 3)))
; to a goal, (p x), you get the following new subgoals (in some pretty
; random order!):
; (P -2)
; (P -1)
; (P 0)
; (P 1)
; (P 2)
; (P 3)
; (IMPLIES (< X -2) (P X))
; (IMPLIES (< 3 X) (P X))
; (IMPLIES (NOT (INTEGERP X)) (P X))
; For the hint to work properly, i and j should be quoted integer constants.
; Example Use: The following is not a theorem but the thm command will
; show the cases generated by the enumerate hint.
#||
(defstub p (x) t)
(thm (p x)
:hints
(("Goal" :use (:instance enumerate (term x) (i -2)(j 3))))
:otf-flg t)
||#
(in-package "ACL2")
(defun enumerate! (term i j)
(declare (xargs :measure (acl2-count (nfix (- (+ 1 (ifix j)) (ifix i))))))
(cond ((and (integerp i)
(integerp j)
(<= i j))
(if (equal term i)
t
(enumerate! term (+ i 1) j)))
(t nil)))
(defthm enumerate
(implies (and (integerp term)
(integerp i)
(integerp j)
(<= i term)
(<= term j))
(enumerate! term i j))
:rule-classes nil)
(defthm enumerate-expander
(and
(implies (and (syntaxp (and (quotep i)
(quotep j)))
(integerp i)
(integerp j)
(< j i))
(equal (enumerate! term i j) nil))
(implies (and (syntaxp (and (quotep i)
(quotep j)))
(integerp i)
(integerp j)
(<= i j))
(equal (enumerate! term i j)
(or (equal term i)
(enumerate! term (+ i 1) j))))))
(in-theory (disable enumerate!))
|