Email Gateway (Aug 23 2022 at 08:19): Email Gateway (Aug 23 2022 at 08:19):From: Randy Pollack <rpollack@inf.ed.ac.uk>
I don't understand the point of (this appears as a class declaration
in Enum.thy):
locale enum =
fixes enum :: "'a list"
fixes enum_all :: "('a ⇒ bool) ⇒ bool"
fixes enum_ex :: "('a ⇒ bool) ⇒ bool"
assumes UNIV_enum: "UNIV = set enum"
and enum_distinct: "distinct enum0"
assumes enum_all_UNIV: "enum_all P ⟷ Ball UNIV P"
assumes enum_ex_UNIV: "enum_ex P ⟷ Bex UNIV P"
It seems to say "give me a distinct list that covers a finite
type, and I will return a finite enumerated set."
The following seems more general without loss:
locale enum =
fixes enum :: "'a list"
fixes enum_all :: "('a ⇒ bool) ⇒ bool"
fixes enum_ex :: "('a ⇒ bool) ⇒ bool"
assumes enum_distinct: "distinct enum"
assumes enum_all_UNIV: "enum_all P ⟷ Ball (set enum) P"
assumes enum_ex_UNIV: "enum_ex P ⟷ Bex (set enum) P"
It seems to say "give me any distinct list of any type, and I will
return a finite enumerated set."
Does the official declaration have something to do with its use as a
class? I'm using enum as part of specifying a notion of "language" (a
finite ordered set), and I want to talk about extending the language
with new symbols, which the official declaration doesn't seem to
cover.
--Randy
Email Gateway (Aug 23 2022 at 08:19):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
At least the way we’re using it in l4v, the reason is indeed its use as a class, where we want the code generator and other tools to know how to enumerate all values of a type. I assume the idea is the same for the Isabelle distribution.
It might be possible to divorce the two or to make a two-stage definition. First the one you have at the bottom, and then the one at the top as a class, assuming UNIV_enum in addition.
Cheers,
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC