← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2002/cowles-flat/support/flat-primitive.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/2002/cowles-flat/support/flat-primitive.lisp
 
1
; Introduction of an arbitrary primitive-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-primitive" 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
functions h that are monotonic in their second argument, in the 
 
44
following theorem,
 
45
 
 
46
(defthm generic-primitive-recursive-f
 
47
    (equal (f x)
 
48
           (if (test x) (base x) (h x (f (st x)))))).
 
49
 
 
50
The book primitive.lisp gives an alternative (and simpler) 
 
51
construction of such a primitive-recursive f.
 
52
|#
 
53
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
54
;; Add some basic arithmetic facts:
 
55
 
 
56
(local
 
57
 (defthm
 
58
   commutativity-2-of-+
 
59
   (equal (+ x y z)
 
60
          (+ y x z))))
 
61
 
 
62
(local
 
63
 (defthm
 
64
   associate-constants-left-+
 
65
   (implies (and (syntaxp (quotep x))
 
66
                 (syntaxp (quotep y)))
 
67
            (equal (+ x (+ y z))
 
68
                   (+ (+ x y) z)))))
 
69
 
 
70
(local
 
71
 (defthm
 
72
   minus-inverse-+-a
 
73
   (implies (acl2-numberp y)
 
74
            (equal (+ (- x) x y)
 
75
                   y))))
 
76
 
 
77
(local
 
78
 (defthm
 
79
   minus-inverse-+-b
 
80
   (implies (acl2-numberp y)
 
81
            (equal (+ x (- x) y)
 
82
                   y))))
 
83
 
 
84
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
85
;; Proceed with the construction:
 
86
 
 
87
(defstub
 
88
  test (*) => *)
 
89
 
 
90
(defstub 
 
91
  base (*) => *)
 
92
 
 
93
(defstub 
 
94
  st (*) => *)
 
95
 
 
96
(encapsulate
 
97
 (((h * *) => *))
 
98
 
 
99
 (local
 
100
  (defun
 
101
      h (x y)
 
102
    (declare (ignore x y))
 
103
    ($bottom$)))
 
104
 
 
105
 (defthm
 
106
     h-is-monotonic-2
 
107
     (implies ($<=$ y1 y2)
 
108
              ($<=$ (h x y1)(h x y2))))
 
109
 ) ;; end encapsulate
 
110
 
 
111
(defthm
 
112
    h-is-monotonic-2-a
 
113
    (implies (and (syntaxp (not (equal y '($bottom$))))
 
114
                  (not (equal (h x ($bottom$)) ($bottom$))))
 
115
             (equal (h x y)(h x ($bottom$))))
 
116
    :hints (("Goal"
 
117
             :in-theory (disable h-is-monotonic-2)
 
118
             :use (:instance
 
119
                   h-is-monotonic-2
 
120
                   (y1 ($bottom$))
 
121
                   (y2 y)))))
 
122
    
 
123
(defun
 
124
    f-chain (i x)
 
125
    (if (zp i)
 
126
        ($bottom$)
 
127
        (if (test x)
 
128
            (base x)
 
129
            (h x (f-chain (- i 1)(st x))))))
 
130
 
 
131
(defthm
 
132
    base-of-f-chain=$bottom$
 
133
    (implies (zp i)
 
134
             (equal (f-chain i x) 
 
135
                    ($bottom$))))
 
136
 
 
137
(defthm
 
138
    f-chain-is-$<=$-chain
 
139
    (implies (and (integerp i)
 
140
                  (>= i 0))
 
141
             ($<=$ (f-chain i x)
 
142
                   (f-chain (+ 1 i) x))))
 
143
 
 
144
;; Choose an ``index'' for definition of lub of f-chain:
 
145
 
 
146
(defchoose
 
147
    lub-f-chain-i i (x)
 
148
    (not (equal (f-chain i x) 
 
149
                ($bottom$))))
 
150
 
 
151
(defthm
 
152
    lub-f-chain-i-rewrite
 
153
    (implies (equal (f-chain (lub-f-chain-i x) x)
 
154
                    ($bottom$))
 
155
             (equal (f-chain i x) ($bottom$)))
 
156
    :hints (("Goal"
 
157
             :use lub-f-chain-i)))
 
158
 
 
159
;; Make sure the chosen index is a nonneg. integer:
 
160
 
 
161
(defun
 
162
    lub-f-chain-nat-i (x)
 
163
    (nfix (lub-f-chain-i x)))
 
164
 
 
165
;; Define the least upper bound of f-chain:
 
166
 
 
167
(defun
 
168
    lub-f-chain (x)
 
169
    (f-chain (lub-f-chain-nat-i x) x))
 
170
 
 
171
(in-theory (disable (:executable-counterpart
 
172
                     lub-f-chain)))
 
173
 
 
174
(defthm
 
175
    lub-f-chain-is-upper-bound
 
176
    ($<=$ (f-chain i x)
 
177
          (lub-f-chain x))
 
178
    :hints (("Goal"
 
179
             :by
 
180
             (:functional-instance
 
181
              lub-$bottom$-based-chain-is-upper-bound
 
182
              ($bottom$-based-chain f-chain) 
 
183
              (lub-$bottom$-based-chain lub-f-chain)
 
184
              (lub-$bottom$-based-chain-nat-i lub-f-chain-nat-i)
 
185
              (lub-$bottom$-based-chain-i lub-f-chain-i)))
 
186
            ("Subgoal 2"
 
187
             :use f-chain-is-$<=$-chain)))
 
188
 
 
189
(defun
 
190
    f (x)
 
191
    (lub-f-chain x))
 
192
 
 
193
(defun
 
194
    g-chain (i x)
 
195
    (f-chain (+ 1 i) x))
 
196
 
 
197
(defun
 
198
    ub-g-chain (x)
 
199
    (if (test x)
 
200
        (base x)
 
201
        (h x (f (st x)))))
 
202
 
 
203
(defthm
 
204
    g-chain-$<=$-ub-g-chain
 
205
    (implies (and (integerp i)
 
206
                  (>= i 0))
 
207
             ($<=$ (g-chain i x)
 
208
                   (ub-g-chain x)))
 
209
    :hints (("Subgoal 2"
 
210
             :in-theory (disable lub-f-chain-is-upper-bound)
 
211
             :use (:instance
 
212
                   lub-f-chain-is-upper-bound
 
213
                   (x (st x))))))
 
214
 
 
215
(defun
 
216
    Skolem-f (x)
 
217
    (lub-f-chain-nat-i (st x)))
 
218
 
 
219
(defthm
 
220
    ub-g-chain-=-g-chain-Skolem-f
 
221
    (equal (ub-g-chain x)
 
222
           (g-chain (Skolem-f x) x)))
 
223
 
 
224
(defthm
 
225
    lub-f-chain=ub-g-chain
 
226
    (equal (lub-f-chain x)(ub-g-chain x))
 
227
    :rule-classes nil
 
228
    :hints (("Goal"
 
229
             :by 
 
230
             (:functional-instance
 
231
              lub-$chain$=ub-shifted-$chain$
 
232
              ($chain$ f-chain)
 
233
              (lub-$chain$ lub-f-chain)
 
234
              (lub-$chain$-i lub-f-chain-i)
 
235
              (lub-$chain$-nat-i lub-f-chain-nat-i)
 
236
              ($f$ Skolem-f)
 
237
              (shifted-$chain$ g-chain)
 
238
              (ub-shifted-$chain$ ub-g-chain)))
 
239
            ("Subgoal 5"
 
240
             :use g-chain-$<=$-ub-g-chain)
 
241
            ("Subgoal 4"
 
242
             :use f-chain-is-$<=$-chain)
 
243
            ))
 
244
 
 
245
(defthm 
 
246
    generic-primitive-recursive-f
 
247
    (equal (f x)
 
248
           (if (test x) 
 
249
               (base x) 
 
250
               (h x (f (st x)))))
 
251
    :hints (("Goal"
 
252
             :use lub-f-chain=ub-g-chain)))