<term>Pre-conditions:</term>
<listitem>
<para><command>t</command> must have type
- <command>T<subscript>1</subscript> → ... →
+ <command>T<subscript>1</subscript> → … →
T<subscript>n</subscript> → G</command>
where <command>G</command> can be unified with the conclusion
of the current sequent.</para>
<title>cases</title>
<titleabbrev>cases</titleabbrev>
<para><userinput>
- cases t hyps
+ cases t pattern hyps
</userinput></para>
<para>
<variablelist>
<listitem>
<para>
<emphasis role="bold">cases</emphasis>
- &term; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+ &term; &pattern; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
</para>
</listitem>
</varlistentry>
It proceed by cases on <command>t</command>. The new generated
hypothesis in each branch are named according to
<command>hyps</command>.
+ The elimintation predicate is restricted by
+ <command>pattern</command>. In particular, if some hypothesis
+ is listed in <command>pattern</command>, the hypothesis is
+ generalized and cleared before proceeding by cases on
+ <command>t</command>. Currently, we only support patterns of the
+ form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
</para>
</listitem>
</varlistentry>
<sect1 id="tac_elim">
<title>elim</title>
<titleabbrev>elim</titleabbrev>
- <para><userinput>elim t using th hyps</userinput></para>
+ <para><userinput>elim t pattern using th hyps</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">elim</emphasis> &sterm; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
+ <para><emphasis role="bold">elim</emphasis> &sterm; &pattern; [<emphasis role="bold">using</emphasis> &sterm;] &intros-spec;</para>
</listitem>
</varlistentry>
<varlistentry>
<listitem>
<para>It proceeds by cases on the values of <command>t</command>,
according to the elimination principle <command>th</command>.
+ The induction predicate is restricted by
+ <command>pattern</command>. In particular, if some hypothesis
+ is listed in <command>pattern</command>, the hypothesis is
+ generalized and cleared before eliminating <command>t</command>
</para>
</listitem>
</varlistentry>