(*<*)
theory find2
imports Main
begin
lemma "A \ B"
(*>*)
txt‹\index{finding
theorems}
\index{searching
theorems}
In
\S\ref{sec:find}, we introduced
Proof General
's \pgmenu{Find} button
for finding
theorems in the database via pattern matching.
If we are
inside a
proof, we can be more specific; we can search
for introduction,
elimination
and destruction rules
\emph{
with respect
to the current goal}.
For this purpose,
\pgmenu{Find} provides three aditional search criteria:
\texttt{intro},
\texttt{elim}
and \texttt{dest}.
For example, given the goal @{subgoals[display,indent=0,margin=65]}
you can click on
\pgmenu{Find}
and type
in the search expression
\texttt{intro}. You will be shown a few rules ending
in ‹==> ?P
∧ ?Q
›,
among them @{
thm[source]conjI}
\@. You may even discover that
the very
theorem you are trying
to prove
is already
in the
database. Given the goal
›
(*<*)
oops
lemma "A \ A"
(*>*)
txt‹\vspace{-
\bigskipamount}
@{subgoals[display,indent=0,margin=65]}
the search
for \texttt{intro} finds not just @{
thm[source] impI}
but
also @{
thm[source] imp_refl}: @{
thm imp_refl}.
As before, search criteria can be combined freely:
for example,
\begin{ttbox}
"_ \at\ _" intro
\end{ttbox}
searches
for all introduction rules that match the current goal
and
mention the
‹@
› function.
Searching
for elimination
and destruction rules via
\texttt{elim}
and
\texttt{dest}
is analogous
to \texttt{intro} but takes the assumptions
into account, too.
›
(*<*)
oops
end
(*>*)
