Email Gateway (Apr 24 2025 at 09:18): Email Gateway (Apr 24 2025 at 09:18):From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Isabelle users,
I would have a question for you, as follows.
The following command:
value "{0 :: nat} Un {1}"
outputs:
"{0, 1}"
:: "nat set"
However, the following command:
value "{a :: nat} Un {b}"
outputs:
"set (List.insert a [b])"
:: "nat set"
whereas the following command:
value [simp] "{a :: nat} Un {b}"
outputs:
"set (if b = a | a : {} then [b] else [a, b])"
:: "nat set"
Upon using the value command, or the @{value} antiquotation, to compute a
finite set such as {a :: nat} Un {b}, I wonder whether there is any way to
rather obtain an output in the same form as the one resulting from the first
command above, namely:
"{a, b}"
:: "nat set"
Do you know whether this is possible, and how? For example, is it possible to
pass an assumption such as "a ~= b" to the command or to the antiquotation, or
else to tell them to allow for the possible presence of multiple occurrences
of the same element in their output?
Thank you very much, best regards,
Pasquale Noce
Last updated: May 06 2025 at 08:28 UTC