Re: [isabelle] Storing theorems on the fly

On Wed, 28 Nov 2012, Ognjen Maric wrote:

A single subterm might appear many times, and I'd like to store the generated theorems to avoid repeating the work.

This part in isolation sounds like an application of Thm.cterm_cache or Thm.thm_cache, i.e. it is semantically plain function application with operational tuning for re-use earlier values (in a thread-safe way, with a little overhead).

Clearly, they could be manually threaded through the recursive calls, but I'd like to avoid doing the plumbing myself, especially since I'd like to be able to retrieve them later (outside of the function) as well.

So I assume I should be using one of the context.*_Data structures to
store the theorems in an Item_Net (indexed by the terms). Questions:

1. Right now I'm trying to do this from an ML {* *} block within Isar
text, using Generic_Data and then storing the generated theorems with
Context.>>. However, it appears that the theorems only actually get
stored after the whole ML {* *} block is executed. Is this a feature,
and if so, how to get around to it?

Sounds all too much like implicit destructive stateful programming to me, i.e. not what you normally do in Isabelle/ML.

What are you trying to achieve concretely?

The normal way is to "thread through" values, usually using the Isabelle/ML combinators for that (variations on |> and fold/map/fold_map as explained in the implementation manual). This also avoids the seeming Context.>> problem above (ML commands have their own linear context that can be updated implicitly -- at compile-time, not run-time).

2. Could this be done within a proof tactic, and how?

Probably not. Depends what you actually need. Tactical proof steps cannot change the context. (I am very glad for that, now that I know how messy this is in other major provers on the market.)


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