Der Beweis, dass zwei spezifische Sätze gleiche Kardinalität in Isabelle

Question

haben Ich habe Probleme zu beweisen, dass zwei Sätze die gleiche Kardinalität haben. Alle folgenden Sätze sind endlich.

Erste Nehmen wir an, wir haben festgelegt (M :: b Satz) und eine Funktion foo :: "b Satz ⇒ b Satz ⇒ bool"
, so dass (foo AC = foo BC ⟷ A = B) und für jedes A in M ​​gibt es tatsächlich ein C, so dass foo A C.

Ich versuche, diese Karte zu zeigen {S. ∃A∈M. (S = {C. foo A C})} = Karte M. Der informelle Beweis dafür ist offensichtlich, aber ich kann keinen effizienten Beweis finden in Isabelle; weder für den ≤ noch für den ≥ Teil.

Answer 1

Okay, also der erste Schritt ist, dass Sie dieses Set Verständnis {S. ∃A∈M. (S = {C. foo A C}) } auf eine bequemere Weise schreiben sollten. Ein erster Schritt wäre {{C. foo A C} |A. A ∈ M}, aber ich würde die ‚Set Bild‘ Betreiber vorschlägt, mit:

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

Dann können Sie einfach die Tatsache nutzen, dass (λA. {C. foo A C}) injektiv und die Regel card_image, das besagt, dass die Mächtigkeit des Bildes eines Satzes unter einer injektiven Funktion ist der gleiche wie der des ursprünglichen Satzes:

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