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.
>>
>> Many thanks in advance!
>>
>> Best regards,
>>
>> Diego
> 




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