[isabelle] qed and done take long for large goal states



Dear Isar experts,

I am looking for ways to speed up the processing of some of my Isar proofs. Something I noticed is that when there are no subgoals left, "done" and "qed" nevertheless take between 2 and 7 seconds of processing (according to the Isabelle timing panel in jEdit).

I guess that the delays must have something to do with the size of the statement being proved. They only occur for large proof states. For example, large elimination rules (with approx. 20 cases) or the cases for induction proves about functions defined with partial_function. The delays are particularly annoying for the latter case, because each induction proof has many subcases and the delay occurs for each of the subcases.

Are there any options or tweaks to speed up the processing of qed/done?

As the delays also appear inside proofs (i.e., not for top-level lemma statements), I suspect that attributes and propagation of facts to locale interpretations are not to be blamed.

My machine is still the usual one:

Linux lenovoal 3.13.0-91-generic #138-Ubuntu SMP Fri Jun 24 17:00:34 UTC 2016 x86_64 x86_64 x86_64 GNU/Linux
Intel(R) Core(TM) i7-3630QM CPU @ 2.40GHz
16GB of RAM

Thanks in advance,
Andreas




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