added find thms section
authornipkow
Tue Jun 21 21:38:27 2005 +0200 (2005-06-21)
changeset 16518086c6a97f340
parent 16517 4699288139f4
child 16519 b3235bd87da7
added find thms section
doc-src/TutorialI/Misc/simp.thy
     1.1 --- a/doc-src/TutorialI/Misc/simp.thy	Tue Jun 21 18:55:57 2005 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Tue Jun 21 21:38:27 2005 +0200
     1.3 @@ -378,34 +378,34 @@
     1.4  produces the following trace in Proof General's \textsf{Trace} buffer:
     1.5  
     1.6  \begin{ttbox}\makeatother
     1.7 -[0]Applying instance of rewrite rule "List.rev.simps_2":
     1.8 +[1]Applying instance of rewrite rule "List.rev.simps_2":
     1.9  rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
    1.10  
    1.11 -[0]Rewriting:
    1.12 +[1]Rewriting:
    1.13  rev [a] \(\equiv\) rev [] @ [a]
    1.14  
    1.15 -[0]Applying instance of rewrite rule "List.rev.simps_1":
    1.16 +[1]Applying instance of rewrite rule "List.rev.simps_1":
    1.17  rev [] \(\equiv\) []
    1.18  
    1.19 -[0]Rewriting:
    1.20 +[1]Rewriting:
    1.21  rev [] \(\equiv\) []
    1.22  
    1.23 -[0]Applying instance of rewrite rule "List.op @.append_Nil":
    1.24 +[1]Applying instance of rewrite rule "List.op @.append_Nil":
    1.25  [] @ ?y \(\equiv\) ?y
    1.26  
    1.27 -[0]Rewriting:
    1.28 +[1]Rewriting:
    1.29  [] @ [a] \(\equiv\) [a]
    1.30  
    1.31 -[0]Applying instance of rewrite rule
    1.32 +[1]Applying instance of rewrite rule
    1.33  ?x2 # ?t1 = ?t1 \(\equiv\) False
    1.34  
    1.35 -[0]Rewriting:
    1.36 +[1]Rewriting:
    1.37  [a] = [] \(\equiv\) False
    1.38  \end{ttbox}
    1.39  The trace lists each rule being applied, both in its general form and
    1.40  the instance being used. The \texttt{[}$i$\texttt{]} in front (where
    1.41 -above $i$ is always \texttt{0}) indicates that we are inside the $i$th
    1.42 -recursive invocation of the simplifier. Each attempt to apply a
    1.43 +above $i$ is always \texttt{1}) indicates that we are inside the $i$th
    1.44 +invocation of the simplifier. Each attempt to apply a
    1.45  conditional rule shows the rule followed by the trace of the
    1.46  (recursive!) simplification of the conditions, the latter prefixed by
    1.47  \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
    1.48 @@ -418,6 +418,82 @@
    1.49  advisable to reset the \textsf{Trace Simplifier} flag after having
    1.50  obtained the desired trace.  *}
    1.51  
    1.52 +subsection{*Finding Theorems*}
    1.53 +
    1.54 +text{* Isabelle's large database of already proved theorems requires
    1.55 +and offers a powerful yet simple search engine. Its only limitation is
    1.56 +its restriction to the theories currently loaded.
    1.57 +
    1.58 +\begin{pgnote}
    1.59 +The search engine is started by clicking on Proof General's \textsf{Find} icon.
    1.60 +You specify your search textually in the input buffer at the bottom
    1.61 +of the window.
    1.62 +\end{pgnote}
    1.63 +
    1.64 +The simplest form of search is that for theorems containing particular
    1.65 +patterns: just type in the pattern(s). A pattern can be any term (even
    1.66 +a single identifier) and may contain ``\texttt{\_}''. Here are some
    1.67 +examples:
    1.68 +\begin{ttbox}
    1.69 +length
    1.70 +"_ # _ = _ # _"
    1.71 +"_ + _"
    1.72 +"_ * (_ - (_::nat))"
    1.73 +\end{ttbox}
    1.74 +Note the ability to specify types to narrow searches involving overloaded
    1.75 +operators.
    1.76 +
    1.77 +If you specify more than one pattern, all of them must be present in a
    1.78 +theorem to match.
    1.79 +
    1.80 +\begin{warn}
    1.81 +Always use ``\texttt{\_}'' rather than variable names: searching for
    1.82 +\texttt{"x + y"} will usually not find any matching theorems
    1.83 +because they would need to contain literally \texttt{x} and \texttt{y}.
    1.84 +This is a feature, not a  bug.
    1.85 +
    1.86 +When searching for infix operators, do not just type in the symbol:
    1.87 +\texttt{+} is not a proper term, you  need to say \texttt{"_ + _"}.
    1.88 +This applies to other, more complicated syntaxes, too.
    1.89 +\end{warn}
    1.90 +
    1.91 +If you are looking for theorems potentially simplifying some term, you
    1.92 +need to prefix the pattern with \texttt{simp:}.
    1.93 +\begin{ttbox}
    1.94 +simp: "_ * (_ + _)"
    1.95 +\end{ttbox}
    1.96 +This searches all (possibly conditional) equations of the form
    1.97 +@{text[display]"_ * (_ + _) = \<dots>"}
    1.98 +i.e.\ all distributivity rules.
    1.99 +Note that the given pattern needs to be simplified
   1.100 +at the root, not somewhere inside.
   1.101 +
   1.102 +You may also search theorems by name. To make this useful you merely
   1.103 +need to give a substring. For example, you could try and search for all
   1.104 +commutativity theorems like this:
   1.105 +\begin{ttbox}
   1.106 +name: comm
   1.107 +\end{ttbox}
   1.108 +This retrieves all theorems whose name contains \texttt{comm}.
   1.109 +
   1.110 +Search criteria can also be negated by prefixing them with ``\texttt{-}'':
   1.111 +\begin{ttbox}
   1.112 +-name: HOL
   1.113 +\end{ttbox}
   1.114 +finds theorems whose name does not contain \texttt{HOL}. This is useful for
   1.115 +excluding particular theories from the search because the (long) name of
   1.116 +a theorem contains the name of the theory it comes from.
   1.117 +
   1.118 +Finallly, different search criteria can be combined arbitrarily:
   1.119 +\begin{ttbox}
   1.120 +"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
   1.121 +\end{ttbox}
   1.122 +looks for theorems containg a plus but no minus which are not distributivity
   1.123 +rules and whose name contains \texttt{assoc}.
   1.124 +
   1.125 +Further search criteria are explained in \S\ref{sec:find:ied}.
   1.126 +*}
   1.127 +
   1.128  (*<*)
   1.129  end
   1.130  (*>*)