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.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.
A ?- u ==> v ============== FILTER_DISCH_TAC w A u {u} ?- v

- 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 Kananaskis-14