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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and