时间戳

首页 > 解决方案 > 简单基数证明

set - 简单基数证明

问题描述

所以我试图用基数来做一个简单的证明。看起来像：

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

这似乎是有道理的，但由于某种原因blast挂起，其余的证明者无法申请，并且sledgehammer超时。我认为我对基数的了解是否存在差距？如果不是，我该如何证明这个引理？

提前致谢！

标签： setisabellecardinality

解决方案

我相信您试图证明的引理没有适当考虑无限集的情况。

在 Isabelle/HOL 中，无限基数用零表示。正如我们可以通过以下引理看到的。

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

如果我们考虑无限集A和一个元素的集合 的情况B，那么假设交集A ∩ B是一个空集。

我们剩下：

card (A ∪ B) = 0因为他们的结合也将是无限的。

card A = 0

card B = 1

所以我们可以看到，在这种情况下，引理不成立。

可以通过断言两个集合都是有限的来纠正引理：

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

card_Un_disjoint这与证明使用的基本相同：

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

推荐阅读