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


>  -"is c in color"...meaning "is c an instance of color?"
> Exactly the c's of type color are in color.  > The set of all colors is "UNIV :: color set".
1. My question is how can i write this kind of predicate:
(red \in color)   .................which is of type bool
I dont know it yet, since
"red ∈ (UNIV :: color set)" doesnt seem the right way to write it, since for
--datatype color = red | blue
lemma "red ∈ (UNIV :: color set)" is proven true,--
but also
lemma "green ∈ (UNIV :: color set)" is also true..which should be false.  ??

2. Concerning the cardinality... how do i prove the following
lemma "card( UNIV :: color set) = 2"
Cause by simp, this just simplifies in :    "card UNIV = 2"
Thank you!

On Sa, 2015-06-27 at 13:06 +0200, Roger H. wrote: Hi.
> 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?"
Exactly the c's of type color are in color.   The set of all colors is "UNIV :: color set".

> -"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong
Just "ALL c::color. P c". Here, the ::color is a type constraint, which forces the bound variable "c" to have type color, but is not explicitly visible in the parsed term.

> -length function..number of elements in the datatype .. so that it returns here length (color) = 2
It's "card( UNIV :: color set)", provided color is a finite type.

> 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}

This is not possible in HOL's type system. An approximation would be     f :: color => nat+bool   Here, nat+bool is the sum type, that has the   elements Inl (n::nat) and Inr (b::bool) >


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