Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] locale enum?


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC