Re: [isabelle] Instantiating to a lambda expression



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


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
>  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.