Simplifies the conclusion of a theorem according to the given simpset
and theorem rewrites.
LIBRARY
simpLib
DESCRIPTION
SIMP_RULE simplifies the conclusion of a theorem, adding the given
theorems to the simpset parameter as rewrites. The way in which terms
are transformed as a part of simplification is described in the entry
for SIMP_CONV.
FAILURE
Never fails, but may diverge.
EXAMPLE
The following also demonstrates the higher order rewriting
possible with simplification (FORALL_AND_THM states
|- (!x. P x /\ Q x) = (!x. P x) /\ (!x. Q x)):
- SIMP_RULE bool_ss [boolTheory.FORALL_AND_THM]
(ASSUME (Term`!x. P (x + 1) /\ R x /\ x < y`));
> val it = [.] |- (!x. P (x + 1)) /\ (!x. R x) /\ (!x. x < y) : thm
COMMENTS
SIMP_RULE ss thmlist is equivalent to CONV_RULE (SIMP_CONV ss thmlist).