# [isabelle] Reflexive rewriting

Hallo,

`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.
`
Cheers,
Manuel

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