/usr/share/acl2-4.3/books/meta/term-defuns.lisp is in acl2-books-source 4.3-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 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 | ; ACL2 books on arithmetic metafunctions
; Copyright (C) 1997 Computational Logic, Inc.
; This book is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This book is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this book; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by: John Cowles and Matt Kaufmann
; Computational Logic, Inc.
; 1717 West Sixth Street, Suite 290
; Austin, TX 78703-4776 U.S.A.
(in-package "ACL2")
(set-verify-guards-eagerness 2)
; Jared removed this rule because (1) it's slow, and (2) there's an identical rule
; that is built into ACL2, TRUE-LISTP-APPEND.
;; (defthm append-true-listp-type-prescription
;; (implies (true-listp y)
;; (true-listp (append x y)))
;; :rule-classes :type-prescription)
(defun memb (a x)
(if (consp x)
(or (equal a (car x))
(memb a (cdr x)))
nil))
(defun del (x y)
(if (consp y)
(if (equal x (car y))
(cdr y)
(cons (car y) (del x (cdr y))))
y))
(defthm true-listp-del
(implies (true-listp x)
(true-listp (del a x)))
:rule-classes :type-prescription)
(defun subbagp (x y)
(if (consp x)
(if (memb (car x) y)
(subbagp (cdr x) (del (car x) y))
nil)
t))
(defun bagdiff (x y)
(if (consp y)
(if (memb (car y) x)
(bagdiff (del (car y) x) (cdr y))
(bagdiff x (cdr y)))
x))
(defthm true-listp-bagdiff
(implies (true-listp x)
(true-listp (bagdiff x y)))
:rule-classes :type-prescription)
(defun bagint (x y)
(if (consp x)
(if (memb (car x) y)
(cons (car x)
(bagint (cdr x) (del (car x) y)))
(bagint (cdr x) y))
nil))
(defun
term-list-to-type-term ( unary-op-name lst )
(declare (xargs :guard (and (symbolp unary-op-name)
(true-listp lst) )))
(cond ((null lst)
''t)
((null (cdr lst))
(list unary-op-name (car lst)))
(t
(list 'if
(list unary-op-name (car lst))
(term-list-to-type-term unary-op-name (cdr lst))
''nil))))
(defun
binary-op_fringe (binary-op-name x)
(declare (xargs :guard (and (symbolp binary-op-name)
(not (eq binary-op-name 'quote))
(pseudo-termp x))))
(if (and (consp x)
(eq (car x) binary-op-name))
(append (binary-op_fringe binary-op-name (cadr x))
(binary-op_fringe binary-op-name (caddr x)))
(cons x nil)))
(defun binary-op_tree (binary-op-name constant-name fix-name lst)
(declare (xargs :guard (and (symbolp binary-op-name)
(atom constant-name)
(true-listp lst))))
(if (endp lst)
(list 'quote constant-name)
(if (endp (cdr lst))
(list fix-name (car lst))
(if (endp (cddr lst))
(list binary-op-name (car lst) (cadr lst))
(list binary-op-name (car lst)
(binary-op_tree binary-op-name constant-name fix-name
(cdr lst)))))))
(defun binary-op_tree-simple (binary-op-name constant-name lst)
(declare (xargs :guard (and (symbolp binary-op-name)
(atom constant-name)
(true-listp lst))))
(if (endp lst)
(list 'quote constant-name)
(if (endp (cdr lst))
(car lst)
(list binary-op-name (car lst)
(binary-op_tree-simple binary-op-name constant-name
(cdr lst))))))
(defun
remove-duplicates-memb (lst)
(if (consp lst)
(if (memb (car lst)(cdr lst))
(remove-duplicates-memb (cdr lst))
(cons (car lst)
(remove-duplicates-memb (cdr lst))))
nil))
(defun fringe-occur (binop arg term)
(declare (xargs :guard (and (pseudo-termp term)
(symbolp binop)
(not (eq binop 'quote)))))
(cond
((and (consp term)
(eq (car term) binop))
(or (fringe-occur binop arg (cadr term))
(fringe-occur binop arg (caddr term))))
(t (equal arg term))))
|