| | | B.4.7 instantiate: Instantiate Variables in Formula |
instantiate V1, V2, ... in F
In proving mode.
This command takes the label F of a formula of the current state such that
this formula is either a universally quantified assumption or an existentially
quantified goal with n bound variables. It also takes n instantiation
values V1, V2, ..., Vn such that each Vi is either the reserved
identifier '_' or a term with a type that matches the type Ti of the
corresponding variable. The command then creates a child state that is
identical to the current state except that an instantiated version of the
universal assumption is added as an additional assumption respectively an
instantiated version of the existential goal is added as an additional goal
(see the rules depicted below). In the instantiated version of the formula,
for every term Vi different from '_', every free occurrence
of the corresponding variable in the body of the quantified formula is
replaced by Vi (potentially renaming some variables bound within
the body) and the variable is removed from the list of bound variables. If no
value Vi is '_', all variables are replaced and the
quantifier is dropped from the instantiation result. The type of term
Vi needs not equal Ti; if necessary, a side condition p(Vi)
is generated and an additional proof state with goal p(Vi) is created.
If F does not denote a universal assumption or existential goal of the
current proof state, if the number of instantiation values V1,
V2, ..., Vn does not equal the number of bound
variables of the formula, if some Ti cannot be type-checked or has a type
that does not match the type of the corresponding variable, or if all
instantiation terms are '_', no child state is generated.
The following rules describe the case of the instantiation of a quantified
formula with two variables whose first is instantiated (corresponding to an
application of the command instantiate V1, _ in ...):
[E] ..., /\ x1 in T1, x2 in T2: G, ..., /\ x2 in T2: G[V1/x1] |- ...
[E] ..., /\ x1 in T1, x2 in T2: G, ... |- p(V1)
[E, p(V1)] |- V1:T1
--------------------------------------------------------------------
[E] ..., /\ x1 in T1, x2 in T2: G, ... |- ...
[E] ... |- ..., \/ x1 in T1, x2 in T2: G, ... \/ x2 in T2: G[V1/x1]
[E] ... |- p(V1)
[E, p(V1)] |- V1:T1
-------------------------------------------------------------------
[E] ... |- ..., \/ x1 in T1, x2 in T2: G ...
An additional proof state may be generated for a type checking condition corresponding to the values V1, V2, ....
| | | B.4.7 instantiate: Instantiate Variables in Formula |