Re: [isabelle] Storing theorems on the fly

On Wed, 28 Nov 2012, Ognjen Maric wrote:

They can of course be threaded through, but I haven't been able to come up with an elegant way to express it in this case. A stateful solution would be straightforward, though (that is, once you offload all the worries about potential concurrency issues and whatnot to somebody else :) At any rate, it's just an annoyance, not a showstopper.

I wouldn't use "stateful" and "straightforward" in the same sentence. Even without the omnipresent parallelism in Isabelle, it is better to say explicitly how you fiddle with your values and updated environment.

See again section 0.3 "Canonical argument order" in -- it is one of the success stories of Isabelle/ML. We gradually eloborated this purely functional combinator style for aesthetic reasons over the years, and later we found ourselves in the lucky situation to be able to get on the multicore train early, with minimal cleanup of the code base.

Sequentialism is a very strong assumption that is better not imposed on any serious program today.

Concretely, I prove refinement between monadic programs (I'm aware of Peter's AFP entry). In my particular case, the data refinement typically affects a few primitive "procedures", for which I prove refinement (manually). More complex procedures are then built by combining these with monadic operations. Their refinement proofs are straightforward (and tedious). Basically unfold their definitions, build refinement theorems for the components, combine them appropriately and fold the definitions inside the resulting theorems. It is these theorems I'd like to cache (since the "intermediate" procedures can appear many times), and eventually also export into the context, so that they can be used later on in other "top-level" proofs.

I've seen the AFP entry Refine_Monadic occasionally from a distance, but am not familiar with it.

Generally, it depends a lot how you want to organize things, or rather how you need to organize things.

Within a tactical expression or Isar proof method, you can access the Proof.context only as a local immutable value (of course it can be updated in a functional manner). The context might contain funny quasi-functional elements, such as lazy values or caches of values, but that is semantically still functional. You cannot have a tactic do some ad-hoc poking in a non-monotonic manner.

Within a proof, you can have commands updating the context according to its block structure. The most basic approach is to make an attribute (see the 'attribute_setup' command in the isar-ref manual) and use that with 'note' or other fact producing commands in the proof. Whatever you do, it will be local to the proof. Proofs are formally irrelevant, i.e. you cannot export anything from them. The main result is specified before, and already determined before commencing the proof.

Within the theory context, you can have commands of the form "theory -> theory" or "local_theory -> local_theory". You can store whatever you want in the theory context, as long as it is plain functional data in any of the senses above.

You could try to move results you discover within a proof back to the toplevel context, by exporting it in some logical obvious way.

In a trivial manner, this happens all the time when you work with Isabelle:

   lemma B
        fix x
        assume "A x"
        txt {* Oh, I need "lemma C x" *}

At that point you merely go back in the text and prepend this *before* it:

    fixes x
    assumes "A x"
    shows "C x"

with its proof. So you re-assemble the text in the editor, without funny tricks about implicit context extension in the middle of the other proof.

In more specific, or more complex situations, one could consider making this assembly of properly ordered proof documents supported by some tool. It is up to your imagination.


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