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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and