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

Hi Lars,

>      assume X: "âx :: 'a. f x â a â f x = xâ

> Here, "simp add: X" fails, even though all its premises can be solved by
> "assumption" -- or, as the second line shows, by "simp". Has anyone got
> an idea why this is the case?

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â



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