[isabelle-dev] NEWS: More robust (and more strict) treatment of abstractions within the context

Makarius makarius at sketis.net
Tue Oct 19 22:00:10 CEST 2021

*** ML ***

* Term operations under abstractions are now more robust (and more
strict) by using the formal proof context in subsequent operations:


This works under the assumption that terms are always properly declared
to the proof context (e.g. via Variable.declare_term). Failure to do so,
or working with the wrong context, will cause an error (exception Fail,
based on Term.USED_FREE from Term.dest_abs_fresh).

The Simplifier and equational conversions now use the above operations
routinely, and thus require user-space tools to be serious about the
proof context (notably in their use of Goal.prove, SUBPROOF etc.).
INCOMPATIBILITY in add-on tools is to be expected occasionally: a proper
context discipline needs to be followed.

* Former operations Term.dest_abs and Logic.dest_all (without a proper
context) have been discontinued. INCOMPATIBILITY, either use
Variable.dest_abs etc. above, or the following operations that imitate
the old behavior to a great extent:


This works under the assumption that the given (sub-)term directly shows
all free variables that need to be avoided when generating a fresh name.
A violation of the assumption are variables stemming from the enclosing
context that get involved in a proof only later.

This refers to Isabelle/7f06e317fe25 + AFP/0cfcfc7a85ea.

The actual change is rather minor, but it required several days to go through
old (and some new) applications that still did not work with the proof context
correctly, e.g. see https://isabelle-dev.sketis.net/rISABELLE8ee3d5d3c1 for
HOL-Nominal or https://isabelle-dev.sketis.net/rAFPe1f8faf5261f for AFP/Simpl.

The new setup will prevent such inaccurate treatment of contexts in the
future, because it fails rather quickly on bad situations --- with a proper
error instead of just a warning from > 15 years ago


More information about the isabelle-dev mailing list