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
|
; RP-REWRITER
; Note: The license below is based on the template at:
; http://opensource.org/licenses/BSD-3-Clause
; Copyright (C) 2019, Regents of the University of Texas
; All rights reserved.
; Redistribution and use in source and binary forms, with or without
; modification, are permitted provided that the following conditions are
; met:
; o Redistributions of source code must retain the above copyright
; notice, this list of conditions and the following disclaimer.
; o Redistributions in binary form must reproduce the above copyright
; notice, this list of conditions and the following disclaimer in the
; documentation and/or other materials provided with the distribution.
; o Neither the name of the copyright holders nor the names of its
; contributors may be used to endorse or promote products derived
; from this software without specific prior written permission.
; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
; "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
; LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
; A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
; HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
; SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
; LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
; DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
; THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
; (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
; OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
; Original Author(s):
; Mertcan Temel <mert@utexas.edu>
(in-package "RP")
(include-book "tools/flag" :dir :system)
(local (include-book "centaur/meta/def-formula-checks" :dir :system)) ; this could perhaps be reduced
;; lemmas that are to be used locally
;(make-flag pseudo-termp :defthm-macro-name defthm-pseudo-termp)
(defthm cdr-pseudo-termp
(implies (and
(not (quotep term))
(consp term)
(pseudo-termp term))
(pseudo-term-listp (cdr term))))
(defthm strip-cdrs-pseudo-termlistp
(implies
(PSEUDO-TERM-LISTP (STRIP-CDRS alist))
(pseudo-termp (cdr (assoc-equal key alist)))))
|
