Re: [isabelle] code generation for saturated naturals
On 08/09/2011, at 8:00 AM, Florian Haftmann wrote:
> the theory is in regression:
>> 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.
> 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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and