[isabelle] Reflexive rewriting


I occasionally run into problems where a simplification rule leads to infinite reflexive rewriting, e.g. if I have a constant f and a rule like "f ?x 1 = f 0 1", then the simplifier will loop on goals like "f x 1 = f y 1", since "f 0 1" will get rewritten to itself infinitely often.

I know how to fix this with NO_MATCH, but my question is this: why do we not introduce a check in the simplifier that prevents it from rewriting a term to itself? I don't know much about the simplifier, but I should be surprised if such a check were difficult to implement, and I do not think there would be a significant loss of performance. It also should not break any existing proofs or code.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.