Robert Soeldner (Jul 18 2021 at 17:56): Robert Soeldner (Jul 18 2021 at 17:56):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 ∧...?
Mathias Fleury (Jul 18 2021 at 18:01):lemma ‹n ≠ (0:: nat)›
supply [[simp_trace]]
apply simp
oops
shows that the culprint is thm neq0_conv.
Mathias Fleury (Jul 18 2021 at 18:01):It is declared is iff rule
Mathias Fleury (Jul 18 2021 at 18:02):So:
(simp add: fresh_def del: neq0_conv)
How do you handle infinite sets in fresh?
Mathias Fleury (Jul 18 2021 at 18:05):like UNIV:: 'a :: linorder set
Robert Soeldner (Jul 18 2021 at 18:06):This makes sense, is supply similar to using [[...]] ?
In my specific use-case, the set is always finite.
Mathias Fleury (Jul 18 2021 at 18:07):Yes for supply
Mathias Fleury (Jul 18 2021 at 18:07):For the finite case: sure, but won't that make it impossible to make the code executable?
Manuel Eberl (Jul 18 2021 at 18:07):I'm surprised Least is executable at all. It can't be efficient.
Mathias Fleury (Jul 18 2021 at 18:08):Well no by default but if the set is finite you can iterate over it to find the first missing value…
Manuel Eberl (Jul 18 2021 at 18:08):I'd recommend using something like if X = {} then 0 else Suc (Max X) instead.
Mathias Fleury (Jul 18 2021 at 18:09):… or directly remember the upper bound N on the indices and use {0..N} whenever you need the set
Mathias Fleury (Jul 18 2021 at 18:10):But: both approaches create holes in the indices (if you also remove some indices)
Manuel Eberl (Jul 18 2021 at 18:10):Yes, but you're going to have to supply custom code equations for this.
Manuel Eberl (Jul 18 2021 at 18:11):Frankly, I'd just use the Max approach. Easier to reason about, and you get executability for free.
Robert Soeldner (Jul 18 2021 at 18:11):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?
Mathias Fleury (Jul 18 2021 at 18:12):The side of me that proves things agrees with you Manuel… but the side that generates fast code strongly disagrees with you ;-)
Manuel Eberl (Jul 18 2021 at 18:12):(Little-known fact, Sup also exists for nats and is executable. It's basically the same as Max, except that Max {} is undefined while Sup ({} :: nat set) = 0).
Manuel Eberl (Jul 18 2021 at 18:12):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.
Manuel Eberl (Jul 18 2021 at 18:12):I was simply arguing for Max over Least.
Manuel Eberl (Jul 18 2021 at 18:13):Fresh name generation is always a pain
Manuel Eberl (Jul 18 2021 at 18:13):For strings, the obvious approach is to just use some string encoding of numbers as all your variable names.
Robert Soeldner (Jul 18 2021 at 18:14):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 ?
Manuel Eberl (Jul 18 2021 at 18:14):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.
Manuel Eberl (Jul 18 2021 at 18:15):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.
Robert Soeldner (Jul 18 2021 at 18:16):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
Manuel Eberl (Jul 18 2021 at 18:17):I don't really understand what it is you're trying to do here. Are you developing an Isabelle tool?
Mathias Fleury (Jul 18 2021 at 18:17):why would there be a default option to encode strings as nat?
Mathias Fleury (Jul 18 2021 at 18:18):(such bijection exists because countable)
Robert Soeldner (Jul 18 2021 at 18:18):Mathias Fleury said:
why would there be a default option to encode strings as nat?
not a default, but user supplied.
Mathias Fleury (Jul 18 2021 at 18:20):Not that I know of
Robert Soeldner (Jul 18 2021 at 18:20):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
Mathias Fleury (Jul 18 2021 at 18:21):When I needed a mapping from string to nat, I used a hashmap and a fresh index …
Robert Soeldner (Jul 18 2021 at 18:22):I'm still very new to Isabelle, your comments are highly appreciated.
Mathias Fleury (Jul 18 2021 at 18:24):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)
Mathias Fleury (Jul 18 2021 at 18:24):But the Refinement Framework might be overkill for you
Robert Soeldner (Jul 18 2021 at 18:25):Yea, I will initially take the Max approach and might ask again :-)
Manuel Eberl (Jul 18 2021 at 18:29):You could presumably replace all the string variables with natural-number variables in a (possibly unverified) pre-processing step.
Last updated: Dec 21 2024 at 16:20 UTC