Next: Transformation Tactics
Up: Tactics
Previous: Miscellaneous
The autotactics are used primarily for typechecking.
Trivial
-
- Does various steps of trivial reasoning, including
- NthHyp
- NthDecl
- Eq
- Contradiction - Both P and
occur in hypothesis list.
- Concl is the term True or one of the hypotheses is either
the term False or the term Void.
Auto
-
- Repeatedly tries the following until no further progress is made.
- Trivial
- GenExRepD
- MemCD for member and EqCD on reflexive equality
conclusions. Only works on non-recursive primitive terms.
- Arith
- Arithmetic equality reasoning, in case concl is
where a and b arithmetically simplify to same. (By arithmetically
simplify, we mean simplify subterms which involve the
basic arithmetic operators
and rem
.)
- If concl is
or
where T is subset of the
integers, then open up T.
SIAuto
-
- Like Auto but also tries using the SupInf tactic.
Auto'
-
- Like Auto but uses the SupInf' tactic instead of the
Arith tactic.
Auto and its variants frequently encounter the same goals over and
over again, so
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996