[isabelle] Trying to implement conditional skip-proofs, need advice.



Hello there.

I've been using Isabelle for some while, and have become a tad frustrated with the amount of time which is spent re-running proof scripts as I move from file to file. Many of these proofs have been unchanged in my repository for years now, and have presumably been re-executed thousands of times.

The idea is to use the proof-recording mechanism to get a list of dependencies when a theorem is proved, which goes in to some kind of cache. When a theorem is stated, we can check whether it hits anything in the cache, and if so, whether the assumptions exist in the current context and match term-for-term. If all of this is true, we can skip the proof, since it would probably have succeeded anyway. It's not perfect, and you'd certainly have to do regression tests regularly, but it could make a big difference to the cost of manipulating a large proof repository.

The checks seem fairly straightforward, but I'm stuck on hooking this thing into Isar. It's fairly clear that the hook for skipping the proof should be in begin_proof in toplevel.ML, where skip_proofs is checked already. The information available at this point (in a Proof.state) does not, however, tell us exactly what the final theorem will look like. Instead we have an intermediate theorem and a list of assumptions.

One option was to work entirely in terms of the intermediate theorem, giving us a good match for our skip hook. However, in a proof that ends "by auto", the final Proof.state, the one manipulated by end_proof, is the one that existed before auto was run, and doesn't have a complete list of dependencies.

The next step down the abstraction chain seems to be to try to work with a Context.proof, at which point the just-proved theorem seems to become
anonymous, and I get totally lost.

Does anyone have a sensible idea for where to put the hook for trapping
completed theorems? Additionally, if this is done after the theorem is
converted from its intermediate to its final form, is there an easy way to check one against the other? (This may be a related question, since one thing we can certainly do when deciding whether to skip is to skip and complete the proof, and see what gets caught at our hooks).

I appreciate that this may not be possible, and will be interested in the discussion regardless.

Yours,
	Thomas.





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