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

Hi everyone,
today I stumbled upon some behaviour of simp I don't understand.
Consider the following simple theory
theory Scratch imports Main begin
consts P :: "bool"
consts f :: "'a â 'a"
notepad begin
fix a b :: 'a
assume X: "âx :: 'a. f x â a â f x = x"
have "f b â a â f b = b"
apply (simp add: X)
apply (subst X) apply simp_all
done
sorry
end
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?
Looking at the the simp trace, one seees that the simplifier tries
recursively to rewrite the premis "f x ~= a". This fails ultimately. But
I would have expected it trying to solve the premis by assumption, then.
-- Lars 'simp is not simple' Noschinski

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