Stream: Beginner Questions

Topic: countably infinite

Robert Soeldner (Oct 05 2023 at 10:13):

Is there a typeclass for countably infinite types?

I've tried the following:

class countably_infinite = countable +
  assumes "∀n. ∃(x::'a). to_nat x = n"

(Also some variations with x::'a::countable, ..., as this definition is rejected from Isablle):

Type unification failed: Variable 'a::type not of sort countable

Failed to meet type constraint:

Term:  λx. to_nat x = n :: ??'b ⇒ bool
Type:  'a ⇒ ??'a

Or with countable:

Additional type variable(s) in locale specification "countably_infinite": 'a
Type variable has two distinct sorts
The error(s) above occurred in axiom "class.countably_infinite_def"

Dmitriy Traytel (Oct 05 2023 at 10:42):

to_nat is defined outside the countable class, so it does not exist without the sort constraint. You could try

class countably_infinite = countable +
  assumes cinf_surj: "∀(n :: nat). ∃(x::'a). Eps inj x = n"

lemma "∀n. ∃(x::'a :: countably_infinite). to_nat x = n"
  unfolding to_nat_def by (rule cinf_surj)

(And indeed there is no such type class. Not even one for just infinite types. If there was, one could use the sort {countable, infinite}.)

Robert Soeldner (Oct 05 2023 at 10:46):

this makes sense, thank you @Dmitriy Traytel
Is there any particular reason this is not part of the HOL library, or was it just not needed? I'm asking to ensure I'm not going into a rabbit hole :-)

Dmitriy Traytel (Oct 05 2023 at 10:54):

I needed something like that in a recent (not-yet-published) formalization of mine. There I defined the type of countably infinite sets 'a cinfset. In the type definition, I used predicates countable and infinite and to prove non-emptiness 'a has to be infinite, so I created a type class for infinite types locally (my formulation was using cardinals and required a bit more that was useful in my context). Having an infinite type class in the library would make sense IMO.

Last updated: Apr 27 2024 at 20:14 UTC