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.