I'm trying to generate fresh names (which can be executed). The idea is to keep track of the prev. used names and to pick the `smallest`

element, see.

```
definition fresh :: "'a :: linorder set ⇒ 'a × 'a set" where
"fresh used = (let f = LEAST x. x ∉ used in (f, insert f used))"
```

The simple example works as expected

```
lemma "fresh {1::nat} = x"
apply (simp add: fresh_def)
```

but when starting at 0

```
lemma "fresh {0::nat,1} = x"
apply (simp add: fresh_def)
```

I do get the following goal:

```
proof (prove)
goal (1 subgoal):
1. (let f = LEAST x. 0 < x ∧ x ≠ Suc 0 in (f, {f, 0, Suc 0})) = x
```

So, why is the first part of the goal given by `0 < x ∧...`

and not `x ≠ 0 ∧...`

?

```
lemma ‹n ≠ (0:: nat)›
supply [[simp_trace]]
apply simp
oops
```

shows that the culprint is `thm neq0_conv`

.

It is declared is `iff`

rule

So:

```
(simp add: fresh_def del: neq0_conv)
```

How do you handle infinite sets in `fresh`

?

like `UNIV:: 'a :: linorder set`

This makes sense, is `supply`

similar to `using [[...]]`

?

In my specific use-case, the set is always finite.

Yes for supply

For the finite case: sure, but won't that make it impossible to make the code executable?

I'm surprised `Least`

is executable at all. It can't be efficient.

Well no by default but if the set is finite you can iterate over it to find the first missing value…

I'd recommend using something like `if X = {} then 0 else Suc (Max X)`

instead.

… or directly remember the upper bound `N`

on the indices and use `{0..N}`

whenever you need the set

But: both approaches create holes in the indices (if you also remove some indices)

Yes, but you're going to have to supply custom code equations for this.

Frankly, I'd just use the `Max`

approach. Easier to reason about, and you get executability for free.

this case is limited to nat, I was hoping to use strings as well... Or I could use `of_char`

while parsing and `to_char`

for printing?

The side of me that proves things agrees with you Manuel… but the side that generates fast code strongly disagrees with you ;-)

(Little-known fact, `Sup`

also exists for `nat`

s and is executable. It's basically the same as `Max`

, except that `Max {}`

is undefined while `Sup ({} :: nat set) = 0`

).

Mathias Fleury said:

The side of me that proves things agrees with you Manuel… but the side that generates fast code strongly disagrees with you ;-)

Well sure, it's better to just remember the max index in the first place.

I was simply arguing for `Max`

over `Least`

.

Fresh name generation is always a pain

For strings, the obvious approach is to just use some string encoding of numbers as all your variable names.

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

Otherwise, one can do a "name variant" approach, i.e. start with some "desired" name and then append stuff to it (e.g. `'`

or `a`

, `b`

, `c`

, etc.) until you find one that isn't taken yet.

Robert Soeldner said:

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

I don't understand what you mean.

Manuel Eberl said:

Robert Soeldner said:

Manuel Eberl said:

Fresh name generation is always a pain

This is good to know. What would be the keyword to check if I want to encode strings while parsing and later, back, while printing ?

I don't understand what you mean.

Isnt there an option to instruct Isabelle to encode strings to nats while parsing? This would allow me to work with nat internally

I don't really understand what it is you're trying to do here. Are you developing an Isabelle tool?

why would there be a default option to encode strings as nat?

(such bijection exists because countable)

Mathias Fleury said:

why would there be a default option to encode strings as nat?

not a default, but user supplied.

Not that I know of

Manuel Eberl said:

I don't really understand what it is you're trying to do here. Are you developing an Isabelle tool?

I started developing a verification framework for the graph programming language GP2. Especially the logic given in https://arxiv.org/abs/2012.01662v1

When I needed a mapping from string to nat, I used a hashmap and a fresh index …

I'm still very new to Isabelle, your comments are highly appreciated.

In short: I used the refinement framework to go from a string version to a nat version with the mapping because some operations required to the original string (sorting on the strings)

But the Refinement Framework might be overkill for you

Yea, I will initially take the `Max`

approach and might ask again :-)

You could presumably replace all the string variables with natural-number variables in a (possibly unverified) pre-processing step.

Last updated: Sep 25 2022 at 22:23 UTC