Re: [isabelle] Recommended use of try and try0



On 08.03.2013 00:07, Christoph LANGE wrote:
I learned about the "try" and "try0" tools to search for proof methods.
  Now I wonder what's the right way of using them.

Some of the proof methods in Isabelle are pretty similar on a higher level, but have different strengths (in particular auto/fastforce/force). try0 was invented so that one does not need to try all the different calls by hand.

Reporting the timing is only a nice side effect, so one can easily distinguish fast and slow proofs, not necessarily find "the fastest".

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.

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.

  -- Lars





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