← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to doc/HTML/HINTS.html

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/HTML/HINTS.html
1
1
<html>
2
 
<head><title>HINTS.html  --  ACL2 Version 3.0.1</title></head>
 
2
<head><title>HINTS.html  --  ACL2 Version 3.1</title></head>
3
3
<body text=#000000 bgcolor="#FFFFFF">
4
4
<h2>HINTS</h2>advice to the theorem proving process
5
5
<pre>Major Section:  <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
190
190
<code>:INDUCT</code><br>
191
191
 
192
192
<code>Value</code> is either <code>t</code> or a term containing at least one recursively
193
 
defined function symbol; if <code>t</code>, this hint indicates that the system
194
 
should proceed to apply its induction heuristic to the specified
195
 
goal produced (without trying simplification, etc.); if <code>value</code> is
196
 
a term other than <code>t</code>, then not only should the system apply
197
 
induction immediately, but it should analyze <code>value</code> rather than
198
 
the goal to generate its <a href="INDUCTION.html">induction</a> scheme.  Merging and the
199
 
other <a href="INDUCTION.html">induction</a> heuristics are applied.  Thus, if <code>value</code>
200
 
contains several mergeable <a href="INDUCTION.html">induction</a>s, the ``best'' will be
 
193
defined function symbol.  If <code>t</code>, this hint indicates that the system
 
194
should proceed to apply its <a href="INDUCTION.html">induction</a> heuristic to the specified goal
 
195
(without trying simplification, etc.).  If <code>value</code> is of the form
 
196
<code>(f x1 ... xk)</code>, where <code>f</code> is a recursively defined function and <code>x1</code>
 
197
through <code>xk</code> are distinct variables, then the system is to induct according
 
198
to the <a href="INDUCTION.html">induction</a> scheme that was stored for <code>f</code>.  For example, for the
 
199
hint <code>:induct (true-listp x)</code>, ACL2 will assume that the goal holds for
 
200
<code>(cdr x)</code> when proving the induction step because <code><a href="TRUE-LISTP.html">true-listp</a></code> recurs
 
201
on the <code><a href="CDR.html">cdr</a></code>.  More generally, if <code>value</code> is a term other than <code>t</code>,
 
202
then not only should the system apply induction immediately, but it should
 
203
analyze <code>value</code> rather than the goal to generate its <a href="INDUCTION.html">induction</a> scheme.
 
204
Merging and the other <a href="INDUCTION.html">induction</a> heuristics are applied.  Thus, if
 
205
<code>value</code> contains several mergeable <a href="INDUCTION.html">induction</a>s, the ``best'' will be
201
206
created and chosen.  E.g., the <code>:induct</code> hint
202
207
 
203
208
<pre>