1\DOC
2
3\TYPE {DEEP_INTRO_TAC : thm -> tactic}
4
5\SYNOPSIS
6Applies an introduction-rule backwards; instantiating a predicate variable.
7
8\KEYWORDS
9matching
10
11\DESCRIBE
12The function {DEEP_INTRO_TAC} expects a theorem of the form
13{
14   antecedents ==> P (term-pattern)
15}
16where {P} is a variable, and {term-pattern} is a pattern describing
17the form of an expected sub-term in the goal.  When {th} is of this
18form, the tactic {DEEP_INTRO_TAC th} finds a higher-order
19instantiation for the variable {P} and a first order instantiation for
20the variables in {term-pattern} such that the instantiated conclusion
21of {th} is identical to the goal.  It then applies {MATCH_MP_TAC} to
22turn the goal into an instantiation of the antecedents of {th}.
23
24\FAILURE
25Fails if there is no (free) instance of {term-pattern} in the goal.
26Also fails if {th} is not of the required form.
27
28\EXAMPLE
29The theorem {SELECT_ELIM_THM} states
30{
31   |- !P Q. (?x. P x) /\ (!x. P x ==> Q x) ==> Q ($@ P)
32}
33This is of the required form for use by {DEEP_INTRO_TAC}, and can be
34used to transform a goal mentioning Hilbert Choice (the {@} operator)
35into one that doesn't.  Indeed, this is how {SELECT_ELIM_TAC} is
36implemented.
37
38\SEEALSO
39Tactic.MATCH_MP_TAC, Tactic.SELECT_ELIM_TAC.
40
41\ENDDOC
42