Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

DISCH_TAC

Tactic.DISCH_TAC : tactic

Moves the antecedent of an implicative goal into the assumptions.

    A ?- u ==> v
   ==============  DISCH_TAC
    A u {u} ?- v

Note that DISCH_TAC treats ~u as u ==> F, so will also work when applied to a goal with a negated conclusion.

Failure

DISCH_TAC will fail for goals which are not implications or negations.

Solving goals of the form u ==> v by rewriting v with u, although the use of DISCH_THEN is usually more elegant in such cases.

Comments

If the antecedent already appears in the assumptions, it will be duplicated.

See also

Thm.DISCH, Drule.DISCH_ALL, Thm_cont.DISCH_THEN, Tactic.FILTER_DISCH_TAC, Tactic.FILTER_DISCH_THEN, Drule.NEG_DISCH, Tactic.STRIP_TAC, Drule.UNDISCH, Drule.UNDISCH_ALL, Tactic.UNDISCH_TAC