Re: [isabelle] Storing theorems on the fly

> 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.

Sounds interesting. I have a similar problem, when trying to
automatically refine terms to more executable versions (replacing sets
by red-black-trees, etc.). Once the basic operations are proven,
refining more complex terms is straightforward. However, in order to
refine a term that contains defined constants (procedures in your
speaking), one either has to prove a separate refinement lemma for each
constant manually, or unfold all such constants beforehand (one then
gets one big term, and looses the structure), or do something like you
propose, i.e., extract those constants from the term first, and
automatically generate refined versions.

We have experimented with the first two options already, and they are
not too bad for our use-cases. For the third option, I thought about
implementing it as an outer-level command, something like: 
  "refine constant as name", that would generate the refinement of
constant (and, recursively, of all constants used in the term that need
to be unfolded), then define a new constant name, and generate a
refinement lemma name.refine: "new-constant refines constant".

Note the similarity of this problem to code generation: Also the
code-generator collects code-theorems for constants and, recursively,
for constants that are used in those code-theorems.


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