Email Gateway (Aug 18 2022 at 13:21): Email Gateway (Aug 18 2022 at 13:21):From: Peter Gammie <peteg42@gmail.com>
Hello,
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.:
theory t
imports Main
begin
constdefs
f :: "nat ⇒ nat ⇒ nat"
"f x y ≡ x + y"
g :: "nat ⇒ nat ⇒ nat"
"g x y ≡ y + x"
lemma "f = g"
unfolding f_def g_def
sorry
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?
In my particular cases I can use extensionality, but I'm keen to know
if there are alternatives.
Thanks,
Peter.
Email Gateway (Aug 18 2022 at 13:21):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 13:21):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting Makarius <makarius@sketis.net>:
There is another workaround that I have used before. You can just use
an eta-expanded version of your lemma, like this:
definition "f' x y = x + y"
definition "g' x y = y + x"
lemma foo: "(%x y. f' x y) = (%x y. g' x y)"
unfolding f'_def g'_def
sorry
Also note that the eta-expanded version of a lemma will work anywhere
the eta-contracted version will, for example:
lemma bar: "f' = g'"
by (rule foo)
Email Gateway (Aug 18 2022 at 13:21):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Last updated: May 03 2024 at 04:19 UTC