Nachweis der Kardinalität eines endlichen Satzes

Question

Wie kann ich in Isabelle die einfache lemma cd : "card {m∈ℕ. m <4} = 4" Aussage beweisen?

auto hilft mir nicht und seltsam sledgehammer mal aus (auch wenn ich verschiedene Werte auf der rechten Seite verwenden, wie 3 oder 5 sicher zu machen, dass ich nicht ein paar technische Details Isabelle übersehen, die vielleicht tatsächlich machen die Kardinalität zu einer dieser Zahlen auswerten.)

Ich habe den Eindruck, dass ich einige Lemmas (oder Inspiration) von Set_Interval.thy verwenden müssen, da dort Sätze dieser Art ausgiebig verwendet werden, aber bis jetzt habe ich es nicht geschafft Fortschritte machen.

Answer 1

Das Problem mit Ihrer Aussage ist, dass es nicht wahr ist. Betrachten Sie die Definition von n mit thm Nats_def: ℕ = range of_nat

of_nat der kanonischen Homomorphismus von dem naturals in ein semiring_1 ist, also einen Halbring das hat eine 1. Die Definition von n im Grunde sagt, dass n all Elemente des Rings besteht das sind die Form of_nat n für eine natürliche Zahl n. Wenn Sie sich die Art von {m∈ℕ. m <4} ansehen, werden Sie sehen, dass es 'a ist, oder wenn Sie eine declare [[show_sorts]] davor tun, 'a :: {ord, semiring_1}, d.h. ein Semiring mit einer 1 und irgendeine Art von Bestellung darauf. Diese Reihenfolge muss nicht mit der Ringstruktur kompatibel sein, noch muss es linear sein.

Sie können denken, dass die von Ihnen definierte Menge immer die Menge {0, 1, 2, 3} ist, aber da die Bestellung nicht mit der Ringstruktur kompatibel sein muss, ist dies nicht der Fall. Die Reihenfolge könnte trivial sein, so erhalten Sie alle natürliche Zahlen.

Außerdem, selbst wenn der Satz ist{0, 1, 2, 3}, ist seine Mächtigkeit nicht unbedingt 4. (man denke an dem Ring z/2ℤ - dann wird dieser Satz auf {0, 1} gleich sein, so dass die Mächtigkeit 2)

Sie werden wahrscheinlich den Typ Ihres Ausdrucks ein wenig einschränken wollen. Ich denke, die richtige Typenklasse ist hier linordered_semidom, d. H. Ein Semiring mit einer 1, keine Nullteiler und eine lineare Ordnung, die mit der Ringstruktur kompatibel ist. Dann können Sie tun:

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 

Der Beweis ist ein bisschen hässlich, wenn man bedenkt, wie intuitiv offensichtlich der Vorschlag ist; Die Lösung besteht hier nicht darin, die Menge, die Sie beschreiben wollen, auf diese relativ unbequeme Weise aufzuschreiben. Es braucht ein wenig Erfahrung zu wissen, wie man Dinge auf eine bequeme Art und Weise schreibt.

Answer 2

Ich wollte nur hinzufügen, dass, wenn Sie Ihr Lemma zu "card {m::nat. m < n} = n" umschreiben, hat Isabelle kein Problem, es zu beweisen.

* Bearbeitet, danke Manuel.