Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 11:03):

From: "Roger H." <s57076@hotmail.com>
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!

Email Gateway (Aug 19 2022 at 11:03):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 19 2022 at 11:03):

From: René Thiemann <rene.thiemann@uibk.ac.at>
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!

Last updated: Apr 23 2024 at 08:19 UTC