4
(ld ;; Newline to fool dependency scanner
5
"theorems.lisp" :ld-pre-eval-print t)
9
------------------------------
10
Author------------------: Fares Fraij
11
Email-------------------: fares@ahu.edu.jo
12
Date of last revision---: July 25, 2008
13
The used version of ACL2: 2.9.2 (under WindowsXP)
17
The goal of this book is to provide some proofs in directed acyclic graph
18
(DAG) theory. First, we prove that given an acyclic directed graph, the
19
replacement of any node within the graph with its siblings will NOT
20
introduce cycles (i.e., the acyclicity of the graph is maintained). Second,
21
we prove that dereferencing a certain index, within such a graph, and
22
dereferencing the same index after replacing an index with its sibling will
27
The acyclic directed graph is modeled by a list. Each entry of the list
28
has two components: a node, which is a natural number referred to as index
29
henceforth, and a data object represents the nodes' direct siblings.
30
This object may be an index, a string, or a structure consisting of
31
indexes, strings, or a combination of both. The graph is assumed to have
32
indexes as internal nodes and terminals (i.e., strings) as leafs.
34
This work proofs that applying certain substitutions (on the form of rules)
35
to an acyclic graph maintains certain properties. A rule is a tuple
36
consisting of two components: an index, which represents a node in the
37
graph, and a data object which represents the nodes' direct siblings (or
38
the transitive closure of the nodes' direct siblings). One of the properties
39
that we are interested in is that applying such a rule to an acyclic graph
40
will maintain acyclicity. We are also interested in proving that dereferencing
41
a certain index in the graph, before and after applying sucha rule, is the same.
45
(include-book "./functions")
46
;; Lemma: assoc-replaceValue
47
;; This lemma describes the relation between the functions assoc and replaceValue.
48
(defthm assoc-replaceValue
49
(implies (uniqueNodeIDp cp)
50
(equal (assoc p (replaceValue i v cp))
52
(if (equal p i) (cons p v) (assoc p cp))
56
;; Lemma: uniqueNodeIDp-replaceValue
57
;; This lemma states that replaceValue preserves uniqueNodeIDp
58
(defthm uniqueNodeIDp-replaceValue
59
(implies (uniqueNodeIDp cp)
60
(uniqueNodeIDp (replaceValue i v cp))))
62
;; Lemma: acyclicp1-perm-congruence
63
;; This lemma states that given to lists, seen1 and seen2,
64
;; which are permutations of each others, then chasing
65
;; an object in both of them leads to the same result.
66
(defthm acyclicp1-perm-congruence
67
(implies (perm seen1 seen2)
68
(equal (acyclicp1 p cp seen1) (acyclicp1 p cp seen2)))
69
:rule-classes :congruence)
71
;; Lemma: valueOf-replaceValue
72
;; This lemma describes the relation between the functions valueOf and replaceValue.
73
(defthm valueOf-replaceValue
74
(implies (and (uniqueNodeIDp cp)
76
(equal (valueOf p (replaceValue i q cp))
82
:hints (("Goal" :in-theory (enable valueOf))))
85
;; This lemma states that given the index x that exists as the car
86
;; of an entry in the constant pool cp, then the car of that entry
90
(equal (car (assoc x cp)) x)))
94
;; This lemma states that given a rule that belongs to the constant pool
95
;; cp, then the cdr of the result of looking up the car of rule in cp is
96
;; the cdr of rule itself.
98
(implies (and (uniqueNodeIDp cp)
99
(member-equal rule cp))
100
(equal (cdr (assoc (car rule) cp)) (cdr rule))))
103
;; This lemma states that given an index i, which ocuurs as
104
;; the car of an entry in cp and cp is well formed, then i is
107
(implies (and (assoc i cp)
110
:rule-classes :forward-chaining)
112
;; Lemma: no-immediate-loops
113
;; This lemma states that given that the natural number index i and
114
;; that the object obj is acyclic in cp and the list that results
115
;; from adding i to seen, then there is no match between obj and
116
;; any entry that has i as its car.
117
(defthm no-immediate-loops
118
(implies (and (natp i)
119
(acyclicp1 obj cp (cons i seen)))
120
(not (matchValueRulep obj (cons i x))))
123
;; Lemma: no-immediate-loops-useful
124
;; This lemma is a good rewrite rule version of the above lemma,
125
;; namely no-immediate-loops since it does not contain free variables.
126
(defthm no-immediate-loops-useful
127
(implies (and (uniqueNodeIDp cp)
128
(assoc (car rule) cp) ;;
129
(acyclicp1 (cdr rule)
130
cp (cons (car rule) seen)))
131
(not (matchValueRulep (cdr rule)
133
:hints (("Goal" :use (:instance no-immediate-loops
138
(in-theory (enable acyclicp))
140
;; Lemma: acyclicp-car
141
;; This lemma states that given the acyclic object p in cp
142
;; and p is a cons, then the car of p is acyclic in cp.
144
(implies (and (consp p)
146
(acyclicp (car p) cp)))
148
;; Lemma: acyclicp-cdr
149
;; This lemma states that given the acyclic object p in cp
150
;; and p is a cons, then the cdr of p is acyclic in cp.
152
(implies (and (consp p)
154
(acyclicp (cdr p) cp)))
156
;; Lemma: acyclicp-valueOf
157
;; This next proof is a little more interesting: If p is
158
;; acyclic, then (valueOf p c) is acyclic1 with respect to
159
;; seen = (cons p nil). But then by the acyclic1-cons theorem,
160
;; (valueOf p c) is acyclic1 with respect to seen = nil, which means
162
(defthm acyclicp-valueOf
163
(implies (and (natp p)
165
(acyclicp (valueOf p cp) cp))
167
(("Goal'" :expand (acyclicp1 p cp nil))))
169
;; Now I turn it back off...
170
(in-theory (disable acyclicp))
172
;; Lemma: valueOf-apply-rule-to-entry-1
173
;; This lemma descibes the behavior of the functions valueOf and
174
;; apply-rule-to-entry-1: (valueOf p (apply-rule-to-entry-1 rule i c)).
175
(defthm valueOf-apply-rule-to-entry-1
176
(implies (and (uniqueNodeIDp cp)
178
(equal (valueOf p (apply-rule-to-entry-1 rule i cp))
180
(if (matchValueRulep (valueOf p cp) rule)
181
(applySubstitution (valueOf p cp) rule)
184
:hints (("Goal" :in-theory (enable valueOf))))
186
;; Lemma: valueOf-apply-rule-to-entry
187
;; I prove a similar lemma of the above that describes the behavior of
188
;; the functions valueOf and apply-rule-entry:
189
;; (valueOf p (apply-rule-to-entry rule i c)).
190
(defthm valueOf-apply-rule-to-entry
191
(implies (and (uniqueNodeIDp cp)
193
(equal (valueOf p (apply-rule-to-entry rule i cp))
194
(if (ok-rulep rule cp)
195
(valueOf p (apply-rule-to-entry-1 rule i cp))
197
:hints (("Goal" :in-theory (disable apply-rule-to-entry-1))))
199
;; Lemma: natp-car-assoc-i-c
200
;; This lemma states that if the car of looking up the index i in cp
201
;; is a natural number, then i exists as the car of an enry in cp.
202
(defthm natp-car-assoc-i-c
203
(implies (natp (car (assoc i cp)))
207
;; The following Lemmas are two types:
208
;; (1) The first types states that given an index p that exists
209
;; as the car of an entry in cp, then this index also exists
210
;; in cp after applying the following functions to it:
211
;; apply-rule-to-entry-1, apply-rule-to-entry,
212
;; apply-rule-list-to-entry, and once_tdl.
213
;; (2) The second types states that given a well formed cp,
214
;; then the cp will also be well fomed after applying
215
;; apply-rule-to-entry-1, apply-rule-to-entry,
216
;; apply-rule-list-to-entry, and once_tdl.
218
(defthm assoc-p-apply-rule-to-entry-1
219
(implies (assoc p cp)
221
(apply-rule-to-entry-1 rule i cp)))
222
:hints (("Goal" :in-theory (enable valueOf))))
224
(defthm assoc-p-apply-rule-to-entry
225
(implies (assoc p cp)
227
(apply-rule-to-entry rule i cp)))
228
:hints (("Goal" :in-theory (disable apply-rule-to-entry-1))))
231
(defthm uniqueNodeIDp-apply-rule-to-entry
232
(implies (uniqueNodeIDp cp)
233
(uniqueNodeIDp (apply-rule-to-entry rule
237
;; Theorem: acyclicp1-applySubstitution
238
;; This theorem states that given the well formed constant pool cp,
239
;; the object p, which is acyclic in cp given seen, and a rule that
240
;; has an acyclic cdr, then the object that results from replacing
241
;; the occurences of (car rule) in p with (cdr rule) is also acyclic
242
;; in cp given the same seen.
243
(defthm acyclicp1-applySubstitution
244
(implies (and (uniqueNodeIDp cp)
245
(acyclicp1 p cp seen)
246
(acyclicp1 (cdr rule) cp seen))
247
(acyclicp1 (applySubstitution p rule) cp seen)))
249
;; Theorem: acyclicp-applySubstitution
250
;; This theorem states that given the well formed constant pool cp,
251
;; the object p, which is acyclic in cp, and a well fomed rule in cp,
252
;; then the object that results from replacing the occurences of
253
;; (car rule) in p with (cdr rule) is also acyclic in cp. Note that
254
;; this theorem serves as a wrapper for the previous theorem, namely
255
;; acyclicp1-applySubstitution
257
(defthm acyclicp-applySubstitution
258
(implies (and (uniqueNodeIDp cp)
260
(acyclicp (cdr rule) cp))
261
(acyclicp (applySubstitution p rule) cp))
262
:hints (("Goal" :in-theory (enable acyclicp))))
264
;; Lemma: acyclicp-assoc
265
;; This lemma states that given the natural number p that
266
;; is acyclic in cp, then p exists as the car of one of the
268
(defthm acyclicp-assoc
269
(implies (and (natp p)
272
:hints (("Goal" :expand (acyclicp p cp))))
274
;; Lemma: assoc-acyclicp1-seen-acyclicp1-nil
275
;; This lemma states that given that natural number p
276
;; which occur as the car of one of the entries of cp and
277
;; the value bounded to p in cp is acyclic in cp given the
278
;; list (cons p seen), then p is acyclic in cp given the
280
(defthm assoc-acyclicp1-seen-acyclicp1-nil
281
(implies (and (natp p)
283
(acyclicp1 (valueOf p cp) cp (cons p seen)))
284
(acyclicp1 p cp nil))
285
:hints (("goal" :expand (acyclicp1 p cp nil)
286
:use (:instance subsetp-acyclicp1
289
(visited2 (cons p seen))))))
292
;; Lemma: acyclicp1-seen-acyclicp1-nil
293
;; This lemma states that if the index p is acyclic
294
;; in cp given the list seen, the p is also acyclic
295
;; in cp given the empty list, nil.
296
(defthm acyclicp1-seen-acyclicp1-nil
297
(implies (acyclicp1 p cp seen)
298
(acyclicp1 p cp nil)))
300
;; Lemma: acyclicp1-p-acyclicp1-valueOf
301
;; This lemma states that if the index p is acyclic
302
;; in cp given the list seen, the (valueOf p cp) is also acyclic
303
;; in cp given seen = (cons p seen)
304
(defthm acyclicp1-seen-acyclicp1-valueOf-seen
305
(implies (and (acyclicp1 p cp seen)
307
(acyclicp1 (valueOf p cp) cp seen))
308
:rule-classes :forward-chaining)
310
;; Theorem: dref-applySubstitution
311
;; This theorem states that given the well formed cp, the well formed
312
;; rule in cp, and the acyclic object p in cp, then the result of dereferencing
313
;; p in cp is the same as dereferencing the modified p in cp. P is modified by
314
;; replacing every ocuurence of the (car rule) in p with (cdr rule).
316
(defthm dref-applySubstitution
317
(implies (and (uniqueNodeIDp cp)
319
(acyclicp (cdr rule) cp)
320
(equal (dref (car rule) cp)
321
(dref (cdr rule) cp))) ;;
322
(equal (dref (applySubstitution p rule) cp)
324
:hints (("Goal" :in-theory (enable acyclicp))))
326
;; Lemma: subsetp-union-equal-or
327
;; This lemma states that if x is a subset of y
328
;; and a is a subset of x union y, then either
329
;; a is subset of x or a is subset of y.
330
(defthm subsetp-union-equal-or
331
(implies (and (subsetp x y)
332
(subsetp a (union-equal x y)))
335
:rule-classes :forward-chaining)
338
; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.]
340
;; Lemma: member-is-member-equal
341
;; This I developed since I wanted to
342
;; consentarate on the use of member-equal
343
;; instead of member. These two predicates are
344
;; equivalent in the logic mode; however,
345
;; they are different in the programming mode.
346
(defthm member-is-member-equal
347
(equal (member i seen)
348
(member-equal i seen)))
351
;; Lemma(s): The following set of lemmas are general
352
;; facts about set theory operations.
353
;; Begin of set general set theory lemmas
354
(defthm member-equal-intersectp
355
(implies (member-equal i x)
356
(intersectp-equal x (cons i seen))))
358
(defthm intersectp-equal-x-y-seen
359
(iff (intersectp-equal (union-equal x
362
(or (intersectp-equal x seen)
363
(intersectp-equal y seen))))
366
(defthm intersectp-equal-not-acyclicp1
367
(implies (intersectp-equal (all-indexes-in-obj obj) seen)
371
(defthm not-acyclicp-cons-any
372
(implies (not (acyclicp1 obj cp seen))
373
(not (acyclicp1 obj cp (cons any seen)))))
375
;; Lemma-3: needs Lemma-1 + Lemma-2
376
(defthm intersectp-equal-indexes-acyclicp1
377
(implies (intersectp-equal (indexes-from-obj i cp)
379
(equal (acyclicp1 i cp seen) nil)))
381
(defthm member-intersectp-equal
382
(implies (and (member-equal e x)
384
(intersectp-equal x y)))
386
(defthm member-equal-union-equal
387
(iff (member-equal i (union-equal y z))
388
(or (member-equal i z)
389
(member-equal i y))))
390
;; End of set general set theory lemmas
391
;;--------------------------------------------------
393
;;--------------------------------------------------
394
;; Lemma: transitivity-of-member-equal
395
;; In this lemma I start to use the function
396
;; indexes-from-obj, which takes as inputs the object p
397
;; and a cp and returns all the indexes on the paths starting
399
;; This lemma states that given that the index i is member
400
;; on the set of all indexes in cp strating from p and
401
;; j is a member on the set of all indexes in cp starting
402
;; from i, then j is a member on the set of all indexes in
403
;; cp starting from p.
404
;; Another way to express the idea of this lemma is that:
405
;; if the index i is within the subtree of the indexes strating
406
;; from p and the index j is within the subtree of indexes
407
;; starting from i, then j is within the subtree of indexes
411
(defthm acyclicp-member-equal-all-indexes
412
(implies (and (acyclicp obj cp)
413
(member-equal i (all-indexes-in-obj obj))
414
(member-equal j (indexes-from-obj i cp)))
415
(member-equal j (indexes-from-obj obj cp))))
417
;; Lemma-2 needs Lemma-1
418
(defthm transitivity-of-member-equal
419
(implies (and (member-equal i (indexes-from-obj p cp))
420
(member-equal j (indexes-from-obj i cp)))
421
(member-equal j (indexes-from-obj p cp))))
424
;;------------------------------------------------------------
425
;; Lemma: member-equal-subset-index-from-obj
426
;; This lemma states that if the index i is within the
427
;; the subtree starting from p, then the set of indexes
428
;; starting from i in cp is a subset from the set of
429
;; indexes strating from p in cp.
430
(defthm acyclicp-member-equal-all-indexes-from
431
(implies (and (acyclicp obj cp)
432
(member-equal i (all-indexes-in-obj obj)))
433
(subsetp (indexes-from-obj i cp)
434
(indexes-from-obj obj cp))))
436
(defthm member-equal-subset-index-from-obj
437
(implies (member-equal i (indexes-from-obj p cp))
438
(subsetp (indexes-from-obj i cp)
439
(indexes-from-obj p cp))))
442
;;------------------------------------------------------------
443
;; Lemma: subsetp-member-equal-i-subsetp-cons-i
444
;; This lemma states that given the set of indexes
445
;; starting from i in cp is a subset from the set
446
;; of indexes strating from p in cp and i is
447
;; within the subtree starting from p, then
448
;; the set that results from adding the index i to
449
;; the set of indexes starting from the index
450
;; associated with i in cp is a subset from the set
451
;; of indexes strating from p.
452
;; The following lemmas are about the relation between
453
;; subset, indexes-from-obj, and member.
454
;;---------------------------------------------------
455
;; Begin of lemmas that are about the relation between
456
;; subset, indexes-from-obj, and member.
457
(defthm acyclicp-member-equal-all-indexes-fron-valueOf
458
(implies (and (acyclicp obj cp)
459
(member-equal i (all-indexes-in-obj obj)))
460
(subsetp (indexes-from-obj (valueOf i cp) cp)
461
(indexes-from-obj obj cp))))
463
(defthm subsetp-member-equal-i-subsetp-cons-i
464
(implies (and (subsetp (indexes-from-obj i cp)
465
(indexes-from-obj p cp))
466
(member-equal i (indexes-from-obj p cp)))
467
(subsetp (cons i (indexes-from-obj (valueOf i cp) cp))
468
(indexes-from-obj p cp)))
469
:rule-classes :forward-chaining)
471
(defthm subsetp-member-equal-i-subsetp-cons-i-1
472
(implies (and (subsetp (indexes-from-obj i cp)
473
(indexes-from-obj p cp))
474
(member-equal i (indexes-from-obj p cp)))
475
(subsetp (indexes-from-obj (valueOf i cp) cp)
476
(indexes-from-obj p cp)))
477
:rule-classes :forward-chaining)
479
(defthm not-subsetp-pfo-valueOf-not-member-equal-pfo
480
(implies (not (subsetp (indexes-from-obj (valueOf i cp) cp)
481
(indexes-from-obj p1 cp)))
482
(not (member-equal i (indexes-from-obj p1 cp))))
483
:rule-classes :forward-chaining)
485
(defthm not-subsetp-cons-pfo-valueOf-not-member-equal-pfo
486
(implies (not (subsetp (cons i (indexes-from-obj (valueOf i cp) cp))
487
(indexes-from-obj p1 cp)))
488
(not (member-equal i (indexes-from-obj p1 cp))))
489
:rule-classes :forward-chaining)
490
;;---------------------------------------------------
491
;; End of lemmas that are about the relation between
492
;; subset, indexes-from-obj, and member.
493
;;----------------------------------------------------
495
;; Lemma acyclicp1-car-cdr states that given an object p
496
;; in which its first and its second components are acyclic
497
;; in the constant pool cp, Then the object p itself is
500
(defthm acyclicp1-car-cdr
501
(implies (and (consp p)
502
(acyclicp1 (car p) cp seen)
503
(acyclicp1 (cdr p) cp seen))
505
:hints (("Goal" :in-theory (enable acyclicp))))
507
;; Lemma acyclicp1-valueOf-p-c-assoc-p-c states that given
508
;; a natural number p for which the object associated
509
;; with in cp is acyclic in cp with respect to list of
510
;; encountered indexes so far, namely seen, then p
511
;; itself is acyclic in cp with respect to seen.
513
(defthm acyclicp1-valueOf-p-c-assoc-p-c
514
(implies (and (natp p)
515
(acyclicp1 (valueOf p cp) cp (cons p seen)))
517
:hints (("Goal" :in-theory (enable valueOf acyclicp))))
519
;; Lemma acyclicp1-valueOf-p-c-acyclicp1-p is a more
520
;; restricted version of the Lemma
521
;; acyclicp1-valueOf-p-c-assoc-p-c (above).
523
(defthm acyclicp1-valueOf-p-c-acyclicp1-p
524
(implies (and (natp p)
525
(acyclicp1 (valueOf p cp) cp (cons p seen)))
527
:hints (("Goal" :in-theory (enable acyclicp))))
529
;; Lemma assoc-p-c-assoc-p-replaceValue-i-x-c states that if
530
;; an index is associated with a cp, then it is also
531
;; associated with the cp that results from inserting
532
;; an index i in original cp.
533
(defthm assoc-p-c-assoc-p-replaceValue-i-x-c
534
(implies (assoc p cp)
535
(assoc p (replaceValue i x cp))))
537
;; Lemma acyclicp1-a-replaceValue-i-x-c-seen-1 states that given
538
;; an ok constant pool, an acyclic pointer, p, in the cp
539
;; wrt seen, and i is not reachable from p, then p is
540
;; also acyclic wrt seen in the result of inserting
541
;; an index i associated with object x in the original cp.
544
(local (in-theory (disable
545
intersectp-equal-indexes-acyclicp1
551
(defthm acyclicp1-a-replaceValue-i-x-c-seen-1
552
(implies (and (uniqueNodeIDp cp)
553
(acyclicp1 p cp seen)
557
(all-indexes-in-obj p))))
560
(not (member-equal i (indexes-from-obj p cp))))
561
(acyclicp1 p (replaceValue i x cp) seen))))
564
;; Lemma acyclicp-applySubstitution-replaceValue-1 is a more restricted
565
;; version of Lemma acyclicp1-a-replaceValue-i-x-c-seen-1 (above)
567
(defthm acyclicp-applySubstitution-replaceValue-1
568
(implies (and (uniqueNodeIDp cp)
571
(not (member-equal i (all-indexes-in-obj p))))
574
(not (member-equal i (indexes-from-obj p cp))))
576
(replaceValue i any cp)))
577
:hints (("Goal" :in-theory (enable acyclicp))))
579
;; Lemma not-subsetp-not-member-equal-1 states that given
580
;; that the set of indexes starting from i in cp is not a subset
581
;; of that from x in cp, then i does not belong to the set
582
;; of indexes from x in cp.
584
(defthm not-subsetp-not-member-equal-1
585
(implies (not (subsetp (indexes-from-obj i cp)
586
(indexes-from-obj x cp)))
587
(not (member-equal i (indexes-from-obj x cp)))))
589
;; Lemma acyclicp1-subsetp-pfo-valueOf-pfo states that given an ok
590
;; constant pool, cp, the index i is associated with an entry in cp,
591
;; and i is acyclic in cp wrt seen, then the set of indexes
592
;; starting from the object associated with i in cp is a subset
593
;; of that from i in cp.
595
(defthm acyclicp1-subsetp-pfo-valueOf-pfo
596
(implies (and (assoc i cp)
598
(acyclicp1 i cp seen))
599
(subsetp (indexes-from-obj (valueOf i cp) cp)
600
(indexes-from-obj i cp)))
601
:rule-classes :forward-chaining)
603
;; Lemma acyclicp-subsetp-pfo-valueOf-pfo is a more restrictive
604
;; version of Lemma acyclicp1-subsetp-pfo-valueOf-pfo (above).
605
(defthm acyclicp-subsetp-pfo-valueOf-pfo
606
(implies (and (assoc i cp)
609
(subsetp (indexes-from-obj (valueOf i cp) cp)
610
(indexes-from-obj i cp)))
611
:rule-classes :forward-chaining)
613
;; Lemma acyclicp1-not-member-equal-pfo states that given an ok
614
;; constant pool, cp, the index i is associated with an entry in cp,
615
;; and i is acyclic in cp wrt seen, then i does not belong to
616
;; the set of indexes starting from the object assocted with
619
(defthm acyclicp1-not-member-equal-pfo
620
(implies (and (assoc i cp)
622
(acyclicp1 i cp seen))
623
(not (member-equal i (indexes-from-obj (valueOf i cp) cp))))
624
:rule-classes (:rewrite :forward-chaining))
626
;; Lemma acyclicp-not-member-equal-pfo is a more restrictive
627
;; version of Lemma acyclicp1-not-member-equal-pfo (above).
628
(defthm acyclicp-not-member-equal-pfo
629
(implies (and (assoc i cp)
632
(not (member-equal i (indexes-from-obj (valueOf i cp) cp))))
633
:hints (("Goal" :in-theory (enable acyclicp)))
634
:rule-classes (:rewrite :forward-chaining))
636
;; Lemma subsetp-not-subsetp-member-equal states that
637
;; if x is subset of the list that results from adding
638
;; the element i to y, and x is not a subset of y,
639
;; then i is equal to x.
640
(defthm subsetp-not-subsetp-member-equal
641
(implies (and (subsetp x
646
:rule-classes :forward-chaining)
648
;; Lemma perm-list-1 states that given the acyclic object (valueOf i cp), which represents
649
;; the object associated with i in cp, wrt to the list that consists of adding
650
;; i and p to seen, then the object (valueOf i cp) is also acyclic in cp wrt the
651
;; list that consists of adding p and i to seen.
653
(implies (acyclicp1 (valueOf i cp) cp (list* p i seen))
654
(acyclicp1 (valueOf i cp) cp (list* i p seen)))
655
:rule-classes :forward-chaining)
657
;; Lemma member-equal-subsetp-member-equal states that
658
;; if the element i is member in the list x, and x is a subset
659
;; of the list y, then i is belongs to y.
660
(defthm member-equal-subsetp-member-equal
661
(implies (and (member-equal i x)
665
;; Lemma matchValueRulep-valueOf-rule-implies-member-objp-r1-valueOf states that
666
;; if there is a match between the object valueOf and rule, then
667
;; the first component of the rule belongs to valueOf.
669
(defthm matchValueRulep-valueOf-rule-implies-member-objp-r1-valueOf
670
(implies (matchValueRulep valueOf rule)
671
(member-objp (car rule) valueOf)))
674
;; Lemma acyclicp1-obj-member-objp-i-acyclicp1-i states that given
675
;; an acyclic object valueOf in cp wrt seen and the element i belongs to valueOf,
676
;; then i is also acyclic in cp wrt seen.
678
(defthm acyclicp1-obj-member-objp-i-acyclicp1-i
679
(implies (and (acyclicp1 valueOf cp seen)
680
(member-objp i valueOf))
681
(acyclicp1 i cp seen)))
684
;; Lemma acyclicp1-obj-member-objp-i-acyclicp1-i-1 is a restricted
685
;; version of Lemma acyclicp1-obj-member-objp-i-acyclicp1-i (above).
687
(defthm acyclicp1-obj-member-objp-i-acyclicp1-i-1
688
(implies (and (acyclicp valueOf cp)
689
(member-objp i valueOf))
693
(defthm matchValueRulep-member-i-valueOf-subsetp-pfo-i
694
(implies (and (matchValueRulep valueOf rule)
695
(acyclicp1 valueOf cp seen))
696
(subsetp (indexes-from-obj (car rule) cp)
697
(indexes-from-obj valueOf cp))))
700
;; Lemma i-not-member-valueOf-subsetp-pfo-r1-valueOf states that
701
;; given that the index i is not reachable from the object valueOf in cp,
702
;; there is a match between the index i and rule, and valueOf is acyclic
703
;; in cp wrt seen, then i is not reachable from the first
704
;; component of rule.
705
(defthm i-not-member-valueOf-subsetp-pfo-r1-valueOf
706
(implies (and (not (member-equal i (indexes-from-obj valueOf cp)))
707
(matchValueRulep valueOf rule)
708
(acyclicp1 valueOf cp seen))
709
(not (member-equal i (indexes-from-obj (car rule) cp)))))
712
;; Lemma not-member-i-pfo-valueOf-matchValueRulep-valueOf-rule-not-member-i-pfo-cdr-rule
713
;; states that given that the index i is not reachable from object valueOf
714
;; in cp, there is a match between valueOf and rule, valueOf is acyclic in cp
715
;; wrt seen, and the set of indexes accumulated from the second
716
;; component of rule in cp is a subset of that accumulated from the
717
;; first component of rule in cp, then the index i is not reachable
718
;; from the second component of rule in cp.
719
(defthm not-member-i-pfo-valueOf-matchValueRulep-valueOf-rule-not-member-i-pfo-cdr-rule
720
(implies (and (not (member-equal i (indexes-from-obj valueOf cp)))
721
(matchValueRulep valueOf rule)
722
(acyclicp1 valueOf cp seen)
723
(subsetp (indexes-from-obj (cdr rule) cp)
724
(indexes-from-obj (car rule) cp)))
725
(not (member-equal i (indexes-from-obj (cdr rule) cp)))))
729
(local (in-theory (disable
731
intersectp-equal-not-acyclicp1
733
intersectp-equal-indexes-acyclicp1
739
not-subsetp-not-member-equal-1
740
not-acyclicp-cons-any
741
acyclicp1-obj-member-objp-i-acyclicp1-i-1
743
acyclicp-member-equal-all-indexes
746
;; Lemma acyclicp1-not-member-equal-pfo-applySubstitution
747
;; states that given a rule that represent a cons, the first
748
;; component of the rule appears as the first component of
749
;; an entry in cp, an ok constant pool, cp, the set of indexes
750
;; accumulated from the second component of rule in cp is
751
;; a subset of that accumulated from the first component of
752
;; rule in cp, the second component of the rule is acyclic
753
;; in cp wrt seen, the object x is acyclic in cp wrt seen,
754
;; and the index i is not reachable from object x in cp,
755
;; then the index i is not reachable from the object that
756
;; results from replacing every occurence of the rhs of
757
;; the rule in x with the lhs of the rule.
759
(defthm acyclicp1-not-member-equal-pfo-applySubstitution
760
(implies (and (consp rule)
762
(assoc (car rule) cp)
763
(subsetp (indexes-from-obj (cdr rule) cp)
764
(indexes-from-obj (car rule) cp))
765
(acyclicp1 (cdr rule) cp seen)
766
(acyclicp1 x cp seen)
767
(not (member-equal i (indexes-from-obj x cp))))
770
(applySubstitution x rule)
774
;; Lemma not-assoc-i-cp-replaceValue-i-cp-is-cp states that
775
;; given the ok constant pool cp and the index i
776
;; does not belong to the domain of cp, then
777
;; the result of inserting the object that associates
778
;; the index i with the object any is actually cp itself.
779
(defthm not-assoc-i-cp-replaceValue-i-cp-is-cp
780
(implies (and (uniqueNodeIDp cp)
782
(equal (replaceValue i any cp)
787
(local (in-theory (disable
788
intersectp-equal-not-acyclicp1
790
intersectp-equal-indexes-acyclicp1
796
;; Lemma acyclicp1-applySubstitution-replaceValue-1 states that
797
;; given an ok constant pool, cp, the index i is
798
;; acyclic in cp wrt seen, the object p is acyclic
799
;; in cp wrt seen, the index i is not reachable
800
;; from the object p in cp, then the object p is
801
;; acyclic in the new cp, which results from associating
802
;; the index i with the bject any in the orignal cp,
804
(defthm acyclicp1-applySubstitution-replaceValue-1
805
(implies (and (uniqueNodeIDp cp)
806
(acyclicp1 i cp seen)
807
(acyclicp1 p cp seen)
808
(not (member-equal i (all-indexes-in-obj p)))
809
(not (member-equal i (indexes-from-obj p cp))))
811
(replaceValue i any cp)
814
;; Lemma acyclicp1-not-member-equal-pfo-acyclicp1
815
;; states that given an acyclic index, i, in cp
816
;; wrt seen and i is not reachable from the index p,
817
;; i is not reachable from the index p,
818
;; then the index i is acyclic in cp wrt to the new
819
;; list that results from adding p to seen.
820
(defthm acyclicp1-not-member-equal-pfo-acyclicp1
821
(implies (and (acyclicp1 i cp seen)
822
(not (member-equal p (all-indexes-in-obj i)))
823
(not (member-equal p (indexes-from-obj i cp))))
824
(acyclicp1 i cp (cons p seen))))
828
;; Lemma acyclicp1-assoc-acyclicp1-valueOf states that given
829
;; an ok constant pool, cp, an acyclic index i in cp
830
;; wrt seen, and i appears as the first component of
831
;; of an entry in cp, then the object associated with
832
;; i in cp is also acyclic wrt seen.
834
(defthm acyclicp1-assoc-acyclicp1-valueOf
835
(implies (and (uniqueNodeIDp cp)
836
(acyclicp1 i cp seen)
838
(acyclicp1 (valueOf i cp) cp seen))
839
:rule-classes :forward-chaining)
842
;; Lemma acyclicp-assoc-acyclicp1-valueOf is a restricted
843
;; version of Lemma acyclicp1-assoc-acyclicp1-valueOf (above).
844
(defthm acyclicp-assoc-acyclicp1-valueOf
845
(implies (and (uniqueNodeIDp cp)
848
(acyclicp (valueOf i cp) cp))
849
:rule-classes :forward-chaining)
852
;; Lemma acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-1
853
;; states that given an ok constant pool, cp, an acyclic
854
;; index i in cp wrt seen, i appears as the first component of
855
;; of an entry in cp, and the index x belongs to the object
856
;; (valueOf i cp) that is associated with i in cp, then x
857
;; is acyclic in cp wrt seen.
859
(defthm acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-1
860
(implies (and (uniqueNodeIDp cp)
861
(acyclicp1 i cp seen)
863
(member-objp x (valueOf i cp)))
864
(acyclicp1 x cp seen)))
867
;; Lemma acyclicp-obj-member-objp-i-acyclicp1-i-1-prime-1
868
;; is a restricted version of Lemma
869
;; acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-1 (above).
870
(defthm acyclicp-obj-member-objp-i-acyclicp1-i-1-prime-1
871
(implies (and (uniqueNodeIDp cp)
874
(member-objp x (valueOf i cp)))
878
;; Lemma acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-2
879
;; states that given an ok constant pool, cp, an acyclic
880
;; index i in cp wrt seen, i appears as the first component of
881
;; of an entry in cp, and the index x is equal to i, then x
882
;; is acyclic in cp wrt seen.
884
(defthm acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-2
885
(implies (and (uniqueNodeIDp cp)
886
(acyclicp1 i cp seen)
888
(member-equal x (all-indexes-in-obj i)))
889
(acyclicp1 x cp seen)))
892
;; Lemma acyclicp-obj-member-objp-i-acyclicp1-i-1-prime-2-1
893
;; is a restricted version of Lemma
894
;; acyclicp1-obj-member-objp-i-acyclicp1-i-1-prime-2 (above).
895
(defthm acyclicp-obj-member-objp-i-acyclicp1-i-1-prime-2-1
896
(implies (and (uniqueNodeIDp cp)
899
(member-equal x (all-indexes-in-obj i)))
903
;; Lemma matchValueRulep-member-i-valueOf-subsetp-pfo-i-1
904
;; states that given an ok constant pool, cp, an acyclic
905
;; index i in cp wrt seen, i appears as the first component of
906
;; of an entry in cp, and a match exists between
907
;; the object (valueOf i cp), which represents the object
908
;; associated with i in cp, and rule, then
909
;; the set of indexes accumulated from the first component
910
;; of rule in cp is a subset of that accumulated from i in cp.
911
(defthm matchValueRulep-member-i-valueOf-subsetp-pfo-i-1
912
(implies (and (matchValueRulep (valueOf i cp) rule)
914
(acyclicp1 i cp seen)
916
(subsetp (indexes-from-obj (car rule) cp)
917
(indexes-from-obj i cp))))
920
;; Lemma matchValueRulep-member-i-valueOf-subsetp-pfo-i-1-1
921
;; is a restricted version of Lemma
922
;; matchValueRulep-member-i-valueOf-subsetp-pfo-i-1 (above).
923
(defthm matchValueRulep-member-i-valueOf-subsetp-pfo-i-1-1
924
(implies (and (matchValueRulep (valueOf i cp) rule)
928
(subsetp (indexes-from-obj (car rule) cp)
929
(indexes-from-obj i cp)))
930
:hints (("Goal" :use ((:instance matchValueRulep-member-i-valueOf-subsetp-pfo-i-1
932
:in-theory (e/d (acyclicp)
933
(matchValueRulep-member-i-valueOf-subsetp-pfo-i-1)))))
936
;;----------------------------------
938
(local (in-theory (disable
939
intersectp-equal-not-acyclicp1
941
intersectp-equal-indexes-acyclicp1
947
;; Lemma i-not-member-valueOf-subsetp-pfo-r1-valueOf-1-
948
;; states that given the object p is not reachable
949
;; from the index i, an ok constant pool, cp,
950
;; an acyclic index i in cp wrt seen, i appears
951
;; as the first component of of an entry in cp,
952
;; and a match exists between the object (valueOf i cp),
953
;; which represents the object associated with i
954
;; in cp, and rule, then p is not reachable
955
;; from the first component of rule.
957
(defthm i-not-member-valueOf-subsetp-pfo-r1-valueOf-1-
958
(implies (and (not (member-equal p (indexes-from-obj i cp)))
960
(acyclicp1 i cp seen)
962
(matchValueRulep (valueOf i cp) rule))
963
(not (member-equal p (indexes-from-obj (car rule) cp)))))
966
;; Lemma i-not-member-valueOf-subsetp-pfo-r1-valueOf-1-1- is
967
;; a restricted version of Lemma
968
;; i-not-member-valueOf-subsetp-pfo-r1-valueOf-1-
969
(defthm i-not-member-valueOf-subsetp-pfo-r1-valueOf-1-1-
970
(implies (and (not (member-equal p (indexes-from-obj i cp)))
974
(matchValueRulep (valueOf i cp) rule))
975
(not (member-equal p (indexes-from-obj (car rule) cp))))
976
:hints (("Goal" :in-theory (enable acyclicp))))
979
;; Lemma |(cdr rule) is not reachable from p|
980
;; states that given that the object p is not reachable
981
;; from the index i, a match exists between the object (valueOf i cp),
982
;; which represents the object associated with i
983
;; in cp, and rule, an acyclic index i in cp wrt seen,
984
;; an ok constant pool, cp, i appears as the first
985
;; component of of an entry in cp, and the set of
986
;; indexes accumulated from the second component of rule
987
;; in cp is a subset of that accumulated from the
988
;; first component of rule in cp, then p is not reachable
989
;; from the second component of rule.
990
(defthm |(cdr rule) is not reachable from p|
991
(implies (and (not (member-equal p (indexes-from-obj i cp)))
992
(matchValueRulep (valueOf i cp) rule)
993
(acyclicp1 i cp seen)
996
(subsetp (indexes-from-obj (cdr rule) cp)
997
(indexes-from-obj (car rule) cp)))
998
(not (member-equal p (indexes-from-obj (cdr rule) cp))))
999
:rule-classes :forward-chaining)
1003
;; |(cdr rule) is not reachable from p rst|
1004
;; is a restricted version of Lemma
1005
;; |(cdr rule) is not reachable from p|
1007
(defthm |(cdr rule) is not reachable from p rst|
1008
(implies (and (not (member-equal p (indexes-from-obj i cp)))
1009
(matchValueRulep (valueOf i cp) rule)
1013
(subsetp (indexes-from-obj (cdr rule) cp)
1014
(indexes-from-obj (car rule) cp)))
1015
(not (member-equal p (indexes-from-obj (cdr rule) cp))))
1016
:hints (("Goal" :in-theory (enable acyclicp)))
1017
:rule-classes :forward-chaining)
1021
;; Lemma replaceValue-i-valueOf-i-cp-is-cp states that given an
1022
;; ok constant pool cp, then the result of inseting
1023
;; i and the object (valueOf i cp), which represent the
1024
;; object associted with i in cp, back in the cp
1025
;; is equal to the original cp.
1026
(defthm replaceValue-i-valueOf-i-cp-is-cp
1027
(implies (uniqueNodeIDp cp)
1028
(equal (replaceValue i (valueOf i cp) cp)
1030
:hints (("Goal" :cases ((not (assoc i cp)))
1031
:in-theory (enable valueOf assoc))))
1034
;; Lemma acyclicp1-replaceValue-i-i-x states that given an acyclic
1035
;; index, i, in cp, and i appears as the first
1036
;; component of an entry in cp, and cp is an ok
1037
;; constant pool, then i is also acyclic in
1038
;; the new cp that results from insering i with its associated
1039
;; object in cp, (valueOf i cp), in the original cp wrt seen.
1041
(defthm acyclicp1-replaceValue-i-i-x
1042
(implies (and (acyclicp1 i cp seen)
1045
(acyclicp1 i (replaceValue i (valueOf i cp) cp) seen)))
1048
;; Lemma not-matchValueRulep-applySubstitution-does-not-chaged
1049
;; states that if there is no match between an object
1050
;; x and a rule, then the result of replacing every
1051
;; ocuurence of the lhs of rule in x with rhs of rule
1052
;; will be equal to the original x.
1053
(defthm not-matchValueRulep-applySubstitution-does-not-chaged
1054
(implies (not (matchValueRulep x rule))
1055
(equal (applySubstitution x rule)
1060
;;---------------------------------------------------------------------------
1061
;; Begin: acyclicp1-p-replaceValue-i-applySubstitution
1062
;; this part is an attempt to proof (acyclicp1 p (replaceValue i (applySubstitution (valueOf i
1063
;; cp) cp seen). I had first to split the main goal into two cases:
1064
;; (1) (equal p i) and (2) (not (equal p i)).
1065
;; The first part seems to be straightforward; however, for the second
1066
;; part I had to split it into two cases:
1067
;; (2.1) (matchValueRulep (valueOf i cp) cp) (2.2) (not (matchValueRulep (valueOf i cp) cp))
1068
;;---------------------------------------------------------------------------
1070
;;---------------------------------------------------------------------------
1072
(local (in-theory (disable
1073
intersectp-equal-not-acyclicp1
1075
intersectp-equal-indexes-acyclicp1
1081
(defthm not-member-ifo-applySubstitution
1082
(implies (and (consp rule)
1084
(assoc (car rule) cp)
1085
(subsetp (indexes-from-obj (cdr rule) cp)
1086
(indexes-from-obj (car rule) cp))
1087
(acyclicp1 (cdr rule) cp seen)
1088
(acyclicp1 i cp seen)
1090
(not (member-equal i
1092
(applySubstitution (valueOf i cp) rule) cp))))
1093
:hints (("Goal" :cases ((matchValueRulep (valueOf i cp) rule))))
1094
:rule-classes :forward-chaining)
1098
(defthm not-member-ifo-applySubstitution-1
1099
(implies (and (consp rule)
1101
(assoc (car rule) cp)
1102
(subsetp (indexes-from-obj (cdr rule) cp)
1103
(indexes-from-obj (car rule) cp))
1104
(acyclicp (cdr rule) cp)
1107
(not (member-equal i
1109
(applySubstitution (valueOf i cp) rule) cp))))
1110
:hints (("Goal" :in-theory (enable acyclicp)))
1111
:rule-classes :forward-chaining)
1114
(defthm acyclicp1-obj-member-equal-1
1115
(implies (and (uniqueNodeIDp cp)
1117
(acyclicp1 i cp seen)
1118
(acyclicp1 obj cp seen)
1119
(not (member-equal i (all-indexes-in-obj obj)))
1120
(not (member-equal i (indexes-from-obj obj cp))))
1121
(acyclicp1 i (replaceValue i obj cp) seen))
1122
:hints (("Goal" :expand (acyclicp1 i (replaceValue i obj cp) seen))))
1125
(defthm acyclicp1-obj-member-equal-2
1126
(implies (and (uniqueNodeIDp cp)
1128
(acyclicp1 i cp seen)
1129
(acyclicp1 obj cp seen)
1130
(not (member-equal i (all-indexes-in-obj obj)))
1131
(not (member-equal i (indexes-from-obj obj cp))))
1132
(acyclicp1 i (replaceValue i obj cp) seen)))
1136
(defthm acyclicp1-obj-member-equal
1137
(implies (and (uniqueNodeIDp cp)
1138
(acyclicp1 i cp seen)
1139
(acyclicp1 obj cp seen)
1140
(not (member-equal i (all-indexes-in-obj obj)))
1141
(not (member-equal i (indexes-from-obj obj cp))))
1142
(acyclicp1 i (replaceValue i obj cp) seen))
1143
:hints (("Goal" :cases ((assoc i cp)))))
1144
; :rule-classes :forward-chaining)
1147
(defthm acyclicp1-i-seen-acyclicp1-valueOf
1148
(implies (and (uniqueNodeIDp cp)
1149
(acyclicp1 i cp seen))
1150
(acyclicp1 (valueOf i cp) cp seen))
1151
:hints (("Goal" :cases ((assoc i cp)))
1152
("Subgoal 2'" :in-theory (enable valueOf)))
1153
:rule-classes :forward-chaining)
1156
(defthm matchValueRulep-obj-cons-r1-r2
1157
(implies (and (assoc r1 cp)
1159
(matchValueRulep obj (cons r1 r2))
1162
:rule-classes :forward-chaining)
1165
(defthm matchValueRulep-obj-member-equal
1166
(implies (and (matchValueRulep obj (cons r1 r2))
1169
(member-equal r1 (all-indexes-in-obj obj))))
1173
(local (in-theory (disable
1175
not-subsetp-not-member-equal-1
1177
acyclicp-member-equal-all-indexes
1180
not-acyclicp-cons-any)))
1183
(defthm acyclicp1-obj-member-equal-all
1184
(implies (and (acyclicp1 obj cp seen)
1185
(member-equal i (all-indexes-in-obj obj)))
1186
(acyclicp1 i cp seen)))
1190
(defthm acyclicp-obj-member-equal
1191
(implies (and (acyclicp obj cp)
1192
(member-equal i (all-indexes-in-obj obj)))
1194
:hints (("Goal" :in-theory (enable acyclicp))))
1199
(defthm matchValueRulep-acyclicp1-indexes-from-obj
1200
(implies (and (matchValueRulep obj rule)
1201
(acyclicp1 obj cp seen))
1202
(subsetp (indexes-from-obj (car rule) cp)
1203
(indexes-from-obj obj cp))))
1206
(defthm matchValueRulep-acyclicp-indexes-from-obj
1207
(implies (and (matchValueRulep obj rule)
1209
(subsetp (indexes-from-obj (car rule) cp)
1210
(indexes-from-obj obj cp)))
1211
:hints (("Goal" :in-theory (enable acyclicp))))
1214
(defthm not-member-equal-acyclicp1-all-indexes-from-obj-matchValueRulep
1215
(implies (and (not (member-equal i (all-indexes-in-obj obj)))
1216
(matchValueRulep obj rule)
1217
(acyclicp1 obj cp seen))
1218
(not (member-equal i (all-indexes-in-obj (car rule))))))
1221
(defthm not-member-equal-acyclicp-all-indexes-from-obj-matchValueRulep
1222
(implies (and (not (member-equal i (all-indexes-in-obj obj)))
1223
(matchValueRulep obj rule)
1225
(not (member-equal i (all-indexes-in-obj (car rule)))))
1226
:hints (("Goal" :in-theory (enable acyclicp)))))
1228
;;----------------------------------------------------
1229
(defthm member-equal-matchValueRulep-acyclicp1-member-equal
1230
(implies (and (uniqueNodeIDp cp)
1233
(member-equal i (all-indexes-in-obj r2))
1234
(matchValueRulep (valueOf i cp) (cons r1 r2))
1235
(acyclicp1 r2 cp seen))
1236
(member-equal r1 (indexes-from-obj r2 cp)))
1237
:rule-classes :forward-chaining)
1239
(defthm member-equal-acyclicp1-assoc-r1
1240
(implies (and (uniqueNodeIDp cp)
1242
(acyclicp1 r1 cp seen))
1243
(not (member-equal r1 (indexes-from-obj r1 cp))))
1244
:rule-classes :forward-chaining)
1247
(defthm not-member-equal-i-all-indexes-in-ob
1248
(implies (and (uniqueNodeIDp cp)
1251
(matchValueRulep (valueOf i cp) (cons r1 r2))
1252
(acyclicp1 r1 cp seen)
1253
(acyclicp1 r2 cp seen)
1254
(not (member-equal r1
1255
(all-indexes-in-obj r2)))
1256
(subsetp (indexes-from-obj r2 cp)
1257
(indexes-from-obj r1 cp)))
1258
(not (member-equal i (all-indexes-in-obj r2))))
1259
:rule-classes :forward-chaining
1260
:hints (("Goal" :use ((:instance member-equal-matchValueRulep-acyclicp1-member-equal)
1261
(:instance member-equal-acyclicp1-assoc-r1))
1262
:in-theory (disable member-equal-matchValueRulep-acyclicp1-member-equal
1263
member-equal-acyclicp1-assoc-r1))))
1267
(defthm not-member-all-indexes-in-obj-replaced
1268
(implies (and (not (member-equal i (all-indexes-in-obj (valueOf i cp))))
1269
(not (member-equal i (all-indexes-in-obj r2))))
1270
(not (member-equal i
1272
(applySubstitution (valueOf i cp)
1275
(defthm not-member-all-indexes-in-obj-replaced-1
1276
(implies (and (uniqueNodeIDp cp)
1279
(matchValueRulep (valueOf i cp) (cons r1 r2))
1280
(acyclicp1 r1 cp seen)
1281
(acyclicp1 r2 cp seen)
1282
(not (member-equal r1
1283
(all-indexes-in-obj r2)))
1284
(subsetp (indexes-from-obj r2 cp)
1285
(indexes-from-obj r1 cp))
1286
(acyclicp1 i cp seen))
1287
(not (member-equal i
1289
(applySubstitution (valueOf i cp)
1291
:hints (("Goal" :use ((:instance not-member-equal-i-all-indexes-in-ob)
1292
(:instance not-member-all-indexes-in-obj-replaced))
1293
:in-theory (disable not-member-equal-i-all-indexes-in-ob
1294
not-member-all-indexes-in-obj-replaced))))
1297
(defthm not-member-all-indexes-in-obj-replace
1298
(implies (and (uniqueNodeIDp cp)
1300
(assoc (car rule) cp)
1301
(matchValueRulep (valueOf i cp) rule)
1302
(acyclicp1 (car rule) cp seen)
1303
(acyclicp1 (cdr rule) cp seen)
1304
(not (member-equal (car rule)
1305
(all-indexes-in-obj (cdr rule))))
1306
(subsetp (indexes-from-obj (cdr rule) cp)
1307
(indexes-from-obj (car rule) cp))
1308
(acyclicp1 i cp seen))
1309
(not (member-equal i
1310
(all-indexes-in-obj (applySubstitution (valueOf i cp)
1312
:hints (("Goal" :do-not-induct t
1313
:do-not '(generalize fertilize )
1314
:use ((:instance not-member-all-indexes-in-obj-replaced-1
1319
not-member-all-indexes-in-obj-replaced-1
1320
not-member-equal-i-all-indexes-in-ob))))
1323
;;------------------------------------------
1324
;; Main Theorem (Equal Part)
1325
;;------------------------------------------
1326
(defthm acyclicp1-i-replaceValue-i-applySubstitution-1
1327
(implies (and (consp rule)
1328
(matchValueRulep (valueOf i cp) rule)
1330
(assoc (car rule) cp)
1331
(not (member-equal (car rule)
1332
(all-indexes-in-obj (cdr
1334
(subsetp (indexes-from-obj (cdr rule) cp)
1335
(indexes-from-obj (car rule) cp))
1336
(acyclicp1 (cdr rule) cp seen)
1337
(acyclicp1 i cp seen))
1338
(acyclicp1 i (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1339
:hints (("Goal" :do-not-induct t
1340
:do-not '(generalize fertilize eliminate-destructors)
1341
:use ((:instance not-member-ifo-applySubstitution
1343
(:instance not-member-all-indexes-in-obj-replace)
1344
(:instance acyclicp1-obj-member-equal-all
1345
(obj (applySubstitution (valueOf i cp) rule)))
1346
(:instance acyclicp1-applySubstitution
1347
(p (valueOf i cp))))
1349
:in-theory (disable acyclicp1-obj-member-equal-all
1350
not-member-ifo-applySubstitution
1351
not-member-all-indexes-in-obj-replace
1352
not-member-equal-i-all-indexes-in-ob
1353
acyclicp1-applySubstitution
1357
intersectp-equal-indexes-acyclicp1
1359
not-subsetp-not-member-equal-1
1360
acyclicp-member-equal-all-indexes
1363
(defthm acyclicp1-i-replaceValue-i-applySubstitution-2
1364
(implies (and (consp rule)
1366
(assoc (car rule) cp)
1367
(not (member-equal (car rule)
1368
(all-indexes-in-obj (cdr
1370
(subsetp (indexes-from-obj (cdr rule) cp)
1371
(indexes-from-obj (car rule) cp))
1372
(acyclicp1 (cdr rule) cp seen)
1373
(acyclicp1 i cp seen))
1374
(acyclicp1 i (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1375
:hints (("Goal" :cases ((matchValueRulep (valueOf i cp) rule))
1376
:in-theory (disable acyclicp1
1379
intersectp-equal-indexes-acyclicp1
1381
not-subsetp-not-member-equal-1
1382
acyclicp-member-equal-all-indexes
1385
;;------------------------------------------
1386
;; Main Theorem (i is equal p)
1387
;;------------------------------------------
1388
(defthm acyclicp1-i-replaceValue-i-applySubstitution-3
1389
(implies (and (consp rule)
1391
(assoc (car rule) cp)
1392
(not (member-equal (car rule)
1393
(all-indexes-in-obj (cdr
1395
(subsetp (indexes-from-obj (cdr rule) cp)
1396
(indexes-from-obj (car rule) cp))
1397
(acyclicp (cdr rule) cp)
1399
(acyclicp i (replaceValue i (applySubstitution (valueOf i cp) rule) cp)))
1400
:hints (("Goal" :in-theory (e/d (acyclicp)
1404
intersectp-equal-indexes-acyclicp1
1406
not-subsetp-not-member-equal-1
1407
acyclicp-member-equal-all-indexes
1411
;;------------------------------------------
1412
;; Main Theorem (i is not reachable from p)
1413
;;------------------------------------------
1414
(defthm acyclicp1-replaceValue-main-21
1415
(implies (and (uniqueNodeIDp cp)
1416
(acyclicp1 p cp seen)
1417
(not (member-equal i (all-indexes-in-obj p)))
1418
(not (member-equal i (indexes-from-obj p cp))))
1419
(acyclicp1 p (replaceValue i obj cp) seen))
1420
:hints (("Goal" :in-theory (disable
1422
intersectp-equal-indexes-acyclicp1
1423
not-subsetp-not-member-equal-1
1424
acyclicp-member-equal-all-indexes
1428
(defthm acyclicp1-i-replaceValue-i-applySubstitution-A-1
1429
(implies (and (consp rule)
1431
(assoc (car rule) cp)
1432
(not (member-equal (car rule)
1433
(all-indexes-in-obj (cdr
1435
(subsetp (indexes-from-obj (cdr rule) cp)
1436
(indexes-from-obj (car rule) cp))
1437
(member-equal i (all-indexes-in-obj p))
1438
(not (member-equal i (indexes-from-obj p cp)))
1439
(acyclicp1 (cdr rule) cp seen)
1440
(acyclicp1 p cp seen)
1441
(acyclicp1 i cp seen))
1442
(acyclicp1 p (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1443
:hints (("Goal" :in-theory (e/d (acyclicp)
1445
intersectp-equal-indexes-acyclicp1
1446
not-subsetp-not-member-equal-1
1447
acyclicp-member-equal-all-indexes
1450
intersectp-equal-indexes-acyclicp1
1452
not-subsetp-not-member-equal-1
1454
acyclicp-member-equal-all-indexes
1459
(defthm acyclicp1-i-replaceValue-i-applySubstitution-A-2
1460
(implies (and (consp rule)
1462
(assoc (car rule) cp)
1463
(not (member-equal (car rule)
1464
(all-indexes-in-obj (cdr
1466
(subsetp (indexes-from-obj (cdr rule) cp)
1467
(indexes-from-obj (car rule) cp))
1468
(not (member-equal i (indexes-from-obj p cp))) ;;;;;
1469
(acyclicp1 (cdr rule) cp seen)
1470
(acyclicp1 p cp seen)
1471
(acyclicp1 i cp seen))
1472
(acyclicp1 p (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1473
:hints (("Goal" :in-theory (enable acyclicp)
1474
:cases ((member-equal i (all-indexes-in-obj p))))))
1478
;;------------------------------------------
1479
;; Main Theorem (Not Equal Part)
1480
;;------------------------------------------
1482
(local (in-theory (disable union-equal
1483
intersectp-equal-indexes-acyclicp1
1484
not-subsetp-not-member-equal-1
1485
acyclicp-member-equal-all-indexes
1488
intersectp-equal-indexes-acyclicp1
1490
not-subsetp-not-member-equal-1
1492
acyclicp-member-equal-all-indexes
1495
;; Lemma acyclicp1-member-equal-pfo-not-member-equal
1496
;; states that if p is a natural number, cp is an ok
1497
;; constant pool, p is acyclic in cp wrt seen,
1498
;; and p is reachable from i, then i is NOT reachable
1500
(defthm acyclicp1-member-equal-pfo-not-member-equal
1501
(implies (and (natp p )
1503
(acyclicp1 p cp seen)
1504
(member-equal i (indexes-from-obj p cp)))
1505
(not (member-equal p (indexes-from-obj i cp))))
1506
:rule-classes :forward-chaining
1507
:hints (("Goal" :use ((:instance member-equal-acyclicp1-assoc-r1
1509
:in-theory (disable member-equal-acyclicp1-assoc-r1)))))
1512
;; Lemma not-member-equal-p-indexes-i-cp states that
1513
;; if cp is an ok constant pool, the object that is associated
1514
;; with p in cp, (valueOf p cp), is acyclic in cp wrt (cons p seen),
1515
;; and the object (valueOf p cp) is reachable from i, then i is NOT reachable
1517
(defthm not-member-equal-p-indexes-i-cp
1518
(implies (and (uniqueNodeIDp cp)
1519
(acyclicp1 (valueOf p cp) cp (cons p seen))
1520
(member-equal i (indexes-from-obj (valueOf p cp) cp)))
1521
(not (member-equal p (indexes-from-obj i cp))))
1522
:rule-classes :forward-chaining)
1524
;; Lemma acyclicp1-i-cp-cons-p-seen states that
1525
;; given an an ok constant pool, cp, i is acyclic
1526
;; in cp wrt seen, i is not equal to p, i appears
1527
;; as the first component of one of the cp's entries,
1528
;; the object that is associated with p in cp,
1529
;; (valueOf p cp), is acyclic in cp wrt (cons p seen),
1530
;; and the object (valueOf p cp) is reachable from i,
1531
;; then i is also acyclic in cp wrt (cons p seen).
1533
(defthm acyclicp1-i-cp-cons-p-seen
1534
(implies (and (uniqueNodeIDp cp)
1535
(acyclicp1 i cp seen)
1538
(acyclicp1 (valueOf p cp) cp (cons p seen))
1539
(member-equal i (indexes-from-obj (valueOf p cp) cp)))
1540
(acyclicp1 i cp (cons p seen)))
1541
:rule-classes :forward-chaining)
1543
;; Lemma acyclicp1-member-equal-pfo-not-member-equal-1
1544
;; states that given a natural number p, an an ok
1545
;; constant pool, cp, p is acyclic in cp wrt seen,
1546
;; i is not equal to p, and p is reachable from i,
1547
;; then i is not reachable from p.
1549
(defthm acyclicp1-member-equal-pfo-not-member-equal-1
1550
(implies (and (natp p)
1552
(acyclicp1 p cp seen)
1553
(not (member-equal i (all-indexes-in-obj p))) ;(not (equal p i))
1554
(member-equal i (indexes-from-obj p cp)))
1555
(not (member-equal p (indexes-from-obj i cp))))
1556
:rule-classes :forward-chaining)
1559
;; Lemma not-member-equal-p-indexes-cdr-rule states that
1560
;; if i is not reachable from p, there is a match between
1561
;; the object (valueOf i cp) and rule, i is acyclic in cp wrt seen,
1562
;; cp is an ok constant pool, i apprears as the first components
1563
;; in one of the cp's entries, the set of indexes collected in
1564
;; cp starting from (cdr rule) are subset of that of the (car rule),
1565
;; then (cdr rule) is not reachable from p.
1566
(defthm not-member-equal-p-indexes-cdr-rule
1567
(implies (and (not (member-equal p (indexes-from-obj i cp)))
1568
(matchValueRulep (valueOf i cp) rule)
1569
(acyclicp1 i cp seen)
1572
(subsetp (indexes-from-obj (cdr rule) cp)
1573
(indexes-from-obj (car rule) cp)))
1574
(not (member-equal p (indexes-from-obj (cdr rule) cp))))
1575
:rule-classes :forward-chaining)
1580
(defthm p-is-not-reachable-from-cdr-rule
1583
(matchValueRulep (valueOf i cp) rule)
1584
(not (member-equal i (all-indexes-in-obj p)))
1585
(member-equal i (indexes-from-obj p cp))
1586
(acyclicp1 i cp seen)
1587
(acyclicp1 p cp seen)
1590
(subsetp (indexes-from-obj (cdr rule) cp)
1591
(indexes-from-obj (car rule) cp)))
1592
(not (member-equal p (indexes-from-obj (cdr rule) cp))))
1593
:rule-classes :forward-chaining)
1596
(defthm p-is-not-reachable-from-cdr-rule-1
1599
(matchValueRulep (valueOf i cp) rule)
1601
(member-equal i (indexes-from-obj p cp))
1602
(acyclicp1 i cp seen)
1603
(acyclicp1 p cp seen)
1606
(subsetp (indexes-from-obj (cdr rule) cp)
1607
(indexes-from-obj (car rule) cp)))
1608
(not (member-equal p (indexes-from-obj (cdr rule) cp))))
1609
:rule-classes :forward-chaining)
1612
(defthm p-is-not-reachable-from-p
1613
(implies (and (acyclicp1 p cp seen)
1615
(not (member-equal p (indexes-from-obj p cp))))
1616
:rule-classes :forward-chaining)
1620
(defthm p-is-not-reachable-from-i
1621
(implies (and (assoc i cp)
1624
(acyclicp1 p cp seen)
1625
(member-equal i (indexes-from-obj p cp)))
1626
(not (member-equal p (indexes-from-obj i cp)))))
1629
(defthm indexes-car-rule-subset-i
1630
(implies (and (assoc i cp)
1632
(acyclicp1 i cp seen)
1633
(matchValueRulep (valueOf i cp) rule)
1634
(member-equal i (indexes-from-obj p cp))
1635
(subsetp (indexes-from-obj (cdr rule) cp)
1636
(indexes-from-obj (car rule) cp)))
1637
(subsetp (indexes-from-obj (car rule) cp)
1638
(indexes-from-obj i cp)))
1639
:hints (("Goal" :in-theory (enable acyclicp))))
1642
(defthm car-rule-is-reachable-from-p
1643
(implies (and (natp p)
1646
(acyclicp1 i cp seen)
1647
(acyclicp1 p cp seen)
1648
(matchValueRulep (valueOf i cp) rule)
1649
(member-equal i (indexes-from-obj p cp))
1650
(subsetp (indexes-from-obj (cdr rule) cp)
1651
(indexes-from-obj (car rule) cp)))
1652
(not (member-equal p (indexes-from-obj (car rule) cp)))))
1657
acyclicp-member-equal-all-indexes
1659
member-equal-subsetp-member-equal
1661
not-subsetp-not-member-equal-1
1663
member-equal-subset-index-from-obj))
1666
(defthm cdr-rule-is-reachable-from-i
1667
(implies (and (acyclicp1 cdr-rule cp seen)
1668
(member-equal p (all-indexes-in-obj cdr-rule))
1669
(member-equal i (indexes-from-obj p cp)))
1670
(member-equal i (indexes-from-obj cdr-rule cp))))
1672
(defthm not-acyclicp1-i-cp-seen
1673
(implies (and (member-equal i (indexes-from-obj i cp))
1675
(equal (acyclicp1 i cp seen)
1678
(defthm not-member-p-in-object-cdr-rule
1679
(implies (and (acyclicp1 (cdr rule) cp seen)
1681
(member-equal i (indexes-from-obj p cp))
1683
(acyclicp1 i cp seen)
1684
(subsetp (indexes-from-obj (cdr rule) cp)
1685
(indexes-from-obj (car rule) cp))
1686
(matchValueRulep (valueOf i cp) rule))
1687
(not (member-equal p (all-indexes-in-obj (cdr rule)))))
1688
:hints (("Goal" :use ((:instance cdr-rule-is-reachable-from-i
1689
(cdr-rule (cdr rule)))
1690
(:instance not-acyclicp1-i-cp-seen))
1691
:in-theory (disable cdr-rule-is-reachable-from-i
1692
not-acyclicp1-i-cp-seen)
1697
(defthm |lemma 1-Subgoal*1/3|
1700
(member-equal i (indexes-from-obj p cp))
1703
(assoc (car rule) cp)
1704
(matchValueRulep (valueOf i cp) rule)
1705
(acyclicp1 i cp seen)
1706
(acyclicp1 p cp seen)
1707
(not (member-equal (car rule)
1708
(all-indexes-in-obj (cdr rule))))
1709
(subsetp (indexes-from-obj (cdr rule) cp)
1710
(indexes-from-obj (car rule) cp))
1711
(acyclicp1 (cdr rule) cp seen))
1712
(acyclicp1 i cp (cons p seen)))
1713
:hints (("Goal" :do-not-induct t
1714
:use ((:instance acyclicp1-i-cp-cons-p-seen))
1715
:in-theory (disable acyclicp1-i-cp-cons-p-seen))))
1717
(in-theory (disable acyclicp1))
1718
(in-theory (disable matchValueRulep all-indexes-in-obj indexes-from-obj))
1720
(defthm |Subgoal *1/3- p is not reachable from i|
1722
(and (not (consp p))
1725
(member-equal i (indexes-from-obj p cp))
1726
(not (member-equal p seen))
1727
(implies (and (consp rule)
1730
(assoc (car rule) cp)
1731
(matchValueRulep (valueOf i cp) rule)
1732
(acyclicp1 i cp (cons p seen))
1733
(acyclicp1 (valueOf p cp) cp (cons p seen))
1734
(not (member-equal (car rule)
1735
(all-indexes-in-obj (cdr rule))))
1736
(subsetp (indexes-from-obj (cdr rule) cp)
1737
(indexes-from-obj (car rule) cp))
1738
(acyclicp1 (cdr rule) cp (cons p seen)))
1739
(acyclicp1 (valueOf p cp)
1740
(replaceValue i (applySubstitution (valueOf i cp) rule)
1746
(assoc (car rule) cp)
1747
(matchValueRulep (valueOf i cp) rule)
1748
(acyclicp1 i cp seen)
1749
(acyclicp1 p cp seen)
1750
(not (member-equal (car rule)
1751
(all-indexes-in-obj (cdr rule))))
1752
(subsetp (indexes-from-obj (cdr rule) cp)
1753
(indexes-from-obj (car rule) cp))
1754
(acyclicp1 (cdr rule) cp seen))
1756
(replaceValue i (applySubstitution (valueOf i cp) rule)
1759
:hints (("Subgoal 2" :in-theory (enable acyclicp1))
1760
("Subgoal 1" :expand
1763
(applySubstitution (valueOf i cp) rule)
1768
(in-theory (enable acyclicp1))
1769
(in-theory (enable matchValueRulep all-indexes-in-obj indexes-from-obj))
1771
(defthm acyclicp1-p-replaceValue-replace
1772
(implies (and (uniqueNodeIDp cp)
1773
(not (member-equal i (indexes-from-obj p cp)))
1774
(assoc (car rule) cp)
1775
(acyclicp1 i cp seen)
1776
(acyclicp1 p cp seen)
1779
(all-indexes-in-obj (cdr
1781
(subsetp (indexes-from-obj (cdr rule) cp)
1782
(indexes-from-obj (car rule) cp))
1783
(acyclicp1 (cdr rule) cp seen))
1784
(acyclicp1 p (replaceValue i
1785
(applySubstitution (valueOf i cp) rule)
1788
(defthm acyclicp1-p-replaceValue-i-applySubstitution
1789
(implies (and (consp rule)
1792
(assoc (car rule) cp)
1793
(matchValueRulep (valueOf i cp) rule)
1794
(acyclicp1 i cp seen)
1795
(acyclicp1 p cp seen)
1796
(not (member-equal (car rule)
1797
(all-indexes-in-obj (cdr
1799
(subsetp (indexes-from-obj (cdr rule) cp)
1800
(indexes-from-obj (car rule) cp))
1801
(acyclicp1 (cdr rule) cp seen))
1802
(acyclicp1 p (replaceValue i
1803
(applySubstitution (valueOf i cp) rule)
1805
:hints (("Subgoal *1/3" :cases
1806
((not (member-equal i (indexes-from-obj p cp)))))
1807
("Subgoal *1/3.2" :use
1808
((:instance |Subgoal *1/3- p is not reachable from i|))
1809
:in-theory (disable |Subgoal *1/3- p is not reachable from i|))
1810
("Subgoal *1/3.1" :use ((:instance
1811
acyclicp1-p-replaceValue-replace))
1812
:in-theory (disable acyclicp1-p-replaceValue-replace)))))
1815
(defthm acyclicp1-i-replaceValue-i-applySubstitution-general
1816
(implies (and (consp rule)
1819
(assoc (car rule) cp)
1820
(acyclicp1 i cp seen)
1821
(acyclicp1 p cp seen)
1822
(not (member-equal (car rule)
1823
(all-indexes-in-obj (cdr
1825
(subsetp (indexes-from-obj (cdr rule) cp)
1826
(indexes-from-obj (car rule) cp))
1827
(acyclicp1 (cdr rule) cp seen))
1828
(acyclicp1 p (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1829
:hints (("Goal" :cases ((matchValueRulep (valueOf i cp) rule)))))
1832
(defthm acyclicp1-p-replaceValue-i-obj-cp
1833
(implies (and (acyclicp1 p cp seen)
1836
(acyclicp1 p (replaceValue i obj cp) seen)))
1838
(defthm acyclicp1-i-replaceValue-i-applySubstitution-general-*1
1839
(implies (and (uniqueNodeIDp cp)
1840
(assoc (car rule) cp)
1841
(acyclicp1 i cp seen)
1842
(acyclicp1 p cp seen)
1843
(not (member-equal (car rule)
1844
(all-indexes-in-obj (cdr
1846
(subsetp (indexes-from-obj (cdr rule) cp)
1847
(indexes-from-obj (car rule) cp))
1848
(acyclicp1 (cdr rule) cp seen))
1849
(acyclicp1 p (replaceValue i (applySubstitution (valueOf i cp) rule) cp) seen))
1850
:hints (("Goal" :cases ((assoc i cp)))))
1852
(defthm acyclicp-i-replaceValue-i-applySubstitution-general
1853
(implies (and (consp rule)
1855
(assoc (car rule) cp) ;;
1858
(not (member-equal (car rule)
1859
(all-indexes-in-obj (cdr
1861
(subsetp (indexes-from-obj (cdr rule) cp)
1862
(indexes-from-obj (car rule) cp))
1863
(acyclicp (cdr rule) cp))
1864
(acyclicp p (replaceValue i (applySubstitution (valueOf i cp) rule) cp)))
1865
:hints (("Goal" :in-theory (enable acyclicp))))
1869
(defthm acyclicp-i-replaceValue-i-applySubstitution-general-1
1870
(implies (and (ok-rulep rule cp)
1874
(acyclicp p (replaceValue i (applySubstitution (valueOf i cp) rule) cp))))
1876
(defthm dref-replaceValue
1879
(equal (dref (car rule) cp)
1880
(dref (cdr rule) cp)) ;;
1881
(assoc (car rule) cp) ;;
1884
(acyclicp (cdr rule) cp)
1885
(not (member-equal (car rule)
1886
(all-indexes-in-obj (cdr
1888
(subsetp (indexes-from-obj (cdr rule) cp)
1889
(indexes-from-obj (car rule) cp)))
1890
(equal (dref p (replaceValue i (applySubstitution (valueOf i cp) rule) cp))
1894
(defthm dref-replaceValue-ok-rulep
1895
(implies (and (ok-rulep rule cp)
1899
(equal (dref p (replaceValue i (applySubstitution (valueOf i cp) rule) cp))
1902
(defthm acyclicp1-apply-rule-to-entry-1
1903
(implies (and (uniqueNodeIDp cp)
1904
(assoc (car rule) cp) ;;
1905
(acyclicp1 i cp seen) ;;
1906
(acyclicp1 p cp seen)
1907
(not (member-equal (car rule)
1908
(all-indexes-in-obj (cdr
1910
(subsetp (indexes-from-obj (cdr rule) cp)
1911
(indexes-from-obj (car rule) cp))
1912
(acyclicp1 (cdr rule) cp seen))
1913
(acyclicp1 p (apply-rule-to-entry-1 rule i cp) seen)))
1916
(in-theory (disable apply-rule-to-entry-1))
1918
(defthm acyclicp-apply-rule-to-entry-1
1919
(implies (and (uniqueNodeIDp cp)
1920
(assoc (car rule) cp) ;;
1923
(not (member-equal (car rule)
1924
(all-indexes-in-obj (cdr
1926
(subsetp (indexes-from-obj (cdr rule) cp)
1927
(indexes-from-obj (car rule) cp))
1928
(acyclicp (cdr rule) cp))
1929
(acyclicp p (apply-rule-to-entry-1 rule i cp)))
1930
:hints (("Goal" :in-theory (enable acyclicp))))
1933
(defthm acyclicp-apply-rule-to-entry-1-new
1934
(implies (and (ok-rulep rule cp)
1938
(acyclicp p (apply-rule-to-entry-1 rule i cp))))
1941
(defthm dref-apply-rule-to-entry-1
1944
(equal (dref (car rule) cp)
1945
(dref (cdr rule) cp)) ;;
1946
(assoc (car rule) cp) ;;
1949
(acyclicp (cdr rule) cp)
1950
(not (member-equal (car rule)
1951
(all-indexes-in-obj (cdr
1953
(subsetp (indexes-from-obj (cdr rule) cp)
1954
(indexes-from-obj (car rule) cp)))
1956
(equal (dref p (apply-rule-to-entry-1 rule i cp))
1958
:hints (("Goal" :in-theory (enable acyclicp apply-rule-to-entry-1))))
1961
(defthm dref-apply-rule-to-entry-1-new
1962
(implies (and (ok-rulep rule dag)
1966
(equal (dref p (apply-rule-to-entry-1 rule i dag))
1968
:hints (("Goal" :in-theory (enable ok-rulep))))
1971
;; Now we prove that given an all-indexes-acyclicp-cp, cp, and an acyclicp
1972
;; object p in cp, the result of dreferencing p in cp contains NO indexes.
1974
(defthm no-pointersp-dref
1975
(implies (and (acyclic-constant-poolp cp)
1977
(no-indexesp (dref p cp))))
added
removed
books/workshops/2009/fraij-roach/support/theorems.lisp
