[isabelle] Strange simplifier behaviour
I found that the simplifier fails to apply certain simplification rules
when I would have expected it to. This occurs both in the development
version and Isabelle 2014. (see attachment)
I suspect it has something to do with higher-order unification. Is there
some kind of workaround?
F :: "('a \<Rightarrow> 'a) \<Rightarrow> 'c"
definition "g x = x"
lemma F_g: "F (\<lambda>x::'a. f (g x)) = F (\<lambda>x::'a. f x)"
by (simp add: g_def)
have "F (\<lambda>x::'a. g x) = F (\<lambda>x::'a. x)"
(* apply (simp only: F_g) <- does not work *)
apply (subst F_g, rule refl) (* <- works *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and