FILTER_DISCH_THEN : (thm_tactic -> term -> tactic)
STRUCTURE
SYNOPSIS
Conditionally gives to a theorem-tactic the antecedent of an implicative goal.
DESCRIPTION
If FILTER_DISCH_THEN’s second argument, a term, does not occur in the antecedent, then FILTER_DISCH_THEN removes the antecedent and then creates a theorem by ASSUMEing it. This new theorem is passed to FILTER_DISCH_THEN’s first argument, which is subsequently expanded. For example, if
    A ?- t
   ========  f (ASSUME u)
    B ?- v
then
    A ?- u ==> t
   ==============  FILTER_DISCH_THEN f
       B ?- v
Note that FILTER_DISCH_THEN treats ~u as u ==> F.
FAILURE
FILTER_DISCH_THEN will fail if a term which is identical, or alpha-equivalent to w occurs free in the antecedent. FILTER_DISCH_THEN will also fail if the theorem is an implication or a negation.
COMMENTS
FILTER_DISCH_THEN is most easily understood by first understanding DISCH_THEN.
USES
For preprocessing an antecedent before moving it to the assumptions, or for using antecedents and then throwing them away.
SEEALSO
HOL  Kananaskis-13