Re: [isabelle] Cardinality for infinite sets



... though this may be too heavy for your intended application, e.g., if you don't care about distinguishing between different infinite cardinalities. The heaviness comes from having to use ordinal embedding (denoted <o and <=o) and isomorphism (denoted =o) instead of (in)equality of natural numbers.


Cheers,


Andrei



________________________________
From: Andrei Popescu
Sent: 21 March 2018 19:19:28
To: Diego Marmsoler; isabelle-users at cl.cam.ac.uk
Subject: Re: Cardinality for infinite sets


Hi Diego,


Please see


https://isabelle.in.tum.de/dist/library/HOL/HOL/BNF_Cardinal_Arithmetic.html


and, for a more complete set of results,


https://isabelle.in.tum.de/dist/library/HOL/HOL-Cardinals/index.html


These are all documented in the ITP 2014 paper


http://andreipopescu.uk/pdf/card.pdf


Let me know should you have any problems using these.


Cheers,


Andrei

________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Diego Marmsoler <diego.marmsoler at tum.de>
Sent: 21 March 2018 18:19:24
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] Cardinality for infinite sets

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.