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.

Best,
Andreas

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!
  		 	   		





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