Re: [isabelle] Recommended use of try and try0



Am 08.03.2013 um 08:14 schrieb Lars Noschinski <noschinl at in.tum.de>:

>> When "try0" says that, e.g. "by fastforce" is the fastest way to prove
>> something, does this automatically mean that I should _use_ "by
>> fastforce"?  Or are there hidden traps?
> 
> Using "by fastforce" in this case is perfectly fine. Keep in mind that the timings may vary.

I should add that the timings can be off, since we're using threads intensively. Sometimes it says 11 ms for blast and 12 ms for auto when the actual numbers are more like 1 ms for blast and 2 ms for auto. Take these timings with a grain of salt, as upper bounds.

>> More generally, is it a recommended practice to occasionally revisit my
>> proofs, replace "by<some automated method>" by "try" everywhere, and
>> then generally use the proof methods that "try" recommends?
> 
> If you have a working proof which is robust and not too slow I don't see any need to revisit this proof.

If you have the feeling that your theory is processed slowly, you can spend some time doing that. I've achieved significant gains for Andrei Popescu and Dmitriy Traytel's formalization of cardinals, by turning on global timing and trying various things (often manually, sometimes with try0 or try). But if you're happy with the processing speed, there's no reason to bother.

Jasmin






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