doc-src/TutorialI/Rules/document/find2.tex

added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

%
\begin{isabellebody}%
\def\isabellecontext{find{\isadigit{2}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
\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 \begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ B%
\end{isabelle}
you can click on \pgmenu{Find} and type in the search expression
\texttt{intro}. You will be shown a few rules ending in \isa{{\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q},
among them \isa{conjI}\@. You may even discover that
the very theorem you are trying to prove is already in the
database.  Given the goal%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
\vspace{-\bigskipamount}
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ A\ {\isasymlongrightarrow}\ A%
\end{isabelle}
the search for \texttt{intro} finds not just \isa{impI}
but also \isa{imp{\isacharunderscore}refl}: \isa{{\isacharquery}P\ {\isasymlongrightarrow}\ {\isacharquery}P}.

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 \isa{{\isacharat}} 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.%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: