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.