Search code examples
setisabellecardinality

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!

Solution

  • 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