[isabelle] Strange simplifier behaviour



Hallo,

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?

Cheers,

Manuel
theory Foo
imports Complex_Main
begin

consts 
  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)

notepad
begin
  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 *)
    done
end

end


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