matita/matita/help/C/html/tacticals.html

   1 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
   2 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Tacticals</title><link rel="stylesheet" type="text/css" href="docbook.css" /><meta name="generator" content="DocBook XSL Stylesheets Vsnapshot" /><link rel="home" href="index.html" title="Matita V0.99.5 User Manual (rev. 0.99.5 )" /><link rel="up" href="sec_tacticals.html" title="Chapter 6. Tacticals" /><link rel="prev" href="proofstatus.html" title="The proof status" /><link rel="next" href="sec_tactics.html" title="Chapter 7. Tactics" /></head><body><a xmlns="" href="../../../"><div class="matita_logo"><img src="figures/matita.png" alt="Tiny Matita logo" /><span>Matita Home</span></div></a><div class="navheader"><table width="100%" summary="Navigation header"><tr><th colspan="3" align="center">Tacticals</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="proofstatus.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tacticals</th><td width="20%" align="right"> <a accesskey="n" href="sec_tactics.html">Next</a></td></tr></table><hr /></div><div class="sect1"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tacticals"></a>Tacticals</h2></div></div></div><div class="table"><a id="idm2266"></a><p class="title"><strong>Table 6.1. proof script</strong></p><div class="table-contents"><table class="table" summary="proof script" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.proofscript"></a><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.proofscript">proof-script</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.proofstep">proof-step</a></em></span> [<span class="emphasis"><em><a class="link" href="tacticals.html#grammar.proofstep">proof-step</a></em></span>]…</td><td class="auto-generated" style=""> </td></tr></tbody></table></div></div><br class="table-break" /><p>Every proof step can be immediately executed.</p><div class="table"><a id="idm2281"></a><p class="title"><strong>Table 6.2. proof steps</strong></p><div class="table-contents"><table class="table" summary="proof steps" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.proofstep"></a><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.proofstep">proof-step</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span></td><td style="">The tactical is applied to each
   3         <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
   4         Each new sequent becomes a selected sequent.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>.</strong></span></td><td style="">The first
   5         <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a> becomes
   6         the only one selected. All the remaining previously selected sequents
   7         are proposed to the user one at a time when the next
   8         "<span class="bold"><strong>.</strong></span>" is used.
   9        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>;</strong></span></td><td style="">Nothing changes. Use this proof step as a separator in
  10         concrete syntax.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>[</strong></span></td><td style="">Every <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>
  11         becomes a <a class="link" href="proofstatus.html#siblingsequents">sibling sequent</a>
  12         that constitute a branch in the proof.
  13         Moreover, the first sequent is also selected.
  14        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>|</strong></span></td><td style="">Stop working on the current branch of the innermost branching
  15         proof.
  16         The sibling branches become the <a class="link" href="proofstatus.html#siblingsequents">sibling
  17         sequents</a> and the first one is also selected.
  18        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>[<span class="bold"><strong>,</strong></span><span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>]…<span class="bold"><strong>:</strong></span></td><td style="">The <a class="link" href="proofstatus.html#siblingsequents">sibling sequents</a>
  19         specified by the user become the next
  20         <a class="link" href="proofstatus.html#selectedsequents">selected sequents</a>.
  21        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>*:</strong></span></td><td style="">Every sibling branch not considered yet in the innermost
  22         branching proof becomes a
  23         <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
  24        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>skip</strong></span></td><td style="">Accept the automatically provided instantiation (not shown
  25         to the user) for the currently selected
  26         <a class="link" href="proofstatus.html#solvedsequents">automatically closed sibling sequent</a>.
  27        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>]</strong></span></td><td style="">Stop analyzing branches for the innermost branching proof.
  28         Every sequent opened during the branching proof and not closed yet
  29         becomes a <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
  30        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>focus</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span> [<span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>]…</td><td style="">
  31         Selects the sequents specified by the user. The selected sequents
  32         must be completely closed (no new sequents left open) before doing an
  33         "<span class="bold"><strong>unfocus</strong></span> that restores
  34         the current set of sibling branches.
  35        </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>unfocus</strong></span></td><td style="">
  36         Used to match the innermost
  37         "<span class="bold"><strong>focus</strong></span>" tactical
  38         when all the sequents selected by it have been closed.
  39         Until "<span class="bold"><strong>unfocus</strong></span>" is
  40         performed, it is not possible to progress in the rest of the
  41         proof.
  42        </td></tr></tbody></table></div></div><br class="table-break" /><div class="table"><a id="idm2377"></a><p class="title"><strong>Table 6.3. tactics and LCF tacticals</strong></p><div class="table-contents"><table class="table" summary="tactics and LCF tacticals" style="border-collapse: collapse;border-top: 1px solid ; border-bottom: 1px solid ; "><colgroup><col /><col /><col /><col /></colgroup><tbody><tr><td style=""><a id="grammar.LCFtactical"></a><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span></td><td style="">::=</td><td style=""><span class="emphasis"><em><a class="link" href="sec_tactics.html#grammar.tactic">tactic</a></em></span></td><td style="">Applies the specified tactic.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span> <span class="bold"><strong>;</strong></span> <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span></td><td style="">Applies the first tactical first and the second tactical
  43         to each sequent opened by the first one.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>
  44         <span class="bold"><strong>[</strong></span>
  45         [<span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]
  46         [<span class="bold"><strong>|</strong></span> <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]…
  47         <span class="bold"><strong>]</strong></span>
  48        </td><td style="">Applies the first tactical first and each tactical in the
  49         list of tacticals to the corresponding sequent opened by the
  50         first one. The number of tacticals provided in the list must be
  51         equal to the number of sequents opened by the first tactical.</td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>do</strong></span> <span class="emphasis"><em><a class="link" href="sec_terms.html#grammar.nat">nat</a></em></span>
  52         <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>
  53        </td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>repeat</strong></span>
  54         <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>
  55        </td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  56         <span class="bold"><strong>first [</strong></span>
  57         [<span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]
  58         [<span class="bold"><strong>|</strong></span> <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]…
  59         <span class="bold"><strong>]</strong></span>
  60        </td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>try</strong></span> <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span></td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style="">
  61         <span class="bold"><strong>solve [</strong></span>
  62         [<span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]
  63         [<span class="bold"><strong>|</strong></span> <span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span>]…
  64         <span class="bold"><strong>]</strong></span>
  65        </td><td style=""><span class="emphasis"><em>TODO</em></span></td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>(</strong></span><span class="emphasis"><em><a class="link" href="tacticals.html#grammar.LCFtactical">LCF-tactical</a></em></span><span class="bold"><strong>)</strong></span></td><td style="">Used for grouping during parsing.</td></tr></tbody></table></div></div><br class="table-break" /></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="proofstatus.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tacticals.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="sec_tactics.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">The proof status </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> Chapter 7. Tactics</td></tr></table></div></body></html>