removing individual rewrites from a simpset

[xrchz]

It would be nice to be able to remove things from simpsets (especially for interactive development, or when ensuring something does not get added in the first place is infeasible). For arbitrary conversions this may be impossible without a significant performance penalty (applying the filter every time the simpset is used). But for rewrite theorems, it should be possible to remove them outright by matching against the conclusion of the theorem.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

Anthony's commit is definitely a step in the right direction, but I think it would be nice to be able to remove by name too. The simpLib code already allows for conversions to be named, but rewrites are currently just all called <rewrite>. If we extended the internal APIs a bit so that theorems added via export_rewrites got added with names, it should then be relatively easy to pull them out by name as well. (The names should probably be theory$name forms of course.)

One change I'd make to the commit in b02e20a would be to remove by LHS rather than the full statement of the theorem. It's easy enough to get from theorem to LHS, and if there's something annoying happening with a particular pattern it'd be easier to simply turn that LHS off rather than have to figure out which theorem it is that is acting on that term.

[xrchz]

What happens when there are multiple theorems with the same LHS? Should this trigger a warning or error (if it doesn't already)?

[mn200]

Just remove them all. I don't believe having multiple theorems with the same LHS is likely, but you could always put back ones that you did want.