summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 21 Jun 2005 21:41:08 +0200 | |

changeset 16519 | b3235bd87da7 |

parent 16518 | 086c6a97f340 |

child 16520 | 7a9cda53bfa2 |

*** empty log message ***

--- a/doc-src/TutorialI/Misc/document/simp.tex Tue Jun 21 21:38:27 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Jun 21 21:41:08 2005 +0200 @@ -454,34 +454,34 @@ produces the following trace in Proof General's \textsf{Trace} buffer: \begin{ttbox}\makeatother -[0]Applying instance of rewrite rule "List.rev.simps_2": +[1]Applying instance of rewrite rule "List.rev.simps_2": rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] -[0]Rewriting: +[1]Rewriting: rev [a] \(\equiv\) rev [] @ [a] -[0]Applying instance of rewrite rule "List.rev.simps_1": +[1]Applying instance of rewrite rule "List.rev.simps_1": rev [] \(\equiv\) [] -[0]Rewriting: +[1]Rewriting: rev [] \(\equiv\) [] -[0]Applying instance of rewrite rule "List.op @.append_Nil": +[1]Applying instance of rewrite rule "List.op @.append_Nil": [] @ ?y \(\equiv\) ?y -[0]Rewriting: +[1]Rewriting: [] @ [a] \(\equiv\) [a] -[0]Applying instance of rewrite rule +[1]Applying instance of rewrite rule ?x2 # ?t1 = ?t1 \(\equiv\) False -[0]Rewriting: +[1]Rewriting: [a] = [] \(\equiv\) False \end{ttbox} The trace lists each rule being applied, both in its general form and the instance being used. The \texttt{[}$i$\texttt{]} in front (where -above $i$ is always \texttt{0}) indicates that we are inside the $i$th -recursive invocation of the simplifier. Each attempt to apply a +above $i$ is always \texttt{1}) indicates that we are inside the $i$th +invocation of the simplifier. Each attempt to apply a conditional rule shows the rule followed by the trace of the (recursive!) simplification of the conditions, the latter prefixed by \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. @@ -495,6 +495,88 @@ obtained the desired trace.% \end{isamarkuptext}% \isamarkuptrue% +% +\isamarkupsubsection{Finding Theorems% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle's large database of already proved theorems requires +and offers a powerful yet simple search engine. Its only limitation is +its restriction to the theories currently loaded. + +\begin{pgnote} +The search engine is started by clicking on Proof General's \textsf{Find} icon. +You specify your search textually in the input buffer at the bottom +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 +examples: +\begin{ttbox} +length +"_ # _ = _ # _" +"_ + _" +"_ * (_ - (_::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. + +\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. + +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. +\end{warn} + +If you are looking for theorems potentially simplifying some term, you +need to prefix the pattern with \texttt{simp:}. +\begin{ttbox} +simp: "_ * (_ + _)" +\end{ttbox} +This searches all (possibly conditional) equations of the form +\begin{isabelle}% +\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}% +\end{isabelle} +i.e.\ all distributivity rules. +Note that the given pattern needs to be simplified +at the root, not somewhere inside. + +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 +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{-}'': +\begin{ttbox} +-name: HOL +\end{ttbox} +finds theorems whose name does not contain \texttt{HOL}. This is useful for +excluding particular theories from the search because the (long) name of +a theorem contains the name of the theory it comes from. + +Finallly, different search criteria can be combined arbitrarily: +\begin{ttbox} +"_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc +\end{ttbox} +looks for theorems containg a plus but no minus which are not distributivity +rules and whose name contains \texttt{assoc}. + +Further search criteria are explained in \S\ref{sec:Find:ied}.% +\end{isamarkuptext}% +\isamarkuptrue% \isamarkupfalse% \end{isabellebody}% %%% Local Variables: