Re: [isabelle] finite set syntax


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

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.