[isabelle] simp fails on rewriting with "âx :: 'a. f x â a â f x = x"
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"
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
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