Re: [isabelle] code generation for saturated naturals


On 08/09/2011, at 8:00 AM, Florian Haftmann wrote:

> the theory is in regression:

Great, thanks.

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