← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/cowles/books/tarai2.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/cowles/books/tarai2.lisp
 
1
; An ACL2 Tarai Function book.
 
2
; Copyright (C) 2000  John R. Cowles, University of Wyoming
 
3
 
 
4
; This book is free software; you can redistribute it and/or modify
 
5
; it under the terms of the GNU General Public License as published by
 
6
; the Free Software Foundation; either version 2 of the License, or
 
7
; (at your option) any later version.
 
8
 
 
9
; This book is distributed in the hope that it will be useful,
 
10
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
11
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
12
; GNU General Public License for more details.
 
13
 
 
14
; You should have received a copy of the GNU General Public License
 
15
; along with this book; if not, write to the Free Software
 
16
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
17
 
 
18
; Written by:
 
19
; John Cowles
 
20
; Department of Computer Science
 
21
; University of Wyoming
 
22
; Laramie, WY 82071-3682 U.S.A.
 
23
 
 
24
;; The function Fb satisfies the tarai recursion and the
 
25
;;  restricted tarai recursion for lists of length 6.
 
26
 
 
27
;; (certify-book "C:/acl2/tak/tarai2")
 
28
 
 
29
(in-package "ACL2")
 
30
 
 
31
(defmacro
 
32
    last-el (lst)
 
33
    "Return the last element in the list lst."
 
34
    (list 'car (list 'last lst)))
 
35
 
 
36
(defun
 
37
    Gb (lst)
 
38
    "Bailey's g function for Knuth's Theorem 4.
 
39
     The input lst is intended to be a nonempty
 
40
     list of integers."
 
41
    (declare (xargs :guard (and (integer-listp lst)
 
42
                                (consp lst))))
 
43
    (cond ((consp (nthcdr 3 lst))    ;; (len lst) > 3
 
44
           (if (or (equal (first lst)
 
45
                          (+ (second lst) 1))
 
46
                   (> (second lst)
 
47
                      (+ (third lst) 1)))
 
48
               (Gb (rest lst))
 
49
               (max (third lst)
 
50
                    (last-el lst))))
 
51
          (t (last-el lst))))       ;; (len lst) <= 3
 
52
(defun
 
53
    decreasing-p (lst)
 
54
    "Determine if the elements in lst are strictly decreasing."
 
55
    (declare (xargs :guard (rational-listp lst)))
 
56
    (if (consp (rest lst))         ;; (len lst) > 1
 
57
        (and (> (first lst)(second lst))
 
58
             (decreasing-p (rest lst)))
 
59
        t))
 
60
 
 
61
(defun
 
62
    first-non-decrease (lst)
 
63
    "Return the front of lst up to and including the first
 
64
     element that does not strictly decrease."
 
65
    (declare (xargs :guard (and (rational-listp lst)
 
66
                                (not (decreasing-p lst)))))
 
67
    (if (consp (rest lst))        ;; (len lst) > 1
 
68
        (if (<= (first lst)(second lst))
 
69
            (list (first lst)(second lst))
 
70
            (cons (first lst)
 
71
                  (first-non-decrease (rest lst))))
 
72
        lst))
 
73
 
 
74
(defun
 
75
    Fb (lst)
 
76
    "Bailey's f function for Knuth's theorem 4.
 
77
     The input lst is intended to be a nonempty
 
78
     list of integers."
 
79
    (declare (xargs :guard (and (integer-listp lst)
 
80
                                (consp lst))))
 
81
    (if (decreasing-p lst)
 
82
        (first lst)
 
83
        (Gb (first-non-decrease lst))))
 
84
(defun
 
85
    rotate (lst)
 
86
    "Return the result of shifting the first element
 
87
     of the list lst onto the tail end of lst."
 
88
    (declare (xargs :guard (true-listp lst)))
 
89
    (if (consp lst)
 
90
        (append (rest lst)(list (first lst)))
 
91
        nil))
 
92
 
 
93
(defun
 
94
    minus-1 (lst)
 
95
    "Return the result of replacing (first lst)
 
96
     with (first lst) - 1."
 
97
    (declare (xargs :guard (and (rational-listp lst)
 
98
                                (consp lst))))
 
99
    (if (consp lst)
 
100
        (cons (- (first lst) 1)
 
101
              (rest lst))
 
102
        lst))
 
103
 
 
104
(defun
 
105
    lst-rotates-with-minus-1 (n lst)
 
106
    "Return the list of n+1 successive rotates of the 
 
107
     list lst with the first of each rotate replaced 
 
108
     by the first minus 1."
 
109
    (declare (xargs :guard (and (rational-listp lst)
 
110
                                (consp lst)
 
111
                                (integerp n)
 
112
                                (>= n 0))))
 
113
    (if (zp n)
 
114
        (list (minus-1 lst))
 
115
        (cons (minus-1 lst)
 
116
              (lst-rotates-with-minus-1 (- n 1)
 
117
                                        (rotate lst)))))
 
118
 
 
119
(defun
 
120
    Fb-lst (lst)
 
121
    (if (consp lst)
 
122
        (cons (Fb (first lst))
 
123
              (Fb-lst (rest lst)))
 
124
        nil))
 
125
 
 
126
(defun
 
127
    dec-front-len (lst)
 
128
    "Return the number of strictly decreasing elements 
 
129
     at the front of the list lst."
 
130
    (declare (xargs :guard (rational-listp lst))) 
 
131
    (cond ((consp (rest lst))  ;; (len lst) > 1
 
132
           (if (<= (first lst)(second lst))
 
133
               1
 
134
               (+ 1 (dec-front-len (rest lst)))))
 
135
          ((consp lst) 1)      ;; (len lst) = 1
 
136
          (t 0)))              ;; (len lst) = 0
 
137
;;----------------------------------------------------------
 
138
;; Fb satisfies the tarai recursion equation when lst is a
 
139
;;  true list of integers of length 5.
 
140
 
 
141
(local
 
142
 (defthm
 
143
     lst-rotates-with-minus-1-6a
 
144
     (let ((lst (list first second third forth fifth sixth)))
 
145
       (equal (lst-rotates-with-minus-1 1 lst)
 
146
              (list (list (- first 1) second third forth fifth sixth)
 
147
                    (list (- second 1) third forth fifth sixth first))))
 
148
     :hints (("Goal"
 
149
              :expand ((lst-rotates-with-minus-1 
 
150
                        1
 
151
                        (list first second third forth fifth sixth))))))
 
152
 )
 
153
 
 
154
(local
 
155
 (defthm
 
156
     lst-rotates-with-minus-1-6b
 
157
     (let ((lst (list first second third forth fifth sixth)))
 
158
       (equal (lst-rotates-with-minus-1 2 lst)
 
159
              (list (list (- first 1) second third forth fifth sixth)
 
160
                    (list (- second 1) third forth fifth sixth first)
 
161
                    (list (- third 1) forth fifth sixth first second)))))
 
162
 )
 
163
 
 
164
(local
 
165
 (defthm
 
166
     lst-rotates-with-minus-1-6c
 
167
     (let ((lst (list first second third forth fifth sixth)))
 
168
       (equal (lst-rotates-with-minus-1 3 lst)
 
169
              (list (list (- first 1) second third forth fifth sixth)
 
170
                    (list (- second 1) third forth fifth sixth first)
 
171
                    (list (- third 1) forth fifth sixth first second)
 
172
                    (list (- forth 1) fifth sixth first second third)))))
 
173
 )
 
174
 
 
175
(local
 
176
 (defthm
 
177
     lst-rotates-with-minus-1-6d
 
178
     (let ((lst (list first second third forth fifth sixth)))
 
179
       (equal (lst-rotates-with-minus-1 4 lst)
 
180
              (list (list (- first 1) second third forth fifth sixth)
 
181
                    (list (- second 1) third forth fifth sixth first)
 
182
                    (list (- third 1) forth fifth sixth first second)
 
183
                    (list (- forth 1) fifth sixth first second third)
 
184
                    (list (- fifth 1) sixth first second third forth)
 
185
                    ))))
 
186
 )
 
187
 
 
188
(local
 
189
 (defthm
 
190
     lst-rotates-with-minus-1-6e
 
191
     (let ((lst (list first second third forth fifth sixth)))
 
192
       (equal 
 
193
        (lst-rotates-with-minus-1 5 lst)
 
194
        (list (list (- first 1) second third forth fifth sixth)
 
195
              (list (- second 1) third forth fifth sixth first)
 
196
              (list (- third 1) forth fifth sixth first second)
 
197
              (list (- forth 1) fifth sixth first second third)
 
198
              (list (- fifth 1) sixth first second third forth)
 
199
              (list (- sixth 1) first second third forth fifth)
 
200
              ))))
 
201
 )
 
202
 
 
203
(defthm
 
204
    ;;Time:  703.87 seconds (prove: 327.38, print: 376.44, other: 0.05)
 
205
    Fb-sat-tarai-def-6
 
206
    (implies (and (integerp first)
 
207
                  (integerp second)
 
208
                  (integerp third)
 
209
                  (integerp forth)
 
210
                  (integerp fifth)
 
211
                  (integerp sixth))
 
212
             (let ((lst (list first second third forth fifth sixth)))
 
213
               (equal (Fb lst)
 
214
                      (if (<= (first lst)
 
215
                              (second lst))
 
216
                          (second lst)
 
217
                        (Fb (Fb-lst (lst-rotates-with-minus-1 
 
218
                                     (- (len lst) 1)
 
219
                                     lst)))))))
 
220
    :rule-classes nil)
 
221
 
 
222
(defthm 
 
223
   ;;Time:  253.60 seconds (prove: 122.80, print: 130.74, other: 0.06)
 
224
    Fb-sat-tarai-def-6a
 
225
    (implies (and (integerp first)
 
226
                  (integerp second)
 
227
                  (integerp third)
 
228
                  (integerp forth)
 
229
                  (integerp fifth)
 
230
                  (integerp sixth))
 
231
             (let ((lst (list first second third forth fifth sixth)))
 
232
               (equal (Fb lst)
 
233
                      (if (<= (first lst)
 
234
                              (second lst))
 
235
                          (second lst)
 
236
                        (Fb (Fb-lst (lst-rotates-with-minus-1 
 
237
                                     (- (dec-front-len lst) 1)
 
238
                                     lst)))))))
 
239
    :rule-classes nil)