# Re: [isabelle] Datatype + cardinality + polymorphismus?

```Or rather
1.datatype color = red |blue
fun f:: color => nat setf red = {1}f blue = {2}
how do i prove
lemma "(âx. f x) = {1,2}"  ?
Thank you.
From: s57076 at hotmail.com
To: isabelle-users at cl.cam.ac.uk
Subject: RE: [isabelle] Datatype + cardinality + polymorphismus?
Date: Sat, 27 Jun 2015 19:19:29 +0200

> I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.

Thank you Larry, this is a clear answer for one of my questions.
My other questions were:
1. Assume I have
datatype color = red |blue
fun f:: color => nat setf red = {1}f blue = {2}
definition M :: "nat set" whereM = the union...over all x in color...of  f(x)     //the result should be M = {1} union {2} = {1,2}
I dont know how to write the implementation of M in isabelle syntax.

2. card (color) = 2 ? or size (color) = 2  ?  I am looking for the name of the function that gets a type and returns its number of constructors  (for such simple finite non-recursive types)

Thank you!

> Subject: Re: [isabelle] Datatype + cardinality + polymorphismus?
> From: lp15 at cam.ac.uk
> Date: Sat, 27 Jun 2015 18:02:46 +0100
> CC: isabelle-users at cl.cam.ac.uk
> To: s57076 at hotmail.com
>
> I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed.
>
> Larry Paulson
>
>
> > On 27 Jun 2015, at 12:22, Larry Paulson <lp15 at cam.ac.uk> wrote:
> >
> > Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website http://isabelle.in.tum.de/documentation.html.
> >
> > Larry Paulson
> >
> >
> >> On 27 Jun 2015, at 12:06, Roger H. <s57076 at hotmail.com> wrote:
> >>
> >> Hello,
> >> 1. If i have datatype color = red | blue
> >> how do i write smth like
> >> -"is c in color"...meaning "is c an instance of color?"
> >> -"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
> >> -length function..number of elements in the datatype .. so that it returns here length (color) = 2
> >> 2. How do i write a function which maps different instances of the datatype to subsets of different types(like nat and bool):
> >> f :: color -> ??red |-> {1,2}blue |-> {True}
> >> cause range f = UNIV isnt right.
> >> Many thanks!
> >
>
```

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