Доказательство того, что два конкретных множества имеют равную мощность в Изабель

Мне трудно доказать, что два набора имеют одинаковую мощность. Все следующие множества конечны.

Сначала предположим, что у нас есть набор (M :: b set) и функция foo :: "b set ⇒ b set ⇒ bool"
такая, что (foo AC = foo BC ⟷ A = B) и для каждого A в M действительно существует C, такая что foo A C.

Я пытаюсь показать эту карту {С. ∃A∈M. (S = {C. foo A C})} = card M. Неофициальное доказательство этого очевидно, но я не могу найти эффективного доказательства у Изабель; ни для части ≤, ни для части ≥.


set cardinality isabelle
person RichiePoor    schedule 15.06.2017    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Итак, первый шаг - вы должны написать это понимание набора {S. ∃A∈M. (S = {C. foo A C}) } более удобным способом. Первым шагом будет {{C. foo A C} |A. A ∈ M}, но я бы предложил использовать оператор «установить изображение»:

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

Затем вы можете просто использовать тот факт, что (λA. {C. foo A C}) является инъективным, и правило card_image, которое говорит, что мощность изображения набора при инъективной функции такая же, как у исходного набора:

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
person Manuel Eberl    schedule 15.06.2017