Is there a way to dynamically retrieve the name of variables in Isabelle/HOL?
I am trying to do something like this (in a simplified version):
consts sa :: "nat set"
sb :: "nat set"
axiomatization where
sa_fin: "finite sa"
and sb_fin: "finite sb"
definition expand :: "nat set set ⇒ string set" where
"expand S = {nameof(s)| s. s ∈ S}"
Basically, for the U below
definition U :: "nat set set" where "U = {sa, sb}"
the expand function will return {"sa", "sb"}. Is it possible at all within Isabelle/HOL? TIA
In general, no. Your expand function cannot exist as a HOL function because you did not assume anywhere that sa and sb are distinct. If they are the same, there logically cannot be a function rhat returns ''sa'' for sa and ''sb'' for sb.
Of course, if you do know that sa ≠ sb you can easily define a function that does this manually, e.g. nameof x = (if x = sa then ''sa'' else ''sb''). Generating a function like this automatically for a given set of constants is possible in Isabelle/ML. Finding all constants that were declared in a given theory should also be possible in Isabelle/ML.
But all of this seems a bit odd to me. I would wager that whatever you are trying to do here is probably possible in a more direct way. It's hard to say more without knowing what your exact use case is.