*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Datatype + cardinality + polymorphismus?*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sat, 27 Jun 2015 19:10:42 +0200*In-reply-to*: <BAY179-W7B8FADA4272A999BD73B08FAC0@phx.gbl>*References*: <BAY179-W69F3F04876BC324F1120B78FAC0@phx.gbl> , <126A5885-E7A2-4648-B6CA-EEF271A229C5@cam.ac.uk> , <BAY179-W8843DB1B6A95438B6E842F8FAC0@phx.gbl> <BAY179-W7B8FADA4272A999BD73B08FAC0@phx.gbl>

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

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

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

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

- Previous by Date: Re: [isabelle] Datatype + cardinality + polymorphismus?
- 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