Re: [isabelle] Reflexive rewriting

I agree with Makarius, although I suspect there wouldn't be many broken proofs. On the other hand I am sure it would impact performance noticeably. Now that we have NO_MATCH, I am reluctant to add a special case to the simplifier code.


On 13/07/2015 14:24, Makarius wrote:
On Mon, 13 Jul 2015, Manuel Eberl wrote:

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.

I am also not an expert on the Simplifier myself, but by default the blind
assumptions above need to be inverted. Just empirically, any tiny change
anywhere will cause lots of unexpected problems in obscure places.

This does not mean, reforms should not be done -- we do it all the time. But it
usually takes really long and hard work to push a change through.


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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