; Solutions to the Exercises
;            in

; How To Prove Theorems Formally
; Matt Kaufmann   J Strother Moore
; AMD             UT Austin

; This file contains our solutions to the exercises in the paper
; above.  Remember, your solutions may be different but just as
; nice -- or nicer!

; This is a certified book.  Assuming the connected book directory
; (see set-cbd) is set to the directory containing this file, to
; recertify it, execute

; (certify-book "how-to-prove-thms")

; To include this book in a new session, execute

; (include-book "how-to-prove-thms")

; (or use the full pathname to this file from wherever directory
; you are on).

; However, we don't think this is a useful certified book and we certify
; it just to reassure ourselves that every event in it succeeds.  The
; real value of this book is to read it or to read the output produced
; by recertifying it.

; Another way to use the book is to load it into ACL2 and then use
; :ubt to undo back through some event in it so you can play with
; alternative scripts for some problem.

; (ld "how-to-prove-thms.lisp" :ld-pre-eval-print t)

; The output shown here is that for ACL2 Version 2.8.  It may well be
; different from the output of newer ACL2 releases.  But we expect
; the reported behavior to be very very similar.

; ---------------------------------------------------------------------------

(in-package "ACL2")

; ---------------------------------------------------------------------------
; Section 4 - Programming in ACL2

; The definitions of and, or, not, implies, and iff are part of the
; ACL2 system.  You can print them with :pe, e.g.,
; ACL2 !>:pe implies
;  V    -4864  (DEFUN IMPLIES (P Q)
;                     (DECLARE (XARGS :MODE :LOGIC :GUARD T))
;                     (IF P (IF Q T NIL) T))
; You will note that AND and OR are macros.

; Here are the other functions defined in the section:

(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)

; Solutions to the Exercises in Section 4:

; Problem 4.1:
(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)

; Problem 4.2
(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)

; Problem 4.3
(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)

; Problem 4.4
(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 . nil))))
  :rule-classes nil)

; Problem 4.5
(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 . nil) (k . 123))) nil)) 
  :rule-classes nil)

; Problem 4.6
(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 . nil) (k . 123))) t))
  :rule-classes nil)

; Problem 4.7
(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)

; Problem 4.8
(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)

; Problem 4.9
; We define (loneseomep e lst) to determine whether e occurs exactly
; once in lst.  We do it without arithmetic, since we haven't
; introduced arithmetic yet.  The idea is to determine if e is a
; member of lst and not a member of the sublist that starts after that
; occurrence of e.  To make this definition we need:

(defun mem (e x) ; where does e occur in 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)
; collect elements of a that are lonesome in 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) ; the leaves of 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)

; ---------------------------------------------------------------------------
; Section 5 - Elementary Proofs in the ACL2 Logic

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

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

; Solutions to Exercises in Section 5

; Problem 5.1
(defthm associativity-of-app
  (equal (app (app a b) c) (app a (app b c))))

; Problem 5.2
(defthm dup-app
  (equal (dup (app a b)) (app (dup a) (dup b))))

; Problem 5.3
(defthm dup-mapnil
  (equal (dup (mapnil a))
         (mapnil (dup a))))

; Problem 5.4
(defthm properp-app-nil
  (properp (app a nil)))

; Problem 5.5
(defthm swaptree-swaptree
  (equal (swaptree (swaptree x)) x))

; Problem 5.6
(defthm memp-app
  (equal (memp e (app a b))
         (or (memp e a) (memp e b))))

; ---------------------------------------------------------------------------
; Section 6 - Three Basic Proof Techniques

; Solution to the Exercises in Section 6

; The single exercise in this section was not numbered because it is
; not really solvable.  But here is our discussion of the problem.
; Pretend the problem was named 6.1.

; If you undo or disable memp-app above and try to prove the theorem
; of Problem 6.1 you get the failed proof, partially reproduced, below:

#|
(defthm problem-6-1
  (equal (memp e (app a a)) (memp e a)))

Name the formula above *1.

Perhaps we can prove *1 by induction.  Two induction schemes are suggested
by this conjecture.  Subsumption reduces that number to one.  

We will induct according to a scheme suggested by (MEMP E A).  This
suggestion was produced using the :induction rules APP and MEMP.  If
we let  (:P A E) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP A)) (:P A E))
     (IMPLIES (AND (CONSP A)
                   (NOT (EQUAL E (CAR A)))
                   (:P (CDR A) E))
              (:P A E))
     (IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
              (:P A E))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P).  When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.

Subgoal *1/3
(IMPLIES (NOT (CONSP A))
         (EQUAL (MEMP E (APP A A)) (MEMP E A))).

But simplification reduces this to T, using the :definitions APP and
MEMP and the :executable-counterpart of EQUAL.

Subgoal *1/2
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (EQUAL (MEMP E (APP (CDR A) (CDR A)))
                     (MEMP E (CDR A))))
         (EQUAL (MEMP E (APP A A)) (MEMP E A))).

This simplifies, using the :definitions APP and MEMP, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to

Subgoal *1/2'
(IMPLIES (AND (CONSP A)
              (NOT (EQUAL E (CAR A)))
              (EQUAL (MEMP E (APP (CDR A) (CDR A)))
                     (MEMP E (CDR A))))
         (EQUAL (MEMP E (APP (CDR A) A))
                (MEMP E (CDR A)))).

The destructor terms (CAR A) and (CDR A) can be eliminated by using
CAR-CDR-ELIM to replace A by (CONS A1 A2), (CAR A) by A1 and (CDR A)
by A2.  This produces the following goal.

... <much omitted> ...

Subgoal *1.1.1/1'''
(IMPLIES (AND (NOT (EQUAL (MEMP E (APP A6 (CONS A1 A6)))
                          (MEMP E (APP A6 A6))))
              (EQUAL (MEMP E (APP A6 (LIST* A1 A5 A6)))
                     (MEMP E (APP A6 (CONS A5 A6))))
              (NOT (EQUAL E A1))
              (NOT (EQUAL E A3))
              (NOT (EQUAL E A5)))
         (EQUAL (MEMP E (APP A6 (LIST* A1 A3 A5 A6)))
                (MEMP E (APP A6 (LIST* A3 A5 A6))))).

Name the formula above *1.1.1.2.


This formula is subsumed by one of its parents, *1.1, which we're in
the process of trying to prove by induction.  When an inductive proof
gives rise to a subgoal that is less general than the original goal
it is a sign that either an inappropriate induction was chosen or that
the original goal is insufficiently general.  In any case, our proof
attempt has failed.

Summary
Form:  ( DEFTHM PROBLEM-6-1 ...)
Rules: ((:DEFINITION APP)
        (:DEFINITION MEMP)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION APP)
        (:INDUCTION MEMP)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.14 seconds (prove: 0.09, print: 0.05, other: 0.00)

******** FAILED ********  See :DOC failure  ******** FAILED ********
|#

; Note the checkpoint formula, Subgoal *1/2', above.  See how we have
; (APP (CDR A) (CDR A)) in the hypothesis and (APP (CDR A) A) in the
; conclusion?  That's a strong suggestion that the theorem is not strong
; enough.

; If we proved the more general memp-app, the proof of Problem 6.1 is
; trivial:

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

; ---------------------------------------------------------------------------
; Section 7 - ACL2's Proof Strategy

; Problem 7.1
; We have already run the theorem prover on Problems 5.1 - 5.6 above.

; Section 8 - Decomposition into Lemmas - The Method

; Below we reproduce the script shown in the paper for triple-rev and
; then show the final scripts produced by The Method for the problems
; in this section.  You should realize however that there are always
; alternatives to any particular lemma decomposition.  So take our
; solutions merely as examples of working solutions.

; --- Script for proving triple-rev ---
(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)))
; --- The End ---

; ---------------------------------------------------------------------------
; Solutions to the Exercises of Section 8

; Problem 8.1

; --- Script for proving complicated-memp-theorem ---

; These two lemmas are just obvious and are developed
; as the initial plan for the proof. 

(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)
; --- The End ---

; Problem 8.2
; --- Script for proving leaves-swaptree --- 

; If you haven't, define the leaves of a binary tree as

(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))))

; Note that the proof depends on rev-app, proved earlier.
; --- The End ---

; Problem 8.3
; --- Script for proving subp-x-x --- 

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

(defthm subp-reflexive
  (subp x x))
; --- The End ---

; Problem 8.4
; --- Script for proving int-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)))

; --- The End ---

; Problem 8.5
; --- Script for proving subp-transitive

; Subp-transitive is actually proved without help right now,
; using subp-cdr and three inductions.  But using the method
; we discover a generally useful lemma.

; The first checkpoint in the (successful) proof of subp-transitive
; here is:
; Subgoal *1/3'
; (IMPLIES (AND (CONSP X)
;               (NOT (MEMP (CAR X) Z))
;               (MEMP (CAR X) Y)
;               (SUBP (CDR X) Y))
;          (NOT (SUBP Y Z)))

; Swap the conclusion and the second hyp (unnegating both) to get
; the equivalent:

; (implies (and (consp x)
;               (subp y z)
;               (memp (car x) y)
;               (subp (cdr x) y))
;          (memp (car x) z))

; Observe the key lemma here is:

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

; The lemma above contains a free variable, y.  That is, to apply this
; theorem to rewrite (memp alpha beta), the theorem prover must find a
; term, say gamma, such that it can prove (subp gamma beta) and (memp
; alpha gamma).  It is not very good at guessing instantiations of
; free variables.  See :doc free-variables.

(defthm subp-transitive
  (implies (and (subp x y)
                (subp y z))
           (subp x z)))
; --- The End ---

; Problem 8.6
; --- Script for proving subp-app-a-a

(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))

; --- The End ---

; Problem 8.7
; --- Script for proving seteqp-rev

(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))

; --- The End ---

; Problem 8.8
; --- Script for proving app-commutative

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

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

; --- The End ---

; Problem 8.9

; This problem illustrates the utility of introducing a new concept,
; namely, that of a list of atoms.  The basic idea is that if you take
; the leaves of a list of atoms, you get the same list back with an
; extra NIL at the end.  Then you just observe that (leaves x) is a
; list of atoms.  The thing about (leaves (leaves x)) that is
; suggestive of a problem is that leaves "wants" to explore the car
; and cdr of its argument, but produces a linear list.  So an
; induction to unwind the inner leaves is feeding the outer leaves
; something it cannot very well recur on.  You could probably find
; lemmas to tear it apart, through the apps produced by the inner
; leaves, but this decomposition is much nicer.

; --- Script for proving leaves-leaves

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

; Note: We could have required the terminator to be nil.  But had we
; done that, the following beautiful theorem would not hold.  We'll
; just add a properp hypothesis when we need it.

(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))))
; --- The End ---

; Problem 8.10
; --- Script for proving memp-lonesomes

(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)))
  )

; Note: Actually, we would not use the lemma decomposition shown above
; because we don't like the lemmas.  But they do achieve a "simplify,
; induct, simplify" proof.  The reason they're needed is that when the
; theorem prover tries to prove memp-collect-lonesomep it invents an
; inductive argument that is a mixture of collect-lonesomep and memp.
; Its invention in this case is unfortunate and leads to an
; excessively complicated proof.  By telling it to do the induction
; suggested by collect-lonesomep alone, the proof is immediate.

; So in our first use of The Method here we looked at the induction
; argument generated, didn't like it, and added the following hint
; argument to the defthm for memp-collect-lonesomep:

;       :hints (("Goal" :induct (collect-lonesomep lst leaves)))

; And it went through simply.  However, since the student hasn't been
; told how to use hints, we decided this solution was not fair and
; followed The Method using only the techniques available to the reader.

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

; --- The End ---

; Problem 8.11

; Do not be put off by the number of lemmas.  Just look how beautiful
; they are!  You are developing the first few lemmas of a treastise on
; Peano arithmetic.

; --- Script for proving raise-add ---

(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))))

; --- The End ---

; One of the primary motivations of the remaining problems is just to
; set up enough basic simulated arithmetic to make the factorial
; proof go through.

; Problem 8.12
; --- Script for proving add-commutativity ---
(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)))

; --- The End ---

; Problem 8.13
; --- Script for proving add-commutativity-2 ---

(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))))

; --- The End ---

; Problem 8.14
; --- Script for proving mult-commutativity ---

(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)))

; --- The End ---

; Problem 8.15
; --- Script for proving mult-commutativity-2 ---

(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))))

; --- The End ---


; ---------------------------------------------------------------------------
; Section 9 - Accumulators

; --- Script for proving rev1-nil-is-rev ---

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

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

; --- The End ---

; Solutions to the Exercises in Section 9

; Problem 9.1
; --- Script for proving fact1-is-fact ---

(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)))
; --- The End ---

; Problem 9.2
; --- Script for proving mc-flatten ---

(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)))

; --- The End ---