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

Hi 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.


On 28/05/13 00:24, Roger H. wrote:

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!

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