File: all-ones.lisp

package info (click to toggle)
acl2 6.5-2
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 108,856 kB
  • ctags: 110,136
  • sloc: lisp: 1,492,565; xml: 7,958; perl: 3,682; sh: 2,103; cpp: 1,477; makefile: 1,470; ruby: 453; ansic: 358; csh: 125; java: 24; haskell: 17
file content (19 lines) | stat: -rw-r--r-- 474 bytes parent folder | download | duplicates (19) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
 
(in-package "ACL2")

(defund all-ones (n)
  (declare (xargs :guard (and (integerp n) (<= 0 n))))
  (if (zp n)
      0 ;degenerate case
    (1- (expt 2 n))))

(defthm all-ones-of-non-integer
  (implies (not (integerp n))
           (equal (all-ones n)
                  0))
  :hints (("Goal" :in-theory (enable all-ones))))

(defthm all-ones-of-negative
  (implies (< n 0)
           (equal (all-ones n)
                  0))
  :hints (("Goal" :in-theory (enable all-ones))))