# HG changeset patch # User paulson # Date 1119612128 -7200 # Node ID bed540afd4b314c94763093f380dd33b6e2ea38c # Parent 2916415680b9208047a9c7c2e8dd87b7645cd589 stylistic tweaks concerning Find diff -r 2916415680b9 -r bed540afd4b3 doc-src/TutorialI/Misc/document/simp.tex --- 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}. diff -r 2916415680b9 -r bed540afd4b3 doc-src/TutorialI/Misc/simp.thy --- 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]"_ * (_ + _) = \"} -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"_ + _ = \"} 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}. diff -r 2916415680b9 -r bed540afd4b3 doc-src/TutorialI/Rules/document/find2.tex --- 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 diff -r 2916415680b9 -r bed540afd4b3 doc-src/TutorialI/Rules/find2.thy --- 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"\ ?P \ ?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"\ ?P \ ?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 \ 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