doc-src/TutorialI/document/find2.tex

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/document/find2.tex	Thu Jul 26 19:59:06 2012 +0200
@@ -0,0 +1,101 @@
+%
+\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}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\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{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\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}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A%
+\end{isabelle}
+the search for \texttt{intro} finds not just \isa{impI}
+but also \isa{imp{\isaliteral{5F}{\isacharunderscore}}refl}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\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{{\isaliteral{40}{\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: