Re: [isabelle] Invariants on free vs. fixed variables in simplifier / proof tools

On 09/10/2019 22:26, Norbert Schirmer via Cl-isabelle-users wrote:

> I wonder if I have either encountered a bug in the simplifier or otherwise I was 
> breaking some assumptions / invariants on the relation of free variables in a term
> vs. fixed variables in the context.
> I did not find the answer in the implementation manual, hence my question here:
> Are there any assumptions / invariants / (strong) guidelines on the usage of 
> free vs. fixed variables in the simplifier (or other proof tools in general) ?
> I have rules in mind like:
> * Fix every free variable in the context before calling a proof tool.
> * Always set the 'body' flag in the context before calling a proof tool.
> * Declare a term to the context before calling a proof tool.

I will look at your examples in detail later, but here are some abstract

Generally, you should make your formal items as official in the context
as possible: the minimum is a variant of Variable.declare_term, but it
is better to use Variable.add_fixes or similar to make it really right.
Sometimes the latter is not possible for historical reasons.

There are many intermediate situations for variables in the context, for
the sake of old tools that don't register properly in the context. It
would be better to be really strict about demanding everything to be
properly "fixed" in the context, but this will break some old tools.

Ah, and the word "bug" has not meaning in the Isabelle context:
everything is so complex that we can only talk about behaviour that is
expected / unexpected, simple / complex, desirable / undesirable,
changeable / unchangeable (for now).

The usual strategy of survival is to do things in a "canonical" way,
including certain context disciplines. (Example: normally you should
*not* change context flags like "is_body": that belongs to the system
infrastructure, not the user-space tools).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.