[isabelle-dev] generating fresh variables in Isabelle/ML

[Makarius]

On Sat, 4 Aug 2012, Christian Sternagel wrote:

> in changeset 206144b13849, we can (still) find the following lines in 
> List.thy (which seem to indicate that this is not the right way to 
> introduce a fresh variable):
>
>  (* FIXME proper name context!? *)
>  val x =
>    Free (singleton (Name.variant_list
>      (fold Term.add_free_names [p, e] [])) "x", dummyT);

The origin of the comment is:

changeset:   43324:2b47822868e4
user:        wenzelm
date:        Thu Jun 09 16:34:49 2011 +0200
discontinued Name.variant to emphasize that this is old-style / indirect;

There were two instances of it: in lc_tr (list comprehension) and case_tr 
(datatype case syntax).

Both translations are still not exactly right concerning scoping of bound 
variables.  What is also missing is support for formal source positions, 
but that is a different story.


In isolation, the above changeset is merely another move away from very 
old-fashioned operations that are often wrong in contempory Isabelle. 
Name.variant used to be *the* way to generate fresh names wrt. a list of 
"used" names > 10 years ago.  Now the problem is often that "used" 
contains too little information (lacking the full context); it is also too 
concrete as a data structure to get it right and efficient in practice.

So "proper name context" above means first just type Name.context with 
corresponding operations. Second, it could mean to refer to the standard 
context with its Name.context obtained by Variable.names_of, or operations 
directly on Proof.context.

Note that syntax translations are somewhat special and often more direct 
Name.context coverage of the visible pre-term material is right, without 
taking the full logical context into account. For logical tools standard 
context operations are usually better, e.g. Variable.variant_fixes.

BTW, the implementation manual has sections both on module Name and 
Variable, with the most prominent operations listed in the text.


> If this is not the right way to do it, I was wondering, whether the 
> following was:
>
>  fun fresh_var ts ctxt =
>    let
>      val ctxt' = fold Variable.declare_term ts ctxt
>    in
>      singleton (Variable.variant_frees ctxt' []) ("x", dummyT)
>    end
>
>  val x = Free (fresh_var [p, e] ctxt)

What is right depends on the context.  What is your application?

Above you produce a fresh free variable that is apart from some terms and 
the logical context.  The variable is not yet fixed, but could be made so 
by Variable.add_fixes_direct.  Alternatively, one could use 
Variable.variant_fixes or similar, to get fixed variables apart from the 
context on the spot, or just Variable.add_fixes and relying on the 
implicit renaming policy of the context.

Specifically for the list compresion and case syntax, one needs to look 
again very closely how this could be done.  It is really "done" once there 
are no FAQs needed for it, and the formal position markup produces the 
correct scope information.


 	Makarius