From isar-ref.pdf, page 267, it gives the following notes on try0
and try
:
- try0 attempts to prove a subgoal using a combination of standard proof methods (auto, simp, blast, etc.). Additional facts supplied via simp:, intro:, elim:, and dest: are passed to the appropriate proof methods.
- try attempts to prove or disprove a subgoal using a combination of provers and disprovers (
solve_direct
,quickcheck
,try0
,sledgehammer
,nitpick
).
So if the description is complete in the Isar Reference manual, then try
is try0
plus two provers, solve_direct
and sledgehammer
, and two counterexample finders, quickcheck
and nitpick
.
To not run the provers of try0
, as far as I know, you would have to run solve_direct
and sledgehammer
individually.
If try0
is hanging the PIDE, then it's mostly likely going into a bad loop of some kind, where enabling Auto Methods
in Plugin Options / Isabelle
can also cause these loops, since it does something similar to try0
.
There are two kind of loops that I've experienced, where I can only remember the 2nd one listed next as hanging the PIDE:
simp
rule loops caused bysimp
or methods that callsimp
, such asauto
,force
,fastforce
,slowsimp
, andbestsimp
. To stop an infinite loop, I just have to delete the command.blast
loops caused byauto
callingblast
. For these kind, it either happens immediately, or after I've let the command run for 5 seconds or so.
You can try to narrow down which automatic proof method is causing try0
and try
to hang the PIDE.
You can get a list of the try0
methods used like this (I don't know if the list of provers it shows is complete):
lemma "False"
try0
(*Trying "simp", "auto", "fast", "fastforce", "force", "blast", "metis",
"linarith", and "presburger"...*)
oops
From that list, if apply(simp)
is looping, you know there's a simp
rule loop (or simp
rules that take a long time to complete), which would make auto
, fastforce
and force
loop, since they call simp
.
If auto
is looping, then it could be simp
or blast
, since auto
can call each of those, so you can try apply(blast)
to see if blast
is the problem.
With Isabelle2013-2, for me, the hanging of the PIDE has been because of auto
, because it calls blast
. Supposedly, that has been fixed for the next release.