Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] finite set syntax

Email Gateway (Aug 18 2022 at 10:10):

From: Temesghen Kahsai <lememta@gmail.com>
Hi all,

Is there a way to have a quantification over a finite set of names;
something like

ALL (finite name B) P.

P is another type. I am confused about the syntax of the finite set
in HOL.

In list would be something like:

ALL (B :: name list) P.

Thanks in advance for any help.

-T

Email Gateway (Aug 18 2022 at 10:10):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Temesghen Kahsai wrote:

Hi all,

Is there a way to have a quantification over a finite set of names;
something like

ALL (finite name B) P.

Not really sure if I got your point, but

ALL B . finite B --> P

would do the job for finite sets B.

Hope it helped
Peter Lammich

P is another type. I am confused about the syntax of the finite set in
HOL.

In list would be something like:

ALL (B :: name list) P.

Thanks in advance for any help.

-T

Email Gateway (Aug 18 2022 at 10:11):

From: Tjark Weber <tjark.weber@gmx.de>
Temesghen,

I'm not quite sure what you're asking for, but you can write

"\<forall>x\<in>A. P x",

where A is an arbitrary set. E.g. you can write

"\<forall>x\<in>{a,b,c}. P x"

to express that "P a", "P b" and "P c" all hold. If you need to use
lists, a function called "set" takes a list and returns the set of its
elements:

"\<forall>x\<in>set [a,b,c]. P x"

Best,
Tjark

Last updated: May 03 2024 at 08:18 UTC