convert-perm-to-how-many

other

(in-package "ACL2")

include-book

(include-book "perm")

include-book

(include-book "how-many")

perm-counter-examplefunction

(defun perm-counter-example
  (x y)
  (cond ((atom x) (car y))
    ((not (memb (car x) y)) (car x))
    (t (perm-counter-example (cdr x) (rm (car x) y)))))

how-many-rmtheorem

(defthm how-many-rm
  (implies (not (equal a b))
    (equal (how-many a (rm b x)) (how-many a x))))

not-memb-implies-rm-is-no-optheorem

(defthm not-memb-implies-rm-is-no-op
  (implies (and (not (memb a x)) (true-listp x))
    (equal (rm a x) x)))

true-listp-rmtheorem

(defthm true-listp-rm
  (implies (true-listp x) (true-listp (rm a x)))
  :rule-classes :type-prescription)

not-memb-implies-how-many-is-0theorem

(defthm not-memb-implies-how-many-is-0
  (implies (not (memb a x)) (equal (how-many a x) 0)))

how-many-rm-generaltheorem

(defthm how-many-rm-general
  (equal (how-many a (rm b x))
    (if (and (equal a b) (memb a x))
      (1- (how-many a x))
      (how-many a x))))

perm-counter-example-is-counterexample-for-true-liststheorem

(defthm perm-counter-example-is-counterexample-for-true-lists
  (implies (and (true-listp x) (true-listp y))
    (equal (perm x y)
      (equal (how-many (perm-counter-example x y) x)
        (how-many (perm-counter-example x y) y))))
  :rule-classes nil)

tlfixfunction

(defun tlfix
  (x)
  (if (endp x)
    nil
    (cons (car x) (tlfix (cdr x)))))

perm-tlfixtheorem

(defthm perm-tlfix (perm (tlfix x) x))

perm-counter-example-tlfix-1theorem

(defthm perm-counter-example-tlfix-1
  (equal (perm-counter-example (tlfix x) y)
    (perm-counter-example x y)))

rm-tlfixtheorem

(defthm rm-tlfix (equal (rm a (tlfix x)) (tlfix (rm a x))))

memb-tlfixtheorem

(defthm memb-tlfix (equal (memb a (tlfix x)) (memb a x)))

perm-counter-example-tlfix-2theorem

(defthm perm-counter-example-tlfix-2
  (equal (perm-counter-example x (tlfix y))
    (perm-counter-example x y)))

how-many-tlfixtheorem

(defthm how-many-tlfix
  (equal (how-many a (tlfix x)) (how-many a x)))

convert-perm-to-how-manytheorem

(defthm convert-perm-to-how-many
  (equal (perm x y)
    (equal (how-many (perm-counter-example x y) x)
      (how-many (perm-counter-example x y) y)))
  :hints (("Goal" :use ((:instance perm-counter-example-is-counterexample-for-true-lists
        (x (tlfix x))
        (y (tlfix y)))))))

convert-perm-to-how-many

Included Books