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
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.
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.
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.
21
; Department of Computer Science
22
; University of Wyoming
23
; Laramie, WY 82071-3682 U.S.A.
26
; Last modified 20 December 2001.
28
To certify (originally in ACL2 Version 2.6):
32
*common-lisp-symbols-from-main-lisp-package*))
34
(certify-book "flat-nested" 1 nil ; compile-flg
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,
45
(defthm generic-nested-recursive-f
47
(sq-if (test x) (base x) (f (f (st x)))))).
49
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
50
;; Add some basic arithmetic facts:
60
associate-constants-left-+
61
(implies (and (syntaxp (quotep x))
69
(implies (acl2-numberp y)
76
(implies (acl2-numberp y)
80
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
81
;; Proceed with the construction:
84
sq-if (test then else)
85
"Sequential version of IF."
86
`(if (equal ,test ($bottom$))
88
(if ,test ,then ,else)))
101
(equal (test ($bottom$))($bottom$)))
116
(f-chain (- i 1)(f-chain (- i 1)(st x))))))
119
base-of-f-chain=$bottom$
125
f-chain-is-$<=$-chain
126
(implies (and (integerp i)
129
(f-chain (+ 1 i) x))))
131
;; Choose an ``index'' for definition of lub of f-chain:
135
(not (equal (f-chain i x)
139
lub-f-chain-i-rewrite
140
(implies (equal (f-chain (lub-f-chain-i x) x)
142
(equal (f-chain i x) ($bottom$)))
144
:use lub-f-chain-i)))
146
;; Make sure the chosen index is a nonneg. integer:
149
lub-f-chain-nat-i (x)
150
(nfix (lub-f-chain-i x)))
152
;; Define the least upper bound of f-chain:
156
(f-chain (lub-f-chain-nat-i x) x))
158
(in-theory (disable (:executable-counterpart
162
lub-f-chain-is-upper-bound
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)))
174
:use f-chain-is-$<=$-chain)))
177
f-chain-is-$<=$-chain-f
178
(implies (and (>= i (lub-f-chain-nat-i x))
180
(equal (lub-f-chain x)
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)))))
206
g-chain-$<=$-ub-g-chain
207
(implies (and (integerp i)
212
:in-theory (disable lub-f-chain-is-upper-bound)
214
lub-f-chain-is-upper-bound
217
lub-f-chain-is-upper-bound
222
(max (lub-f-chain-nat-i (st x))
223
(lub-f-chain-nat-i (f (st x)))))
226
ub-g-chain-=-g-chain-Skolem-f
227
(equal (ub-g-chain x)
228
(g-chain (Skolem-f x) x))
231
f-chain-is-$<=$-chain-f
235
f-chain-is-$<=$-chain-f
237
(i (Skolem-f x)))))))
240
lub-f-chain=ub-g-chain
241
(equal (lub-f-chain x)(ub-g-chain x))
245
(:functional-instance
246
lub-$chain$=ub-shifted-$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)
252
(shifted-$chain$ g-chain)
253
(ub-shifted-$chain$ ub-g-chain)))
255
:use g-chain-$<=$-ub-g-chain)
257
:use f-chain-is-$<=$-chain)
261
generic-nested-recursive-f
267
:in-theory (disable lub-f-chain
268
ub-g-chain-=-g-chain-Skolem-f)
269
:use lub-f-chain=ub-g-chain)))