[isabelle-dev] Functional type theory

[Makarius]

On Wed, 31 Jul 2013, Makarius wrote:

> * Type theory is now immutable, without any special treatment of
> drafts or linear updates (which could lead to "stale theory" errors in
> the past).  Discontinued obsolete operations like Theory.copy,
> Theory.checkpoint, and the auxiliary type theory_ref.  Minor
> INCOMPATIBILITY.

Here are some further explanations on this:

Tools may now update a theory value locally in arbitrary ways, i.e. to 
explore certain situations that are given up later on (e.g. to see if a 
type may be declared without producing an error).

What does *not* work is to update the background theory of some proof 
context, and then continue deriving results from it.  There is no "export" 
from such adhoc theory extensions, so the result would live in the 
extended theory and cannot be transferred back. This also explains why 
theory and Proof.context are different things, and why a background theory 
is not a proper context. (Interestingly, Coq has only one context, and 
tools occasionally extend that globally during proof construction, leading 
to great confusion and bad performance.)

This fine point about theory update is also relevant to 
Context_Position.set_visible_global: solve_direct can afford changing the 
theory locally to silence certain internal operations, since it merely 
retrieves existing results without deriving results.  General proof tools 
(e.g. tactics) cannot do that since the final result needs to be from the 
original theory.


 	Makarius