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

give each time slice its own lambda translation

%
\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: