\subsection{Generalization clause processor}

\begin{frame}[fragile] 
\frametitle{Generalization clause processor}

\Highlight{Simple-generalize-cp} lets you specify how a clause should be
generalized

{\footnotesize \begin{verbatim}
(include-book "clause-processors/generalize" :dir :system)

(defstub foo (x) x)
(defstub bar (x) x)

(thm (equal (foo x) (bar y))
  :hints(("Goal"
          :clause-processor
          (simple-generalize-cp clause '(((bar y) . z))))))

We now apply the verified :CLAUSE-PROCESSOR function SIMPLE-GENERALIZE-
CP to produce one new subgoal.

Goal'
(EQUAL (FOO X) Z).
\end{verbatim}}
\end{frame}

\begin{frame}[fragile] 
\frametitle{Supporting hint-directed generalization}

Tools for generating fresh variables
\begin{itemize}
\item \Code{(make-n-vars n root m avoid)}
\item \Code{(term-vars x)} and \Code{(term-vars-list x)}
\end{itemize}

\SmallSkip
Examples:
\begin{verbatim}
  ACL2 !>(make-n-vars 3 'foo 0 '(x y z foo0 foo1 foo2))
  (FOO3 FOO4 FOO5)

  ACL2 !>(term-vars '(if x y z))
  (X Y Z)
\end{verbatim}

\end{frame}
