# [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.*