--- /dev/null
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!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
+ <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
+ 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
+ <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a> becomes
+ the only one selected. All the remaining previously selected sequents
+ are proposed to the user one at a time when the next
+ "<span class="bold"><strong>.</strong></span>" is used.
+ </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
+ 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>
+ becomes a <a class="link" href="proofstatus.html#siblingsequents">sibling sequent</a>
+ that constitute a branch in the proof.
+ Moreover, the first sequent is also selected.
+ </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
+ proof.
+ The sibling branches become the <a class="link" href="proofstatus.html#siblingsequents">sibling
+ sequents</a> and the first one is also selected.
+ </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>
+ specified by the user become the next
+ <a class="link" href="proofstatus.html#selectedsequents">selected sequents</a>.
+ </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
+ branching proof becomes a
+ <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
+ </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
+ to the user) for the currently selected
+ <a class="link" href="proofstatus.html#solvedsequents">automatically closed sibling sequent</a>.
+ </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.
+ Every sequent opened during the branching proof and not closed yet
+ becomes a <a class="link" href="proofstatus.html#selectedsequents">selected sequent</a>.
+ </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="">
+ Selects the sequents specified by the user. The selected sequents
+ must be completely closed (no new sequents left open) before doing an
+ "<span class="bold"><strong>unfocus</strong></span> that restores
+ the current set of sibling branches.
+ </td></tr><tr><td style=""> </td><td style="">|</td><td style=""><span class="bold"><strong>unfocus</strong></span></td><td style="">
+ Used to match the innermost
+ "<span class="bold"><strong>focus</strong></span>" tactical
+ when all the sequents selected by it have been closed.
+ Until "<span class="bold"><strong>unfocus</strong></span>" is
+ performed, it is not possible to progress in the rest of the
+ proof.
+ </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
+ 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>
+ <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> <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="">Applies the first tactical first and each tactical in the
+ list of tacticals to the corresponding sequent opened by the
+ first one. The number of tacticals provided in the list must be
+ 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>
+ <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=""><span class="bold"><strong>repeat</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="">
+ <span class="bold"><strong>first [</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> <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=""><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="">
+ <span class="bold"><strong>solve [</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> <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=""><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>
\ No newline at end of file
projects / helm.git / blobdiff