[isabelle] Datatype + cardinality + polymorphismus?



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.