SIMP_RULE

bossLib.SIMP_RULE : simpset -> thm list -> thm -> thm

Also exported as simpLib.SIMP_RULE.

Simplifies the conclusion of a theorem according to the given simpset and theorem rewrites.

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).

See also

simpLib.ASM_SIMP_RULE, bossLib.SIMP_CONV, bossLib.SIMP_TAC, bossLib.bool_ss