Re: [isabelle] Datatype + cardinality + polymorphismus?



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.