← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/bags/meta.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/coi/bags/meta.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
 
6
31
(in-package "BAG")
7
32
 
8
33
(include-book "basic")
96
121
              (syntax-memberp x (caddr term))) ;Else, skip the cons.
97
122
          (if (and (equal (car term) 'binary-append)   ;; '(binary-append arg1 arg2)
98
123
                   (null (cdddr term)) ;consider inlining this?
99
 
                   ) 
 
124
                   )
100
125
              (or (syntax-memberp x (cadr term))
101
126
                  (syntax-memberp x (caddr term)))
102
127
;            (if (and (equal (car term) 'list::fix)   ;; '(list::fix arg1)
112
137
  )
113
138
 
114
139
;We expect TERM to be of the form (memberp x y).  If not, we do nothing.
115
 
;If so, we call syntax-memberp.  If that function returns t, that means we can show 
 
140
;If so, we call syntax-memberp.  If that function returns t, that means we can show
116
141
;syntactically that X is a memberp of Y.  If that function returns nil, we don't know whether
117
142
;X is a memberp of Y; in this case, we must return something equivalent to TERM,
118
143
;so we return TERM itself !
127
152
      term
128
153
    (if (syntax-memberp-fn nil (cadr term) (caddr term))
129
154
        ''t
130
 
      term 
 
155
      term
131
156
      )))
132
157
 
133
158
(defthm syntax-memberp-implies-memberp
188
213
          (met ((hit result) (run-remove-1 a (cdr x)))
189
214
               (mv hit (cons (car x) result))))
190
215
      (mv nil nil)))
191
 
  
 
216
 
192
217
(defthm v1-run-remove-1
193
218
  (equal (val 1 (run-remove-1 a x))
194
219
         (remove-1 a x)))
221
246
          (let ((arg1 (cadr term))
222
247
                (arg2 (caddr term)))
223
248
            (met ((hit newarg1) (syntax-remove-1 elem arg1))
224
 
                 (if hit 
 
249
                 (if hit
225
250
                     (mv t `(binary-append ,newarg1 ,arg2)) ; jcd - change
226
251
                       ; to... (binary-append ,newarg1 (list::fix ,arg2))) ??
227
252
                   (met ((hit newarg2) (syntax-remove-1 elem arg2))
228
 
                        (if hit 
 
253
                        (if hit
229
254
                            (mv t `(binary-append ,arg1 ,newarg2))
230
255
                          (mv nil term))))))
231
256
        (if (and (equal (car term) 'cons) ;; '(cons arg1 arg2)
238
263
                  ; jcd - change to ... (mv t `(list::fix ,arg2)) ?
239
264
                (met ((hit newarg2) (syntax-remove-1 elem arg2)) ;otherwise, try to remove elem from arg2
240
265
                     (if hit ;if we succeeded in removing it
241
 
                         (mv t `(cons ,arg1 ,newarg2))  ;the return the result of removing it, with arg1 tacked onto the front 
 
266
                         (mv t `(cons ,arg1 ,newarg2))  ;the return the result of removing it, with arg1 tacked onto the front
242
267
                       (mv nil term) ;otherwise, we failed to remove elem from term
243
268
                       ))))
244
269
          (if (and (equal (car term) 'quote) ;; '(quote arg1)
368
393
            (met ((hit newarg1 newterm2) (syntax-remove-bag arg1 term2))
369
394
                 (met ((hit2 newarg2 newerterm2) (syntax-remove-bag arg2 newterm2))
370
395
                      (if (or hit hit2)
371
 
                          (if (and (equal newarg2 ''nil) 
372
 
                                        ;don't bother making an append term of two nils 
 
396
                          (if (and (equal newarg2 ''nil)
 
397
                                        ;don't bother making an append term of two nils
373
398
                                        ;(bzo eventually, avoid making the append term if either arg is nil)
374
399
                                   (equal newarg1 ''nil))
375
400
                              (mv t ''nil newerterm2)
395
420
                   )
396
421
              (let ((arg1 (cadr term1)))
397
422
                (if (consp arg1)
398
 
                    (let ((arg1car `(quote ,(car arg1))) 
 
423
                    (let ((arg1car `(quote ,(car arg1)))
399
424
                          (arg1cdr `(quote ,(cdr arg1))))
400
425
                      (met ((hit newterm2) (syntax-remove-1 arg1car term2))
401
426
                           (met ((hit2 newarg1cdr newerterm2) (syntax-remove-bag arg1cdr newterm2))
420
445
;;                      (declare (ignore hit))
421
446
;;                      (mv t newarg1 newterm2)))
422
447
 
423
 
          
 
448
 
424
449
;term1 isn't a call to binary-append or cons:
425
450
            (met ((hit newterm2) (syntax-remove-bag-1 term1 term2))
426
451
                 (if hit
428
453
                   (mv nil term1 term2))))
429
454
;    )
430
455
          ))
431
 
        
 
456
 
432
457
;term1 is a non-consp:
433
458
    (met ((hit newterm2) (syntax-remove-bag-1 term1 term2))
434
459
         (if hit
435
460
             (mv t '(quote nil) newterm2)
436
461
           (mv nil term1 term2))))
437
462
  )
438
 
  
 
463
 
439
464
 
440
465
(defirrelevant syntax-remove-bag 3 a (term1 term2)
441
466
  :hints (("goal" :do-not '(generalize eliminate-destructors )
442
467
           :in-theory (e/d (SYNTAX-REMOVE-1-FN
443
468
                            syntax-remove-bag-fn
444
469
                            syntax-remove-1-irrelevant
445
 
                            syntax-remove-bag-1-irrelevant) 
 
470
                            syntax-remove-bag-1-irrelevant)
446
471
                           (SYNTAX-REMOVE-1-FN
447
472
                            SYNTAX-REMOVE-BAG-1-FN
448
473
                            RUN-REMOVE-1
529
554
;                   (not (consp (cadr term1)))
530
555
                   )
531
556
 
532
 
;bzo test (here and elsewhere) whether quoted constants are bagps?               
 
557
;bzo test (here and elsewhere) whether quoted constants are bagps?
533
558
              (let ((arg1 (cadr term1)))
534
559
                (if (consp arg1)
535
560
                    (let ((arg1car `(quote ,(car arg1)))
636
661
                                     ))))
637
662
 
638
663
 
639
 
;add guard?                     
 
664
;add guard?
640
665
(defund meta-remove-bag (x y)
641
666
  (remove-bag x y))
642
667
 
647
672
|#
648
673
 
649
674
;remove this?
650
 
;add guard?                     
651
 
(defun any-subbagp (term list) 
652
 
  (declare (type t term list)) 
653
 
  (if (consp list) 
654
 
      (or (subbagp term (car list)) 
655
 
          (any-subbagp term (cdr list))) 
 
675
;add guard?
 
676
(defun any-subbagp (term list)
 
677
  (declare (type t term list))
 
678
  (if (consp list)
 
679
      (or (subbagp term (car list))
 
680
          (any-subbagp term (cdr list)))
656
681
    nil))
657
682
 
658
683
 
659
684
 
660
685
 
661
686
 
662
 
;add guard?                     
 
687
;add guard?
663
688
(defund hide-disjoint (x y)
664
689
  (disjoint x y))
665
690
 
670
695
  :hints (("Goal" :in-theory (enable hide-disjoint))))
671
696
 
672
697
 
673
 
;add guard?                     
 
698
;add guard?
674
699
(defund hide-unique (list)
675
700
  (unique list))
676
701
 
681
706
  :hints (("Goal" :in-theory (enable hide-unique))))
682
707
 
683
708
 
684
 
;add guard?                     
 
709
;add guard?
685
710
(defund hide-subbagp (x y)
686
711
  (subbagp x y))
687
712
 
695
720
  (hide-subbagp z z)
696
721
  :hints (("Goal" :in-theory (enable hide-subbagp))))
697
722
 
698
 
;add guard?                     
 
723
;add guard?
699
724
(defund hide-memberp (x y)
700
725
  (memberp x y))
701
726
 
785
810
(set-well-founded-relation e0-ord-<)
786
811
 
787
812
(defthm v0-remove-1-subbagp
788
 
  (implies 
 
813
  (implies
789
814
   (v0 (syntax-remove-bag-1 list1 list2))
790
815
   (subbagp (syntax-ev list1 a) (syntax-ev list2 a)))
791
816
  :rule-classes (:rewrite :forward-chaining))
847
872
           (memberp elem (syntax-ev term2 a)))
848
873
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
849
874
           :in-theory (enable syntax-remove-bag-fn))))
850
 
 
 
875
 
851
876
 
852
877
 
853
878
 
875
900
    0))
876
901
 
877
902
;(include-book "arithmetic/top" :dir :system)
878
 
;(include-book "arithmetic-2/meta/top" :dir :system)
879
903
 
880
904
 
881
905
(defthm syntax-count-of-non-consp
890
914
  :rule-classes (:rewrite :linear)
891
915
  :hints (("Goal" :in-theory (enable SYNTAX-REMOVE-1-fn))))
892
916
 
893
 
;(include-book "arithmetic-2/meta/top" :dir :system)
894
917
 
895
918
(defthm count-in-SYNTAX-REMOVE-bag-1-linear
896
919
  (>= (COUNT ELEM (SYNTAX-EV (VAL 1 (SYNTAX-REMOVE-bag-1 x Y)) a))
907
930
 
908
931
(encapsulate
909
932
 ()
910
 
 
 
933
 
911
934
 (local (defthm syntax-remove-1-did-something-iff-1
912
935
          (implies (val 0 (syntax-remove-1 elem term))
913
936
                   (syntax-memberp elem term))
914
937
          :hints (("Goal" :in-theory (enable syntax-remove-1-fn)
915
 
                   :do-not '(generalize eliminate-destructors))) 
 
938
                   :do-not '(generalize eliminate-destructors)))
916
939
          ))
917
940
 
918
941
 
919
942
 (local (defthm syntax-remove-1-did-something-iff-2
920
943
          (implies (syntax-memberp elem term)
921
944
                   (val 0 (syntax-remove-1 elem term)))
922
 
          :hints (("Goal" :in-theory (enable list::memberp-when-not-memberp-of-cdr-cheap 
 
945
          :hints (("Goal" :in-theory (enable list::memberp-when-not-memberp-of-cdr-cheap
923
946
                                             syntax-remove-1-fn syntax-memberp-fn)
924
 
                   :do-not '(generalize eliminate-destructors))) 
 
947
                   :do-not '(generalize eliminate-destructors)))
925
948
          ))
926
949
 
927
950
 (defthm syntax-remove-1-did-something-iff
964
987
  :rule-classes (:rewrite :linear)
965
988
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
966
989
           :in-theory (enable syntax-remove-bag-fn))))
967
 
     
 
990
 
968
991
 
969
992
#|kill?
970
993
(thm
1019
1042
                   (if hit
1020
1043
                       (list 'cons arg1 (syntax-intersection arg2 newterm2))
1021
1044
                     (syntax-intersection arg2 term2))))
1022
 
          
 
1045
 
1023
1046
;;           (if (and (equal (car term1) 'list::fix) ;; '(list::fix arg1)
1024
1047
;;                    (null (cddr term1))
1025
1048
;;                    )
1036
1059
                         (if hit
1037
1060
                             `(cons ,arg1car ,(syntax-intersection arg1cdr newterm2))
1038
1061
                           (syntax-intersection arg1cdr term2))))
1039
 
                  ''nil 
 
1062
                  ''nil
1040
1063
                  ))
1041
 
            
 
1064
 
1042
1065
;term1 isn't a call to binary-append or cons or list::fix:
1043
1066
            (met ((hit newterm2) (syntax-remove-bag-1 term1 term2))
1044
1067
                 (declare (ignore newterm2))
1093
1116
                                  (SYNTAX-REMOVE-1 OTHER-TERM TERM)))))
1094
1117
  :hints (("Goal" :in-theory (enable SYNTAX-REMOVE-1-fn
1095
1118
                                     SYNTAX-REMOVE-BAG-1-FN SYNTAX-MEMBERP-FN))))
1096
 
  
 
1119
 
1097
1120
(defthm smith-blah
1098
1121
  (IMPLIES (NOT (SYNTAX-MEMBERP elem term))
1099
1122
           (NOT (SYNTAX-MEMBERP elem (VAL 2 (SYNTAX-REMOVE-BAG other-term term)))))
1114
1137
 
1115
1138
 
1116
1139
(in-theory (disable SYNTAX-MEMBERP-FN))
1117
 
 
 
1140
 
1118
1141
(defthm hack-eric
1119
1142
  (implies (and (val 0 (syntax-remove-bag-1 other-term y))
1120
1143
                (not (syntax-memberp x y))
1137
1160
           (not (syntax-memberp x (syntax-intersection other-term y))))
1138
1161
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
1139
1162
           :in-theory (e/d (syntax-intersection syntax-memberp
1140
 
                              ) 
 
1163
                              )
1141
1164
                           (poopsmith
1142
1165
                            (:induction  syntax-memberp))))))
1143
1166
 
1171
1194
  :hints (("Goal" :in-theory (disable syntax-remove-bag-cannot-increase-count-two)
1172
1195
           :use (:instance syntax-remove-bag-cannot-increase-count-two (term1 (val 1 (syntax-remove-bag term1 term2))) (term2 term3)))))
1173
1196
 
1174
 
(defthm checkinemail    
 
1197
(defthm checkinemail
1175
1198
  (<= (count (syntax-ev elem a)
1176
1199
             (syntax-ev (syntax-intersection term1 term2) a))
1177
1200
      (count (syntax-ev elem a)
1180
1203
           :in-theory (enable syntax-intersection-fn))))
1181
1204
 
1182
1205
(defthm syntax-remove-bag-does-the-right-thing-helper
1183
 
  (equal (- (count elem (syntax-ev term1 a)) 
 
1206
  (equal (- (count elem (syntax-ev term1 a))
1184
1207
            (count elem (syntax-ev term2 a)))
1185
1208
         (- (count elem (syntax-ev (v1 (syntax-remove-bag term1 term2)) a))
1186
1209
            (count elem (syntax-ev (v2 (syntax-remove-bag term1 term2)) a))))
1187
1210
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
1188
1211
           :in-theory (e/d (syntax-remove-bag-fn)
1189
 
                           (v1-syntax-remove-1-perm-remove-1 
 
1212
                           (v1-syntax-remove-1-perm-remove-1
1190
1213
                            ;for efficiency:
1191
1214
                            SYNTAX-REMOVE-BAG-1-FN
1192
1215
                            MEMBERP-OF-SYNTAX-REMOVE-BAG-ONE
1198
1221
  (implies (not (syntax-memberp elem term))
1199
1222
           (equal (val 1 (syntax-remove-1 elem term))
1200
1223
                  term)))
1201
 
                              
1202
 
 
1203
 
(in-theory (disable SYNTAX-REMOVE-BAG-1-fn SYNTAX-MEMBERP-fn))                   
 
1224
 
 
1225
 
 
1226
(in-theory (disable SYNTAX-REMOVE-BAG-1-fn SYNTAX-MEMBERP-fn))
1204
1227
 
1205
1228
(in-theory (disable SUBBAGP-OF-REMOVE-1-FROM-SUBBAGP)) ;why needed?
1206
1229
 
1224
1247
                            (syntax-ev (val 2 (syntax-remove-bag other-term term)) alist))))
1225
1248
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
1226
1249
          :in-theory (enable syntax-remove-bag SYNTAX-REMOVE-BAG-1))))
1227
 
                 
 
1250
 
1228
1251
;bzo make equal
1229
1252
(defthm syntax-remove-bag-does-the-right-thing
1230
1253
  (implies (subbagp (syntax-ev term1 alist) (syntax-ev term2 alist))
1272
1295
 (implies (not (syntax-ev (val 2 (syntax-remove-bag x y)) alist))
1273
1296
          (subbagp (syntax-ev y alist) (syntax-ev x alist)))
1274
1297
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
1275
 
          :in-theory (enable syntax-remove-bag 
 
1298
          :in-theory (enable syntax-remove-bag
1276
1299
                             subbagp
1277
1300
                             ))))
1278
1301
 
1480
1503
            (list (caddr term)))
1481
1504
        (let ((hit (syntax-memberp x list)))
1482
1505
          (if hit
1483
 
              '(quote t) 
 
1506
              '(quote t)
1484
1507
            term)))
1485
1508
    term))
1486
1509
 
1504
1527
 
1505
1528
#|
1506
1529
(thm
1507
 
 (implies (and (true-listp x) 
 
1530
 (implies (and (true-listp x)
1508
1531
               (true-listp y))
1509
1532
          (equal (ACL2-COUNT (BINARY-APPEND Y X))
1510
1533
                 (+ (acl2-count x) (acl2-count y))))
1523
1546
                 (remove-bag (syntax-ev x alist)
1524
1547
                             (syntax-ev y alist))))
1525
1548
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
1526
 
          :in-theory (enable syntax-remove-bag-1 
 
1549
          :in-theory (enable syntax-remove-bag-1
1527
1550
                             ;unique
1528
1551
                             ))))
1529
1552
 
1535
1558
            (equal (syntax-ev (v1 (syntax-remove-bag-1 x list)) alist)
1536
1559
                   (remove-bag (syntax-ev x alist) (syntax-ev list alist))))
1537
1560
   :hints (("goal" :do-not '(generalize eliminate-destructors)
1538
 
            :in-theory (e/d (remove-bag-append-disjoint 
 
1561
            :in-theory (e/d (remove-bag-append-disjoint
1539
1562
                             syntax-remove-bag-1
1540
1563
;remove-bag
1541
1564
                             )
1542
 
                            (remove-bag-append))))) 
 
1565
                            (remove-bag-append)))))
1543
1566
|#
1544
1567
 
1545
1568
;when do we use these?
1549
1572
                 (v0 (syntax-remove-1 elem term)))
1550
1573
            (list::equiv (syntax-ev (v1 (syntax-remove-1 elem term)) a)
1551
1574
                         (remove-1 (syntax-ev elem a) (syntax-ev term a))))
1552
 
   :hints (("Goal" :in-theory (e/d ( ;remove-1 
 
1575
   :hints (("Goal" :in-theory (e/d ( ;remove-1
1553
1576
                                    syntax-remove-1-fn
1554
 
                                    REMOVE-1-APPEND 
 
1577
                                    REMOVE-1-APPEND
1555
1578
                                    remove-bag-append-disjoint
1556
1579
                                    disjoint-memberp-implies-non-membership
1557
1580
                                    SYNTAX-MEMBERP-fn
1575
1598
   :hints (("Goal" :in-theory (enable syntax-remove-bag))))
1576
1599
|#
1577
1600
 
1578
 
;bzo it would be nice if this returned a simplified term even if the first arg didn't simplify to nil.  
 
1601
;bzo it would be nice if this returned a simplified term even if the first arg didn't simplify to nil.
1579
1602
(defun syntax-meta-remove-bag-wrapper (term)
1580
1603
   (declare (type t term)
1581
1604
            (xargs :guard (pseudo-termp term)))
1585
1608
 ;           (consp (cddr term))
1586
1609
            (null  (cdddr term)))
1587
1610
       (met ((hit v1 v2) (syntax-remove-bag-fn nil (cadr term) (caddr term)))
1588
 
            
 
1611
 
1589
1612
            (if (and hit
1590
1613
 
1591
 
                     (equal v1 '(quote nil))  
 
1614
                     (equal v1 '(quote nil))
1592
1615
                     )
1593
1616
                ;bzo consider remove-bag here?
1594
1617
                ;`(meta-remove-bag ,v1 ,v2)
1595
1618
                v2
1596
 
              
 
1619
 
1597
1620
              term))
1598
1621
     term))
1599
1622
 
1688
1711
                (equal in2 (not in1))
1689
1712
                )
1690
1713
           (equal (perm list1 list2)
1691
 
                  (perm (replace-perm in1 x y list1) 
 
1714
                  (perm (replace-perm in1 x y list1)
1692
1715
                        (replace-perm in2 x y list2))))
1693
1716
  :hints (("Goal" :in-theory (enable meta-subbagp meta-remove-bag))))
1694
1717
 
1699
1722
  (declare (type t term1 term2))
1700
1723
  (met ((hit xterm1 xterm2) (syntax-remove-bag term1 term2))
1701
1724
       (declare (ignore xterm2))
1702
 
       (if (not hit) 
 
1725
       (if (not hit)
1703
1726
           (mv nil nil)
1704
1727
         (met ((hit xterm1 sub) (syntax-remove-bag xterm1 term1))
1705
1728
              (declare (ignore xterm1))
1706
 
              (mv 
 
1729
              (mv
1707
1730
               hit ;should this be t?  what if xterm1 is nil?
1708
1731
               sub)))))
1709
 
 
 
1732
 
1710
1733
(defun bind-common-elements (term1 term2 key)
1711
1734
  (declare (type t term1 term2 key))
1712
1735
  (met ((hit common) (common-elements term1 term2))
1738
1761
;  perm-common-elimination
1739
1762
  ))
1740
1763
 
1741
 
;; Nonetheless, perm-common-elimination should be used in 
 
1764
;; Nonetheless, perm-common-elimination should be used in
1742
1765
;; place of such hack rules as these ..
1743
1766
 
1744
1767
(in-theory
1771
1794
;  perm-not-consp-nil
1772
1795
 ; perm-remove-bag-x-x
1773
1796
;  perm-append
1774
 
  perm-cons-append 
 
1797
  perm-cons-append
1775
1798
  perm-append-remove-1
1776
1799
;  perm-remove-1
1777
1800
 ; perm-remove-bag
1792
1815
(in-theory
1793
1816
 (disable
1794
1817
;  meta-remove-bag
1795
 
 ;meta-remove-1 
 
1818
 ;meta-remove-1
1796
1819
  ))
1797
1820
 
1798
1821
 
1799
1822
 
1800
1823
;;=================================================================================
1801
 
;; :meta rule to simplify (memberp x lst) when we know that X is not a member of 
 
1824
;; :meta rule to simplify (memberp x lst) when we know that X is not a member of
1802
1825
;; certain things (namely, things syntactically present in LST).
1803
1826
;==================================================================================
1804
1827
 
1827
1850
(defun get-irrel-list-from-clause (x z clause)
1828
1851
  (declare (type t x clause)
1829
1852
;           (xargs :guard (pseudo-termp term))
1830
 
           )  
 
1853
           )
1831
1854
  (if (not (consp clause))
1832
1855
      nil
1833
1856
    (let ((literal (car clause)))
1859
1882
        nest)
1860
1883
    (if (equal (car nest) 'cons)
1861
1884
        (list 'cons (cadr nest) (simplify-cons-and-append-nest-given-irrelevant-lists (caddr nest) irrel-list))
1862
 
      (if (equal (car nest) 'binary-append) 
 
1885
      (if (equal (car nest) 'binary-append)
1863
1886
       ;We don't have to recur on (cadr nest) because we know it won't be an append or a cons, because of how
1864
1887
       ;nests of those functions get normalized?
1865
1888
          (if (memberp (cadr nest) irrel-list) ;we're appending something irrelevant, so drop it
1872
1895
          nest))
1873
1896
      )
1874
1897
    ))
1875
 
       
 
1898
 
1876
1899
(set-state-ok t)
1877
1900
 
1878
1901
 
1887
1910
    (let ((irrel-list (get-irrel-list-from-clause (cadr term) (caddr term) (mfc-clause mfc))))
1888
1911
      (if (not (consp irrel-list))
1889
1912
          term
1890
 
        (list 'list::memberp 
1891
 
              (cadr term) 
 
1913
        (list 'list::memberp
 
1914
              (cadr term)
1892
1915
              (simplify-cons-and-append-nest-given-irrelevant-lists (caddr term) irrel-list))))))
1893
1916
 
1894
1917
(defun make-not-memberp-claim (x term)
1905
1928
        )
1906
1929
    (if (equal (car nest) 'cons)
1907
1930
        (hyp-fun-simplify-cons-and-append-nest-given-irrelevant-lists x (caddr nest) irrel-list)
1908
 
      (if (equal (car nest) 'binary-append) 
 
1931
      (if (equal (car nest) 'binary-append)
1909
1932
       ;We don't have to recur on (cadr nest) because we know it won't be an append or a cons, because of how
1910
1933
       ;nests of those functions get normalized?
1911
1934
          (if (memberp (cadr nest) irrel-list) ;we're appending something irrelevant, so drop it
1937
1960
 
1938
1961
(encapsulate
1939
1962
 ()
1940
 
 (local 
 
1963
 (local
1941
1964
  (defthm helper-eric
1942
1965
    (implies
1943
1966
     (ev2 (hyp-fun-simplify-cons-and-append-nest-given-irrelevant-lists x nest irrel-list)
1961
1984
          (implies (not (memberp x foo))
1962
1985
                   (equal (memberp x (append a foo))
1963
1986
                          (memberp x a)))
1964
 
          :hints (("Goal" :in-theory (disable LIST::memberp-of-cons 
 
1987
          :hints (("Goal" :in-theory (disable LIST::memberp-of-cons
1965
1988
                                              LIST::MEMBERP-of-APPEND))))))
1966
1989
 
1967
1990
 
1978
2001
            (list2 (caddr term)))
1979
2002
        (let ((hit (syntax-subbagp-fn nil list1 list2)))
1980
2003
          (if hit
1981
 
              '(quote t) 
 
2004
              '(quote t)
1982
2005
            term)))
1983
2006
    term))
1984
2007
 
2008
2031
;(my-syntax-subbagp '(cons a x) '(cons b (cons a x)))
2009
2032
;(my-syntax-subbagp '(cons a x) '(cons a x))
2010
2033
 
2011
 
#| 
 
2034
#|
2012
2035
 
2013
2036
;key lemma for *meta*-syntax-ev-syntax-subbagp
2014
2037
;bzo rename
2038
2061
           (perm (syntax-ev (val 1 (syntax-subbagp-helper term1 term2)) a)
2039
2062
                 (remove-bag (syntax-ev term1 a) (syntax-ev term2 a))))
2040
2063
  :hints (("Goal" :in-theory (enable syntax-subbagp-helper-fn))))
2041
 
 
 
2064
 
2042
2065
(defthm syntax-subbagp-helper-implements-subbagp
2043
2066
  (implies (v0 (syntax-subbagp-helper term1 term2))
2044
2067
           (subbagp (syntax-ev term1 a) (syntax-ev term2 a)))
2118
2141
               `(perm ,newarg1 ,newarg2)
2119
2142
             term))
2120
2143
    term))
2121
 
           
 
2144
 
2122
2145
 
2123
2146
(thm
2124
2147
 (IMPLIES (VAL 0 (SYNTAX-REMOVE-BAG-1 TERM1 TERM2))
2140
2163
                    (REMOVE-1 (SYNTAX-EV elem alist)
2141
2164
                              (SYNTAX-EV TERM2 alist))))
2142
2165
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
2143
 
          :in-theory (enable syntax-remove-bag 
 
2166
          :in-theory (enable syntax-remove-bag
2144
2167
                             subbagp))))
2145
2168
 
2146
2169
(thm
2149
2172
          (subbagp (syntax-ev term1 alist)
2150
2173
                   (syntax-ev term2 a)))
2151
2174
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
2152
 
          :in-theory (enable syntax-remove-bag 
 
2175
          :in-theory (enable syntax-remove-bag
2153
2176
                             subbagp))))
2154
2177
 
2155
2178
 
2188
2211
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
2189
2212
          :in-theory (enable syntax-remove-bag))))
2190
2213
 
2191
 
      
 
2214
 
2192
2215
(defthm meta-perm-cancel
2193
2216
  (equal (syntax-ev term a)
2194
2217
         (syntax-ev (perm-cancel-metafunction term) a))
2219
2242
 :hints (("Goal" :do-not '(generalize eliminate-destructors)
2220
2243
          :in-theory (enable syntax-remove-bag syntax-subbagp-helper))))
2221
2244
 
2222
 
        
 
2245
 
2223
2246
 (VAL
2224
2247
      0
2225
2248
      (SYNTAX-REMOVE-BAG-1 (CADDR TERM1)
2240
2263
                 ''NIL)
2241
2264
          (PERM (SYNTAX-EV (SYNTAX-INTERSECTION TERM1 TERM2) a)
2242
2265
                (SYNTAX-EV TERM1 a)
2243
 
               
 
2266
 
2244
2267
                )))
2245
2268
 
2246
2269
 
2289
2312
           (subbagp (syntax-ev (v1 (syntax-remove-bag term1 term2)) a)
2290
2313
                    (syntax-ev (v2 (syntax-remove-bag term1 term2)) a)))
2291
2314
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
2292
 
           :in-theory (enable syntax-remove-bag; 
 
2315
           :in-theory (enable syntax-remove-bag;
2293
2316
                              ;subbagp
2294
2317
                              ))))
2295
2318
 
2299
2322
         (subbagp (syntax-ev (v1 (syntax-remove-bag term1 term2)) a)
2300
2323
                  (syntax-ev (v2 (syntax-remove-bag term1 term2)) a)))
2301
2324
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
2302
 
           :in-theory (enable syntax-remove-bag ; 
 
2325
           :in-theory (enable syntax-remove-bag ;
2303
2326
;subbagp
2304
2327
                              ))))
2305
2328
 
2322
2345
                 (syntax-count elem term2))))
2323
2346
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
2324
2347
           :in-theory (enable syntax-remove-bag))))
2325
 
                 
2326
 
         
 
2348
 
 
2349
 
2327
2350
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
2328
2351
           :in-theory (enable syntax-remove-bag; subbagp
2329
2352
                              ))))
2382
2405
                (subbagp (syntax-ev blah a) y))
2383
2406
           (memberp (syntax-ev x a) y))
2384
2407
  :hints (("Goal" :use (:instance syntax-memberp-implements-memberp (v x) (x blah) (a a))
2385
 
           :in-theory (e/d ( non-memberp-eric) (syntax-memberp-implements-memberp)))))
 
2408
           :in-theory (e/d ( non-memberp-eric) (syntax-memberp-implements-memberp)))))
 
 
b'\\ No newline at end of file'