----------------------------------------------------------------------
Cong                                                         (simpLib)
----------------------------------------------------------------------
Cong : thm -> thm

SYNOPSIS
Marks a theorem as a congruence rule for the simplifier.

KEYWORDS
Simplification.

DESCRIBE
The {Cong} function marks (or "tags") a theorem so that when passed to
the simplifier, it is not used as a rewrite, but rather as a
congruence rule.  This is a simpler way of adding a congruence rule to
the simplifier than using the underlying {SSFRAG} function.

FAILURE
Never fails.  On the other hand, {Cong} does not check that the
theorem passed as an argument is a valid congruence rule, and
invalid congruence rules may have unpredictable effects on the
behaviour of the simplifier.

EXAMPLE

   - SIMP_CONV pure_ss [] ``!x::P. x IN P /\ Q x``;
   <<HOL message: inventing new type variable names: 'a>>
   ! Uncaught exception:
   ! UNCHANGED
   - RES_FORALL_CONG;
   > val it =
       |- (P = Q) ==>
          (!x. x IN Q ==> (f x = g x)) ==>
          (RES_FORALL P f = RES_FORALL Q g) : thm
   - SIMP_CONV pure_ss [Cong RES_FORALL_CONG] ``!x::P. x IN P ``;
   <<HOL message: inventing new type variable names: 'a>>
   > val it = |- (!x::P. x IN P /\ Q x) = !x::P. T /\ Q x : thm

(Note that {RES_FORALL_CONG} is already included in {bool_ss} and all
simpsets built on it.)

SEEALSO
simpLib.SSFRAG.

----------------------------------------------------------------------