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

You should check out (eg in the manual) how the type system in
Isabelle/HOL works.

Propositions like "x \<in> UNIV" are trivial, because x gets inferred
some type, and UNIV is the set of all elements of this type.

If you write "green", then green is just a variable (of type color).

--
Peter

On Sa, 2015-06-27 at 18:17 +0200, Roger H. wrote:
>
> >  -"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.