Re: [isabelle] Datatype + cardinality + polymorphismus?



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)


--
  Peter





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