439 \isamarkuptrue% |
439 \isamarkuptrue% |
440 % |
440 % |
441 \begin{isamarkuptext}% |
441 \begin{isamarkuptext}% |
442 \indexbold{tracing the simplifier} |
442 \indexbold{tracing the simplifier} |
443 Using the simplifier effectively may take a bit of experimentation. Set the |
443 Using the simplifier effectively may take a bit of experimentation. Set the |
444 Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:% |
444 Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:% |
445 \end{isamarkuptext}% |
445 \end{isamarkuptext}% |
446 \isamarkuptrue% |
446 \isamarkuptrue% |
447 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
447 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
448 \isamarkupfalse% |
448 \isamarkupfalse% |
449 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
449 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% |
450 \isamarkupfalse% |
450 \isamarkupfalse% |
451 % |
451 % |
452 \begin{isamarkuptext}% |
452 \begin{isamarkuptext}% |
453 \noindent |
453 \noindent |
454 produces the following trace in Proof General's \textsf{Trace} buffer: |
454 produces the following trace in Proof General's \pgmenu{Trace} buffer: |
455 |
455 |
456 \begin{ttbox}\makeatother |
456 \begin{ttbox}\makeatother |
457 [1]Applying instance of rewrite rule "List.rev.simps_2": |
457 [1]Applying instance of rewrite rule "List.rev.simps_2": |
458 rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] |
458 rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1] |
459 |
459 |
489 proofs of arithmetic formulae. |
489 proofs of arithmetic formulae. |
490 |
490 |
491 Many other hints about the simplifier's actions may appear. |
491 Many other hints about the simplifier's actions may appear. |
492 |
492 |
493 In more complicated cases, the trace can be very lengthy. Thus it is |
493 In more complicated cases, the trace can be very lengthy. Thus it is |
494 advisable to reset the \textsf{Trace Simplifier} flag after having |
494 advisable to reset the \pgmenu{Trace Simplifier} flag after having |
495 obtained the desired trace.% |
495 obtained the desired trace.% |
496 \end{isamarkuptext}% |
496 \end{isamarkuptext}% |
497 \isamarkuptrue% |
497 \isamarkuptrue% |
498 % |
498 % |
499 \isamarkupsubsection{Finding Theorems% |
499 \isamarkupsubsection{Finding Theorems% |
500 } |
500 } |
501 \isamarkuptrue% |
501 \isamarkuptrue% |
502 % |
502 % |
503 \begin{isamarkuptext}% |
503 \begin{isamarkuptext}% |
|
504 \indexbold{finding theorems}\indexbold{searching theorems} |
504 Isabelle's large database of already proved theorems requires |
505 Isabelle's large database of already proved theorems requires |
505 and offers a powerful yet simple search engine. Its only limitation is |
506 and offers a powerful yet simple search engine. Its only limitation is |
506 its restriction to the theories currently loaded. |
507 its restriction to the theories currently loaded. |
507 |
508 |
508 \begin{pgnote} |
509 \begin{pgnote} |
509 The search engine is started by clicking on Proof General's \textsf{Find} icon. |
510 The search engine is started by clicking on Proof General's \pgmenu{Find} icon. |
510 You specify your search textually in the input buffer at the bottom |
511 You specify your search textually in the input buffer at the bottom |
511 of the window. |
512 of the window. |
512 \end{pgnote} |
513 \end{pgnote} |
513 |
514 |
514 The simplest form of search is that for theorems containing particular |
515 The simplest form of search is that for theorems containing particular |
541 If you are looking for theorems potentially simplifying some term, you |
542 If you are looking for theorems potentially simplifying some term, you |
542 need to prefix the pattern with \texttt{simp:}. |
543 need to prefix the pattern with \texttt{simp:}. |
543 \begin{ttbox} |
544 \begin{ttbox} |
544 simp: "_ * (_ + _)" |
545 simp: "_ * (_ + _)" |
545 \end{ttbox} |
546 \end{ttbox} |
546 This searches all (possibly conditional) equations of the form |
547 This searches \emph{all} (possibly conditional) equations of the form |
547 \begin{isabelle}% |
548 \begin{isabelle}% |
548 \ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}% |
549 \ \ \ \ \ {\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}\ {\isacharequal}\ {\isasymdots}% |
549 \end{isabelle} |
550 \end{isabelle} |
550 i.e.\ all distributivity rules. |
551 not just those with a \isa{simp} attribute. |
551 Note that the given pattern needs to be simplified |
552 Note that the given pattern needs to be simplified |
552 at the root, not somewhere inside. |
553 at the root, not somewhere inside: for example, commutativity of \isa{{\isacharplus}} |
|
554 does not match. |
553 |
555 |
554 You may also search theorems by name. To make this useful you merely |
556 You may also search theorems by name. To make this useful you merely |
555 need to give a substring. For example, you could try and search for all |
557 need to give a substring. For example, you could try and search for all |
556 commutativity theorems like this: |
558 commutativity theorems like this: |
557 \begin{ttbox} |
559 \begin{ttbox} |
559 \end{ttbox} |
561 \end{ttbox} |
560 This retrieves all theorems whose name contains \texttt{comm}. |
562 This retrieves all theorems whose name contains \texttt{comm}. |
561 |
563 |
562 Search criteria can also be negated by prefixing them with ``\texttt{-}'': |
564 Search criteria can also be negated by prefixing them with ``\texttt{-}'': |
563 \begin{ttbox} |
565 \begin{ttbox} |
564 -name: HOL |
566 -name: List |
565 \end{ttbox} |
567 \end{ttbox} |
566 finds theorems whose name does not contain \texttt{HOL}. This is useful for |
568 finds theorems whose name does not contain \texttt{List}. This can be useful, |
|
569 for example, for |
567 excluding particular theories from the search because the (long) name of |
570 excluding particular theories from the search because the (long) name of |
568 a theorem contains the name of the theory it comes from. |
571 a theorem contains the name of the theory it comes from. |
569 |
572 |
570 Finallly, different search criteria can be combined arbitrarily: |
573 Finallly, different search criteria can be combined arbitrarily: |
571 \begin{ttbox} |
574 \begin{ttbox} |
572 "_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc |
575 "_ + _" -"_ - _" -simp: "_ * (_ + _)" name: assoc |
573 \end{ttbox} |
576 \end{ttbox} |
574 looks for theorems containg a plus but no minus which are not distributivity |
577 looks for theorems containg a plus but no minus which do not simplify |
575 rules and whose name contains \texttt{assoc}. |
578 \mbox{\isa{{\isacharunderscore}\ {\isacharasterisk}\ {\isacharparenleft}{\isacharunderscore}\ {\isacharplus}\ {\isacharunderscore}{\isacharparenright}}} at the root and whose name contains \texttt{assoc}. |
576 |
579 |
577 Further search criteria are explained in \S\ref{sec:Find:ied}.% |
580 Further search criteria are explained in \S\ref{sec:find:ied}. |
|
581 |
|
582 \begin{pgnote} |
|
583 Proof General keeps a history of all your search expressions. |
|
584 If you click on \pgmenu{Find}, you can use the arrow keys to scroll |
|
585 through previous searches and just modify them. This saves you having |
|
586 to type in lengthy expressions again and again. |
|
587 \end{pgnote}% |
578 \end{isamarkuptext}% |
588 \end{isamarkuptext}% |
579 \isamarkuptrue% |
589 \isamarkuptrue% |
580 \isamarkupfalse% |
590 \isamarkupfalse% |
581 \end{isabellebody}% |
591 \end{isabellebody}% |
582 %%% Local Variables: |
592 %%% Local Variables: |