HomeIsabelle/Phabricator
More robust (and more strict) treatment of abstractions within the context

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.

Written by makarius on Oct 19 2021, 9:46 PM.
User
Projects
None
Subscribers
None

Event Timeline