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



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.




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