*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Cardinality for infinite sets*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Fri, 23 Mar 2018 09:46:14 +0100*In-reply-to*: <60a22954-3969-4264-9645-a667cc1aa769@BADWLRZ-SWMBB05.ads.mwn.de>*References*: <k95lpx89oaxbqbvi65al88gd.1521656361918@email.android.com> <022a1c8d-1a62-333f-c44b-b8bd801e7be3@in.tum.de> <60a22954-3969-4264-9645-a667cc1aa769@BADWLRZ-SWMBB05.ads.mwn.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

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 >

**References**:**[isabelle] Cardinality for infinite sets***From:*Diego Marmsoler

**Re: [isabelle] Cardinality for infinite sets***From:*Manuel Eberl

**Re: [isabelle] Cardinality for infinite sets***From:*Diego Marmsoler

- Previous by Date: Re: [isabelle] global_interpretation and code generation
- Next by Date: Re: [isabelle] Implicitly referring to previous facts in the moreover-ultimately paradigm
- Previous by Thread: Re: [isabelle] Cardinality for infinite sets
- Next by Thread: [isabelle] Error Building HOL-Word
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list