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

[Christian Sternagel]

On 08/05/2012 11:04 PM, Makarius wrote:
> 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.
Thanks for the precise explanation.

> What is right depends on the context.  What is your application?
My application is list comprehension, i.e, the context is exactly as in 
lc_tr.

cheers

chris