*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Storing theorems on the fly*From*: Ognjen Maric <ognjen.maric at gmail.com>*Date*: Wed, 28 Nov 2012 18:25:17 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1211281336480.26964@macbroy21.informatik.tu-muenchen.de>*References*: <50B5FA16.8090607@gmail.com> <alpine.LNX.2.00.1211281336480.26964@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/17.0 Thunderbird/17.0

On 11/28/2012 01:44 PM, Makarius wrote: > 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). I'm not immediately certain if they will work in my scenario, but they look very useful, thanks. I didn't know they were there. > 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). 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. 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. > 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.) Thanks, this isn't such an important point for my application anyway. Ognjen

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

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

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

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

- Previous by Date: Re: [isabelle] Storing theorems on the fly
- Next by Date: Re: [isabelle] Storing theorems on the fly
- Previous by Thread: Re: [isabelle] Storing theorems on the fly
- Next by Thread: Re: [isabelle] Storing theorems on the fly
- 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