Email Gateway (Oct 19 2021 at 20:00): Email Gateway (Oct 19 2021 at 20:00):From: Makarius <makarius@sketis.net>
* ML *
Term operations under abstractions are now more robust (and more
strict) by using the formal proof context in subsequent operations:
Variable.dest_abs
Variable.dest_abs_cterm
Variable.dest_all
Variable.dest_all_cterm
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:
Term.dest_abs_global
Logic.dest_all_global
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: Jul 15 2022 at 23:21 UTC