Re: [isabelle] Datatype + cardinality + polymorphismus?

```Sorry to repeat myself, but you really do need to read the documentation. Then you will be able to define f within Isabelle itself, and then you might find that Isabelleâs automation will make this example quite easy.

Larry Paulson

> On 27 Jun 2015, at 18:54, Roger H. <s57076 at hotmail.com> wrote:
>
> 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!
>>>
>>
>

```

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