helm/www/matita/docs/manual/tac_inversion.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">
   3 <html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>inversion sterm</title><link rel="stylesheet" href="docbook.css" type="text/css" /><meta name="generator" content="DocBook XSL Stylesheets V1.68.1" /><link rel="start" href="index.html" title="Matita V0.1.0&#10; User Manual (rev. 1α)" /><link rel="up" href="sec_tactics.html" title="Chapter 6. Tactics" /><link rel="prev" href="tac_intros.html" title="intros &lt;intros_spec&gt;" /><link rel="next" href="tac_lapply.html" title="lapply [depth=nat] sterm [to &lt;term list&gt;] [using id]" /></head><body><a xmlns="" href="../../"><div class="matita_logo"><img src="../../images/matita-tiny.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">inversion sterm</th></tr><tr><td width="20%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><th width="60%" align="center">Chapter 6. Tactics</th><td width="20%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr></table><hr /></div><div class="sect1" lang="en" xml:lang="en"><div class="titlepage"><div><div><h2 class="title" style="clear: both"><a id="tac_inversion"></a>inversion <span class="emphasis"><em><a href="sec_terms.html#sterm">sterm</a></em></span></h2></div></div></div><p><strong class="userinput"><code>inversion t</code></strong></p><p>
   4       </p><div class="variablelist"><dl><dt><span class="term">Pre-conditions:</span></dt><dd><p>The type of the term <span><strong class="command">t</strong></span> must be an inductive
   5              type or the application of an inductive type.</p></dd><dt><span class="term">Action:</span></dt><dd><p>It proceeds by cases on <span><strong class="command">t</strong></span> paying attention
   6              to the constraints imposed by the actual "right arguments"
   7              of the inductive type.</p></dd><dt><span class="term">New sequents to prove:</span></dt><dd><p>It opens one new sequent to prove for each case in the
   8              definition of the type of <span><strong class="command">t</strong></span>. With respect to
   9              a simple elimination, each new sequent has additional hypotheses
  10              that states the equalities of the "right parameters"
  11              of the inductive type with terms originally present in the
  12              sequent to prove.</p></dd></dl></div><p>
  13     </p></div><div class="navfooter"><hr /><table width="100%" summary="Navigation footer"><tr><td width="40%" align="left"><a accesskey="p" href="tac_intros.html">Prev</a> </td><td width="20%" align="center"><a accesskey="u" href="sec_tactics.html">Up</a></td><td width="40%" align="right"> <a accesskey="n" href="tac_lapply.html">Next</a></td></tr><tr><td width="40%" align="left" valign="top">intros &lt;intros_spec&gt; </td><td width="20%" align="center"><a accesskey="h" href="index.html">Home</a></td><td width="40%" align="right" valign="top"> lapply [depth=nat] sterm [to &lt;term list&gt;] [using id]</td></tr></table></div></body></html>