Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

CONTR_TAC : thm_tactic

SYNOPSIS

Solves any goal from contradictory theorem.

DESCRIPTION

When applied to a contradictory theorem A' |- F, and a goal A ?- t, the tactic CONTR_TAC completely solves the goal. This is an invalid tactic unless A' is a subset of A.

    A ?- t
   ========  CONTR_TAC (A' |- F)

USES

One quite common pattern is to use a contradictory hypothesis via FIRST_ASSUM CONTR_TAC.

FAILURE CONDITIONS

Fails unless the theorem is contradictory, i.e. has F as its conclusion.

SEE ALSO

CCONTR, CONTR, NOT_ELIM.