*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Datatype + cardinality + polymorphismus?*From*: Roger H. <s57076 at hotmail.com>*Date*: Sat, 27 Jun 2015 18:17:34 +0200*Importance*: Normal*In-reply-to*: <BAY179-W8843DB1B6A95438B6E842F8FAC0@phx.gbl>*References*: <BAY179-W69F3F04876BC324F1120B78FAC0@phx.gbl>, <126A5885-E7A2-4648-B6CA-EEF271A229C5@cam.ac.uk>, <BAY179-W8843DB1B6A95438B6E842F8FAC0@phx.gbl>

> -"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) >

**Follow-Ups**:**Re: [isabelle] Datatype + cardinality + polymorphismus?***From:*C. Diekmann

**Re: [isabelle] Datatype + cardinality + polymorphismus?***From:*Peter Lammich

**References**:**[isabelle] Datatype + cardinality + polymorphismus?***From:*Roger H .

**Re: [isabelle] Datatype + cardinality + polymorphismus?***From:*Larry Paulson

- Previous by Date: Re: [isabelle] Accessing ML terms in Isabelle theory
- Next by Date: Re: [isabelle] Datatype + cardinality + polymorphismus?
- Previous by Thread: Re: [isabelle] Datatype + cardinality + polymorphismus?
- Next by Thread: Re: [isabelle] Datatype + cardinality + polymorphismus?
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list