Re: [isabelle] code generation for saturated naturals

Hi Peter,

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.

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.

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.

Thanks a lot for your contribution.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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