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.