1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{find{\isadigit{2}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isadelimproof |
|
19 % |
|
20 \endisadelimproof |
|
21 % |
|
22 \isatagproof |
|
23 % |
|
24 \begin{isamarkuptxt}% |
|
25 \index{finding theorems}\index{searching theorems} In |
|
26 \S\ref{sec:find}, we introduced Proof General's \pgmenu{Find} button |
|
27 for finding theorems in the database via pattern matching. If we are |
|
28 inside a proof, we can be more specific; we can search for introduction, |
|
29 elimination and destruction rules \emph{with respect to the current goal}. |
|
30 For this purpose, \pgmenu{Find} provides three aditional search criteria: |
|
31 \texttt{intro}, \texttt{elim} and \texttt{dest}. |
|
32 |
|
33 For example, given the goal \begin{isabelle}% |
|
34 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B% |
|
35 \end{isabelle} |
|
36 you can click on \pgmenu{Find} and type in the search expression |
|
37 \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}, |
|
38 among them \isa{conjI}\@. You may even discover that |
|
39 the very theorem you are trying to prove is already in the |
|
40 database. Given the goal% |
|
41 \end{isamarkuptxt}% |
|
42 \isamarkuptrue% |
|
43 % |
|
44 \endisatagproof |
|
45 {\isafoldproof}% |
|
46 % |
|
47 \isadelimproof |
|
48 % |
|
49 \endisadelimproof |
|
50 % |
|
51 \isadelimproof |
|
52 % |
|
53 \endisadelimproof |
|
54 % |
|
55 \isatagproof |
|
56 % |
|
57 \begin{isamarkuptxt}% |
|
58 \vspace{-\bigskipamount} |
|
59 \begin{isabelle}% |
|
60 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A% |
|
61 \end{isabelle} |
|
62 the search for \texttt{intro} finds not just \isa{impI} |
|
63 but also \isa{imp{\isaliteral{5F}{\isacharunderscore}}refl}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P}. |
|
64 |
|
65 As before, search criteria can be combined freely: for example, |
|
66 \begin{ttbox} |
|
67 "_ \at\ _" intro |
|
68 \end{ttbox} |
|
69 searches for all introduction rules that match the current goal and |
|
70 mention the \isa{{\isaliteral{40}{\isacharat}}} function. |
|
71 |
|
72 Searching for elimination and destruction rules via \texttt{elim} and |
|
73 \texttt{dest} is analogous to \texttt{intro} but takes the assumptions |
|
74 into account, too.% |
|
75 \end{isamarkuptxt}% |
|
76 \isamarkuptrue% |
|
77 % |
|
78 \endisatagproof |
|
79 {\isafoldproof}% |
|
80 % |
|
81 \isadelimproof |
|
82 % |
|
83 \endisadelimproof |
|
84 % |
|
85 \isadelimtheory |
|
86 % |
|
87 \endisadelimtheory |
|
88 % |
|
89 \isatagtheory |
|
90 % |
|
91 \endisatagtheory |
|
92 {\isafoldtheory}% |
|
93 % |
|
94 \isadelimtheory |
|
95 % |
|
96 \endisadelimtheory |
|
97 \end{isabellebody}% |
|
98 %%% Local Variables: |
|
99 %%% mode: latex |
|
100 %%% TeX-master: "root" |
|
101 %%% End: |
|