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