Re: [isabelle] Storing theorems on the fly

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.


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