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, ifthen
A ?- t ======== f (ASSUME u) B ?- v

Note that FILTER_DISCH_THEN treats ~u as u ==> F.A ?- u ==> t ============== FILTER_DISCH_THEN f B ?- v

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