[isabelle] Storing theorems on the fly



Hi all,

I'm writing some Isabelle/ML code which, given a term, generates
theorems about it. This is essentially a recursive function which
generates theorems for the subterms and then combines them. A single
subterm might appear many times, and I'd like to store the generated
theorems to avoid repeating the work. 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:

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?

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

Thanks,
Ognjen






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