Filtering...

getprop

books/misc/getprop
other
(in-package "ACL2")
fast-no-duplicatesp1function
(defun fast-no-duplicatesp1
  (lst props)
  (declare (xargs :guard (and (symbol-listp lst) (plist-worldp props))))
  (cond ((endp lst) t)
    ((getprop (car lst)
       'mark
       nil
       'fast-no-duplicatesp-world
       props) nil)
    (t (fast-no-duplicatesp1 (cdr lst)
        (extend-world 'fast-no-duplicatesp-world
          (putprop (car lst) 'mark t props))))))
fast-no-duplicatespfunction
(defun fast-no-duplicatesp
  (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (let ((ans (fast-no-duplicatesp1 lst nil)))
    (prog2$ (retract-world 'fast-no-duplicatesp-world nil) ans)))
sgetprop-means-fast-no-duplicatesp1-failstheorem
(defthm sgetprop-means-fast-no-duplicatesp1-fails
  (implies (and (member e lst)
      (sgetprop e 'mark nil 'fast-no-duplicatesp-world props))
    (not (fast-no-duplicatesp1 lst props))))
all-marked-tfunction
(defun all-marked-t
  (props)
  (cond ((endp props) t)
    (t (and (eq (cadr (car props)) 'mark)
        (eq (cddr (car props)) t)
        (all-marked-t (cdr props))))))
sgetprop-means-in-strip-carstheorem
(defthm sgetprop-means-in-strip-cars
  (implies (all-marked-t props)
    (iff (sgetprop x 'mark nil name props)
      (member x (strip-cars props)))))
member-appendtheorem
(defthm member-append
  (iff (member e (append a b)) (or (member e a) (member e b))))
duplicatesp-preserved-by-appendtheorem
(defthm duplicatesp-preserved-by-append
  (implies (no-duplicatesp (append x y))
    (and (no-duplicatesp x) (no-duplicatesp y))))
no-duplicatesp-append-constheorem
(defthm no-duplicatesp-append-cons
  (equal (no-duplicatesp (append a (cons e b)))
    (and (not (member e a))
      (not (member e b))
      (no-duplicatesp (append a b)))))
fast-no-duplicatesp1-is-no-duplicatesp-appendtheorem
(defthm fast-no-duplicatesp1-is-no-duplicatesp-append
  (implies (and (no-duplicatesp (strip-cars props))
      (all-marked-t props))
    (equal (fast-no-duplicatesp1 lst props)
      (no-duplicatesp (append (strip-cars props) lst)))))
fast-no-duplicatesp-is-no-duplicatesptheorem
(defthm fast-no-duplicatesp-is-no-duplicatesp
  (equal (fast-no-duplicatesp lst) (no-duplicatesp lst)))
other
(set-state-ok t)
timed-fndfunction
(defun timed-fnd
  (lst state)
  (pprogn (set-timer 'fast-no-duplicatesp-time '(0) state)
    (let ((ans (fast-no-duplicatesp lst)))
      (pprogn (increment-timer 'fast-no-duplicatesp-time state)
        (print-timer 'fast-no-duplicatesp-time *standard-co* state)
        (princ$ " secs" *standard-co* state)
        (princ$ #\
 *standard-co* state)
        (pop-timer 'fast-no-duplicatesp-time nil state)
        (value ans)))))
timed-fnd-is-no-duplicatesptheorem
(defthm timed-fnd-is-no-duplicatesp
  (equal (mv-nth 1 (timed-fnd lst state))
    (no-duplicatesp lst))
  :hints (("Goal" :in-theory (disable print-rational-as-decimal))))
make-temp-symbolsfunction
(defun make-temp-symbols
  (n acc)
  (declare (xargs :mode :program))
  (cond ((zp n) acc)
    (t (make-temp-symbols (- n 1)
        (cons (packn (list "TEMP" n)) acc)))))
other
(comp t)
*dup-list*constant
(defconst *dup-list* (make-temp-symbols 20000 '(temp1)))
*no-dup-list*constant
(defconst *no-dup-list* (cons 'temp0 (cdr *dup-list*)))
other
(make-event (er-progn (timed-fnd *dup-list* state)
    (value '(value-triple :invisible))))
other
(make-event (er-progn (timed-fnd *no-dup-list* state)
    (value '(value-triple :invisible))))