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.