FILTER_DISCH_TAC : (term -> tactic)
STRUCTURE
SYNOPSIS
Conditionally moves the antecedent of an implicative goal into the assumptions.
DESCRIPTION
FILTER_DISCH_TAC will move the antecedent of an implication into the assumptions, provided its parameter does not occur in the antecedent.
    A ?- u ==> v
   ==============  FILTER_DISCH_TAC w
    A u {u} ?- v
Note that DISCH_TAC treats ~u as u ==> F. Unlike DISCH_TAC, the antecedent will be STRIPed into its various components before being ASSUMEd. This stripping includes generating multiple goals for case-analysis of disjunctions. Also, unlike DISCH_TAC, should any component of the discharged antecedent directly imply or contradict the goal, then this simplification will also be made. Again, unlike DISCH_TAC, FILTER_DISCH_TAC will not duplicate identical or alpha-equivalent assumptions.
FAILURE
FILTER_DISCH_TAC will fail if a term which is identical, or alpha-equivalent to w occurs free in the antecedent, or if the theorem is not an implication or a negation.
COMMENTS
FILTER_DISCH_TAC w behaves like FILTER_DISCH_THEN STRIP_ASSUME_TAC w.
SEEALSO
HOL  Trindemossen-1