Email Gateway (Aug 22 2022 at 16:58): Email Gateway (Aug 22 2022 at 16:58):From: Diego Marmsoler <diego.marmsoler@tum.de>
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
Email Gateway (Aug 22 2022 at 16:59):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Email Gateway (Aug 22 2022 at 16:59):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
... 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
Email Gateway (Aug 22 2022 at 16:59):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 22 2022 at 17:00):From: Diego Marmsoler <diego.marmsoler@tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 17:00):From: Christian Sternagel <c.sternagel@gmail.com>
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
Last updated: Apr 24 2024 at 04:17 UTC