*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] finite set syntax*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Wed, 14 Feb 2007 13:45:00 +0100*Cc*: Temesghen Kahsai <lememta at gmail.com>*In-reply-to*: <D83FFAB1-B1F2-4D2D-84BC-6F48BC689325@gmail.com>*References*: <D83FFAB1-B1F2-4D2D-84BC-6F48BC689325@gmail.com>*User-agent*: KMail/1.8

Temesghen, On Tuesday 13 February 2007 22:25, Temesghen Kahsai wrote: > 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. 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

**References**:**[isabelle] finite set syntax***From:*Temesghen Kahsai

- Previous by Date: Re: [isabelle] defining a constant with a long-identifier name
- Next by Date: Re: [isabelle] checking if a formula is intuitionistically valid
- Previous by Thread: Re: [isabelle] finite set syntax
- Next by Thread: [isabelle] defining a constant with a long-identifier name
- Cl-isabelle-users February 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list