Re: [isabelle] code generation for saturated naturals



Am 08/09/2011 00:12, schrieb Peter Gammie:
>>> I did this - see the attached. Thanks very much to sledgehammer for doing the most boring bits!
>>
>> Well, the first one(s) did not really perform well, but it was not very
>> difficult to get along without it.
> 
> What do you mean by "the first one(s)"? Lemmas, sledgehammers, ... ?
> 
>> I'm not speaking against sledgehammer, but when you prove fundamental
>> things it is often better to try with less erratic methods like simp,
>> auto etc – this will both increase your understanding of the matter as
>> well as give hints which fundamental rules are still missing.  In
>> application with more rather technical lemmas, sledgehammer is very fine.
> 
> I found sledgehammer very useful for discovering the lemmas needed for the proofs. I agree that the final proofs could be presented better.

I agree with both Florian and Peter: s/h is great for discovering useful
lemmas, and it can be beneficial both for performance and legibility to
transform the generated metis proofs into auto. (But one can easily
waste time on unsuccessful attempts to do so.)

Tobias

>> After the next Isabelle release you might want to add also
>>
>> instantiation sat :: (len) complete_lattice
>>
>> but AFAIS this will require more lemmas about fold.
> 
> You've lost me here - the final instantiation in the theory is precisely this one.
> 
>> Thanks a lot for your contribution.
> 
> Thanks to you and Brian for developing the theory!
> 
> cheers
> peter
> 





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