[isabelle] Instantiating to a lambda expression



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





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