\subsection{Make-flag}

\begin{frame}[fragile] 
\frametitle{Make-flag}

\Highlight{Make-flag} generates a flag function for a mutual-recursion
\begin{itemize}
\item Non-executable; multiple-values and stobjs are fine
\item Measure inferred from existing definitions
\item Efficient proof of equivalence theorem
\item Adds a macro for proving new theorems about these functions
\end{itemize}
\end{frame}



\begin{frame}[fragile] 
\frametitle{Make-flag example}

\begin{verbatim}
(include-book "tools/flag" :dir :system)

(FLAG::make-flag flag-pseudo-termp
                 pseudo-termp
                 :flag-var flag
                 :flag-mapping ((pseudo-termp . term)
                                (pseudo-term-listp . list))
                 :hints(( {for the measure theorem} ))
                 :defthm-macro-name defthm-pseudo-termp)

(defthm-pseudo-termp type-of-pseudo-termp
  (term (booleanp (pseudo-termp x)))
  (list (booleanp (pseudo-term-listp lst)))
  :hints(("Goal" :induct (flag-pseudo-termp flag x lst))))
\end{verbatim}
\end{frame}
