CODEWITHSUNDEEP
setisabellecardinality
Kookie
Kookie

Reputation: 347

Simple Cardinality Proof

So I'm trying to perform a simple proof using cardinalities. It looks like:

⟦(A::nat set) ∩ B = {}⟧ ⟹ (card (A ∪ B) = card A + card B)

Which seems to makes sense, but for some reason blast hangs, the rest of the provers fail to apply, and sledgehammer times out. Is there a gap in what I think I know about cardinalities? If not, how can I prove this lemma?

Thanks in advance!

Upvotes: 0

Views: 181

Answers (1)

braewebb
braewebb

Reputation: 381

I believe that the lemma you are trying to prove does not appropriately consider the case of infinite sets.

In Isabelle/HOL, infinite cardinalities are represented by zero. As we can see by the following lemma.

lemma "¬(finite A) ⟹ card A = 0"
  by simp

If we consider the case of an infinite set, A, and a set of one element, B, then assume the intersection, A ∩ B is an empty set.

We are left with:

card (A ∪ B) = 0 as their union will also be infinite.

card A = 0

card B = 1

So we can see that in this case, the lemma does not hold.

The lemma can be corrected by asserting both sets are finite:

lemma
  "⟦finite A; finite B; ((A::nat set) ∩ B) = {}⟧ ⟹ (card (A ∪ B) = card A + card B)"
  by (simp add: card_Un_disjoint)

Which is essentially the same as the card_Un_disjoint used by the proof:

lemma card_Un_disjoint: "finite A ⟹ finite B ⟹ A ∩ B = {} ⟹ card (A ∪ B) = card A + card B"
  using card_Un_Int [of A B] by simp

Upvotes: 3

Related Questions