證明有限集的基數

如何在Isabelle中證明簡單的lemma cd : "card {m∈ℕ. m <4} = 4"陳述？證明有限集的基數

auto不幫助我，奇怪sledgehammer超時（即使我在右側採用不同的值，比如3或5以確保我沒有忽略一些技術細節伊莎貝爾這或許實際上使在cardinaliy評估這些號碼中的一個。）

我的印象中，我不得不從Set_Interval.thy使用一些引理（或獲得靈感），因爲被廣泛使用集這幾樣，但到目前爲止，我沒有管理取得進展。

2017-02-19 nicht

請在math.stackexchange.com上發帖。 – Jameson

@Jameson你誤解了這個問題 - 這是不是數學，而是*形式化」數學的（在伊莎貝爾），這是在本網站範圍非常 - 這裏還有很多類似的問題，我增加了措辭「在伊莎貝爾」對我的問題，如果標籤沒有澄清這一點。 – nicht

你的陳述的問題是它不是真的。看看ℕ的定義與thm Nats_def：ℕ = range of_nat

of_nat從土黃規範同態成semiring_1，即半環具有1ℕ的定義基本上說，ℕ由環的所有元素其形式爲of_nat n，其自然數爲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

這個證明有點醜陋，考慮命題是多麼直觀明顯;這裏的解決方案並不是先寫下你想描述的這個相對不便的方式。知道如何以便捷的方式寫東西需要一點經驗。

來源

2017-02-19 12:37:52

哇，我從來沒有料到'm∈ℕ'和'n :: nat'有很大的不同。回答： – nicht

正如我所說，HOL是一種類型邏輯。對於數學家來說，這一開始往往令人困惑。雖然傳統數學中也會出現類似的問題，例如，集合「[1; 10]」有多少個元素？十？或無限多。取決於你是否認爲它是一組自然或實際的。同樣，'（0; 1）'是否打開？它是subset的子集，但不是subset的子集。 –

只是想補充一點，如果你把你的引理改寫成"card {m::nat. m < n} = n"，Isabelle沒有任何問題可以證明它。

*編輯，謝謝曼紐爾。

來源

2017-02-19 13:41:34 ammbauer

你可能是指'卡{m :: nat。 m

這非常有幫助，謝謝。 – nicht

證明有限集的基數

回答

相關問題