*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 19:54:24 +0200*Importance*: Normal*In-reply-to*: <BAY179-W60DE56E9344D20FF82E2CF8FAC0@phx.gbl>*References*: <BAY179-W69F3F04876BC324F1120B78FAC0@phx.gbl>, <126A5885-E7A2-4648-B6CA-EEF271A229C5@cam.ac.uk>, <C905135B-ABF8-4E50-A319-6F87116B9700@cam.ac.uk>, <BAY179-W60DE56E9344D20FF82E2CF8FAC0@phx.gbl>

Or rather 1.datatype color = red |blue fun f:: color => nat setf red = {1}f blue = {2} how do i prove lemma "(âx. f x) = {1,2}" ? Thank you. From: s57076 at hotmail.com To: isabelle-users at cl.cam.ac.uk Subject: RE: [isabelle] Datatype + cardinality + polymorphismus? Date: Sat, 27 Jun 2015 19:19:29 +0200 > I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed. Thank you Larry, this is a clear answer for one of my questions. My other questions were: 1. Assume I have datatype color = red |blue fun f:: color => nat setf red = {1}f blue = {2} definition M :: "nat set" whereM = the union...over all x in color...of f(x) //the result should be M = {1} union {2} = {1,2} I dont know how to write the implementation of M in isabelle syntax. 2. card (color) = 2 ? or size (color) = 2 ? I am looking for the name of the function that gets a type and returns its number of constructors (for such simple finite non-recursive types) Thank you! > Subject: Re: [isabelle] Datatype + cardinality + polymorphismus? > From: lp15 at cam.ac.uk > Date: Sat, 27 Jun 2015 18:02:46 +0100 > CC: isabelle-users at cl.cam.ac.uk > To: s57076 at hotmail.com > > I assume that you are talking about Isabelle/HOL (rather than, say, Isabelle/ZF). This is a typed formalism. The property of having a certain type is not a boolean formula, but is part of what it means for a term to be well-formed. > > Larry Paulson > > > > On 27 Jun 2015, at 12:22, Larry Paulson <lp15 at cam.ac.uk> wrote: > > > > Many of your questions are answered by the documentation. You will find it all in the documentation panel of an Isabelle session, or at the website http://isabelle.in.tum.de/documentation.html. > > > > Larry Paulson > > > > > >> On 27 Jun 2015, at 12:06, Roger H. <s57076 at hotmail.com> wrote: > >> > >> 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?" > >> -"for all c in color: bla bla" ... whats the "in"? cause the "element of" symbol is wrong > >> -length function..number of elements in the datatype .. so that it returns here length (color) = 2 > >> 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} > >> cause range f = UNIV isnt right. > >> Many thanks! > > >

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

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

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

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

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

- Previous by Date: Re: [isabelle] Automatic simplification of lambda terms of tuples
- 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