*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Storing theorems on the fly*From*: Peter Lammich <lammich at in.tum.de>*Date*: Thu, 29 Nov 2012 10:58:38 +0100*In-reply-to*: <50B648FD.7080705@gmail.com>*References*: <50B5FA16.8090607@gmail.com> <alpine.LNX.2.00.1211281336480.26964@macbroy21.informatik.tu-muenchen.de> <50B648FD.7080705@gmail.com>

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

**References**:**[isabelle] Storing theorems on the fly***From:*Ognjen Maric

**Re: [isabelle] Storing theorems on the fly***From:*Makarius

**Re: [isabelle] Storing theorems on the fly***From:*Ognjen Maric

- Previous by Date: Re: [isabelle] syntax translation
- Next by Date: [isabelle] nat_code Equation
- Previous by Thread: Re: [isabelle] Storing theorems on the fly
- Next by Thread: [isabelle] ITP 2013: First Call for Papers
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list