Re: [isabelle] Strange eta-expansion on induction



On Thu, 1 Mar 2012, Tobias Nipkow wrote:

The induct method itself does not eta-contract or expand. It merely uses
primitives, in particular resolution, which in turn uses higher-order
unification. And higher-order unification does indeed eta-expand. In
certain situations. This is intentionally not fixed and you should not
expect or rely on a particular behaviour. That is, you may have to
ensure eta-contraction yourself if some part of your proof method is
sensitive to it.

Tobias

Am 01/03/2012 18:53, schrieb Peter Lammich:

I recently encountered a quite strange behavior of the induct method. It
seems to arbitrarily eta-expand its subgoals under certain conditions
(If the induction variable is nested inside higher-order context ???).

As Tobias points out, the Pure Isabelle system conceptually works modulo eta (and beta and alpha) conversion -- although there are well known traps. So to continue the thread, I would also like to see the other part -- the proof tool by Peter that fails here.


	Makarius





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