Re: [isabelle] eta-contracted definitions and unfolding



On Wed, 8 Apr 2009, Peter Gammie wrote:

I've got a few definitions that are supposed to be partially applied, and unfolding them when they are eta-contracted and unsaturated fails (silently in the case of 'unfolding'). I am surprised this doesn't work in Isabelle2008, e.g.:

definition "f' x y ≡ x + y"
definition "g' x y ≡ y + x"

lemma "f' = g'"
unfolding f_def g_def
sorry

end

Has Isabelle always behaved like this?

Yes, unfortunately. It is high time to make unfold/unfolding really "unfold" definitions completely, and not to imitate regular simplification so much (where it is important to observe argument patterns as originally given).

For now you can use the following workaround:

  lemma "f' = g'"
    unfolding f_def_raw g_def_raw ...

This should work, but is not ideal, because it refers to internals of the 'definition' package. On the other hand it is easily cleaned up at a later stage when we provide proper unfolding by default.


	Makarius


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