instantiate : instantiation -> term -> term
Apply a higher-order instantiation to a term.
The call instantiate i t, where i is an instantiation as returned by
term_match, will perform the instantiation indicated by i in the term t:
types and terms will be instantiated and the beta-reductions that are part of
higher-order matching will be applied.
- FAILURE CONDITIONS
Should never fail on a valid instantiation.
We first compute an instantiation:
and now apply it. Notice that the type variable name is not
corrected, as is done inside PART_MATCH:
# let t = `(!x. P x) <=> ~(?x. P x)`;;
Warning: inventing type variables
val t : term = `(!x. P x) <=> ~(?x. P x)`
# let i = term_match  (lhs t) `!p. prime(p) ==> p = 2 \/ ODD(p)`;;
val i : instantiation =
([(1, `P`)], [(`\p. prime p ==> p = 2 \/ ODD p`, `P`)],
# instantiate i t;;
val it : term =
`(!x. prime x ==> x = 2 \/ ODD x) <=> ~(?x. prime x ==> x = 2 \/ ODD x)`
This is probably not useful for most users.
- SEE ALSO
compose_insts, INSTANTIATE, INSTANTIATE_ALL, inst_goal, PART_MATCH, term_match.