简单基数证明
Simple Cardinality Proof
所以我正在尝试使用基数执行一个简单的证明。看起来像：
⟦(A::nat set) ∩ B = {}⟧ ⟹ (card (A ∪ B) = card A + card B)
这似乎是有道理的，但由于某种原因blast挂起，其余证明者申请失败，sledgehammer超时。我认为我对基数的了解有差距吗？如果不是，我如何证明这个引理？
提前致谢！
我认为您试图证明的引理没有适当考虑无限集的情况。
在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
所以我正在尝试使用基数执行一个简单的证明。看起来像：
⟦(A::nat set) ∩ B = {}⟧ ⟹ (card (A ∪ B) = card A + card B)
这似乎是有道理的，但由于某种原因blast挂起，其余证明者申请失败，sledgehammer超时。我认为我对基数的了解有差距吗？如果不是，我如何证明这个引理？
提前致谢！
我认为您试图证明的引理没有适当考虑无限集的情况。
在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