16549
|
1 |
(*<*)
|
|
2 |
theory find2 imports Main begin
|
|
3 |
lemma "A \<and> B"
|
|
4 |
(*>*)
|
|
5 |
|
|
6 |
txt{*\index{finding theorems}\index{searching theorems} In
|
16560
|
7 |
\S\ref{sec:find}, we introduced Proof General's \pgmenu{Find} button
|
16549
|
8 |
for finding theorems in the database via pattern matching. If we are
|
16560
|
9 |
inside a proof, we can be more specific; we can search for introduction,
|
|
10 |
elimination and destruction rules \emph{with respect to the current goal}.
|
|
11 |
For this purpose, \pgmenu{Find} provides three aditional search criteria:
|
16549
|
12 |
\texttt{intro}, \texttt{elim} and \texttt{dest}.
|
|
13 |
|
|
14 |
For example, given the goal @{subgoals[display,indent=0,margin=65]}
|
16560
|
15 |
you can click on \pgmenu{Find} and type in the search expression
|
|
16 |
\texttt{intro}. You will be shown a few rules ending in @{text"\<Longrightarrow> ?P \<and> ?Q"},
|
|
17 |
among them @{thm[source]conjI}\@. You may even discover that
|
|
18 |
the very theorem you are trying to prove is already in the
|
|
19 |
database. Given the goal *}
|
16549
|
20 |
(*<*)
|
|
21 |
oops
|
|
22 |
lemma "A \<longrightarrow> A"
|
|
23 |
(*>*)
|
|
24 |
txt{*\vspace{-\bigskipamount}
|
|
25 |
@{subgoals[display,indent=0,margin=65]}
|
|
26 |
the search for \texttt{intro} finds not just @{thm[source] impI}
|
|
27 |
but also @{thm[source] imp_refl}: @{thm imp_refl}.
|
|
28 |
|
|
29 |
As before, search criteria can be combined freely: for example,
|
|
30 |
\begin{ttbox}
|
|
31 |
"_ \at\ _" intro
|
|
32 |
\end{ttbox}
|
|
33 |
searches for all introduction rules that match the current goal and
|
16560
|
34 |
mention the @{text"@"} function.
|
16549
|
35 |
|
|
36 |
Searching for elimination and destruction rules via \texttt{elim} and
|
|
37 |
\texttt{dest} is analogous to \texttt{intro} but takes the assumptions
|
|
38 |
into account, too.
|
|
39 |
*}
|
|
40 |
(*<*)
|
|
41 |
oops
|
|
42 |
end
|
|
43 |
(*>*)
|