EQ_IMP_RULE : thm -> thm * thm

SYNOPSIS

Derives forward and backward implication from equality of boolean terms.

DESCRIPTION

When applied to a theorem A |- t1 <=> t2, where t1 and t2 both have type bool, the inference rule EQ_IMP_RULE returns the theorems A |- t1 ==> t2 and A |- t2 ==> t1.

              A |- t1 <=> t2
   -----------------------------------  EQ_IMP_RULE
    A |- t1 ==> t2     A |- t2 ==> t1

FAILURE CONDITIONS

Fails unless the conclusion of the given theorem is an equation between boolean terms.

EXAMPLE

  # SPEC_ALL CONJ_SYM;;
  val it : thm = |- t1 /\ t2 <=> t2 /\ t1

  # EQ_IMP_RULE it;;
  val it : thm * thm = (|- t1 /\ t2 ==> t2 /\ t1, |- t2 /\ t1 ==> t1 /\ t2)

SEE ALSO

EQ_MP, EQ_TAC, IMP_ANTISYM_RULE.