CONTRAPOS : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Deduces the contrapositive of an implication.
DESCRIPTION
When applied to a theorem
A |- s ==> t
, the inference rule
CONTRAPOS
returns its contrapositive,
A |- ~t ==> ~s
.
A |- s ==> t ---------------- CONTRAPOS A |- ~t ==> ~s
FAILURE
Fails unless the theorem is an implication.
SEEALSO
CCONTR
,
CONTR
,
CONTRAPOS_CONV
,
NOT_ELIM
HOL
Trindemossen-1