Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generating fresh variable names


view this post on Zulip Email Gateway (Aug 19 2022 at 17:24):

From: Andrew Gacek <andrew.gacek@gmail.com>
I'm trying to write a function in Isabelle/HOL to generate a fresh
variable name (given a finite set of used names). I'm having trouble,
in part, because proving termination for the function requires knowing
that the set is finite (I don't care about the function output when
infinite). Does anybody have a suggestion about how to proceed?

I was hoping to create a function like

fresh_string :: string set => string => string

That might work like

fresh_string {''A'', ''B'', ''A0'', ''A1''} ''A'' = ''A2''

That is, the second argument is used as a base for the generated
variable name. And the theorem I'd want to prove is

finite xs ==> fresh_string xs y \notin xs

This is the closest I've come, but I'm not hopeful about being able to
prove termination:

fun string_of_nat :: "nat ⇒ string"
where
"string_of_nat n = (if n < 10 then [char_of_nat (48 + n)] else
string_of_nat (n div 10) @ [char_of_nat (48 + (n mod 10))])"

fun fresh_string_aux :: "string set ⇒ string ⇒ nat ⇒ string" where
"fresh_string_aux xs y n = (if finite xs then
(if y @ string_of_nat n ∈ xs then
fresh_string_aux xs y (Suc n)
else
y @ string_of_nat n)
else
undefined)"

fun fresh_string :: "string set ⇒ string ⇒ string" where
"fresh_string xs y = fresh_string_aux xs y 0"

The reason for all this is that I'm writing a function that will
require fresh variable names and I'd like to be able to actually
execute that function and get readable results.

Thanks,
Andrew

view this post on Zulip Email Gateway (Aug 19 2022 at 17:25):

From: Peter Lammich <lammich@in.tum.de>
Hi,

find attached what we use in CoCon
(http://www21.in.tum.de/~popescua/rs3/CoCon.html) to generate fresh IDs.
The function "fresh" there exactly matches your signature, and
is executable.

The formalization of "fresh" is mostly by Andrei Popescu.
Fresh.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 17:26):

From: Tobias Nipkow <nipkow@in.tum.de>
My recommendation in such situations is to use a list rather than a set. Of
course the callers of fresh_string will also need to use lists, and so on. But
since function "set" converts a list into a set, the change is usually not very
painful.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Aug 19 2022 at 17:27):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Andrew,

you can find a theory "Name" in the IsaFoR-repository.
It contains fresh-name generators for strings like the ones you desire.
(fresh_string, fresh_string_list, ...)

Hope this helps,
René

PS: IsaFoR/CeTA is freely available under http://cl-informatik.uibk.ac.at/software/ceta/

view this post on Zulip Email Gateway (Aug 19 2022 at 17:29):

From: Peter Lammich <lammich@in.tum.de>

The function "fresh" there exactly matches your signature

Oops, function fresh there actually uses a list, rather than a set:
fresh :: string list => string => string


Last updated: Mar 28 2024 at 20:16 UTC