1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC CONTR_TAC
\TYPE {CONTR_TAC : thm_tactic}
\SYNOPSIS
Solves any goal from contradictory theorem.
\KEYWORDS
tactic, contradiction.
\DESCRIBE
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
Fails unless the theorem is contradictory, i.e. has {F} as its conclusion.
\SEEALSO
CCONTR, CONTR, NOT_ELIM.
\ENDDOC
|
