param - ACL2 Book

Included Books

extra-operations hons-help2 rulesets take top top-with-meta

other

(in-package "ACL2")

include-book

(include-book "extra-operations")

include-book

(include-book "misc/hons-help2" :dir :system)

include-book

(include-book "tools/rulesets" :dir :system)

local

(local (include-book "std/lists/take" :dir :system))

local

(local (include-book "arithmetic/top" :dir :system))

local

(local (in-theory (disable* default-car
      default-cdr
      default-+-2
      default-+-1
      default-<-2
      default-<-1
      (:ruleset canonicalize-to-q-ite)
      equal-by-eval-bdds)))

local

(local (in-theory (enable eval-bdd
      eval-bdd-list
      ubddp
      ubdd-listp
      q-compose
      q-compose-list)))

other

(defn find-diff
  (a b)
  (declare (xargs :measure (+ (acl2-count a) (acl2-count b))))
  (if (and (atom a) (atom b))
    nil
    (if (hqual (qcdr a) (qcdr b))
      (cons t (find-diff (qcar a) (qcar b)))
      (cons nil (find-diff (qcdr a) (qcdr b))))))

other

(defn find-diff-of-length
  (a b n)
  (declare (xargs :measure (nfix n)))
  (if (zp (nfix n))
    nil
    (if (and (atom a) (atom b))
      (cons nil (find-diff-of-length a b (1- n)))
      (if (hqual (qcdr a) (qcdr b))
        (cons t (find-diff-of-length (qcar a) (qcar b) (1- n)))
        (cons nil (find-diff-of-length (qcdr a) (qcdr b) (1- n)))))))

head-tail-bind-fnfunction

(defun head-tail-bind-fn
  (bindings body)
  (if (atom bindings)
    body
    (let ((b (car bindings)))
      `(mv-let (,(CAR B) ,(CADR B))
        (if (consp ,(CADDR B))
          (mv (car ,(CADDR B)) (cdr ,(CADDR B)))
          (mv nil nil))
        (declare (ignorable ,(CAR B) ,(CADR B)))
        ,(HEAD-TAIL-BIND-FN (CDR BINDINGS) BODY)))))

head-tail-bindmacro

(defmacro head-tail-bind
  (bindings body)
  (head-tail-bind-fn bindings body))

other

(defn q-ite-list
  (x ys zs)
  (declare (xargs :measure (+ (acl2-count ys) (acl2-count zs))))
  (if (and (atom ys) (atom zs))
    nil
    (head-tail-bind ((z1 zr zs) (y1 yr ys))
      (cons (q-ite x y1 z1) (q-ite-list x yr zr)))))

other

(defn q-zipper
  (l1 l2)
  (declare (xargs :measure (+ (len l1) (len l2))))
  (if (and (atom l1) (atom l2))
    nil
    (head-tail-bind ((l11 l1r l1) (l21 l2r l2))
      (cons (qcons l11 l21) (q-zipper l1r l2r)))))

in-theory

(in-theory (disable q-zipper))

other

(defn qv-list
  (start by n)
  (declare (xargs :measure (nfix n)))
  (if (zp (nfix n))
    nil
    (cons (qv (nfix start))
      (qv-list (ec-call (binary-+ by start)) by (1- n)))))

other

(defn bfix-list
  (l)
  (if (atom l)
    nil
    (cons (if (car l)
        t
        nil)
      (bfix-list (cdr l)))))

other

(defn q-param
  (x nvars)
  (cond ((zp (nfix nvars)) nil)
    ((atom x) (qv-list 0 1 nvars))
    ((not (car x)) (cons nil (q-param (cdr x) (1- nvars))))
    ((not (cdr x)) (cons t (q-param (car x) (1- nvars))))
    (t (cons (qv 0)
        (q-zipper (q-param (car x) (1- nvars))
          (q-param (cdr x) (1- nvars)))))))

other

(defn q-param-inv
  (x nvars)
  (cond ((zp (nfix nvars)) nil)
    ((atom x) (qv-list 0 1 nvars))
    ((not (car x)) (let ((x (q-param-inv (cdr x) (1- nvars))))
        (q-zipper x x)))
    ((not (cdr x)) (let ((x (q-param-inv (car x) (1- nvars))))
        (q-zipper x x)))
    (t (cons (qv 0)
        (q-zipper (q-param-inv (car x) (1- nvars))
          (q-param-inv (cdr x) (1- nvars)))))))

other

(defn max-max-depth
  (x)
  (if (atom x)
    0
    (max (max-depth (car x)) (max-max-depth (cdr x)))))

other

(defn extend-list
  (a b)
  (declare (xargs :measure (+ (len a) (len b))))
  (if (and (atom a) (atom b))
    a
    (head-tail-bind ((a1 ar a) (b1 br b))
      (cons a1 (extend-list ar br)))))

ebmde-indfunction

(defun ebmde-ind
  (x l l2)
  (if (atom x)
    (list l l2)
    (list (ebmde-ind (car x) (cdr l) (cdr l2))
      (ebmde-ind (cdr x) (cdr l) (cdr l2)))))

eval-bdd-max-depth-extendtheorem

(defthm eval-bdd-max-depth-extend
  (implies (<= (max-depth x) (len l))
    (equal (eval-bdd x (extend-list l l2)) (eval-bdd x l)))
  :hints (("goal" :induct (ebmde-ind x l l2)
     :in-theory (e/d (default-car default-cdr max-depth) nil))))

eval-bdd-list-max-max-depth-extendtheorem

(defthm eval-bdd-list-max-max-depth-extend
  (implies (<= (max-max-depth x) (len l))
    (equal (eval-bdd-list x (extend-list l l2))
      (eval-bdd-list x l)))
  :hints (("goal" :in-theory (disable))))

len-eval-bdd-listtheorem

(defthm len-eval-bdd-list
  (equal (len (eval-bdd-list x l)) (len x)))

ubddp-cons-forward-chaintheorem

(defthm ubddp-cons-forward-chain
  (implies (and (ubddp x) (consp x))
    (and (ubddp (car x)) (ubddp (cdr x))))
  :rule-classes :forward-chaining)

ubddp-atom-forward-chaintheorem

(defthm ubddp-atom-forward-chain
  (implies (and (ubddp x) (not (consp x)))
    (or (equal x nil) (equal x t)))
  :rule-classes :forward-chaining)

car-nthcdrtheorem

(defthm car-nthcdr (equal (car (nthcdr n l)) (nth n l)))

nth-implies-consp-nthcdrtheorem

(defthm nth-implies-consp-nthcdr
  (implies (nth n l) (consp (nthcdr n l))))

cdr-nthcdrtheorem

(defthm cdr-nthcdr
  (equal (nthcdr n (cdr l)) (cdr (nthcdr n l))))

eval-bdd-difftheorem

(defthm eval-bdd-diff
  (implies (and (ubddp a) (ubddp b) (not (equal a b)))
    (not (equal (eval-bdd a (find-diff a b))
        (eval-bdd b (find-diff a b)))))
  :hints (("Goal" :induct (find-diff a b))))

eval-bdd-diff-of-lengththeorem

(defthm eval-bdd-diff-of-length
  (implies (and (ubddp a)
      (ubddp b)
      (not (equal a b))
      (<= (max-depth a) (nfix n))
      (<= (max-depth b) (nfix n)))
    (not (equal (eval-bdd a (find-diff-of-length a b n))
        (eval-bdd b (find-diff-of-length a b n)))))
  :hints (("goal" :in-theory (enable max-depth))))

find-diff-of-length-lentheorem

(defthm find-diff-of-length-len
  (equal (len (find-diff-of-length a b n)) (nfix n)))

q-and-equals-ttheorem

(defthm q-and-equals-t
  (implies (equal (q-and x y) t)
    (and (implies (ubddp x) (equal x t))
      (implies (ubddp y) (equal y t))))
  :hints (("goal" :in-theory (enable q-and)))
  :rule-classes :forward-chaining)

ubddp-q-not-t-implies-nottheorem

(defthmd ubddp-q-not-t-implies-not
  (implies (and (ubddp x) x) (not (equal (q-not x) t)))
  :hints (("goal" :in-theory (enable q-not))))

ubddp-q-not-nil-implies-ttheorem

(defthmd ubddp-q-not-nil-implies-t
  (implies (and (ubddp x) (not (q-not x)))
    (equal (equal x t) t))
  :hints (("goal" :in-theory (enable q-not))))

ubdd-listp-q-ite-listtheorem

(defthm ubdd-listp-q-ite-list
  (implies (and (ubddp x) (ubdd-listp ys) (ubdd-listp zs))
    (ubdd-listp (q-ite-list x ys zs)))
  :hints (("goal" :induct (q-ite-list x ys zs))))

q-compose-to-eval-bddtheorem

(defthm q-compose-to-eval-bdd
  (implies (and (ubddp x) (ubdd-listp l))
    (equal (eval-bdd (q-compose x l) vals)
      (eval-bdd x (eval-bdd-list l vals)))))

q-ite-list-correcttheorem

(defthm q-ite-list-correct
  (implies (and (ubddp x)
      (ubdd-listp ys)
      (ubdd-listp zs)
      (equal (len ys) (len zs)))
    (equal (eval-bdd-list (q-ite-list x ys zs) vals)
      (if (eval-bdd x vals)
        (eval-bdd-list ys vals)
        (eval-bdd-list zs vals)))))

eval-bdd-q-compose-commutes-with-q-itetheorem

(defthm eval-bdd-q-compose-commutes-with-q-ite
  (implies (and (ubddp x)
      (ubddp y)
      (ubdd-listp l1)
      (ubdd-listp l2)
      (equal (len l1) (len l2)))
    (equal (eval-bdd (q-ite x (q-compose y l1) (q-compose y l2)) vals)
      (eval-bdd (q-compose y (q-ite-list x l1 l2)) vals)))
  :hints (("goal" :in-theory (disable q-compose))))

q-compose-commutes-with-q-itetheorem

(defthm q-compose-commutes-with-q-ite
  (implies (and (ubddp x)
      (ubddp y)
      (ubdd-listp l1)
      (ubdd-listp l2)
      (equal (len l1) (len l2)))
    (equal (q-ite x (q-compose y l1) (q-compose y l2))
      (q-compose y (q-ite-list x l1 l2))))
  :hints (("Goal" :in-theory (enable equal-by-eval-bdds))))

q-compose-list-correcttheorem

(defthm q-compose-list-correct
  (implies (and (ubdd-listp ys) (ubdd-listp zs))
    (equal (eval-bdd-list (q-compose-list ys zs) vals)
      (eval-bdd-list ys (eval-bdd-list zs vals)))))

eval-bdd-q-compose-associativetheorem

(defthm eval-bdd-q-compose-associative
  (implies (and (ubddp x) (ubdd-listp ys) (ubdd-listp zs))
    (equal (eval-bdd (q-compose (q-compose x ys) zs) vals)
      (eval-bdd (q-compose x (q-compose-list ys zs)) vals))))

q-compose-associativetheorem

(defthm q-compose-associative
  (implies (and (ubddp x) (ubdd-listp ys) (ubdd-listp zs))
    (equal (q-compose (q-compose x ys) zs)
      (q-compose x (q-compose-list ys zs))))
  :hints (("Goal" :in-theory (enable equal-by-eval-bdds))))

eval-bdd-depththeorem

(defthm eval-bdd-depth
  (implies (<= (max-depth x) (len l))
    (equal (eval-bdd x (append l l2)) (eval-bdd x l)))
  :hints (("goal" :in-theory (enable max-depth))))

in-theory

(in-theory (enable q-zipper))

ubdd-listp-q-zippertheorem

(defthm ubdd-listp-q-zipper
  (implies (and (ubdd-listp l1) (ubdd-listp l2))
    (ubdd-listp (q-zipper l1 l2))))

len-q-zippertheorem

(defthm len-q-zipper
  (equal (len (q-zipper l1 l2)) (max (len l1) (len l2))))

nth-q-zipper-indfunction

(defun nth-q-zipper-ind
  (n a b)
  (if (zp n)
    (cons a b)
    (head-tail-bind ((a1 ar a) (b1 br b))
      (nth-q-zipper-ind (1- n) ar br))))

nth-q-zippertheorem

(defthm nth-q-zipper
  (implies (and (<= (nfix n) (len a)) (<= (nfix n) (len b)))
    (equal (nth n (q-zipper a b)) (qcons (nth n a) (nth n b))))
  :hints (("goal" :induct (nth-q-zipper-ind n a b))))

in-theory

(in-theory (disable q-zipper))

nth-qv-list-indfunction

(defun nth-qv-list-ind
  (m start by n)
  (if (zp m)
    (list start by n)
    (nth-qv-list-ind (1- m) (+ start by) by (1- n))))

nth-qv-listtheorem

(defthm nth-qv-list
  (implies (and (integerp n)
      (integerp m)
      (<= 0 m)
      (< m n)
      (integerp start)
      (<= 0 start)
      (integerp by)
      (<= 0 by))
    (equal (nth m (qv-list start by n)) (qv (+ start (* m by)))))
  :hints (("goal" :induct (nth-qv-list-ind m start by n)
     :in-theory (enable qv zp nfix)) (and (case-match id (((0 1) . &) t))
      '(:expand (qv-list start by n)))))

eval-bdd-extend-listtheorem

(defthm eval-bdd-extend-list
  (equal (eval-bdd-list (extend-list a b) vars)
    (extend-list (eval-bdd-list a vars) b)))

eval-q-zippertheorem

(defthm eval-q-zipper
  (equal (eval-bdd-list (q-zipper l1 l2) vars)
    (if (car vars)
      (eval-bdd-list (extend-list l1 l2) (cdr vars))
      (eval-bdd-list (extend-list l2 l1) (cdr vars))))
  :hints (("goal" :in-theory (enable q-zipper))))

ubddp-qv-alltheorem

(defthm ubddp-qv-all (ubddp (qv n)))

ubdd-listp-qv-listtheorem

(defthm ubdd-listp-qv-list
  (ubdd-listp (qv-list start by n)))

len-qv-listtheorem

(defthm len-qv-list
  (equal (len (qv-list start by n)) (nfix n)))

max-max-depth-q-zipper-upper-boundtheorem

(defthm max-max-depth-q-zipper-upper-bound
  (implies (and (<= (max-max-depth x) c) (<= (max-max-depth y) c))
    (<= (max-max-depth (q-zipper x y)) (+ 1 c)))
  :hints (("goal" :in-theory (enable q-zipper max-depth)))
  :rule-classes (:rewrite :linear))

max-depth-qvtheorem

(defthm max-depth-qv
  (equal (max-depth (qv n)) (1+ (nfix n)))
  :hints (("goal" :in-theory (enable max-depth qv))))

max-max-depth-qv-listencapsulate

(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthm max-max-depth-qv-list
    (implies (and (natp start) (natp by) (posp n))
      (equal (max-max-depth (qv-list start by n))
        (+ 1 start (* by (1- n)))))
    :hints (("goal" :in-theory (enable max-depth natp posp)) ("Subgoal *1/5" :expand (qv-list start by 1))))
  (defthm max-max-depth-make-list-ac
    (equal (max-max-depth (make-list-ac n nil acc))
      (max-max-depth acc)))
  (defthm len-q-param-inv
    (implies (<= (max-depth x) (nfix nvars))
      (<= (max-max-depth (q-param x nvars))
        (len (q-param-inv x nvars))))
    :hints (("goal" :in-theory (enable max-depth)) ("Subgoal *1/16" :use ((:instance max-max-depth-q-zipper-upper-bound
           (x (q-param (car x) (1- nvars)))
           (y (q-param (cdr x) (1- nvars)))
           (c (len (q-param-inv (car x) (+ -1 nvars))))) (:instance max-max-depth-q-zipper-upper-bound
            (x (q-param (car x) (1- nvars)))
            (y (q-param (cdr x) (1- nvars)))
            (c (len (q-param-inv (cdr x) (+ -1 nvars))))))))
    :rule-classes :linear))

max-max-depth-q-paramtheorem

(defthm max-max-depth-q-param
  (<= (max-max-depth (q-param pred n)) (nfix n))
  :rule-classes (:rewrite :linear))

max-max-depth-q-param-invtheorem

(defthm max-max-depth-q-param-inv
  (<= (max-max-depth (q-param-inv pred n)) (nfix n))
  :rule-classes (:rewrite :linear))

not-eval-bdd-qv-niltheorem

(defthm not-eval-bdd-qv-nil (not (eval-bdd (qv n) nil)))

eval-bdd-qv1theorem

(defthm eval-bdd-qv1
  (equal (eval-bdd (qv n) vars)
    (if (nth n vars)
      t
      nil)))

local

(local (encapsulate nil
    (local (include-book "arithmetic/top" :dir :system))
    (defthm take-bfix-list
      (equal (take (len vars) (bfix-list vars)) (bfix-list vars)))))

bfix-list-bfix-listtheorem

(defthm bfix-list-bfix-list
  (equal (bfix-list (bfix-list x)) (bfix-list x)))

eval-qv-listtheorem

(defthm eval-qv-list
  (implies (natp start)
    (equal (eval-bdd-list (qv-list start 1 n) vars)
      (bfix-list (take n (nthcdr start vars)))))
  :hints (("Goal" :in-theory (enable take))))

ubdd-listp-make-list-actheorem

(defthm ubdd-listp-make-list-ac
  (equal (ubdd-listp (make-list-ac n nil acc))
    (ubdd-listp acc)))

ubdd-listp-q-paramtheorem

(defthm ubdd-listp-q-param (ubdd-listp (q-param x depth)))

len-of-make-list-actheorem

(defthm len-of-make-list-ac
  (equal (len (make-list-ac n val acc))
    (+ (nfix n) (len acc))))

len-q-paramtheorem

(defthm len-q-param
  (equal (len (q-param x depth)) (nfix depth)))

q-param-eval-bdd-indfunction

(defun q-param-eval-bdd-ind
  (x depth vars)
  (if (atom x)
    (cons depth vars)
    (list (q-param-eval-bdd-ind (car x) (1- depth) (cdr vars))
      (q-param-eval-bdd-ind (cdr x) (1- depth) (cdr vars))
      (q-param-eval-bdd-ind (car x) (1- depth) vars)
      (q-param-eval-bdd-ind (cdr x) (1- depth) vars))))

eval-q-paramtheorem

(defthm eval-q-param
  (implies (and (natp depth) (<= (max-depth x) depth) (ubddp x) x)
    (equal (eval-bdd x (eval-bdd-list (q-param x depth) vars))
      t))
  :hints (("Goal" :induct (q-param-eval-bdd-ind x depth vars)
     :in-theory (enable max-depth))))

local

(local (defthm bfix-list-list-fix
    (equal (bfix-list (list-fix x)) (bfix-list x))))

other

(defn eqpib-ind
  (x vars)
  (cond ((atom vars) x)
    ((atom x) vars)
    ((not (car x)) (eqpib-ind (cdr x) (cdr vars)))
    ((not (cdr x)) (eqpib-ind (car x) (cdr vars)))
    (t (list (eqpib-ind (car x) (cdr vars))
        (eqpib-ind (cdr x) (cdr vars))))))

extend-list-lentheorem

(defthm extend-list-len
  (implies (<= (len b) (len a)) (equal (extend-list a b) a)))

ubdd-listp-q-param-invtheorem

(defthm ubdd-listp-q-param-inv
  (ubdd-listp (q-param-inv x nvars)))

eval-q-param-invtheorem

(defthm eval-q-param-inv
  (implies (and (equal (eval-bdd x vars) t)
      (<= (max-depth x) (len vars)))
    (equal (eval-bdd-list (q-param x (len vars))
        (eval-bdd-list (q-param-inv x (len vars)) vars))
      (bfix-list vars)))
  :hints (("goal" :induct (eqpib-ind x vars)
     :in-theory (e/d (max-depth)))))

len-q-param-inv-upper-boundtheorem

(defthm len-q-param-inv-upper-bound
  (<= (len (q-param-inv x nvars)) (nfix nvars))
  :rule-classes :linear)

len-bfix-listtheorem

(defthm len-bfix-list (equal (len (bfix-list x)) (len x)))

compose-q-param-invtheorem

(defthm compose-q-param-inv
  (implies (and (equal (eval-bdd x vars) t)
      (<= (max-depth x) (len vars)))
    (equal (eval-bdd-list (q-compose-list (q-param x (len vars))
          (q-param-inv x (len vars)))
        vars)
      (bfix-list vars))))

bfix-list-boolean-listtheorem

(defthm bfix-list-boolean-list
  (and (boolean-listp (bfix-list x))
    (implies (boolean-listp x) (equal (bfix-list x) x))))

forall-y-p-of-param-of-y-is-truetheorem

(defthm forall-y-p-of-param-of-y-is-true
  (implies (and p (ubddp p) (integerp n) (<= (max-depth p) n))
    (equal (eval-bdd p (eval-bdd-list (q-param p n) y)) t)))

exists-y-such-that-x-is-param-of-ytheorem

(defthm exists-y-such-that-x-is-param-of-y
  (implies (and (equal (eval-bdd p x) t)
      (<= (max-depth p) (len x))
      (boolean-listp x))
    (let ((y (eval-bdd-list (q-param-inv p (len x)) x)))
      (equal (eval-bdd-list (q-param p (len x)) y) x))))

x-is-param-of-y-compose-evaltheorem

(defthm x-is-param-of-y-compose-eval
  (implies (and (equal (eval-bdd p x) t)
      (<= (max-depth p) (len x))
      (boolean-listp x))
    (equal (eval-bdd-list (q-compose-list (q-param p (len x)) (q-param-inv p (len x)))
        x)
      x)))

other

(memoize 'q-param :condition '(consp x))

other

(memoize 'q-param-inv :condition '(consp x))

other

(memoize 'q-compose :condition '(consp x))

other

(defn from-param-space
  (p y)
  (cond ((atom y) (if y
        p
        nil))
    ((atom p) (if p
        y
        nil))
    ((eq (car p) nil) (let ((x (from-param-space (cdr p) y)))
        (qcons nil x)))
    ((eq (cdr p) nil) (let ((x (from-param-space (car p) y)))
        (qcons x nil)))
    (t (qcons (from-param-space (car p) (car y))
        (from-param-space (cdr p) (cdr y))))))

other

(memoize 'from-param-space
  :condition '(or (consp p) (consp y)))

other

(defn to-param-space
  (p y)
  (cond ((atom p) y)
    ((atom y) y)
    ((eq (car p) nil) (to-param-space (cdr p) (cdr y)))
    ((eq (cdr p) nil) (to-param-space (car p) (car y)))
    (t (qcons (to-param-space (car p) (car y))
        (to-param-space (cdr p) (cdr y))))))

other

(memoize 'to-param-space
  :condition '(and (consp p) (consp y) (car p) (cdr p)))

ubddp-to-param-spacetheorem

(defthm ubddp-to-param-space
  (implies (ubddp x) (ubddp (to-param-space p x))))

param-envfunction

(defun param-env
  (p env)
  (declare (xargs :guard t))
  (cond ((atom p) env)
    ((atom env) nil)
    ((eq (car p) nil) (param-env (cdr p) (cdr env)))
    ((eq (cdr p) nil) (param-env (car p) (cdr env)))
    ((car env) (cons t (param-env (car p) (cdr env))))
    (t (cons nil (param-env (cdr p) (cdr env))))))

param-env-to-param-spacetheorem

(defthm param-env-to-param-space
  (implies (eval-bdd p env)
    (equal (eval-bdd (to-param-space p x) (param-env p env))
      (eval-bdd x env)))
  :hints (("Goal" :in-theory (enable eval-bdd to-param-space))))

unparam-envfunction

(defun unparam-env
  (p env)
  (declare (xargs :guard t))
  (cond ((atom p) env)
    ((eq (car p) nil) (cons nil (unparam-env (cdr p) env)))
    ((eq (cdr p) nil) (cons t (unparam-env (car p) env)))
    (t (mv-let (car cdr)
        (if (consp env)
          (mv (car env) (cdr env))
          (mv nil nil))
        (cons car
          (unparam-env (if car
              (car p)
              (cdr p))
            cdr))))))

eval-param-env-of-unparam-envencapsulate

(encapsulate nil
  (local (defun ind
      (x p env)
      (if (consp x)
        (if (consp p)
          (if (car p)
            (if (cdr p)
              (if (car env)
                (ind (car x) (car p) (cdr env))
                (ind (cdr x) (cdr p) (cdr env)))
              (ind x (car p) env))
            (ind x (cdr p) env))
          x)
        env)))
  (defthm eval-param-env-of-unparam-env
    (equal (eval-bdd x (param-env p (unparam-env p env)))
      (eval-bdd x env))
    :hints (("goal" :induct (ind x p env)
       :in-theory (enable default-car default-cdr)) (and stable-under-simplificationp
        '(:expand ((:free (env) (eval-bdd x env))))))))

eval-with-unparam-envtheorem

(defthm eval-with-unparam-env
  (implies (and p (ubddp p)) (eval-bdd p (unparam-env p env))))

unparam-env-indfunction

(defun unparam-env-ind
  (x p env)
  (cond ((atom p) (list x env))
    ((eq (car p) nil) (unparam-env-ind (cdr x) (cdr p) env))
    ((eq (cdr p) nil) (unparam-env-ind (car x) (car p) env))
    (t (unparam-env-ind (if (car env)
          (car x)
          (cdr x))
        (if (car env)
          (car p)
          (cdr p))
        (cdr env)))))

unparam-env-to-param-spacetheorem

(defthmd unparam-env-to-param-space
  (equal (eval-bdd (to-param-space p x) env)
    (eval-bdd x (unparam-env p env)))
  :hints (("goal" :induct (unparam-env-ind x p env)
     :expand ((:free (env) (eval-bdd x env)) (:free (env) (unparam-env p env)))
     :in-theory (enable default-car default-cdr))))

unparam-env-of-param-envtheorem

(defthm unparam-env-of-param-env
  (implies (eval-bdd p env)
    (equal (eval-bdd x (unparam-env p (param-env p env)))
      (eval-bdd x env)))
  :hints (("goal" :use ((:instance param-env-to-param-space) (:instance unparam-env-to-param-space
         (env (param-env p env)))))))

other

(defn to-param-space-list
  (p list)
  (if (atom list)
    nil
    (cons (to-param-space p (car list))
      (to-param-space-list p (cdr list)))))

eval-bdd-lst-to-param-space-lsttheorem

(defthm eval-bdd-lst-to-param-space-lst
  (implies (eval-bdd p env)
    (equal (eval-bdd-list (to-param-space-list p list)
        (param-env p env))
      (eval-bdd-list list env))))

q-param-to-param-indfunction

(defun q-param-to-param-ind
  (p m n)
  (if (atom p)
    (cons m n)
    (cons (q-param-to-param-ind (car p) (1- m) (1- n))
      (q-param-to-param-ind (cdr p) (1- m) (1- n)))))

nth-make-list-ac-nilencapsulate

(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthm nth-make-list-ac-nil
    (equal (nth m (make-list-ac n nil acc))
      (and (<= (nfix n) (nfix m)) (nth (- (nfix m) (nfix n)) acc)))
    :hints (("goal" :induct (make-list-ac n nil acc)))))

q-param-to-paramtheorem

(defthm q-param-to-param
  (implies (and (integerp n)
      (integerp m)
      (<= 0 m)
      (< m n)
      (<= (max-depth p) n))
    (equal (nth m (q-param p n)) (to-param-space p (qv m))))
  :hints (("goal" :induct (q-param-to-param-ind p m n)
     :in-theory (enable max-depth qv))))

q-not-to-paramencapsulate

(encapsulate nil
  (local (in-theory (disable equal-by-eval-bdds)))
  (local (defthm q-not-equal-t
      (implies (ubddp x)
        (equal (equal (q-not x) t) (equal x nil)))
      :hints (("goal" :in-theory (enable q-not)))))
  (local (defthm not-q-not-x
      (implies (ubddp x) (iff (q-not x) (not (equal x t))))
      :hints (("goal" :in-theory (enable q-not)))))
  (local (in-theory (disable q-not-under-iff)))
  (defthm q-not-to-param
    (implies (and p (ubddp p) (ubddp x))
      (equal (q-not (to-param-space p x))
        (to-param-space p (q-not x))))
    :hints (("goal" :in-theory (e/d (q-not) (equal-by-eval-bdds))) ("Subgoal *1/9" :in-theory (e/d (q-not ubddp-q-not-t-implies-not ubddp-q-not-nil-implies-t))))))

q-and-to-param-indencapsulate

(encapsulate nil
  (local (defthm not-consp-not-nil-implies-t
      (implies (and (not (consp (to-param-space p x)))
          (ubddp x)
          (to-param-space p x))
        (equal (to-param-space p x) t))
      :rule-classes :forward-chaining))
  (defun q-and-to-param-ind
    (p x y)
    (if (atom p)
      (cons x y)
      (cons (q-and-to-param-ind (car p) (qcar x) (qcar y))
        (q-and-to-param-ind (cdr p) (qcdr x) (qcdr y)))))
  (defthm q-and-to-param
    (implies (and (ubddp x) (ubddp y))
      (equal (q-and (to-param-space p x) (to-param-space p y))
        (to-param-space p (q-and x y))))
    :hints (("goal" :induct (q-and-to-param-ind p x y)
       :in-theory (e/d (q-and) (ubddp (force)))))))

q-ite-in-terms-of-and-and-nottheorem

(defthm q-ite-in-terms-of-and-and-not
  (implies (and (ubddp x) (ubddp y) (ubddp z))
    (equal (q-ite x y z)
      (q-not (q-and (q-not (q-and x y)) (q-not (q-and (q-not x) z))))))
  :hints (("Goal" :in-theory (enable equal-by-eval-bdds)))
  :rule-classes nil)

q-ite-to-paramtheorem

(defthm q-ite-to-param
  (implies (and p (ubddp p) (ubddp x) (ubddp y) (ubddp z))
    (equal (q-ite (to-param-space p x)
        (to-param-space p y)
        (to-param-space p z))
      (to-param-space p (q-ite x y z))))
  :hints (("goal" :use ((:instance q-ite-in-terms-of-and-and-not) (:instance q-ite-in-terms-of-and-and-not
         (x (to-param-space p x))
         (y (to-param-space p y))
         (z (to-param-space p z)))))))

to-from-param-spacetheorem

(defthm to-from-param-space
  (implies (and (ubddp x) (ubddp p))
    (equal (from-param-space p (to-param-space p x))
      (q-and p x)))
  :hints (("goal" :induct (to-param-space p x)
     :in-theory (e/d (q-and) (ubddp)))))

eval-bdd-of-qconstheorem

(defthm eval-bdd-of-qcons
  (equal (eval-bdd (qcons x y) env)
    (if (car env)
      (eval-bdd x (cdr env))
      (eval-bdd y (cdr env)))))

to-from-indfunction

(defun to-from-ind
  (p x env)
  (if (consp p)
    (cond ((eq (car p) nil) (and (not (car env))
          (to-from-ind (cdr p) (cdr x) (cdr env))))
      ((eq (cdr p) nil) (and (car env) (to-from-ind (car p) (car x) (cdr env))))
      (t (list (to-from-ind (car p) (car x) (cdr env))
          (to-from-ind (cdr p) (cdr x) (cdr env)))))
    (list p x env)))

from-param-space-of-qconstheorem

(defthm from-param-space-of-qcons
  (implies (and (car p) (cdr p))
    (equal (from-param-space p (qcons x y))
      (if (atom (qcons x y))
        (and x p)
        (qcons (from-param-space (car p) x)
          (from-param-space (cdr p) y)))))
  :otf-flg t)

consp-qconstheorem

(defthm consp-qcons
  (equal (consp (qcons x y))
    (not (and (booleanp x) (equal x y)))))

to-from-param-space-evaltheorem

(defthm to-from-param-space-eval
  (equal (eval-bdd (from-param-space p (to-param-space p x)) env)
    (and (eval-bdd p env) (eval-bdd x env)))
  :hints (("goal" :induct (to-from-ind p x env)
     :in-theory (disable qcons))))

to-param-space-selftheorem

(defthm to-param-space-self
  (implies (and (ubddp p) p) (equal (to-param-space p p) t))
  :hints (("Goal" :in-theory (enable ubddp))))

from-to-param-spacetheorem

(defthm from-to-param-space
  (implies (and (ubddp x) (ubddp p) p)
    (equal (to-param-space p (from-param-space p x)) x))
  :hints (("goal" :induct (from-param-space p x)
     :in-theory (e/d (q-and) (ubddp)))))

param-env-indfunction

(defun param-env-ind
  (x p env)
  (cond ((atom p) (list x env))
    ((eq (car p) nil) (param-env-ind x (cdr p) (cdr env)))
    ((eq (cdr p) nil) (param-env-ind x (car p) (cdr env)))
    ((car env) (cons t (param-env-ind (car x) (car p) (cdr env))))
    (t (cons nil (param-env-ind (cdr x) (cdr p) (cdr env))))))

eval-of-from-param-spacetheorem

(defthm eval-of-from-param-space
  (implies (eval-bdd p env)
    (equal (eval-bdd (from-param-space p x) env)
      (eval-bdd x (param-env p env))))
  :hints (("goal" :induct (param-env-ind x p env)
     :expand ((from-param-space p x) (unparam-env p env)
       (:free (env) (eval-bdd x env))
       (eval-bdd p env)))))

other

(defn to-param-space2
  (p y)
  (cond ((atom p) y)
    ((atom y) y)
    ((eq (car p) nil) (let ((x (to-param-space2 (cdr p) (cdr y))))
        (qcons x x)))
    ((eq (cdr p) nil) (let ((x (to-param-space2 (car p) (car y))))
        (qcons x x)))
    (t (qcons (to-param-space2 (car p) (car y))
        (to-param-space2 (cdr p) (cdr y))))))

other

(memoize 'to-param-space2
  :condition '(and (consp p) (consp y) (car p) (cdr p)))

ubddp-to-param-space2theorem

(defthm ubddp-to-param-space2
  (implies (ubddp x) (ubddp (to-param-space2 p x))))

eval-of-to-param-space2encapsulate

(encapsulate nil
  (local (defun eval-of-to-param-space2-ind
      (p y env)
      (cond ((atom p) env)
        ((atom y) env)
        ((eq (car p) nil) (eval-of-to-param-space2-ind (cdr p) (cdr y) (cdr env)))
        ((eq (cdr p) nil) (eval-of-to-param-space2-ind (car p) (car y) (cdr env)))
        (t (list (eval-of-to-param-space2-ind (car p) (car y) (cdr env))
            (eval-of-to-param-space2-ind (cdr p) (cdr y) (cdr env)))))))
  (local (in-theory (disable iff not qcons)))
  (defthm eval-of-to-param-space2
    (implies (eval-bdd p env)
      (equal (eval-bdd (to-param-space2 p y) env)
        (eval-bdd y env)))
    :hints (("goal" :induct (eval-of-to-param-space2-ind p y env)))))

other

(defn to-param-space2-list
  (p list)
  (if (atom list)
    nil
    (cons (to-param-space2 p (car list))
      (to-param-space2-list p (cdr list)))))

eval-bdd-lst-to-param-space2-lsttheorem

(defthm eval-bdd-lst-to-param-space2-lst
  (implies (eval-bdd p env)
    (equal (eval-bdd-list (to-param-space2-list p list) env)
      (eval-bdd-list list env))))

eval-bdd-of-p-under-to-param-space2-listencapsulate

(encapsulate nil
  (local (defthm to-param-space2-list-of-consp-p-qv-list
      (implies (and (consp p) (posp start))
        (equal (to-param-space2-list p (qv-list start 1 n))
          (b* ((rest-car (to-param-space2-list (car p) (qv-list (1- start) 1 n))) (rest-cdr (to-param-space2-list (cdr p) (qv-list (1- start) 1 n))))
            (cond ((eq (car p) nil) (q-zipper rest-cdr rest-cdr))
              ((eq (cdr p) nil) (q-zipper rest-car rest-car))
              (t (q-zipper rest-car rest-cdr))))))
      :hints (("Goal" :induct (qv-list start 1 n)
         :expand ((:free (a b) (to-param-space2-list p (cons a b))) (:free (a b c d) (q-zipper (cons a b) (cons c d)))
           (:free (a b) (to-param-space2 p (cons a b)))
           (qv start))
         :do-not-induct t))))
  (local (defthm consp-of-eval-bdd-list
      (equal (consp (eval-bdd-list x y)) (consp x))
      :hints (("Goal" :in-theory (enable eval-bdd-list)))))
  (local (defthm consp-of-to-param-space2-list
      (equal (consp (to-param-space2-list x y)) (consp y))
      :hints (("Goal" :in-theory (enable to-param-space2-list)))))
  (local (defthm len-of-to-param-space2-list
      (equal (len (to-param-space2-list x y)) (len y))
      :hints (("Goal" :in-theory (enable to-param-space2-list)))))
  (local (defthm consp-of-qv-list
      (equal (consp (qv-list x y z)) (posp z))
      :hints (("Goal" :in-theory (enable qv-list)))))
  (local (defun eval-bdd-of-p-under-to-param-space2-list-ind
      (p n env)
      (if (atom p)
        (list n env)
        (list (eval-bdd-of-p-under-to-param-space2-list-ind (car p)
            (+ -1 n)
            (cdr env))
          (eval-bdd-of-p-under-to-param-space2-list-ind (cdr p)
            (+ -1 n)
            (cdr env))))))
  (defthm eval-bdd-of-p-under-to-param-space2-list
    (implies (and (<= (max-depth p) (nfix n)) (ubddp p) p)
      (eval-bdd p
        (eval-bdd-list (to-param-space2-list p (qv-list 0 1 n)) env)))
    :hints (("goal" :induct (eval-bdd-of-p-under-to-param-space2-list-ind p n env)
       :in-theory (disable to-param-space2-list
         eval-bdd-list
         qv-list
         eval-bdd
         qv
         (qv))
       :do-not-induct t
       :expand ((qv-list 0 1 n) (qv 0)
         (find-diff p nil)
         (:free (a b) (to-param-space2-list p (cons a b)))
         (:free (var) (to-param-space2 p var))
         (:free (a b) (eval-bdd-list (cons a b) env))
         (:free (env) (eval-bdd p env))
         (eval-bdd '(t) env)
         (max-depth p))))))

other

(defn qv-param2
  (p n)
  (declare (xargs :guard (natp n)))
  (cond ((atom p) (qv n))
    ((zp n) (cond ((not (car p)) nil)
        ((not (cdr p)) t)
        (t (hons t nil))))
    ((not (car p)) (let ((rest (qv-param2 (cdr p) (1- n))))
        (qcons rest rest)))
    ((not (cdr p)) (let ((rest (qv-param2 (car p) (1- n))))
        (qcons rest rest)))
    (t (qcons (qv-param2 (car p) (1- n))
        (qv-param2 (cdr p) (1- n))))))

other

(memoize 'qv-param2
  :condition '(and (consp p) (car p) (cdr p) (not (eql n 0))))

qv-param2-is-to-param-space2theorem

(defthm qv-param2-is-to-param-space2
  (equal (qv-param2 p n) (to-param-space2 p (qv n)))
  :hints (("Goal" :in-theory (enable to-param-space2 qv))))