有限集合のカーディナリティを証明する

Question

イザベルでは簡単なlemma cd : "card {m∈ℕ. m <4} = 4"の文をどのように証明できますか？

autoは、私は、おそらく実際に作るいくつかの技術的なイザベルの詳細を見落としていないことを確認する3または5のように、私は右側に異なる値を使用していても（私を助け、奇妙sledgehammer時間はありません枢機卿はこれらの数字の1つを評価します）

Set_Interval.thyからいくつかの補題を使用しなければならないという印象があります。これらの種類のセットは広く使用されていますが、これまでは管理していませんでした進歩する。

Answer 1

あなたの声明の問題は、それが真実ではないということです。 thm Nats_defでℕの定義を見てください：ℕ = range of_nat

of_natはナチュラルから正規の準同型であるsemiring_1に、すなわちA半環ℕの定義は、基本的にℕがリングのすべての要素で構成されていることを述べている1を持っています自然数がnの場合はof_nat nの形式です。 {m∈ℕ. m <4}のタイプを見ると、それは'aであるか、declare [[show_sorts]]の前に'a :: {ord, semiring_1}と表示されます。つまり、1でセミリングして何らかの注文をしています。この注文は、ではなく、はリング構造と互換性がなければならず、線形でなければならない。

あなたが定義したセットは常に{0, 1, 2, 3}と設定されていると思われるかもしれませんが、順序はリング構造と互換性がある必要はないため、そうではありません。順序は自明である可能性がありますので、すべて自然数を取得します。

また、セットが{0, 1, 2, 3}であっても、その基数はないが、必ずしも4（リングℤ/2ℤ考える - そのセットが{0, 1}に等しくなるので、基数は2である）である

式の種類を少し制限したいと思うでしょう。私は右のタイプのクラスはここではlinordered_semidomであると考えます。つまり、ゼロ除数が1であるセミリングと、リング構造と互換性のある線形の順序付けです。そうすれば、次のことができます。

lemma cd : "card {m∈ℕ. m < (4 :: 'a :: linordered_semidom)} = 4" 
proof - 
    have "{m∈ℕ. m < (4 :: 'a)} = {m∈ℕ. m < (of_nat 4 :: 'a)}" by simp 
    also have "… = of_nat ` {m. m < 4}" 
    unfolding Nats_def by (auto simp del: of_nat_numeral) 
    also have "card … = 4" by (auto simp: inj_on_def card_image) 
    finally show ?thesis . 
qed 

この証明は、直感的に明白な命題がどれほどのものかを考えると醜いです。ここでの解決策は、最初にこの比較的不都合な方法で説明したいセットを書き留めないことです。便利な方法で物事を書く方法を知るには、少し経験が必要です。

Answer 2

補題を"card {m::nat. m < n} = n"に書き直すと、Isabelleは問題を証明することはできません。

*編集、ありがとうマヌエル。