author paulson Fri, 24 Jun 2005 13:22:08 +0200 changeset 16560 bed540afd4b3 parent 16559 2916415680b9 child 16561 2bc33f0cfe9a
stylistic tweaks concerning Find
 doc-src/TutorialI/Misc/document/simp.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Misc/simp.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Rules/document/find2.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Rules/find2.thy file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 24 04:18:48 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 24 13:22:08 2005 +0200
@@ -502,8 +502,8 @@
%
\begin{isamarkuptext}%
\indexbold{finding theorems}\indexbold{searching theorems}
-Isabelle's large database of already proved theorems requires
-and offers a powerful yet simple search engine. Its only limitation is
+Isabelle's large database of proved theorems
+offers a powerful search engine. Its chief limitation is
its restriction to the theories currently loaded.

\begin{pgnote}
@@ -512,9 +512,10 @@
of the window.
\end{pgnote}

-The simplest form of search is that for theorems containing particular
-patterns: just type in the pattern(s). A pattern can be any term (even
-a single identifier) and may contain \texttt{\_}''. Here are some
+The simplest form of search finds theorems containing specified
+patterns.  A pattern can be any term (even
+a single identifier).  It may contain \texttt{\_}'', a wildcard standing
+for any term. Here are some
examples:
\begin{ttbox}
length
@@ -522,60 +523,57 @@
"_ + _"
"_ * (_ - (_::nat))"
\end{ttbox}
-Note the ability to specify types to narrow searches involving overloaded
-operators.
-
-If you specify more than one pattern, all of them must be present in a
-theorem to match.
+Specifying types, as shown in the last example,

\begin{warn}
Always use \texttt{\_}'' rather than variable names: searching for
\texttt{"x + y"} will usually not find any matching theorems
-because they would need to contain literally \texttt{x} and \texttt{y}.
-This is a feature, not a  bug.
+because they would need to contain \texttt{x} and~\texttt{y} literally.

-When searching for infix operators, do not just type in the symbol:
-\texttt{+} is not a proper term, you  need to say \texttt{"_ + _"}.
-This applies to other, more complicated syntaxes, too.
+When searching for infix operators, do not just type in the symbol,
+such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
+This remark applies to more complicated syntaxes, too.
\end{warn}

-If you are looking for theorems potentially simplifying some term, you
-need to prefix the pattern with \texttt{simp:}.
+If you are looking for rewrite rules (possibly conditional) that could
+simplify some term, prefix the pattern with \texttt{simp:}.
\begin{ttbox}
simp: "_ * (_ + _)"
\end{ttbox}
-This searches \emph{all} (possibly conditional) equations of the form
+This finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
\begin{isabelle}%
\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}%
\end{isabelle}
-not just those with a \isa{simp} attribute.
-Note that the given pattern needs to be simplified
-at the root, not somewhere inside: for example, commutativity of \isa{{\isacharplus}}
-does not match.
+It only finds equations that can simplify the given pattern
+at the root, not somewhere inside: for example, equations of the form
+\isa{{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}\ {\isacharequal}\ {\isasymdots}} do not match.

-You may also search theorems by name. To make this useful you merely
-need to give a substring. For example, you could try and search for all
+You may also search for theorems by name---you merely
+need to specify a substring. For example, you could search for all
commutativity theorems like this:
\begin{ttbox}
name: comm
\end{ttbox}
This retrieves all theorems whose name contains \texttt{comm}.

-Search criteria can also be negated by prefixing them with \texttt{-}'':
+Search criteria can also be negated by prefixing them with \texttt{-}''.
+For example,
\begin{ttbox}
-name: List
\end{ttbox}
-finds theorems whose name does not contain \texttt{List}. This can be useful,
-for example, for
-excluding particular theories from the search because the (long) name of
+finds theorems whose name does not contain \texttt{List}. You can use this
+to exclude particular theories from the search: the long name of
a theorem contains the name of the theory it comes from.

-Finallly, different search criteria can be combined arbitrarily:
+Finallly, different search criteria can be combined arbitrarily.
+The effect is conjuctive: Find returns the theorerms that satisfy all of
+the criteria. For example,
\begin{ttbox}
"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
\end{ttbox}
-looks for theorems containg a plus but no minus which do not simplify
-\mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root and whose name contains \texttt{assoc}.
+looks for theorems containing plus but not minus, and which do not simplify
+\mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root, and whose name contains \texttt{assoc}.

Further search criteria are explained in \S\ref{sec:find2}.

--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jun 24 04:18:48 2005 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jun 24 13:22:08 2005 +0200
@@ -421,8 +421,8 @@
subsection{*Finding Theorems\label{sec:find}*}

text{*\indexbold{finding theorems}\indexbold{searching theorems}
-Isabelle's large database of already proved theorems requires
-and offers a powerful yet simple search engine. Its only limitation is
+Isabelle's large database of proved theorems
+offers a powerful search engine. Its chief limitation is
its restriction to the theories currently loaded.

\begin{pgnote}
@@ -431,9 +431,10 @@
of the window.
\end{pgnote}

-The simplest form of search is that for theorems containing particular
-patterns: just type in the pattern(s). A pattern can be any term (even
-a single identifier) and may contain \texttt{\_}''. Here are some
+The simplest form of search finds theorems containing specified
+patterns.  A pattern can be any term (even
+a single identifier).  It may contain \texttt{\_}'', a wildcard standing
+for any term. Here are some
examples:
\begin{ttbox}
length
@@ -441,58 +442,55 @@
"_ + _"
"_ * (_ - (_::nat))"
\end{ttbox}
-Note the ability to specify types to narrow searches involving overloaded
-operators.
-
-If you specify more than one pattern, all of them must be present in a
-theorem to match.
+Specifying types, as shown in the last example,

\begin{warn}
Always use \texttt{\_}'' rather than variable names: searching for
\texttt{"x + y"} will usually not find any matching theorems
-because they would need to contain literally \texttt{x} and \texttt{y}.
-This is a feature, not a  bug.
+because they would need to contain \texttt{x} and~\texttt{y} literally.

-When searching for infix operators, do not just type in the symbol:
-\texttt{+} is not a proper term, you  need to say \texttt{"_ + _"}.
-This applies to other, more complicated syntaxes, too.
+When searching for infix operators, do not just type in the symbol,
+such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
+This remark applies to more complicated syntaxes, too.
\end{warn}

-If you are looking for theorems potentially simplifying some term, you
-need to prefix the pattern with \texttt{simp:}.
+If you are looking for rewrite rules (possibly conditional) that could
+simplify some term, prefix the pattern with \texttt{simp:}.
\begin{ttbox}
simp: "_ * (_ + _)"
\end{ttbox}
-This searches \emph{all} (possibly conditional) equations of the form
+This finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
@{text[display]"_ * (_ + _) = \<dots>"}
-not just those with a \isa{simp} attribute.
-Note that the given pattern needs to be simplified
-at the root, not somewhere inside: for example, commutativity of @{text"+"}
-does not match.
+It only finds equations that can simplify the given pattern
+at the root, not somewhere inside: for example, equations of the form
+@{text"_ + _ = \<dots>"} do not match.

-You may also search theorems by name. To make this useful you merely
-need to give a substring. For example, you could try and search for all
+You may also search for theorems by name---you merely
+need to specify a substring. For example, you could search for all
commutativity theorems like this:
\begin{ttbox}
name: comm
\end{ttbox}
This retrieves all theorems whose name contains \texttt{comm}.

-Search criteria can also be negated by prefixing them with \texttt{-}'':
+Search criteria can also be negated by prefixing them with \texttt{-}''.
+For example,
\begin{ttbox}
-name: List
\end{ttbox}
-finds theorems whose name does not contain \texttt{List}. This can be useful,
-for example, for
-excluding particular theories from the search because the (long) name of
+finds theorems whose name does not contain \texttt{List}. You can use this
+to exclude particular theories from the search: the long name of
a theorem contains the name of the theory it comes from.

-Finallly, different search criteria can be combined arbitrarily:
+Finallly, different search criteria can be combined arbitrarily.
+The effect is conjuctive: Find returns the theorerms that satisfy all of
+the criteria. For example,
\begin{ttbox}
"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
\end{ttbox}
-looks for theorems containg a plus but no minus which do not simplify
-\mbox{@{text"_ * (_ + _)"}} at the root and whose name contains \texttt{assoc}.
+looks for theorems containing plus but not minus, and which do not simplify
+\mbox{@{text"_ * (_ + _)"}} at the root, and whose name contains \texttt{assoc}.

Further search criteria are explained in \S\ref{sec:find2}.

--- a/doc-src/TutorialI/Rules/document/find2.tex	Fri Jun 24 04:18:48 2005 +0200
+++ b/doc-src/TutorialI/Rules/document/find2.tex	Fri Jun 24 13:22:08 2005 +0200
@@ -6,21 +6,21 @@
%
\begin{isamarkuptxt}%
\index{finding theorems}\index{searching theorems} In
-\S\ref{sec:find} we introduced Proof General's \pgmenu{Find} button
+\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 and search for introduction,
-elimination and destruction rules \emph{w.r.t.\ the current goal}.
+inside a proof, we can be more specific; we can search for introduction,
+elimination and destruction rules \emph{with respect to the current goal}.
\texttt{intro}, \texttt{elim} and \texttt{dest}.

For example, given the goal \begin{isabelle}%
\end{isabelle}
-when you click on \pgmenu{Find} and type in the search expression
-\texttt{intro} you are shown a few rules ending in \isa{{\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q},
-among them \isa{conjI}. This can be very effective for finding
-if the very theorem you are trying to prove is already in the
-database: given the goal%
+you can click on \pgmenu{Find} and type in the search expression
+\texttt{intro}. You will be shown a few rules ending in \isa{{\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\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%
\isamarkupfalse%
@@ -39,7 +39,7 @@
"_ \at\ _"  intro
\end{ttbox}
searches for all introduction rules that match the current goal and
-contain the \isa{{\isacharat}} function.
+mention the \isa{{\isacharat}} function.

Searching for elimination and destruction rules via \texttt{elim} and
\texttt{dest} is analogous to \texttt{intro} but takes the assumptions
--- a/doc-src/TutorialI/Rules/find2.thy	Fri Jun 24 04:18:48 2005 +0200
+++ b/doc-src/TutorialI/Rules/find2.thy	Fri Jun 24 13:22:08 2005 +0200
@@ -4,19 +4,19 @@
(*>*)

txt{*\index{finding theorems}\index{searching theorems} In
-\S\ref{sec:find} we introduced Proof General's \pgmenu{Find} button
+\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 and search for introduction,
-elimination and destruction rules \emph{w.r.t.\ the current goal}.
+inside a proof, we can be more specific; we can search for introduction,
+elimination and destruction rules \emph{with respect to the current goal}.
\texttt{intro}, \texttt{elim} and \texttt{dest}.

For example, given the goal @{subgoals[display,indent=0,margin=65]}
-when you click on \pgmenu{Find} and type in the search expression
-\texttt{intro} you are shown a few rules ending in @{text"\<Longrightarrow> ?P \<and> ?Q"},
-among them @{thm[source]conjI}. This can be very effective for finding
-if the very theorem you are trying to prove is already in the
-database: given the goal *}
+you can click on \pgmenu{Find} and type in the search expression
+\texttt{intro}. You will be shown a few rules ending in @{text"\<Longrightarrow> ?P \<and> ?Q"},
+among them @{thm[source]conjI}\@. You may even discover that
+the very theorem you are trying to prove is already in the
+database.  Given the goal *}
(*<*)
oops
lemma "A \<longrightarrow> A"
@@ -31,7 +31,7 @@
"_ \at\ _"  intro
\end{ttbox}
searches for all introduction rules that match the current goal and
-contain the @{text"@"} function.
+mention the @{text"@"} function.

Searching for elimination and destruction rules via \texttt{elim} and
\texttt{dest} is analogous to \texttt{intro} but takes the assumptions