证明两个特定集合在Isabelle中具有相同的基数

Question

我很难证明两个集合具有相同的基数。 以下所有集合都是有限的。

首先假设我们已经设定了（M :: b集合）和函数foo ::“b集合⇒b集合⇒bool”
使得（foo AC = foo BC⟷A = B）和对于M中的每一个A，实际上都有一个C，这样foo A.C.

我试图证明那张卡{S。 ∃A∈M。 （S = {C.foo A C}）} = card M. 对此的非正式证明是显而易见的，但我似乎无法在Isabelle找到有效的证据 ;既不是≤也不是≥部分。

Answer 1

好吧，所以第一步是你应该用更方便的方式写下这个集合理解{S. ∃A∈M. (S = {C. foo A C}) }。第一步将是{{C. foo A C} |A. A ∈ M}，但我会建议使用“设置图像”运营商：

lemma "{S. ∃A∈M. (S = {C. foo A C})} = (λA. {C. foo A C}) ` M" by blast 

然后，你可以简单地使用的事实，(λA. {C. foo A C})是单射和规则card_image，它说，图像的基数内集函数的集合与原集合的集合相同：

lemma 
    assumes "⋀A B C. A ∈ M ⟹ B ∈ M ⟹ foo A C = foo B C ⟷ A = B" 
    shows "card {S. ∃A∈M. (S = {C. foo A C})} = card M" 
proof - 
    have "{S. ∃A∈M. (S = {C. foo A C})} = (λA. {C. foo A C}) ` M" 
    by blast 
    also have "inj_on (λA. {C. foo A C}) M" 
    using assms by (auto simp: inj_on_def) 
    hence "card ((λA. {C. foo A C}) ` M) = card M" 
    by (rule card_image) 
    finally show ?thesis . 
qed