[isabelle-dev] generating fresh variables in Isabelle/ML
makarius at sketis.net
Sun Aug 5 16:04:33 CEST 2012
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:
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 =
> val ctxt' = fold Variable.declare_term ts ctxt
> singleton (Variable.variant_frees ctxt' ) ("x", dummyT)
> 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.
More information about the isabelle-dev