Isabelleで2つの特定の集合の基数が等しいことを証明する

Question

2つの集合が同じ基数を持つことを証明するのに問題があります。 以下のすべてのセットは有限です。

最初に、（foo AC = foo BC←A = B）となるようにfoo :: "b set⇒b set⇒bool"を
と設定したとします。 MのすべてのAについて、実際にはCのようなfoo A Cがあります。

そのカード{Sを表示しようとしています。 ∃A∈M。 これについての非公式の証明は明らかですが、Isabelleの効率的な証明 を見つけることはできません。 ≤と≥のどちらの部分でもない。

Answer 1

最初のステップでは、このセットの理解度を{S. ∃A∈M. (S = {C. foo A C}) }と書く方が便利です。最初のステップは、{{C. foo A C} |A. A ∈ M}だろうが、私は「設定した画像」演算子使用することをお勧めします：そして、あなたは、単に(λA. {C. foo A C})が単射と画像のカーディナリティと言うルールcard_image、であるという事実を使用することができます

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

をは、元のセットと同じです：

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