Re: [isabelle] Instantiating to a lambda expression



On Sat, Jan 15, 2011 at 5:55 PM, Lawrence Paulson <lp15 at 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
>>  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.