Re: [isabelle] code generation for saturated naturals



Hi Peter,

the theory is in regression:
http://isabelle.in.tum.de/testboard/Isabelle/rev/fe33d6655186

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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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