[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