Tactic.FILTER_DISCH

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

DISCH, DISCH_ALL, DISCH_TAC, DISCH_THEN, FILTER_DISCH_THEN, NEG_DISCH, STRIP_TAC, UNDISCH, UNDISCH_ALL, UNDISCH_TAC