*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Cardinality for infinite sets*From*: Diego Marmsoler <diego.marmsoler at tum.de>*Date*: Thu, 22 Mar 2018 15:59:00 +0000*Accept-language*: en-US*Authentication-results*: postout.lrz.de (amavisd-new); dkim=pass (2048-bit key) reason="pass (just generated, assumed good)" header.d=tum.de*In-reply-to*: <022a1c8d-1a62-333f-c44b-b8bd801e7be3@in.tum.de>*References*: <k95lpx89oaxbqbvi65al88gd.1521656361918@email.android.com> <022a1c8d-1a62-333f-c44b-b8bd801e7be3@in.tum.de>*Thread-index*: AQHTwUEkh92Kk5bYhEqjX1E3r9xe/6PcOwoAgAAsWzA=*Thread-topic*: [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. > > Many thanks in advance! > > Best regards, > > Diego

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Cardinality for infinite sets***From:*Christian Sternagel

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

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

- Previous by Date: [isabelle] Deadline Extension: ICMS'18 Session on Software for Mathematical Reasoning and Applications
- Next by Date: Re: [isabelle] global_interpretation and code generation
- Previous by Thread: Re: [isabelle] Cardinality for infinite sets
- Next by Thread: Re: [isabelle] Cardinality for infinite sets
- 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