Re: [isabelle] prove countability of a new finite type



Dear Roger,

> the theory Countable in HOL/Library, which also defines the countable class, provides the method countable_datatype to prove instantiations of countable for datatypes automatically.

You can also import Datatype_Order_Generator/Derive from the AFP where this method 
(and other methods) are accessible to derive certain properties automatically.

derive countable Colors (* uses method mentioned by Andreas, solves exactly your problem *)
derive linorder Colors 
...

see Derive_Examples for more examples.

Hope this helps,
René


> On 28/05/13 00:24, Roger H. wrote:
>> Hello,
>> 
>> 
>> i define
>> 
>> 
>> datatype Colors = Red | Yellow | Green
>> 
>> 
>> How can i prove:
>> 
>> 
>> instance Colors :: countable
>> 
>> 
>> ?
>> 
>> 
>> Mathematically, id say the type is finite, so i would give an injection to the natural numbers. can you help me in isabelle?
>> 
>> 
>> Many thanks!
>>  		 	   		
>> 
> 

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck





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