Re: [isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"



You are both right. The "X" violates the golden rule, and the violation is so blatant that the simplifier ignores that rule altogether. It would take a bit of work to emit a warning.

Tobias

On 08/06/2015 16:43, Lars Noschinski wrote:
On 08.06.2015 16:34, Jasmin Blanchette wrote:

The rule âXâ appears to violate the golden rule of thumb when using
âsimpâ, i.e. that both the rhs and the preconditions should be simpler
than the lhs (see Section 2.5.3 of Concrete Semantics). Surely, âf x
~= aâ is not simpler than âf xâ. That bad things happen then doesnât
surprise me so muchâ Cheers, Jasmin

It is only simpler insofar as that it is literally part of the
assumptions. I would not have been surprised if the simplifier had
started looping -- after all, it is not really simpler. But refusal to
rewrite does not yet fit into my mental model of the simplifier.


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



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