# Re: [isabelle] Cardinality for infinite sets

```Dear Diego,

sorry not an answer, just nitpicking ;)
I get the message:

Nitpick found a potentially *spurious* counterexample

I am curious as to why you get a different message.

My point being: With the above message I wouldn't care too much, since
Nitpick already tells you that the counterexample might not be good.
(Maybe, for some reason, it is just constructing a counterexample to "Z
= {}".)

cheers

chris

On 03/22/2018 04:59 PM, Diego Marmsoler wrote:
> 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.
>>