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

« back to all changes in this revision

Viewing changes to books/workshops/2002/cowles-flat/support/flat-nested.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:
 
1
; Introduction of an arbitrary nested-recursive function.
 
2
;  Construction based on flat domains in ACL2.
 
3
; Copyright (C) 2001  John R. Cowles, University of Wyoming
 
4
 
 
5
; This book is free software; you can redistribute it and/or modify
 
6
; it under the terms of the GNU General Public License as published by
 
7
; the Free Software Foundation; either version 2 of the License, or
 
8
; (at your option) any later version.
 
9
 
 
10
; This book is distributed in the hope that it will be useful,
 
11
; but WITHOUT ANY WARRANTY; without even the implied warranty of
 
12
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
13
; GNU General Public License for more details.
 
14
 
 
15
; You should have received a copy of the GNU General Public License
 
16
; along with this book; if not, write to the Free Software
 
17
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
18
 
 
19
; Written by:
 
20
; John Cowles
 
21
; Department of Computer Science
 
22
; University of Wyoming
 
23
; Laramie, WY 82071-3682 U.S.A.
 
24
 
 
25
; Fall 2001.
 
26
;  Last modified 20 December 2001.
 
27
#|
 
28
 To certify (originally in ACL2 Version 2.6):
 
29
 (defpkg 
 
30
     "FLAT" (union-eq 
 
31
              *acl2-exports*
 
32
              *common-lisp-symbols-from-main-lisp-package*))
 
33
 
 
34
 (certify-book "flat-nested" 1 nil ; compile-flg
 
35
               :defaxioms-okp nil 
 
36
               :skip-proofs-okp nil)
 
37
|#
 
38
(in-package "FLAT")
 
39
(include-book "flat")
 
40
#|
 
41
A construction based on flat domains in ACL2, as introduced in
 
42
flat.lisp, of a function f that satisfies the equation, for 
 
43
strict functions (test x), in the following theorem,
 
44
 
 
45
(defthm generic-nested-recursive-f
 
46
    (equal (f x)
 
47
           (sq-if (test x) (base x) (f (f (st x)))))).
 
48
|#
 
49
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
50
;; Add some basic arithmetic facts:
 
51
 
 
52
(local
 
53
 (defthm
 
54
   commutativity-2-of-+
 
55
   (equal (+ x y z)
 
56
          (+ y x z))))
 
57
 
 
58
(local
 
59
 (defthm
 
60
   associate-constants-left-+
 
61
   (implies (and (syntaxp (quotep x))
 
62
                 (syntaxp (quotep y)))
 
63
            (equal (+ x (+ y z))
 
64
                   (+ (+ x y) z)))))
 
65
 
 
66
(local
 
67
 (defthm
 
68
   minus-inverse-+-a
 
69
   (implies (acl2-numberp y)
 
70
            (equal (+ (- x) x y)
 
71
                   y))))
 
72
 
 
73
(local
 
74
 (defthm
 
75
   minus-inverse-+-b
 
76
   (implies (acl2-numberp y)
 
77
            (equal (+ x (- x) y)
 
78
                   y))))
 
79
 
 
80
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
81
;; Proceed with the construction:
 
82
 
 
83
(defmacro
 
84
  sq-if (test then else)
 
85
  "Sequential version of IF."
 
86
   `(if (equal ,test ($bottom$))
 
87
        ($bottom$)
 
88
        (if ,test ,then ,else)))
 
89
 
 
90
(encapsulate
 
91
 (((test *) => *))
 
92
 
 
93
 (local
 
94
  (defun
 
95
      test (x)
 
96
      (declare (ignore x))
 
97
      ($bottom$)))
 
98
 
 
99
 (defthm
 
100
     test-is-strict
 
101
     (equal (test ($bottom$))($bottom$)))
 
102
 ) ;; end encapsulate
 
103
 
 
104
(defstub 
 
105
  base (*) => *)
 
106
 
 
107
(defstub 
 
108
  st (*) => *)
 
109
 
 
110
(defun
 
111
    f-chain (i x)
 
112
    (if (zp i)
 
113
        ($bottom$)
 
114
        (sq-if (test x)
 
115
               (base x)
 
116
               (f-chain (- i 1)(f-chain (- i 1)(st x))))))
 
117
 
 
118
(defthm
 
119
    base-of-f-chain=$bottom$
 
120
    (implies (zp i)
 
121
             (equal (f-chain i x) 
 
122
                    ($bottom$))))
 
123
 
 
124
(defthm
 
125
    f-chain-is-$<=$-chain
 
126
    (implies (and (integerp i)
 
127
                  (>= i 0))
 
128
             ($<=$ (f-chain i x)
 
129
                   (f-chain (+ 1 i) x))))
 
130
 
 
131
;; Choose an ``index'' for definition of lub of f-chain:
 
132
 
 
133
(defchoose
 
134
    lub-f-chain-i i (x)
 
135
    (not (equal (f-chain i x) 
 
136
                ($bottom$))))
 
137
 
 
138
(defthm
 
139
    lub-f-chain-i-rewrite
 
140
    (implies (equal (f-chain (lub-f-chain-i x) x)
 
141
                    ($bottom$))
 
142
             (equal (f-chain i x) ($bottom$)))
 
143
    :hints (("Goal"
 
144
             :use lub-f-chain-i)))
 
145
 
 
146
;; Make sure the chosen index is a nonneg. integer:
 
147
 
 
148
(defun
 
149
    lub-f-chain-nat-i (x)
 
150
    (nfix (lub-f-chain-i x)))
 
151
 
 
152
;; Define the least upper bound of f-chain:
 
153
 
 
154
(defun
 
155
    lub-f-chain (x)
 
156
    (f-chain (lub-f-chain-nat-i x) x))
 
157
 
 
158
(in-theory (disable (:executable-counterpart
 
159
                     lub-f-chain)))
 
160
 
 
161
(defthm
 
162
    lub-f-chain-is-upper-bound
 
163
    ($<=$ (f-chain i x)
 
164
          (lub-f-chain x))
 
165
    :hints (("Goal"
 
166
             :by
 
167
             (:functional-instance
 
168
              lub-$bottom$-based-chain-is-upper-bound
 
169
              ($bottom$-based-chain f-chain) 
 
170
              (lub-$bottom$-based-chain lub-f-chain)
 
171
              (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i)
 
172
              (lub-$bottom$-based-chain-i lub-f-chain-i)))
 
173
            ("Subgoal 2"
 
174
             :use f-chain-is-$<=$-chain)))
 
175
 
 
176
(defthm
 
177
    f-chain-is-$<=$-chain-f
 
178
    (implies (and (>= i (lub-f-chain-nat-i x))
 
179
                  (integerp i))
 
180
             (equal (lub-f-chain x)
 
181
                    (f-chain i x)))
 
182
    :hints (("Goal"
 
183
             :by 
 
184
             (:functional-instance
 
185
              $bottom$-based-chain-is-$<=$-chain-f
 
186
              ($bottom$-based-chain f-chain) 
 
187
              (lub-$bottom$-based-chain lub-f-chain)
 
188
              (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i)
 
189
              (lub-$bottom$-based-chain-i lub-f-chain-i)))))
 
190
 
 
191
(defun
 
192
    f (x)
 
193
    (lub-f-chain x))
 
194
 
 
195
(defun
 
196
    g-chain (i x)
 
197
    (f-chain (+ 1 i) x))
 
198
 
 
199
(defun
 
200
    ub-g-chain (x)
 
201
    (sq-if (test x)
 
202
           (base x)
 
203
           (f (f (st x)))))
 
204
 
 
205
(defthm
 
206
    g-chain-$<=$-ub-g-chain
 
207
    (implies (and (integerp i)
 
208
                  (>= i 0))
 
209
             ($<=$ (g-chain i x)
 
210
                   (ub-g-chain x)))
 
211
    :hints (("Subgoal 2"
 
212
             :in-theory (disable lub-f-chain-is-upper-bound)
 
213
             :use ((:instance
 
214
                    lub-f-chain-is-upper-bound
 
215
                    (x (st x)))
 
216
                   (:instance
 
217
                    lub-f-chain-is-upper-bound
 
218
                    (x (f (st x))))))))
 
219
 
 
220
(defun
 
221
    Skolem-f (x)
 
222
    (max (lub-f-chain-nat-i (st x))
 
223
         (lub-f-chain-nat-i (f (st x)))))
 
224
 
 
225
(defthm
 
226
    ub-g-chain-=-g-chain-Skolem-f
 
227
    (equal (ub-g-chain x)
 
228
           (g-chain (Skolem-f x) x))
 
229
  :hints (("Goal"
 
230
           :use ((:instance
 
231
                  f-chain-is-$<=$-chain-f
 
232
                  (x (st x))
 
233
                  (i (Skolem-f x)))
 
234
                 (:instance
 
235
                  f-chain-is-$<=$-chain-f
 
236
                  (x (f (st x)))
 
237
                  (i (Skolem-f x)))))))
 
238
 
 
239
(defthm
 
240
    lub-f-chain=ub-g-chain
 
241
    (equal (lub-f-chain x)(ub-g-chain x))
 
242
    :rule-classes nil
 
243
    :hints (("Goal"
 
244
             :by 
 
245
             (:functional-instance
 
246
              lub-$chain$=ub-shifted-$chain$
 
247
              ($chain$ f-chain)
 
248
              (lub-$chain$ lub-f-chain)
 
249
              (lub-$chain$-i lub-f-chain-i)
 
250
              (lub-$chain$-nat-i lub-f-chain-nat-i)
 
251
              ($f$ Skolem-f)
 
252
              (shifted-$chain$ g-chain)
 
253
              (ub-shifted-$chain$ ub-g-chain)))
 
254
            ("Subgoal 5"
 
255
             :use g-chain-$<=$-ub-g-chain)
 
256
            ("Subgoal 4"
 
257
             :use f-chain-is-$<=$-chain)
 
258
            ))
 
259
 
 
260
(defthm 
 
261
    generic-nested-recursive-f
 
262
    (equal (f x)
 
263
           (sq-if (test x)
 
264
                  (base x) 
 
265
                  (f (f (st x)))))
 
266
    :hints (("Goal"
 
267
             :in-theory (disable lub-f-chain
 
268
                                 ub-g-chain-=-g-chain-Skolem-f)
 
269
             :use lub-f-chain=ub-g-chain)))