[isabelle-dev] copying contexts
makarius at sketis.net
Wed Dec 2 14:07:27 CET 2009
On Wed, 2 Dec 2009, Lucas Dixon wrote:
> I'm wondering what the right way to copy contexts is. I remember there
> was some references lingering in theories, mostly as unique identifies
> if I remember correctly, but it meant that copying needed to be an
> explicit function. Is this the right way to copy a context:
> Context.map_theory Context.copy_thy
> and so copying a proof context would be:
> Context.proof_map (Context.map_theory Context.copy_thy)
(ML names below refer to the forthcoming Isabelle2009-1 release, e.g. see
The theory type has indeed a double role of providing
(1) formal certificates of a general background context,
(2) default values for content of context data.
Any other formal entities (certified types, terms, theorems etc.) can
maintain a back-reference to that using type theory_ref. The theory
referenced here can evolve monotonically later on. This means we assume
monotonicity of formal correctness wrt. the background context. (This
holds for the basic logical entities, but user concepts that are certified
against theories need to observe this as well.) The Theory.copy primitive
is able to produce a detached side-branch of this linear/monotonic
evolution of certificates. Theory.checkpoint provides another way to
produce a stable stepping stone that can be forked into independent
developments later (the Isar toplevel already checkpoints theory states at
transaction boundary, i.e. before and after each Isar command.)
Luckily, user code rarely has to care about any of this. The reason: most
of the time one works with a Proof.context, not a raw theory. In this
standard setup, user data is maintained via functor Generic_Data,
sometimes Proof_Data, but hardly ever raw Theory_Data.
When working with Proof.context, the usual way of operation is to update
that (purely functionally) on the surface. The background theory
certificate is still there, and might evolve monotonically without further
notice, and usually you don't care.
There are some special situations, where updates on the background theory
do need to be propagated to the surface context, notably in the
implementation of local_theory mechanisms. The ProofContext.theory and
Local_Theory.theory combinators take care of the formal fiddling required
in such situations.
> The reason I want to do this is that when proof planning proves new
> theorems it creates some meta-data which gets stored in the context. I
> want to be able to make a copy the context before I modify any such data
> so that I can compare alternatives and do fair tests. I was previously
> using my own generic context, but would like to cut down code
I would say you merely need to use functor Generic_Data in the usual way:
purely functional content, no copy operations ever. See
src/Pure/Tools/named_thms.ML for a typical example.
BTW, background theories still do support mutable content, which
Theory.copy would take care of if the user data implements it accodingly.
As of Isabelle2009-1 mutable data is essentially a legacy feature, though:
due to performance reasons in an increasingly parallel and asynchronous
environment, mutable state is very expensive.
More information about the isabelle-dev