author | nipkow |

Tue Jun 21 21:41:08 2005 +0200 (2005-06-21) | |

changeset 16519 | b3235bd87da7 |

parent 16518 | 086c6a97f340 |

child 16520 | 7a9cda53bfa2 |

*** empty log message ***

1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Tue Jun 21 21:38:27 2005 +0200 1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Tue Jun 21 21:41:08 2005 +0200 1.3 @@ -454,34 +454,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 @@ -495,6 +495,88 @@ 1.49 obtained the desired trace.% 1.50 \end{isamarkuptext}% 1.51 \isamarkuptrue% 1.52 +% 1.53 +\isamarkupsubsection{Finding Theorems% 1.54 +} 1.55 +\isamarkuptrue% 1.56 +% 1.57 +\begin{isamarkuptext}% 1.58 +Isabelle's large database of already proved theorems requires 1.59 +and offers a powerful yet simple search engine. Its only limitation is 1.60 +its restriction to the theories currently loaded. 1.61 + 1.62 +\begin{pgnote} 1.63 +The search engine is started by clicking on Proof General's \textsf{Find} icon. 1.64 +You specify your search textually in the input buffer at the bottom 1.65 +of the window. 1.66 +\end{pgnote} 1.67 + 1.68 +The simplest form of search is that for theorems containing particular 1.69 +patterns: just type in the pattern(s). A pattern can be any term (even 1.70 +a single identifier) and may contain ``\texttt{\_}''. Here are some 1.71 +examples: 1.72 +\begin{ttbox} 1.73 +length 1.74 +"_ # _ = _ # _" 1.75 +"_ + _" 1.76 +"_ * (_ - (_::nat))" 1.77 +\end{ttbox} 1.78 +Note the ability to specify types to narrow searches involving overloaded 1.79 +operators. 1.80 + 1.81 +If you specify more than one pattern, all of them must be present in a 1.82 +theorem to match. 1.83 + 1.84 +\begin{warn} 1.85 +Always use ``\texttt{\_}'' rather than variable names: searching for 1.86 +\texttt{"x + y"} will usually not find any matching theorems 1.87 +because they would need to contain literally \texttt{x} and \texttt{y}. 1.88 +This is a feature, not a bug. 1.89 + 1.90 +When searching for infix operators, do not just type in the symbol: 1.91 +\texttt{+} is not a proper term, you need to say \texttt{"_ + _"}. 1.92 +This applies to other, more complicated syntaxes, too. 1.93 +\end{warn} 1.94 + 1.95 +If you are looking for theorems potentially simplifying some term, you 1.96 +need to prefix the pattern with \texttt{simp:}. 1.97 +\begin{ttbox} 1.98 +simp: "_ * (_ + _)" 1.99 +\end{ttbox} 1.100 +This searches all (possibly conditional) equations of the form 1.101 +\begin{isabelle}% 1.102 +\ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}% 1.103 +\end{isabelle} 1.104 +i.e.\ all distributivity rules. 1.105 +Note that the given pattern needs to be simplified 1.106 +at the root, not somewhere inside. 1.107 + 1.108 +You may also search theorems by name. To make this useful you merely 1.109 +need to give a substring. For example, you could try and search for all 1.110 +commutativity theorems like this: 1.111 +\begin{ttbox} 1.112 +name: comm 1.113 +\end{ttbox} 1.114 +This retrieves all theorems whose name contains \texttt{comm}. 1.115 + 1.116 +Search criteria can also be negated by prefixing them with ``\texttt{-}'': 1.117 +\begin{ttbox} 1.118 +-name: HOL 1.119 +\end{ttbox} 1.120 +finds theorems whose name does not contain \texttt{HOL}. This is useful for 1.121 +excluding particular theories from the search because the (long) name of 1.122 +a theorem contains the name of the theory it comes from. 1.123 + 1.124 +Finallly, different search criteria can be combined arbitrarily: 1.125 +\begin{ttbox} 1.126 +"_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc 1.127 +\end{ttbox} 1.128 +looks for theorems containg a plus but no minus which are not distributivity 1.129 +rules and whose name contains \texttt{assoc}. 1.130 + 1.131 +Further search criteria are explained in \S\ref{sec:Find:ied}.% 1.132 +\end{isamarkuptext}% 1.133 +\isamarkuptrue% 1.134 \isamarkupfalse% 1.135 \end{isabellebody}% 1.136 %%% Local Variables: