Re: [isabelle] 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.