pure_ss
pureSimps.pure_ss : simpset
A simpset containing only the conditional rewrite generator and no additional rewrites.
This simpset sits at the root of the simpset hierarchy. It contains no rewrites, congruences, conversions or decision procedures. Instead it contains just the code which converts theorems passed to it as context into (possibly conditional) rewrites.
Simplification with pure_ss is analogous to rewriting with
PURE_REWRITE_TAC and others. The only difference is that the theorems
passed to SIMP_TAC pure_ss are interpreted as conditional rewrite
rules. Though the pure_ss can't take advantage of extra contextual
information garnered through congruences, it can still discharge side
conditions. (This is demonstrated in the examples below.)
Failure
Can't fail, as it is not a functional value.
Example
The theorem ADD_EQ_SUB from arithmeticTheory states that
|- !m n p. n <= p ==> ((m + n = p) = m = p - n)
We can use this result to make progress with the following goal in
conjunction with pure_ss in a way that no form of REWRITE_TAC could:
- ASM_SIMP_TAC pure_ss [ADD_EQ_SUB] ([“x <= y”], “z + x = y”);
> val it = ([([`x <= y`], `z = y - x`)], fn) : tactic_result
This example illustrates the way in which the simplifier can do
conditional rewriting. However, the lack of the congruence for
implications means that using pure_ss will not be able to discharge
the side condition in the goal below:
- SIMP_TAC pure_ss [ADD_EQ_SUB] ([], “x <= y ==> (z + x = y)”);
> val it = ([([], `x <= y ==> (z + x = y)`)], fn) : tactic_result
As bool_ss has the relevant congruence included, it does make progress
in the same situation:
- SIMP_TAC bool_ss [ADD_EQ_SUB] ([], “x <= y ==> (z + x = y)”);
> val it = ([([], `x <= y ==> (z = y - x)`)], fn) : tactic_result
The pure_ss simpset might be used in the most delicate simplification
situations, or, mimicking the way it is used within the distribution
itself, as a basis for the construction of other simpsets.
Comments
There is also a pureSimps.PURE_ss ssfrag value. Its usefulness is
questionable.
See also
boolSimps.bool_ss,
Rewrite.PURE_REWRITE_TAC,
simpLib.SIMP_CONV,
simpLib.SIMP_TAC