how-to-prove-thms

(in-package "ACL2")

(defun dup
  (x)
  (if (consp x)
    (cons (car x) (cons (car x) (dup (cdr x))))
    nil))

(defthm dup-examples
  (and (equal (dup '(1 2 3)) '(1 1 2 2 3 3))
    (equal (dup '(hello)) '(hello hello))
    (equal (dup '(a b c . d)) '(a a b b c c)))
  :rule-classes nil)

(defun app
  (x y)
  (if (consp x)
    (cons (car x) (app (cdr x) y))
    y))

(defthm app-examples
  (and (equal (app '(1 2 3) '(4 5 6)) '(1 2 3 4 5 6))
    (equal (app '(3 2 1) '(0)) '(3 2 1 0))
    (equal (app '(a b c . d) '(e f)) '(a b c e f)))
  :rule-classes nil)

(defun memp
  (e x)
  (if (consp x)
    (if (equal e (car x))
      t
      (memp e (cdr x)))
    nil))

(defthm memp-examples
  (and (memp 1 '(0 1 2 3))
    (not (memp 5 '(0 1 2 3)))
    (not (memp 2 '((0) (1) (2))))
    (memp '(2) '((0) (1) (2)))
    (not (memp 2 '(0 1 . 2))))
  :rule-classes nil)

(defun rev
  (x)
  (if (consp x)
    (app (rev (cdr x)) (cons (car x) nil))
    nil))

(defthm rev-examples
  (and (equal (rev '(1 2 3)) '(3 2 1))
    (equal (rev '(ok)) '(ok))
    (equal (rev '(1 2 3 . end)) '(3 2 1)))
  :rule-classes nil)

(defun rev1
  (x a)
  (if (consp x)
    (rev1 (cdr x) (cons (car x) a))
    a))

(defthm rev1-examples
  (and (equal (rev1 '(1 2 3) nil) '(3 2 1))
    (equal (rev1 '(ok) nil) '(ok))
    (equal (rev1 '(1 2 3 . end) nil) '(3 2 1))
    (equal (rev1 '(a b c) '(1 2 3)) '(c b a 1 2 3)))
  :rule-classes nil)

(defun properp
  (x)
  (if (consp x)
    (properp (cdr x))
    (equal x nil)))

(defthm properp-examples
  (and (properp '(1 2 3))
    (not (properp '(1 2 3 . end)))
    (properp '((a . 1) (b . 2) (c . 3)))
    (properp nil)
    (not (properp 7)))
  :rule-classes nil)

(defun mapnil
  (x)
  (if (consp x)
    (cons nil (mapnil (cdr x)))
    nil))

(defthm mapnil-examples
  (and (equal (mapnil '(1 2 3)) '(nil nil nil))
    (equal (mapnil '(hello)) '(nil)))
  :rule-classes nil)

(defun swaptree
  (x)
  (if (consp x)
    (cons (swaptree (cdr x)) (swaptree (car x)))
    x))

(defthm swaptree-examples
  (and (equal (swaptree '((a . b) c . d)) '((d . c) b . a))
    (equal (swaptree '(a b c d)) '((((nil . d) . c) . b) . a)))
  :rule-classes nil)

(defun ziplists
  (x y)
  (if (consp x)
    (cons (cons (car x) (car y)) (ziplists (cdr x) (cdr y)))
    nil))

(defthm ziplists-examples
  (and (equal (ziplists '(a b c) '(1 2 3 4))
      '((a . 1) (b . 2) (c . 3)))
    (equal (ziplists '(a b c) '(1 2)) '((a . 1) (b . 2) (c))))
  :rule-classes nil)

(defun lookup
  (x a)
  (if (consp a)
    (if (equal x (car (car a)))
      (cdr (car a))
      (lookup x (cdr a)))
    nil))

(defthm lookup-examples
  (and (equal (lookup 'b '((a . 1) (b . 2) (c . 3) (a . 4))) 2)
    (equal (lookup 'a '((a . 1) (b . 2) (c . 3) (a . 4))) 1)
    (equal (lookup 'x '((a . 1) (b . 2) (c . 3) (a . 4))) nil)
    (equal (lookup 'j '((i . 1) (j) (k . 123))) nil))
  :rule-classes nil)

(defun foundp
  (x a)
  (if (consp a)
    (if (equal x (car (car a)))
      t
      (foundp x (cdr a)))
    nil))

(defthm foundp-examples
  (and (equal (foundp 'b '((a . 1) (b . 2) (c . 3) (a . 4))) t)
    (equal (foundp 'a '((a . 1) (b . 2) (c . 3) (a . 4))) t)
    (equal (foundp 'x '((a . 1) (b . 2) (c . 3) (a . 4))) nil)
    (equal (foundp 'j '((i . 1) (j) (k . 123))) t))
  :rule-classes nil)

(defun subp
  (x y)
  (if (consp x)
    (if (memp (car x) y)
      (subp (cdr x) y)
      nil)
    t))

(defthm subp-examples
  (and (subp '(a b b a) '(a b))
    (subp '(a b c) '(e d c b a))
    (not (subp '(a b) '(a c a d a f))))
  :rule-classes nil)

(defun int
  (x y)
  (if (consp x)
    (if (memp (car x) y)
      (cons (car x) (int (cdr x) y))
      (int (cdr x) y))
    nil))

(defthm int-examples
  (and (equal (int '(a b c) '(a b a d)) '(a b))
    (equal (int '(a b c) '(x y z)) nil)
    (equal (int '(a a b b) '(a b c)) '(a a b b)))
  :rule-classes nil)

(defun mem
  (e x)
  (if (consp x)
    (if (equal e (car x))
      x
      (mem e (cdr x)))
    nil))

(defun lonesomep
  (e lst)
  (if (mem e lst)
    (not (mem e (cdr (mem e lst))))
    nil))

(defun collect-lonesomep
  (a b)
  (if (consp a)
    (if (lonesomep (car a) b)
      (cons (car a) (collect-lonesomep (cdr a) b))
      (collect-lonesomep (cdr a) b))
    nil))

(defun leaves
  (x)
  (if (consp x)
    (app (leaves (car x)) (leaves (cdr x)))
    (cons x nil)))

(defun lonesomes
  (x)
  (collect-lonesomep (leaves x) (leaves x)))

(defthm lonesomes-examples
  (and (equal (lonesomes '((a . b) c . a)) '(b c))
    (equal (lonesomes '((a . a) . a)) nil)
    (equal (lonesomes '(((a . b) b . c) (x . y) c . x)) '(a y)))
  :rule-classes nil)

(defun treecopy
  (x)
  (if (consp x)
    (cons (treecopy (car x)) (treecopy (cdr x)))
    x))

(defthm treecopy-is-id (equal (treecopy x) x))

(defthm associativity-of-app
  (equal (app (app a b) c) (app a (app b c))))

(defthm dup-app
  (equal (dup (app a b)) (app (dup a) (dup b))))

(defthm dup-mapnil
  (equal (dup (mapnil a)) (mapnil (dup a))))

(defthm properp-app-nil (properp (app a nil)))

(defthm swaptree-swaptree (equal (swaptree (swaptree x)) x))

(defthm memp-app
  (equal (memp e (app a b)) (or (memp e a) (memp e b))))

(defthm problem-6-1
  (equal (memp e (app a a)) (memp e a))
  :rule-classes nil)

(defthm properp-app (equal (properp (app a b)) (properp b)))

(defthm properp-rev (properp (rev x)))

(defthm app-right-identity
  (implies (properp x) (equal (app x nil) x)))

(defthm rev-app
  (equal (rev (app a b)) (app (rev b) (rev a))))

(defthm rev-rev
  (implies (properp z) (equal (rev (rev z)) z)))

(defthm triple-rev (equal (rev (rev (rev a))) (rev a)))

(defthm memp-rev (equal (memp e (rev x)) (memp e x)))

(defthm memp-dup (equal (memp e (dup x)) (memp e x)))

(defthm complicated-memp-theorem
  (implies (memp e c) (memp e (rev (dup (dup c)))))
  :rule-classes nil)

(defun leaves
  (x)
  (if (consp x)
    (app (leaves (car x)) (leaves (cdr x)))
    (cons x nil)))

(defthm leaves-swaptree
  (equal (leaves (swaptree x)) (rev (leaves x))))

(defthm subp-cdr (implies (subp x (cdr y)) (subp x y)))

(defthm subp-reflexive (subp x x))

(defthm subp-int
  (implies (and (properp x) (subp x y)) (equal (int x y) x)))

(defthm int-x-x (implies (properp x) (equal (int x x) x)))

(defthm memp-subp
  (implies (and (subp y z) (memp e y)) (memp e z)))

(defthm subp-transitive
  (implies (and (subp x y) (subp y z)) (subp x z)))

(defthm subp-app-1
  (equal (subp (app a b) c) (and (subp a c) (subp b c))))

(defthm subp-app-a-a (subp (app a a) a))

(defun seteqp (x y) (and (subp x y) (subp y x)))

(defthm subp-app-2 (implies (subp a b) (subp a (app b c))))

(defthm seteq-rev (seteqp (rev a) a))

(defthm subp-app-3 (implies (subp a c) (subp a (app b c))))

(defthm app-commutative (seteqp (app a b) (app b a)))

(defun list-of-atomsp
  (x)
  (if (consp x)
    (and (not (consp (car x))) (list-of-atomsp (cdr x)))
    t))

(defthm list-of-atomsp-app
  (equal (list-of-atomsp (app a b))
    (and (list-of-atomsp a) (list-of-atomsp b))))

(defthm list-of-atomsp-leaves (list-of-atomsp (leaves x)))

(defthm leaves-of-list-of-atoms
  (implies (and (properp x) (list-of-atomsp x))
    (equal (leaves x) (app x '(nil)))))

(defthm properp-leaves (properp (leaves x)))

(defthm leaves-leaves
  (equal (leaves (leaves x)) (app (leaves x) '(nil))))

(defthm lemma8-10a
  (implies (not (mem e leaves))
    (not (memp e (collect-lonesomep lst leaves)))))

(defthm lemma8-10b
  (implies (mem e (cdr (mem e leaves)))
    (not (memp e (collect-lonesomep lst leaves)))))

(defthm memp-collect-lonesomep
  (iff (memp e (collect-lonesomep lst leaves))
    (and (memp e lst) (lonesomep e leaves))))

(defthm memp-lonesomes
  (iff (memp e (lonesomes x))
    (and (memp e (leaves x)) (lonesomep e (leaves x)))))

(defun nump
  (x)
  (if (consp x)
    (and (equal (car x) nil) (nump (cdr x)))
    (equal x nil)))

(defun add
  (x y)
  (if (consp x)
    (cons nil (add (cdr x) y))
    (mapnil y)))

(defun mult
  (x y)
  (if (consp x)
    (add y (mult (cdr x) y))
    nil))

(defun raise
  (x y)
  (if (consp y)
    (mult x (raise x (cdr y)))
    '(nil)))

(defthm nump-mapnil (nump (mapnil x)))

(defthm nump-add (nump (add x y)))

(defthm nump-mult (nump (mult x y)))

(defthm nump-raise (nump (raise x y)))

(defthm add-identity
  (implies (nump x) (equal (add x nil) x)))

(defthm raise-mapnil
  (equal (raise i (mapnil j)) (raise i j)))

(defthm mult-mapnil-1
  (equal (mult (mapnil i) j) (mult i j)))

(defthm mapnil-nump (implies (nump x) (equal (mapnil x) x)))

(defthm add-mapnil-1 (equal (add (mapnil i) j) (add i j)))

(defthm add-associativity
  (equal (add (add a b) c) (add a (add b c))))

(defthm mult-add-distributivity-2
  (equal (mult (add i j) k) (add (mult i k) (mult j k))))

(defthm mult-associative
  (equal (mult (mult a b) c) (mult a (mult b c))))

(defthm raise-add
  (equal (raise b (add i j)) (mult (raise b i) (raise b j))))

(defthm add-identity-2
  (implies (not (consp j)) (equal (add i j) (mapnil i))))

(defthm add-cons
  (equal (add i (cons x j)) (cons nil (add i j))))

(defthm add-commutativity (equal (add i j) (add j i)))

(defthm add-mapnil-2 (equal (add i (mapnil j)) (add i j)))

(defthm add-commutativity2
  (equal (add i (add j k)) (add j (add i k))))

(defthm mult-zero
  (implies (not (consp j)) (equal (mult i j) nil)))

(defthm mult-cons
  (equal (mult i (cons x j)) (add i (mult i j))))

(defthm mult-commutativity (equal (mult i j) (mult j i)))

(defthm mult-mapnil-2
  (equal (mult i (mapnil j)) (mult i j)))

(defthm mult-add-distributivity-1
  (equal (mult k (add i j)) (add (mult k i) (mult k j))))

(defthm mult-commutativity2
  (equal (mult i (mult j k)) (mult j (mult i k))))

(defthm rev1-is-app-rev (equal (rev1 x a) (app (rev x) a)))

(defthm rev1-nil-is-rev (equal (rev1 x nil) (rev x)))

(defun fact
  (n)
  (if (consp n)
    (mult n (fact (cdr n)))
    '(nil)))

(defun fact1
  (n a)
  (if (consp n)
    (fact1 (cdr n) (mult n a))
    a))

(defthm fact1-is-fact-generalized
  (implies (nump a) (equal (fact1 n a) (mult (fact n) a))))

(defthm nump-fact (nump (fact n)))

(defthm fact1-is-fact (equal (fact1 n '(nil)) (fact n)))

(defun mc-flatten
  (x a)
  (if (consp x)
    (mc-flatten (car x) (mc-flatten (cdr x) a))
    (cons x a)))

(defthm mc-flatten-is-leaves-generalized
  (equal (mc-flatten x a) (app (leaves x) a)))

(defthm properp-leaves (properp (leaves x)))

(defthm mc-flatten-is-leaves
  (equal (mc-flatten x nil) (leaves x)))