| | | B.3.6 auto: Close State by Automatic Formula Instantiation |
auto
auto F1, F2, ...
: auto
In proving mode.
This command generates a single child state by automatically instantiating selected quantified formulas by suitable instantiation terms according to the rules listed below. The instantiations terms are taken from those ground terms (terms without free variables) that appear in some formula (goal or assumption) of the state and whose type matches the type of the bound variable to be instantiated. The type of the instantiation expression e needs not equal the type of the bound variable; if necessary, a side condition p(e) is added to the instantiated formula to make the instantiation legal.
If the command is applied as auto, all formulas (assumptions and goals) may be instantiated; if the application is auto F1, F2, ..., only the formulas with labels F1, F2, ... may be instantiated.
The generated child state is only added to the current state, if it can be immediately closed by a decision procedure; otherwise it is discarded and the current state remains without child.
The applied rules are:
[E] ..., /\ x in T: A, ..., p(e) => A[e/x] |- ...
[E,p(e)] |- e:T
-------------------------------------------------
[E] ..., /\ x in T: A, ... |- ...
[E] ... |- ..., \/ x in T: A, ..., p(e) /\ A[e/x]
[E,p(e)] |- e:T
-------------------------------------------------
[E] ... |- ..., \/ x in T: A, ...
For performance reasons, only a limited number of instantiations is performed; thus auto may miss instantiation terms that are able to close the state, even if they appear in the proof state. In this case, one may try to use the form auto F1, F2, ... to limit the instantiations to the "interesting" quantified formulas of the current state.
Since no proof search is implemented, the automatic instantiation of formulas is only useful if it allows a decision procedure to close the state; therefore the command discards the generated state, if it cannot be immediately closed. Use the command instantiate to manually generate instantiations for further use in child states.
| | | B.3.6 auto: Close State by Automatic Formula Instantiation |