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
|
; number-list-defthms.lisp -- theorems about lists of numbers
; 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: Bill Bevier (bevier@cli.com)
; Computational Logic, Inc.
; 1717 West Sixth Street, Suite 290
; Austin, TX 78703-4776 U.S.A.
(in-package "ACL2")
(include-book "number-list-defuns")
(include-book "deflist")
(deflabel number-list-defthms-section)
(defmacro real/rational-listp (x)
#+:non-standard-analysis
`(real-listp ,x)
#-:non-standard-analysis
`(rational-listp ,x))
; ------------------------------------------------------------
; Theorems
; ------------------------------------------------------------
(deflist rational-listp (l) rationalp
(:options :omit-defun))
#+:non-standard-analysis
(deflist real-listp (l) realp
(:options :omit-defun))
(deflist integer-listp (l) integerp
(:options :omit-defun))
(deflist natural-listp (l) (lambda (x) (naturalp x))
(:options :omit-defun))
; ---------- forwardchaining rules ----------
(defthm natural-listp-forward-to-integer-listp
(implies (natural-listp l)
(integer-listp l))
:rule-classes :forward-chaining)
(defthm integer-listp-forward-to-eqlable-listp
(implies (integer-listp l)
(eqlable-listp l)))
; ---------- LINEAR ----------
(defthm <=maxlist
(implies (member-equal x l)
(<= x (maxlist l)))
:rule-classes (:rewrite :linear :forward-chaining))
(defthm minlist<=
(implies (member-equal x l)
(<= (minlist l) x))
:rule-classes (:rewrite :linear :forward-chaining))
; ---------- MEMBER-EQUAL ----------
(defthm member-equal-maxlist
(implies (and (real/rational-listp l)
(consp l))
(member-equal (maxlist l) l)))
(defthm member-equal-minlist
(implies (and (real/rational-listp l)
(consp l))
(member-equal (minlist l) l)))
(defthm member-equal-excess-natural
(implies (natural-listp l)
(not (member-equal (excess-natural l) l)))
:hints (("Goal" :do-not-induct t
:use ((:instance <=maxlist (x (excess-natural l)) (l l)))
:in-theory (disable <=maxlist))))
(defthm numerically-sorted-numeric-insert
(implies (and (real/rationalp x)
(real/rational-listp l)
(numerically-sorted l))
(numerically-sorted (numeric-insert x l)))
:hints (("Goal" :induct (numeric-insert x l))))
(defthm numerically-sorted-numeric-sort
(implies (real/rational-listp l)
(numerically-sorted (numeric-sort l))))
(deftheory number-list-defthms
(set-difference-theories
(current-theory :here)
(current-theory 'number-list-defthms-section)))
|
