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.
have "(\<And>ys zs. length ys < Suc (length zs + length ys))" by simp
hence True apply simp sorry
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and