--- 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,
+constrains searches involving overloaded operators.
\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,
+constrains searches involving overloaded operators.
\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}.
-For this purpose \pgmenu{Find} provides 3 aditional search criteria:
+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}}{\isachardot}\ A\ {\isasymand}\ B%
\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}.
-For this purpose \pgmenu{Find} provides 3 aditional search criteria:
+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 @{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