# Re: [isabelle] eta-contracted definitions and unfolding

Hello Peter,
unfolding tries to rewrite the goal using the provided rewrite rules.

`Both definitions generate theorems f_def and g_def where the function
``constant f or g must be applied to two arguments if the rewrite is
``supposed to happen. This behaviour is useful because one sometimes wants
``to rewrite e.g. only if the function is given its two parameters.
`
> definition "f' x y ≡ x + y"
> definition "g' x y ≡ y + x"
>
> lemma "f' = g'"
> unfolding f_def g_def
> sorry

`I suppose you mean "unfolding f'_def ang g'_def here, f_def and g_def
``should not have any effect on the goal anyway.
`
> In my particular cases I can use extensionality, but I'm keen to know
> if there are alternatives.

`The definition package also generates another theorem called
``<constant>_def_raw, i.e. in your case f'_def_raw and g'_def_raw which
``lambda-abstract over all supplied parameters, i.e
`
thm f'_def_raw gives
f' == op +

`and unfolding works with these, but you will still have a hard time to
``prove f' = g' because the arguments' type is not fixed to nats, so
``commutativity does not hold.
`
Regards,
Andreas

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