# Re: [isabelle] Cardinality for infinite sets

```Dear Manuel,

thank you for the hint! This is exactly what I was trying to do.
However, while doing so, I observed something which I do not understand. Maybe one of you Isabelle experts can help here?

First, I define an extended version of ecard, such as the following (for simplicity I leave out the infinite case here):

definition ecard:: "('a set) ⇒ enat"
where "ecard S ≡ enat (card S)"

So the definition actually just lifts the result of card to enat.

Now, if I try to proof the following lemma (the lifted version of card_0_eq from Finite_Set):

lemma ecard_0_eq:
assumes "finite Z"
and "enat (card Z) = enat 0"
shows "Z = {}"

nitpick tells me that it found a counterexample:

> Nitpick found a counterexample for card 'a = 2:
> Free variable:
>   Z = {a⇩2}

However, I can also come up with a simple proof for the lemma.

Moreover, if I try to confirm the counterexample with the following lemma:

lemma test:
"enat (card {a⇩2}) = enat 0"

nitpicks finds again a counterexample to its counterexample (as expected).

Does someone understand the counterexample generated for lemma ecard_0_eq here?

Many thanks and best regards,

Diego

-----Ursprüngliche Nachricht-----
Von: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] Im Auftrag von Manuel Eberl
Gesendet: Donnerstag, 22. März 2018 15:08
An: cl-isabelle-users at lists.cam.ac.uk
Betreff: Re: [isabelle] Cardinality for infinite sets

Hallo,

a less involved solution would be to define a cardinality function that returns an extended natural number (from Extended_Nat in HOL-Library).

definition ecard :: "'a set ⇒ enat" where
"ecard A = (if finite A then card A else ∞)"

Of course, there will be no library of facts for this (yet).

Manuel

On 2018-03-21 19:19, Diego Marmsoler wrote:
> Dear Isabelle experts,
>
> while playing around with "card" from theory Finite_Set, i recognized that it returns 0 for infinite sets.
> Now i was wondering whether someone knows about a similar construct which, for this case, returns infinity from the extended natural numbers.
>