← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2004/cowles-gamboa/support/WyoM1-utilities.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/2004/cowles-gamboa/support/WyoM1-utilities.lisp
 
1
; The WyoM1 Utility Lemmas
 
2
; Copyright (C) 2004  J Strother Moore,
 
3
;               University of Texas at Austin
 
4
 
 
5
; This program is free software; you can redistribute it and/or 
 
6
; modify it under the terms of the GNU General Public License as
 
7
; published by the Free Software Foundation; either version 2 of
 
8
; the License, or (at your option) any later version.
 
9
 
 
10
; This program 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
 
16
; License along with this program; if not, write to the Free 
 
17
; Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
 
18
; USA.
 
19
 
 
20
; Written by: J Strother Moore
 
21
; email:      Moore@cs.utexas.edu
 
22
; Department of Computer Science
 
23
; University of Texas at Austin
 
24
; Austin, TX 78701 U.S.A.
 
25
 
 
26
; Modified by: John Cowles
 
27
; email:       cowles@uwyo.edu
 
28
; Department of Computer Science
 
29
; University of Wyoming
 
30
; Laramie, WY 82071 U.S.A.
 
31
;==============================================================
 
32
; This file is a certified book containing some simple lemmas
 
33
; used to make it easier to do proofs about WyoM1 programs.
 
34
 
 
35
; Instructions
 
36
 
 
37
; To certify this book, you must first have certified your local
 
38
; copy of WyoM1.lisp.  Then, copy this book to the same directory on 
 
39
; which your certified copy of WyoM1.lisp resides and on which you
 
40
; have write permission, fire up ACL2 while connected to that 
 
41
; directory and then execute the following two events.
 
42
#|
 
43
(include-book "WyoM1")
 
44
 
 
45
(certify-book "WyoM1-utilities" 1)
 
46
|#
 
47
; After certification, the book may be used in an ACL2 session or
 
48
; in other books, by writing the form
 
49
 
 
50
; (include-book "WyoM1-utilities")
 
51
 
 
52
; using the full path name as necessary.
 
53
 
 
54
; End of Instructions
 
55
;----------------------------------------------------------------
 
56
; Every ACL2 book must begin with an in-package form.
 
57
 
 
58
; The following was changed from "WyoM1" by Matt K. for ACL2 2.9.3 because
 
59
; package names may no longer contain lower case characters.
 
60
(in-package "WYO-M1")
 
61
 
 
62
; Some Simple Utility Lemmas
 
63
 
 
64
; The standard arithmetic lemmas are brought in here.
 
65
 
 
66
(include-book "../../../../arithmetic/top")
 
67
 
 
68
; Now make stacks and states behave like abstract data types.
 
69
 
 
70
(defthm stacks
 
71
  (and (equal (top (push x s)) x)
 
72
       (equal (pop (push x s)) s)))
 
73
 
 
74
(in-theory (disable push top pop))
 
75
 
 
76
(defthm binding-bind
 
77
  (equal (binding x (bind var val alist))
 
78
         (if (equal x var)
 
79
             val
 
80
             (binding x alist))))
 
81
 
 
82
(defthm states
 
83
  (and (equal (call-stack (make-state call-stack defs)) 
 
84
              call-stack)
 
85
       (equal (defs (make-state call-stack defs)) defs) 
 
86
       (equal (pc (make-state 
 
87
                   (push (make-frame pc locals stack program)
 
88
                         call-stack)
 
89
                   defs))
 
90
              pc)
 
91
       (equal (locals (make-state 
 
92
                       (push (make-frame pc locals stack program)
 
93
                             call-stack)
 
94
                       defs))
 
95
              locals)
 
96
       (equal (stack (make-state 
 
97
                      (push (make-frame pc locals stack program)
 
98
                            call-stack)
 
99
                      defs))
 
100
              stack)
 
101
       (equal (program (make-state 
 
102
                        (push (make-frame pc locals stack program)
 
103
                              call-stack)
 
104
                        defs))
 
105
              program)))
 
106
 
 
107
(in-theory (disable make-state call-stack defs 
 
108
                    make-frame pc locals stack program))
 
109
 
 
110
; The next block of lemmas force ACL2 to expand certain functions
 
111
; in certain common situations, augmenting its heuristics 
 
112
; controlling expansion.
 
113
 
 
114
(defthm step-opener
 
115
  (implies (consp (next-inst s))
 
116
           (equal (step s) (do-inst (next-inst s) s))))
 
117
 
 
118
(in-theory (disable step))
 
119
 
 
120
(defthm run-opener
 
121
  (and (equal (run s 0) s)
 
122
       (implies (and (integerp n)
 
123
                     (> n 0))
 
124
                (equal (run s n)
 
125
                       (run (step s)(+ -1 n))))))
 
126
 
 
127
(defthm run-sum
 
128
  (implies (and (integerp i)
 
129
                (>= i 0)
 
130
                (integerp j)
 
131
                (>= j 0))
 
132
           (equal (run s (+ i j))
 
133
                  (run (run s i) j))))
 
134
  
 
135
(in-theory (disable run))