Re: [isabelle] Failing simproc



On Wed, 18 Jul 2012, Dmitriy Traytel wrote:

I stumbled upon some funny behaviour which prevents the simplifier in proving "True" in Isabelle2012 (also in 8a1ef12f7e6d). The reduced example is attached.

theory Simproc_Fail
imports Main
begin

notepad
begin
  have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
  hence True apply simp sorry
end

end

This is a hard crash, not a tactic failure. Generally, goal states with polymorphic content (schematic type variables) are pathologic; many proof tools will choke on them. It is of the "don't do it then category": posing goals with schematic type variables is asking for trouble.

Above this happens above after piping the "this" fact into the True goal via the "insert" phase of simp. Instead of 'using' polymoprhic facts, typically those from the background library, one should "add" them somehow to the automated tools, e.g. (simp add: ...), (auto simp add: ...), (auto iff: ...) ...


Anyway, did you have a concrete application where unresolved types in goals were required, or was it just one of the common accidents to get them via bad luck?

This incident remindes me again that I wanted to work out some refined color scheme for term variables with unexpected poloypmorphism, potentially with some extra tool tips apart from the coloring.


	Makarius





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