Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: More robust (and more strict) treatm...


view this post on Zulip Email Gateway (Oct 19 2021 at 20:00):

From: Makarius <makarius@sketis.net>
* ML *

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.

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
https://isabelle-dev.sketis.net/rISABELLE7df8abe926c3

Makarius


isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 04 2024 at 10:08 UTC