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