← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/pipeline/deterministic-systems/top/det-macros.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/2000/manolios/pipeline/pipeline/deterministic-systems/top/det-macros.lisp
 
1
;  Copyright (C) 2000 Panagiotis Manolios
 
2
 
 
3
;  This program is free software; you can redistribute it and/or modify
 
4
;  it under the terms of the GNU General Public License as published by
 
5
;  the Free Software Foundation; either version 2 of the License, or
 
6
;  (at your option) any later version.
 
7
 
 
8
;  This program is distributed in the hope that it will be useful,
 
9
;  but WITHOUT ANY WARRANTY; without even the implied warranty of
 
10
;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
11
;  GNU General Public License for more details.
 
12
 
 
13
;  You should have received a copy of the GNU General Public License
 
14
;  along with this program; if not, write to the Free Software
 
15
;  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
16
 
 
17
;  Written by Panagiotis Manolios who can be reached as follows.
 
18
 
 
19
;  Email: pete@cs.utexas.edu
 
20
 
 
21
;  Postal Mail:
 
22
;  Department of Computer Science
 
23
;  The University of Texas at Austin
 
24
;  Austin, TX 78701 USA
 
25
 
 
26
(in-package "ACL2")
 
27
#|
 
28
 
 
29
This is a set of macros for relating an abstract system and a concrete
 
30
system with a WEB.  The systems are deterministic.
 
31
 
 
32
|#
 
33
 
 
34
(defun bor-macro (lst)
 
35
  (declare (xargs :guard t))
 
36
  (if (consp lst)
 
37
      (if (consp (cdr lst))
 
38
          (list 'if
 
39
                (car lst)
 
40
                t
 
41
                (bor-macro (cdr lst)))
 
42
        (car lst))
 
43
    nil))
 
44
 
 
45
(defmacro bor (&rest args)
 
46
  (bor-macro args))
 
47
 
 
48
; The reason for the bor macro is that (or a b) gets expanded to (if a
 
49
; a b).  This results in extra rewriting in many situations.  bor is
 
50
; equivalent to or if all the arguments are booleans.
 
51
 
 
52
; Generate-Full-System is given abs-step, the function that steps the
 
53
; abstract system for one step, abs-p, the predicate that recognizes
 
54
; abstract states, con-step, the function that steps the concrete
 
55
; system for one step, con-p, the predicate that recognizes concrete
 
56
; states, and con-rank, the rank of a concrete state.  Note that I am
 
57
; assuming that the step of abstract and concrete states depends only
 
58
; on the state.  There may be situations in which this is not the
 
59
; case.  If so, use the non-deterministic versions of these macros.
 
60
; Also, I am assuming that the rank of abstract states is 0.  This may
 
61
; also not be the case in general.  R, B, and rank should be
 
62
; undefined.
 
63
 
 
64
(defmacro generate-full-system (abs-step abs-p con-step con-p 
 
65
                                con-to-abs good-con con-rank)
 
66
  `(progn 
 
67
 
 
68
     (defun WF-rel (x y) 
 
69
       (declare (xargs :normalize nil))
 
70
       (and (,abs-p x)
 
71
            (,con-p y)
 
72
            (,good-con y)
 
73
            (equal x (,con-to-abs y))))
 
74
 
 
75
     (defun B (x y) 
 
76
       (declare (xargs :normalize nil))
 
77
       (bor (WF-rel x y)
 
78
            (WF-rel y x)
 
79
            (equal x y)
 
80
            (and (,con-p x)
 
81
                 (,con-p y)
 
82
                 (,good-con x)
 
83
                 (,good-con y)
 
84
                 (equal (,con-to-abs x)
 
85
                        (,con-to-abs y)))))
 
86
 
 
87
     (defun rank (x) 
 
88
       (declare (xargs :normalize nil))
 
89
       (if (,con-p x)
 
90
           (,con-rank x)
 
91
         0))
 
92
 
 
93
     (defun R (x y)
 
94
       (declare (xargs :normalize nil))
 
95
       (cond ((,abs-p x)
 
96
              (equal y (,abs-step x)))
 
97
             (t (equal y (,con-step x)))))
 
98
 
 
99
     (encapsulate 
 
100
      ()
 
101
      (local (in-theory nil))
 
102
 
 
103
      (defthm WF-rel-fc
 
104
        (equal (Wf-rel x y)
 
105
               (and (,abs-p x)
 
106
                    (,con-p y)
 
107
                    (,good-con y)
 
108
                    (equal x (,con-to-abs y))))
 
109
        :hints (("goal" :by Wf-rel))
 
110
        :rule-classes ((:forward-chaining :trigger-terms ((Wf-rel x y)))))
 
111
 
 
112
      (defthm B-fc
 
113
        (equal (B x y) 
 
114
               (bor (WF-rel x y)
 
115
                    (WF-rel y x)
 
116
                    (equal x y)
 
117
                    (and (,con-p x)
 
118
                         (,con-p y)
 
119
                         (,good-con x)
 
120
                         (,good-con y)
 
121
                         (equal (,con-to-abs x)
 
122
                                (,con-to-abs y)))))
 
123
        :hints (("goal" :by B))
 
124
        :rule-classes ((:forward-chaining :trigger-terms ((B x y)))))
 
125
        
 
126
      (defthm rank-fc
 
127
        (equal (rank x) 
 
128
               (if (,con-p x)
 
129
                   (,con-rank x)
 
130
                 0))
 
131
        :hints (("goal" :by rank))
 
132
        :rule-classes ((:forward-chaining :trigger-terms ((rank x)))))
 
133
 
 
134
      (defthm R-fc 
 
135
        (equal (R x y)
 
136
               (cond ((,abs-p x)
 
137
                      (equal y (,abs-step x)))
 
138
                     (t (equal y (,con-step x)))))
 
139
        :hints (("goal" :by R))
 
140
        :rule-classes ((:forward-chaining :trigger-terms ((R x y)))))
 
141
      )
 
142
     )
 
143
  )
 
144
 
 
145
(defmacro prove-web (abs-step abs-p con-step con-p con-to-abs con-rank)
 
146
  `(progn
 
147
     (defthm B-is-a-WF-bisim-core
 
148
       (let ((u (,abs-step s))
 
149
             (v (,con-step w)))
 
150
         (implies (and (WF-rel s w)
 
151
                       (not (WF-rel u v)))
 
152
                  (and (WF-rel s v)
 
153
                       (e0-ord-< (,con-rank v) 
 
154
                                 (,con-rank w))))))
 
155
 
 
156
     (in-theory (disable b-is-a-wf-bisim-core))
 
157
 
 
158
     (defthm con-to-abs-type
 
159
       (,abs-p (,con-to-abs x)))
 
160
 
 
161
     (defthm abs-step-type
 
162
       (,abs-p (,abs-step x)))
 
163
 
 
164
     (defthm con-step-type
 
165
       (,con-p (,con-step x)))
 
166
 
 
167
     (defthm con-not-abs 
 
168
       (implies (,con-p x)
 
169
                (not (,abs-p x))))
 
170
 
 
171
     (defthm abs-not-con
 
172
       (implies (,abs-p x)
 
173
                (not (,con-p x))))))
 
174
 
 
175
(defmacro wrap-it-up (abs-step abs-p con-step con-p good-con con-to-abs con-rank)
 
176
  `(encapsulate
 
177
    ()
 
178
 
 
179
    (encapsulate 
 
180
     ()
 
181
     (local (in-theory nil))
 
182
 
 
183
     (local (in-theory (enable abs-step-type con-step-type con-not-abs abs-not-con 
 
184
                               con-to-abs-type
 
185
                               Wf-rel-fc B-fc
 
186
                               b-is-a-wf-bisim-core)))
 
187
    
 
188
     (defequiv b
 
189
       :hints (("goal" 
 
190
                :by (:functional-instance
 
191
                     encap-B-is-an-equivalence
 
192
  
 
193
                     (encap-abs-step ,abs-step)
 
194
                     (encap-abs-p ,abs-p)
 
195
                     (encap-con-step ,con-step)
 
196
                     (encap-con-p ,con-p)
 
197
                     (encap-con-to-abs ,con-to-abs)
 
198
                     (encap-good-con ,good-con)
 
199
                     (encap-con-rank ,con-rank)
 
200
                    
 
201
                     (encap-wf-rel wf-rel)
 
202
                     (encap-B B))))))
 
203
     
 
204
    (defthm rank-well-founded 
 
205
      (e0-ordinalp (rank x)))
 
206
 
 
207
    (defun-weak-sk exists-w-succ-for-u-weak (w u)
 
208
      (exists (v)
 
209
        (and (R w v)
 
210
             (B u v))))
 
211
 
 
212
    (defun-weak-sk exists-w-succ-for-s-weak (w s)
 
213
      (exists (v)
 
214
        (and (R w v)
 
215
             (B s v)
 
216
             (e0-ord-< (rank v) (rank w)))))
 
217
 
 
218
    (encapsulate 
 
219
     ()
 
220
     (local (in-theory nil))
 
221
 
 
222
     (defthm exists-w-succ-for-u-weak-fc
 
223
       (implies (and (R w v)
 
224
                     (B u v))
 
225
                (exists-w-succ-for-u-weak w u))
 
226
       :hints (("goal" :by exists-w-succ-for-u-weak-suff))
 
227
       :rule-classes ((:forward-chaining 
 
228
                       :trigger-terms ((r w v) (b u v)
 
229
                                       (exists-w-succ-for-u-weak w u)))))
 
230
 
 
231
     (defthm exists-w-succ-for-s-weak-fc
 
232
       (implies (and (R w v)
 
233
                     (B s v)
 
234
                     (e0-ord-< (rank v) (rank w)))
 
235
                (exists-w-succ-for-s-weak w s))
 
236
       :hints (("goal" :by exists-w-succ-for-s-weak-suff))
 
237
       :rule-classes ((:forward-chaining 
 
238
                       :trigger-terms ((r w v) (b s v)
 
239
                                       (exists-w-succ-for-s-weak w s))))))
 
240
 
 
241
    (local (in-theory nil))
 
242
 
 
243
    (local (in-theory (enable abs-step-type con-step-type con-not-abs abs-not-con 
 
244
                              con-to-abs-type
 
245
                              exists-w-succ-for-s-weak-fc exists-w-succ-for-u-weak-fc
 
246
                              R-fc Wf-rel-fc B-fc rank-fc 
 
247
                              b-is-a-wf-bisim-core)))
 
248
    
 
249
    (defthm b-is-a-wf-bisim-weak
 
250
      (implies (and (b s w)
 
251
                    (r s u))
 
252
               (or (exists-w-succ-for-u-weak w u)
 
253
                   (and (b u w)
 
254
                        (e0-ord-< (rank u) (rank s)))
 
255
                   (exists-w-succ-for-s-weak w s)))
 
256
      :hints (("goal" 
 
257
               :by (:functional-instance
 
258
                    B-is-a-WF-bisim-sk
 
259
                    
 
260
                    (encap-abs-step ,abs-step)
 
261
                    (encap-abs-p ,abs-p)
 
262
                    (encap-con-step ,con-step)
 
263
                    (encap-con-p ,con-p)
 
264
                    (encap-con-to-abs ,con-to-abs)
 
265
                    (encap-good-con ,good-con)
 
266
                    (encap-con-rank ,con-rank)
 
267
                    
 
268
                    (encap-R R)
 
269
                    (encap-wf-rel wf-rel)
 
270
                    (encap-B B)
 
271
                    (encap-rank rank)
 
272
                    
 
273
                    (encap-exists-w-succ-for-u exists-w-succ-for-u-weak)
 
274
                    (encap-exists-w-succ-for-s exists-w-succ-for-s-weak))))
 
275
      :rule-classes nil)
 
276
 
 
277
    (defun-sk exists-w-succ-for-u (w u)
 
278
      (exists (v)
 
279
        (and (R w v)
 
280
             (B u v))))
 
281
 
 
282
    (defun-sk exists-w-succ-for-s (w s)
 
283
      (exists (v)
 
284
        (and (R w v)
 
285
             (B s v)
 
286
             (e0-ord-< (rank v) (rank w)))))
 
287
 
 
288
    (local (in-theory nil))
 
289
    (local (in-theory (enable exists-w-succ-for-s-suff exists-w-succ-for-u-suff)))
 
290
 
 
291
    (defthm b-is-a-wf-bisim
 
292
      (implies (and (b s w)
 
293
                    (r s u))
 
294
               (or (exists-w-succ-for-u w u)
 
295
                   (and (b u w)
 
296
                        (e0-ord-< (rank u) (rank s)))
 
297
                   (exists-w-succ-for-s w s)))
 
298
      :hints (("goal" 
 
299
               :by (:functional-instance
 
300
                    B-is-a-WF-bisim-weak
 
301
                    
 
302
                    (exists-w-succ-for-u-weak exists-w-succ-for-u)
 
303
                    (exists-w-succ-for-s-weak exists-w-succ-for-s))))
 
304
      :rule-classes nil)
 
305
    )
 
306
  )