Filtering...

subset

books/centaur/ubdds/subset

Included Books

extra-operations
other
(in-package "ACL2")
include-book
(include-book "extra-operations")
local
(local (in-theory (enable* (:ruleset canonicalize-to-q-ite))))
qs-subsetfunction
(defund qs-subset
  (x y)
  (declare (xargs :guard t :verify-guards nil))
  (mbe :logic (equal t (q-implies x y))
    :exec (cond ((atom x) (if x
          (and (atom y)
            (if y
              t
              nil))
          t))
      ((atom y) (if y
          t
          nil))
      ((hons-equal x y) t)
      (t (and (qs-subset (car x) (car y))
          (qs-subset (cdr x) (cdr y)))))))
other
(verify-guards qs-subset
  :hints (("Goal" :in-theory (e/d (qs-subset q-implies q-not)
       (canonicalize-q-implies canonicalize-q-not)))))
|(qs-subset nil x)|theorem
(defthm |(qs-subset nil x)|
  (qs-subset nil x)
  :hints (("Goal" :in-theory (e/d (qs-subset q-implies) (canonicalize-q-implies)))))
|(qs-subset x t)|theorem
(defthm |(qs-subset x t)|
  (qs-subset x t)
  :hints (("Goal" :in-theory (e/d (qs-subset q-implies) (canonicalize-q-implies)))))
eval-bdd-when-qs-subsettheorem
(defthm eval-bdd-when-qs-subset
  (implies (and (qs-subset x y) (eval-bdd x values))
    (eval-bdd y values))
  :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (eval-bdd x values) (qs-subset x y))
        (eval-bdd y values)))
    (:rewrite :corollary (implies (and (qs-subset x y) (not (eval-bdd y values)))
        (equal (eval-bdd x values) nil)))
    (:rewrite :corollary (implies (and (not (eval-bdd y values)) (qs-subset x y))
        (equal (eval-bdd x values) nil))))
  :hints (("Goal" :in-theory (e/d (qs-subset) (eval-bdd-of-q-implies))
     :use ((:instance eval-bdd-of-q-implies (x x) (y y))))))
reflexivity-of-qs-subsettheorem
(defthm reflexivity-of-qs-subset
  (qs-subset x x)
  :hints (("Goal" :in-theory (e/d (qs-subset q-implies) (canonicalize-q-implies)))))
transitivity-of-qs-subsetencapsulate
(encapsulate nil
  (local (defthm lemma
      (implies (and (equal t (q-implies x y)) (equal t (q-implies y z)))
        (equal (equal t (q-implies x z)) t))
      :hints (("Goal" :in-theory (e/d (q-implies q-not)
           (canonicalize-q-implies canonicalize-q-not
             equal-by-eval-bdds))))))
  (defthm transitivity-of-qs-subset
    (implies (and (qs-subset x y) (qs-subset y z))
      (equal (qs-subset x z) t))
    :rule-classes ((:rewrite) (:rewrite :corollary (implies (and (qs-subset y z) (qs-subset x y))
          (equal (qs-subset x z) t))))
    :hints (("Goal" :in-theory (e/d (qs-subset)
         (ubddp-of-q-implies canonicalize-q-implies))))))
other
(defsection qs-subset-by-eval-bdds
  (local (in-theory (disable canonicalize-q-implies ubddp-of-q-implies)))
  (local (in-theory (enable qs-subset)))
  (encapsulate (((qs-subset-hyps) => *) ((qs-subset-lhs) => *)
      ((qs-subset-rhs) => *))
    (local (defun qs-subset-hyps nil nil))
    (local (defun qs-subset-lhs nil nil))
    (local (defun qs-subset-rhs nil nil))
    (defthmd qs-subset-by-eval-bdds-constraint
      (implies (qs-subset-hyps)
        (implies (eval-bdd (qs-subset-lhs) arbitrary-values)
          (eval-bdd (qs-subset-rhs) arbitrary-values)))))
  (local (defund qs-subset-badguy
      (x y)
      (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
      (if (or (consp x) (consp y))
        (mv-let (car-successp car-path)
          (qs-subset-badguy (qcar x) (qcar y))
          (if car-successp
            (mv t (cons t car-path))
            (mv-let (cdr-successp cdr-path)
              (qs-subset-badguy (qcdr x) (qcdr y))
              (if cdr-successp
                (mv t (cons nil cdr-path))
                (mv nil nil)))))
        (mv (not (implies x y)) nil))))
  (local (defthm mv-nth-1
      (equal (mv-nth 1 x) (cadr x))
      :hints (("Goal" :in-theory (enable mv-nth)))))
  (local (defthm lemma1
      (implies (car (qs-subset-badguy x y))
        (and (eval-bdd x (cadr (qs-subset-badguy x y)))
          (not (eval-bdd y (cadr (qs-subset-badguy x y))))))
      :hints (("Goal" :in-theory (enable qs-subset-badguy eval-bdd)
         :induct (qs-subset-badguy x y)))))
  (local (defthm q-implies-of-t-when-atom-left
      (implies (not (consp x))
        (equal (equal t (q-implies x y))
          (if x
            (if (atom y)
              (if y
                t
                nil)
              nil)
            t)))
      :hints (("Goal" :in-theory (enable q-implies)))))
  (local (defthm q-implies-of-t-when-atom-right
      (implies (not (consp y))
        (equal (equal t (q-implies x y))
          (if (atom x)
            (if x
              (if (atom y)
                (if y
                  t
                  nil)
                nil)
              t)
            (if y
              t
              (equal t (q-not x))))))
      :hints (("Goal" :in-theory (e/d* (q-implies) (canonicalize-to-q-ite))))))
  (local (defthm equal-t-of-q-implies-of-cons
      (equal (equal t (q-implies (cons a x) (cons b y)))
        (and (equal t (q-implies a b)) (equal t (q-implies x y))))
      :hints (("Goal" :in-theory (enable q-implies)))))
  (local (defthm lemma2
      (implies (and (ubddp x) (ubddp y))
        (equal (car (qs-subset-badguy x y))
          (not (equal t (qs-subset x y)))))
      :hints (("Goal" :induct (qs-subset-badguy x y)
         :in-theory (e/d (qs-subset-badguy ubddp q-not)
           (q-implies-of-nil equal-by-eval-bdds canonicalize-q-not))))))
  (defthm qs-subset-by-eval-bdds
    (implies (and (qs-subset-hyps)
        (ubddp (qs-subset-lhs))
        (ubddp (qs-subset-rhs)))
      (equal (qs-subset (qs-subset-lhs) (qs-subset-rhs)) t))
    :hints (("Goal" :use ((:instance qs-subset-by-eval-bdds-constraint
          (arbitrary-values (cadr (qs-subset-badguy (qs-subset-lhs) (qs-subset-rhs)))))))))
  (defun qs-subset-by-eval-bdds-hint
    (clause pspv stable world)
    (declare (xargs :mode :program))
    (and stable
      (let* ((rcnst (access prove-spec-var pspv :rewrite-constant)) (ens (access rewrite-constant rcnst :current-enabled-structure)))
        (and (enabled-numep (fnume '(:rewrite qs-subset-by-eval-bdds) world)
            ens)
          (let ((conclusion (car (last clause))))
            (and (consp conclusion)
              (eq (car conclusion) 'qs-subset)
              (let* ((lhs (second conclusion)) (rhs (third conclusion))
                  (hyps (dumb-negate-lit-lst (butlast clause 1)))
                  (hint `(:use (:functional-instance qs-subset-by-eval-bdds
                        (qs-subset-hyps (lambda nil (and ,@HYPS)))
                        (qs-subset-lhs (lambda nil ,LHS))
                        (qs-subset-rhs (lambda nil ,RHS))))))
                (prog2$ (cw "~|~%We now appeal to ~s0 in an attempt to show that ~x1 is a ~
                          qs-subset of ~x2.  (You can disable ~s0 to avoid this.)  ~
                          The hint we give is: ~x3~|~%"
                    'qs-subset-by-eval-bdds
                    (untranslate lhs nil world)
                    (untranslate rhs nil world)
                    hint)
                  hint))))))))
  (add-default-hints! '((qs-subset-by-eval-bdds-hint clause
       pspv
       stable-under-simplificationp
       world))))
other
(defsection double-containment
  (local (defthm lemma
      (implies (and (ubddp x) (ubddp y) (qs-subset x y) (qs-subset y x))
        (equal (equal x y) t))))
  (defthm bdd-equality-is-double-containment
    (implies (and (ubddp x) (ubddp y))
      (equal (equal x y) (and (qs-subset x y) (qs-subset y x)))))
  (in-theory (disable equal-by-eval-bdds))
  (defthm qs-subset-when-booleans
    (implies (and (booleanp x) (booleanp y))
      (equal (qs-subset x y)
        (implies (double-rewrite x) (double-rewrite y))))
    :hints (("Goal" :in-theory (enable qs-subset q-implies)))))
other
(def-ruleset qs-subset-mode-rules
  '(bdd-equality-is-double-containment))
|(qs-subset x nil)|theorem
(defthmd |(qs-subset x nil)|
  (implies (ubddp x)
    (equal (qs-subset x nil) (not (double-rewrite x))))
  :hints (("Goal" :in-theory (enable equal-by-eval-bdds))))
|(qs-subset t x)|theorem
(defthmd |(qs-subset t x)|
  (implies (force (ubddp x))
    (equal (qs-subset t x) (equal x t))))
other
(defsection qs-subset-mode-iff-rules
  (defthm qs-subset-canonicalization-of-iff
    (implies (ubddp x) (iff x (not (qs-subset x nil))))
    :rule-classes nil
    :hints (("Goal" :in-theory (disable bdd-equality-is-double-containment)
       :use ((:instance bdd-equality-is-double-containment (x x) (y nil))))))
  (defthm q-ite-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)) (force (ubddp z)))
      (iff (q-ite x y z) (not (qs-subset (q-ite x y z) nil))))
    :hints (("Goal" :use ((:instance qs-subset-canonicalization-of-iff
          (x (q-ite x y z)))))))
  (defthm q-not-iff-for-qs-subset-mode
    (implies (ubddp x)
      (iff (q-not x) (not (qs-subset (q-not x) nil)))))
  (defthm q-and-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-and x y) (not (qs-subset (q-and x y) nil)))))
  (defthm q-or-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-or x y) (not (qs-subset (q-or x y) nil)))))
  (defthm q-implies-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-implies x y) (not (qs-subset (q-implies x y) nil)))))
  (defthm q-or-c2-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-or-c2 x y) (not (qs-subset (q-or-c2 x y) nil)))))
  (defthm q-and-c1-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-and-c1 x y) (not (qs-subset (q-and-c1 x y) nil)))))
  (defthm q-and-c2-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-and-c2 x y) (not (qs-subset (q-and-c2 x y) nil)))))
  (defthm q-iff-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-iff x y) (not (qs-subset (q-iff x y) nil)))))
  (defthm q-xor-iff-for-qs-subset-mode
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (iff (q-xor x y) (not (qs-subset (q-xor x y) nil)))))
  (add-to-ruleset qs-subset-mode-rules
    '(q-ite-iff-for-qs-subset-mode q-not-iff-for-qs-subset-mode
      q-and-iff-for-qs-subset-mode
      q-or-iff-for-qs-subset-mode
      q-implies-iff-for-qs-subset-mode
      q-or-c2-iff-for-qs-subset-mode
      q-and-c1-iff-for-qs-subset-mode
      q-and-c2-iff-for-qs-subset-mode
      q-iff-iff-for-qs-subset-mode
      q-xor-iff-for-qs-subset-mode)))
other
(defsection qs-subset-of-q-ite-left
  (local (defthmd lemma
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w))
          (qs-subset (q-ite x y nil) w)
          (qs-subset (q-ite x nil z) w))
        (qs-subset (q-ite x y z) w))))
  (local (defthmd lemma2
      (implies (and (qs-subset (q-ite x y z) w)
          (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w)))
        (qs-subset (q-ite x y nil) w))))
  (local (defthmd lemma3
      (implies (and (qs-subset (q-ite x y z) w)
          (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w)))
        (qs-subset (q-ite x nil z) w))))
  (defthm qs-subset-of-q-ite-left
    (implies (and (syntaxp (not (equal y ''nil)))
        (syntaxp (not (equal z ''nil)))
        (force (ubddp x))
        (force (ubddp y))
        (force (ubddp z))
        (force (ubddp w)))
      (equal (qs-subset (q-ite x y z) w)
        (and (qs-subset (q-ite x y nil) w)
          (qs-subset (q-ite x nil z) w))))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2) (:instance lemma3))))))
other
(defsection qs-subset-of-q-ite-right
  (local (defthmd lemma
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w))
          (qs-subset (q-ite w x nil) y)
          (qs-subset (q-ite x nil w) z))
        (qs-subset w (q-ite x y z)))))
  (local (defthmd lemma2
      (implies (and (qs-subset w (q-ite x y z))
          (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w)))
        (qs-subset (q-ite w x nil) y))))
  (local (defthmd lemma3
      (implies (and (qs-subset w (q-ite x y z))
          (force (ubddp x))
          (force (ubddp y))
          (force (ubddp z))
          (force (ubddp w)))
        (qs-subset (q-ite x nil w) z))))
  (defthm qs-subset-of-q-ite-right
    (implies (and (force (ubddp x))
        (force (ubddp y))
        (force (ubddp z))
        (force (ubddp w)))
      (equal (qs-subset w (q-ite x y z))
        (and (qs-subset (q-ite w x nil) y)
          (qs-subset (q-ite x nil w) z))))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2) (:instance lemma3))))))
other
(defsection |(qs-subset (q-ite x nil y) x)|
  (local (defthmd gross
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (qs-subset (q-ite x nil y) x)
          (eval-bdd y values))
        (eval-bdd x values))
      :hints (("Goal" :use ((:instance eval-bdd-of-q-ite (y nil) (z y)))))))
  (local (defthmd lemma
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (qs-subset (q-ite x nil y) x))
        (qs-subset y x))
      :hints (("Goal" :in-theory (enable gross)))))
  (local (defthmd lemma2
      (implies (and (force (ubddp x)) (force (ubddp y)) (qs-subset y x))
        (qs-subset (q-ite x nil y) x))))
  (defthm |(qs-subset (q-ite x nil y) x)|
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (qs-subset (q-ite x nil y) x) (qs-subset y x)))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2))))))
other
(defsection |(qs-subset (q-ite x nil y) nil)|
  (local (defthmd gross
      (implies (and (ubddp x)
          (ubddp y)
          (qs-subset (q-ite x nil y) nil)
          (eval-bdd y values))
        (eval-bdd x values))
      :hints (("goal" :use ((:instance eval-bdd-of-q-ite (y nil) (z y)))))))
  (local (defthmd lemma
      (implies (and (ubddp x) (ubddp y) (qs-subset (q-ite x nil y) nil))
        (qs-subset y x))
      :hints (("Goal" :in-theory (enable gross)))))
  (local (defthmd lemma2
      (implies (and (ubddp x) (ubddp y) (qs-subset y x))
        (qs-subset (q-ite x nil y) nil))))
  (defthm |(qs-subset (q-ite x nil y) nil)|
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (qs-subset (q-ite x nil y) nil) (qs-subset y x)))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2))))))
|(qs-subset (q-ite x y nil) x)|theorem
(defthm |(qs-subset (q-ite x y nil) x)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset (q-ite x y nil) x)))
|(qs-subset (q-ite x y nil) y)|theorem
(defthm |(qs-subset (q-ite x y nil) y)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset (q-ite x y nil) y)))
|(qs-subset (q-and x y) x)|theorem
(defthm |(qs-subset (q-and x y) x)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset (q-and x y) x)))
|(qs-subset (q-and x y) y)|theorem
(defthm |(qs-subset (q-and x y) y)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset (q-and x y) y)))
|(qs-subset x (q-and x y))|encapsulate
(encapsulate nil
  (local (defthmd lemma
      (implies (and (force (ubddp x)) (force (ubddp y)) (qs-subset x y))
        (equal (qs-subset x (q-and x y)) t))))
  (local (defthmd lemma2
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (qs-subset x (q-and x y)))
        (equal (qs-subset x y) t))))
  (defthm |(qs-subset x (q-and x y))|
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (qs-subset x (q-and x y)) (qs-subset x y)))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2))))))
|(qs-subset x (q-ite x y nil))|theorem
(defthm |(qs-subset x (q-ite x y nil))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset x (q-ite x y nil)) (qs-subset x y)))
  :hints (("Goal" :use ((:instance |(qs-subset x (q-and x y))|)))))
|(qs-subset y (q-and x y))|theorem
(defthm |(qs-subset y (q-and x y))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset y (q-and x y)) (qs-subset y x)))
  :hints (("Goal" :in-theory (disable canonicalize-q-and
       qs-subset-of-q-ite-right
       |(qs-subset x (q-ite x y nil))|)
     :use ((:instance |(qs-subset x (q-ite x y nil))| (x y) (y x))))))
|(qs-subset y (q-ite x y nil))|theorem
(defthm |(qs-subset y (q-ite x y nil))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset y (q-ite x y nil)) (qs-subset y x)))
  :hints (("Goal" :use ((:instance |(qs-subset y (q-and x y))|)))))
|(qs-subset x (q-ite x t y))|theorem
(defthm |(qs-subset x (q-ite x t y))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset x (q-ite x t y))))
|(qs-subset y (q-ite x t y))|theorem
(defthm |(qs-subset y (q-ite x t y))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset y (q-ite x t y))))
|(qs-subset x (q-or x y))|theorem
(defthm |(qs-subset x (q-or x y))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset x (q-or x y))))
|(qs-subset y (q-or x y))|theorem
(defthm |(qs-subset y (q-or x y))|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (qs-subset y (q-or x y))))
|(qs-subset (q-or x y) x)|encapsulate
(encapsulate nil
  (local (defthmd lemma
      (implies (and (force (ubddp x))
          (force (ubddp y))
          (qs-subset (q-or x y) x))
        (qs-subset y x))))
  (local (defthmd lemma2
      (implies (and (force (ubddp x)) (force (ubddp y)) (qs-subset y x))
        (qs-subset (q-or x y) x))))
  (defthm |(qs-subset (q-or x y) x)|
    (implies (and (force (ubddp x)) (force (ubddp y)))
      (equal (qs-subset (q-or x y) x) (qs-subset y x)))
    :hints (("Goal" :use ((:instance lemma) (:instance lemma2))))))
|(qs-subset (q-ite x t y) x)|theorem
(defthm |(qs-subset (q-ite x t y) x)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset (q-ite x t y) x) (qs-subset y x)))
  :hints (("Goal" :use ((:instance |(qs-subset (q-or x y) x)|)))))
|(qs-subset (q-or x y) y)|theorem
(defthm |(qs-subset (q-or x y) y)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset (q-or x y) y) (qs-subset x y)))
  :hints (("Goal" :in-theory (disable canonicalize-q-or |(qs-subset (q-or x y) x)|)
     :use ((:instance |(qs-subset (q-or x y) x)| (x y) (y x))))))
|(qs-subset (q-ite x t y) y)|theorem
(defthm |(qs-subset (q-ite x t y) y)|
  (implies (and (force (ubddp x)) (force (ubddp y)))
    (equal (qs-subset (q-ite x t y) y) (qs-subset x y)))
  :hints (("Goal" :use ((:instance |(qs-subset (q-or x y) y)|)))))