Filtering...

map

books/std/osets/map
other
(in-package "SET")
other
(include-book "quantify")
other
(set-verify-guards-eagerness 2)
other
(local (in-theory (enable definitions expensive-rules)))
other
(encapsulate (((transform *) => *))
  (local (defun transform (x) x)))
other
(defconst *map-functions*
  '((defun map-list
     (x)
     (declare (xargs :guard (true-listp x)))
     (if (endp x)
       nil
       (cons (transform (car x))
         (map-list (cdr x))))) (defun map
      (x)
      (declare (xargs :guard (setp x)))
      (declare (xargs :verify-guards nil))
      (mbe :logic (if (emptyp x)
          nil
          (insert (transform (head x))
            (map (tail x))))
        :exec (mergesort (map-list x))))
    (defun inversep
      (a b)
      (declare (xargs :guard t))
      (equal (transform a) b))))
other
(instance *map-functions*)
other
(instance-*map-functions*)
other
(quantify-predicate (inversep a b))
other
(defconst *map-theorems*
  '((defthm map-setp (setp (map x))) (defthm map-sfix
      (equal (map (sfix x)) (map x)))
    (defthm map-in
      (equal (in a (map x))
        (not (all<not-inversep> x a))))
    (defthm map-subset
      (implies (subset x y)
        (subset (map x) (map y))))
    (defthm map-insert
      (equal (map (insert a x))
        (insert (transform a) (map x))))
    (defthm map-delete
      (subset (delete (transform a) (map x))
        (map (delete a x))))
    (defthm map-union
      (equal (map (union x y))
        (union (map x) (map y))))
    (defthm map-intersect
      (subset (map (intersect x y))
        (intersect (map x) (map y))))
    (defthm map-difference
      (subset (difference (map x) (map y))
        (map (difference x y))))
    (defthm map-cardinality
      (<= (cardinality (map x))
        (cardinality x))
      :rule-classes :linear)
    (defthm member-of-map-list
      (iff (member a (map-list x))
        (exists-list<inversep> x a)))
    (defthm map-mergesort
      (equal (map (mergesort x))
        (mergesort (map-list x))))
    (defthm map-mbe-equivalence
      (implies (setp x)
        (equal (mergesort (map-list x)) (map x))))
    (defthm map-list-cons
      (equal (map-list (cons a x))
        (cons (transform a) (map-list x))))
    (defthm map-list-append
      (equal (map-list (append x y))
        (append (map-list x) (map-list y))))
    (defthm map-list-nth
      (implies (and (integerp n)
          (<= 0 n)
          (< n (len x)))
        (equal (nth n (map-list x))
          (transform (nth n x)))))
    (defthm map-list-revappend
      (equal (map-list (revappend x acc))
        (revappend (map-list x) (map-list acc))))
    (defthm map-list-reverse
      (equal (map-list (reverse x))
        (reverse (map-list x))))))
other
(instance *map-theorems*)
other
(instance-*map-theorems*)
other
(verify-guards map)
map-function-fnfunction
(defun map-function-fn
  (function in-package
    set-guard
    list-guard
    element-guard
    arg-guard)
  (declare (xargs :mode :program))
  (let* ((name (car function)) (extra-args (cddr function))
      (wrap (app "<" (app (symbol-name name) ">")))
      (map<f> (mksym (app "map" wrap) in-package))
      (map-list<f> (mksym (app "map-list" wrap) in-package))
      (inversep (app "inversep" wrap))
      (ipw (app "<" (app inversep ">")))
      (not-ipw (app "<not-" (app inversep ">")))
      (inversep<f> (mksym inversep in-package))
      (all<inversep<f>> (mksym (app "all" ipw) in-package))
      (exists<inversep<f>> (mksym (app "exists" ipw) in-package))
      (find<inversep<f>> (mksym (app "find" ipw) in-package))
      (filter<inversep<f>> (mksym (app "filter" ipw) in-package))
      (all-list<inversep<f>> (mksym (app "all-list" ipw) in-package))
      (exists-list<inversep<f>> (mksym (app "exists-list" ipw) in-package))
      (find-list<inversep<f>> (mksym (app "find-list" ipw) in-package))
      (filter-list<inversep<f>> (mksym (app "filter-list" ipw) in-package))
      (all<not-inversep<f>> (mksym (app "all" not-ipw) in-package))
      (exists<not-inversep<f>> (mksym (app "exists" not-ipw) in-package))
      (find<not-inversep<f>> (mksym (app "find" not-ipw) in-package))
      (filter<not-inversep<f>> (mksym (app "filter" not-ipw) in-package))
      (all-list<not-inversep<f>> (mksym (app "all-list" not-ipw) in-package))
      (exists-list<not-inversep<f>> (mksym (app "exists-list" not-ipw)
          in-package))
      (find-list<not-inversep<f>> (mksym (app "find-list" not-ipw) in-package))
      (filter-list<not-inversep<f>> (mksym (app "filter-list" not-ipw)
          in-package))
      (subs `(((transform ?x) (,SET::NAME ?x ,@SET::EXTRA-ARGS)) ((map ?x) (,SET::MAP<F> ?x ,@SET::EXTRA-ARGS))
          ((map-list ?x) (,SET::MAP-LIST<F> ?x ,@SET::EXTRA-ARGS))
          ((inversep ?a ?b) (,SET::INVERSEP<F> ?a ?b ,@SET::EXTRA-ARGS))
          ((all<inversep> ?a ?b) (,SET::ALL<INVERSEP<F>> ?a ?b ,@SET::EXTRA-ARGS))
          ((exists<inversep> ?a ?b) (,SET::EXISTS<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((find<inversep> ?a ?b) (,SET::FIND<INVERSEP<F>> ?a ?b ,@SET::EXTRA-ARGS))
          ((filter<inversep> ?a ?b) (,SET::FILTER<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((all-list<inversep> ?a ?b) (,SET::ALL-LIST<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((exists-list<inversep> ?a ?b) (,SET::EXISTS-LIST<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((find-list<inversep> ?a ?b) (,SET::FIND-LIST<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((filter-list<inversep> ?a ?b) (,SET::FILTER-LIST<INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((all<not-inversep> ?a ?b) (,SET::ALL<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((exists<not-inversep> ?a ?b) (,SET::EXISTS<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((find<not-inversep> ?a ?b) (,SET::FIND<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((filter<not-inversep> ?a ?b) (,SET::FILTER<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((all-list<not-inversep> ?a ?b) (,SET::ALL-LIST<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((exists-list<not-inversep> ?a ?b) (,SET::EXISTS-LIST<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((find-list<not-inversep> ?a ?b) (,SET::FIND-LIST<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))
          ((filter-list<not-inversep> ?a ?b) (,SET::FILTER-LIST<NOT-INVERSEP<F>> ?a
              ?b
              ,@SET::EXTRA-ARGS))))
      (theory<f> (mksym (app "map-theory" wrap) in-package))
      (suffix (mksym wrap in-package))
      (thm-names (defthm-names *map-theorems*))
      (thm-name-map (create-new-names thm-names suffix))
      (theory<f>-defthms (sublis thm-name-map thm-names)))
    `(encapsulate nil
      (instance-*map-functions* :subs ,(LIST*
  `((DECLARE (SET::XARGS :GUARD (SET::SETP SET::?SET)))
    (DECLARE
     (SET::XARGS :GUARD
      (AND (SET::SETP SET::?SET) ,@SET::SET-GUARD ,@SET::ARG-GUARD))))
  `((DECLARE (SET::XARGS :GUARD (SET::TRUE-LISTP SET::?LIST)))
    (DECLARE
     (SET::XARGS :GUARD
      (AND (SET::TRUE-LISTP SET::?LIST) ,@SET::LIST-GUARD ,@SET::ARG-GUARD))))
  `((DECLARE (SET::XARGS :GUARD T))
    (DECLARE (SET::XARGS :GUARD (AND ,@SET::ELEMENT-GUARD ,@SET::ARG-GUARD))))
  SET::SUBS)
        :suffix ,SET::NAME)
      (quantify-predicate (,SET::INVERSEP<F> a b ,@SET::EXTRA-ARGS)
        :in-package-of ,IN-PACKAGE
        :set-guard ,SET::SET-GUARD
        :list-guard ,SET::LIST-GUARD
        :arg-guard ,SET::ARG-GUARD)
      (instance-*map-theorems* :subs ,SET::SUBS
        :suffix ,(SET::MKSYM SET::WRAP IN-PACKAGE))
      (verify-guards ,SET::MAP<F>)
      (deftheory ,SET::THEORY<F>
        (union-theories (theory ',(SET::MKSYM (SET::APP "theory" SET::IPW) IN-PACKAGE))
          '(,SET::MAP<F> ,SET::MAP-LIST<F>
            ,SET::INVERSEP<F>
            ,@SET::THEORY<F>-DEFTHMS))))))
map-functionmacro
(defmacro map-function
  (function &key
    in-package-of
    set-guard
    list-guard
    element-guard
    arg-guard)
  (map-function-fn function
    (if in-package-of
      in-package-of
      'in)
    (standardize-to-package "?SET"
      '?set
      set-guard)
    (standardize-to-package "?LIST"
      '?list
      list-guard)
    (standardize-to-package "A" 'a element-guard)
    arg-guard))
other
(deftheory generic-map-theory
  (union-theories (theory 'theory<inversep>)
    `(,@(INSTANCE::DEFTHM-NAMES SET::*MAP-THEOREMS*) map
      map-list
      inversep)))
other
(in-theory (disable generic-map-theory))