← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2002/cowles-primrec/support/tail.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-primrec/support/tail.lisp
 
1
; Introduction of an arbitrary tail-recursive function.
 
2
; Copyright (C) 2001  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
; Fall 2001.
 
25
;  Last modified 26 September 2001.
 
26
#|
 
27
 To certify in ACL2 Version 2.5:
 
28
 (certify-book "tail" 0 nil ; compile-flg
 
29
               :defaxioms-okp nil
 
30
               :skip-proofs-okp nil)
 
31
|#             
 
32
#|
 
33
Show for Pete & J's construction, as reported in defpun.lisp, of 
 
34
tail-recursive f, any constant would do in place of nil in the 
 
35
definition of f.
 
36
|#
 
37
 
 
38
(in-package "ACL2")
 
39
 
 
40
(defstub
 
41
  test (*) => *)
 
42
 
 
43
(defstub 
 
44
  base (*) => *)
 
45
 
 
46
(defstub 
 
47
  st (*) => *)
 
48
 
 
49
(defstub 
 
50
    const () => *)
 
51
 
 
52
(defun stn (x n)
 
53
  (if (zp n) x (stn (st x) (1- n))))
 
54
 
 
55
(defchoose fch (n) (x)
 
56
           (test (stn x n)))
 
57
 
 
58
(defun fn (x n)
 
59
  (declare (xargs :measure (nfix n)))
 
60
  (if (or (zp n) (test x))
 
61
      (base x)
 
62
      (fn (st x) (1- n))))
 
63
 
 
64
;; Here an arbitrary constant, (const), is used in place of nil in
 
65
;;  Pete & J's original definition.
 
66
(defun f (x)
 
67
  (if (test (stn x (fch x)))
 
68
      (fn x (fch x))
 
69
      (const)))
 
70
 
 
71
;;; This proof of generic-tail-recursive-f is a minor
 
72
;;;  variation of Pete & J's proof of generic-tail-recursive-f
 
73
;;;  in defpun.lisp
 
74
(encapsulate
 
75
 ()
 
76
 (local (defthm test-fch
 
77
            (implies (test x)
 
78
                     (test (stn x (fch x))))
 
79
            :hints
 
80
            (("goal" :use ((:instance fch (n 0)))))))
 
81
 
 
82
;; Not needed for Pete & J's proof of generic-tail-recursive-f.
 
83
;;  Also not needed for this proof of generic-tail-recursive-f.
 
84
;;(local (defthm test-f-def
 
85
;;       (implies (test x)
 
86
;;                (equal (f x) (base x)))))
 
87
 
 
88
 (local (defthm open-stn
 
89
            (implies (and (integerp n) (< 0 n))
 
90
                     (equal (stn x n) 
 
91
                            (stn (st x) (1- n))))))
 
92
 
 
93
 (local (defthm +1-1 (equal (+ -1 +1 x) (fix x))))
 
94
 
 
95
 (local (defthm st-stn-fch
 
96
            (implies (test (stn (st x) (fch (st x))))
 
97
                     (test (stn x (fch x))))
 
98
            :hints
 
99
            (("goal" :use
 
100
                     ((:instance fch (n (1+ (nfix (fch (st x))))))
 
101
                      (:instance fch (n 1)))))
 
102
            :rule-classes :forward-chaining))
 
103
 
 
104
 (local (defthm test-nil-fch
 
105
            (implies (not (test x))
 
106
                     (iff (test (stn (st x) 
 
107
                                     (fch (st x))))
 
108
                          (test (stn x (fch x)))))
 
109
            :hints
 
110
            (("subgoal 2" :expand (stn x (fch x))
 
111
                          :use
 
112
                          ((:instance fch (x (st x))
 
113
                                      (n (+ -1 (fch x)))))))))
 
114
 
 
115
 (local (defthm fn-st
 
116
            (implies (and (test (stn x n)) 
 
117
                          (test (stn x m)))
 
118
                     (equal (fn x n) (fn x m)))
 
119
            :rule-classes nil))
 
120
 
 
121
 (defthm generic-tail-recursive-f
 
122
     (equal (f x)
 
123
            (if (test x) (base x) (f (st x))))
 
124
     :hints
 
125
     (("subgoal 1" :expand (fn x (fch x)))
 
126
      ("subgoal 1.2'" :use
 
127
                      ((:instance fn-st (x (st x))
 
128
                                  (n (+ -1 (fch x)))
 
129
                                  (m (fch (st x)))))))
 
130
     :rule-classes nil)
 
131
 ) ;; end encapsulate
 
132
 
 
133