Email Gateway (Aug 18 2022 at 16:56): Email Gateway (Aug 18 2022 at 16:56):From: John Munroe <munddr@gmail.com>
Hi,
If i have
consts
foo :: "real => real"
bar :: "real => real"
and an axiom
same_ax: "ALL (g1::real=>real) g2 x y. (y > x & g1 y - g1 x = g2 y -
g2 x) --> g1 = g2"
I can get a proof quite fine with:
lemma lem1: "foo = bar"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y - bar x"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 - bar r1"
by auto
then show ?thesis
using same_ax
by auto
qed
However, if I change the type of bar to:
bar :: "real => real => real", the following won't go through:
lemma lem1: "ALL x. foo x = bar x 3"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 3 - bar r1 3"
by auto
then show ?thesis
using same_ax
by auto
How come g1 or g2 can't be instantiated to %x. bar x 3, which is of
type real=>real?
Thanks
John
Email Gateway (Aug 18 2022 at 16:56):From: Lawrence Paulson <lp15@cam.ac.uk>
My guess is that this instantiation is possible, but it's asking too much to expect the automation to invent this lambda-expression.
Larry Paulson
Email Gateway (Aug 18 2022 at 16:56):From: John Munroe <munddr@gmail.com>
On Sat, Jan 15, 2011 at 5:55 PM, Lawrence Paulson <lp15@cam.ac.uk> wrote:
My guess is that this instantiation is possible, but it's asking too much to expect the automation to invent this lambda-expression.
I see. Could you please suggest a way to proceed in this proof?
Thanks
John
Larry Paulson
On 15 Jan 2011, at 15:52, John Munroe wrote:
Hi,
If i have
consts
foo :: "real => real"
bar :: "real => real"and an axiom
same_ax: "ALL (g1::real=>real) g2 x y. (y > x & g1 y - g1 x = g2 y -
g2 x) --> g1 = g2"I can get a proof quite fine with:
lemma lem1: "foo = bar"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y - bar x"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 - bar r1"
by auto
then show ?thesis
using same_ax
by auto
qedHowever, if I change the type of bar to:
bar :: "real => real => real", the following won't go through:
lemma lem1: "ALL x. foo x = bar x 3"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 3 - bar r1 3"
by auto
then show ?thesis
using same_ax
by autoHow come g1 or g2 can't be instantiated to %x. bar x 3, which is of
type real=>real?Thanks
John
Email Gateway (Aug 18 2022 at 16:56):From: Tjark Weber <webertj@in.tum.de>
On Sat, 2011-01-15 at 15:52 +0000, John Munroe wrote:
If i have
consts
foo :: "real => real"
bar :: "real => real"and an axiom
same_ax: "ALL (g1::real=>real) g2 x y. (y > x & g1 y - g1 x = g2 y -
g2 x) --> g1 = g2"
Axioms are evil. It's all too easy to introduce inconsistencies.
Here's a proof of False from same_ax:
lemma "False"
apply (cut_tac same_ax)
apply (drule_tac x="%x. 0" in spec)
apply (drule_tac x="%x. 1" in spec)
apply (auto dest: fun_cong)
done
(The problem is that the scope of x and y in same_ax extends all the way
to the end of the formula.)
However, if I change the type of bar to:
bar :: "real => real => real", the following won't go through:
lemma lem1: "ALL x. foo x = bar x 3"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 3 - bar r1 3"
by auto
then show ?thesis
using same_ax
by auto
Here's a proof of lem1 that's similar to the one you provided:
lemma lem1: "ALL x. foo x = bar x 3"
proof -
have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3"
sorry
then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar
r2 3 - bar r1 3"
by auto
then show ?thesis
using same_ax[rule_format, of _ _ _ "%x. bar x 3"]
by (auto dest: fun_cong)
qed
Kind regards,
Tjark
Last updated: Apr 25 2024 at 08:20 UTC