# 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
``http://isabelle.in.tum.de/dist/Isabelle2012/doc/implementation.pdf -- 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:
lemma
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.
`
Makarius

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