[isabelle-dev] generating fresh variables in Isabelle/ML
c-sterna at jaist.ac.jp
Mon Aug 6 03:46:06 CEST 2012
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
More information about the isabelle-dev