remove_ssfrags
simpLib.remove_ssfrags : string list -> simpset -> simpset
Removes named simpset fragments from a simpset.
A call to remove_ssfrags fragnames simpset returns a simpset that is
the same as simpset except that the simpset fragments with names in
the list fragnames are no longer included. As a special case, the
empty name "" matches all unnamed fragments within simpset and
causes them to be removed.
Failure
If no member of fragnames names a fragment in simpset, the
Conv.UNCHANGED exception is raised.
Example
> SIMP_CONV (srw_ss()) [] “MAP ($+ 1) [3;4;5]”;
val it = ⊢ MAP ($+ 1) [3; 4; 5] = [1 + 3; 1 + 4; 1 + 5]: thm
> val myss = simpLib.remove_ssfrags ["REDUCE"] (srw_ss());
Exception- UNCHANGED raised
> SIMP_CONV myss [] “MAP ($+ 1) [3;4;5]”;
Exception- Value or constructor (myss) has not been declared
Fail "Static Errors" raised
Comparison with exclude_ssfrags
remove_ssfrags only strips matching fragments from the simpset's
history; a subsequent ss ++ FRAG_ss would re-add them. By contrast,
exclude_ssfrags also records the exclusion in the simpset itself, so
that subsequent ++ of a fragment with one of the named names is a
silent no-op (until cleared via force_add / SF). exclude_ssfrags
also never raises Conv.UNCHANGED. The Proof[exclude_frags = ...]
attribute uses exclude_ssfrags.
See also
simpLib.exclude_ssfrags,
simpLib.force_add,
BasicProvers.diminish_srw_ss