/usr/share/acl2-8.0dfsg/books/arithmetic-5/top.lisp is in acl2-books-source 8.0dfsg-1.
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 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 | ; Arithmetic-5 Library
; Written by Robert Krug
; Copyright/License:
; See the LICENSE file at the top level of the arithmetic-5 library.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; top.lisp
;;;
;;;
;;; This book collects all the other books together in one place,
;;; establishes a couple of useful theory collections, and sets up
;;; a default starting point.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(deftheory-static arithmetic-5-current-base
;; Presumably the same as 'ground-zero
(current-theory :here))
(deftheory-static arithmetic-5-universal-base
(universal-theory :here))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; This book defines some theories we will use below.
(include-book "lib/basic-ops/top")
(include-book "lib/floor-mod/top")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(deftheory-static arithmetic-5-current-full
(current-theory :here))
(deftheory-static arithmetic-5-universal-full
(universal-theory :here))
;;; Now, let us build our theories piece by piece. This could be done
;;; more efficiently, but slow and simple wins the race.
(deftheory minimal-arithmetic-5-base
;; We want ACL2's base here.
(theory 'arithmetic-5-current-base))
(deftheory default-arithmetic-5-base
;; Rules from the base (whether or not enabled at that time) that are enabled
;; in the full
(intersection-theories (theory 'arithmetic-5-universal-base)
(theory 'arithmetic-5-current-full)))
(deftheory-static minimal-arithmetic-5
;; Using theories defined in lib/basic-ops/top.lisp
(union-theories
(set-difference-theories (theory 'arithmetic-5-minimal-end-a)
(theory 'arithmetic-5-minimal-start-a))
(set-difference-theories (theory 'arithmetic-5-minimal-end-b)
(theory 'arithmetic-5-minimal-start-b))))
(deftheory default-arithmetic-5
(set-difference-theories (theory 'arithmetic-5-current-full)
(theory 'arithmetic-5-current-base)))
(defmacro intersection-theories-3 (x y z)
`(intersection-theories ,x
(intersection-theories ,y ,z)))
(defmacro union-theories-3 (x y z)
`(union-theories ,x
(union-theories ,y ,z)))
(defmacro set-minimal-arithmetic-5-theory ()
;; 1. ground-zero less anything disabled by either arithmetic-5 or the user,
;; i.e., those rules enabled in ground-zero that are enabled both by
;; arithmetic-5 and by the user
;; 2. the minimal arithmetic theory
;; 3. whatever enabled rules the user has added (i.e. not in arithmetic-5 or
;; ground-zero)
`(in-theory (union-theories-3
(intersection-theories-3 (theory 'minimal-arithmetic-5-base)
(theory 'arithmetic-5-current-full)
(current-theory :here))
(theory 'minimal-arithmetic-5)
(set-difference-theories (current-theory :here)
(theory 'arithmetic-5-universal-full)))))
(defmacro set-default-arithmetic-5-theory ()
`(in-theory (union-theories-3
(intersection-theories-3 (theory 'default-arithmetic-5-base)
(theory 'arithmetic-5-current-full)
(current-theory :here))
(theory 'default-arithmetic-5)
(set-difference-theories (current-theory :here)
(theory 'arithmetic-5-universal-full)))))
|