Re: [isabelle] eta-contracted definitions and unfolding
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and