Доказательство мощности конечного множества

Question

Как я могу доказать в Изабель простое lemma cd : "card {m∈ℕ. m <4} = 4" заявление?

auto не помогает мне и как ни странно sledgehammer время ожидания (даже если я использую разные значения в правой части, например 3 или же 5 чтобы убедиться, что я не пропустил некоторые технические детали Изабеллы, которые, возможно, на самом деле заставляют кардиналов оценить один из этих номеров.)

У меня сложилось впечатление, что я должен использовать некоторые леммы (или получить вдохновение) от Set_Interval.thy поскольку такие наборы широко используются, но пока мне не удалось добиться прогресса.

Answer 1

Просто хотел добавить, что если переписать свою лемму "card {m::nat. m < n} = n"Изабель без проблем докажет это.

* Отредактировано, спасибо Мануэль.

Answer 2

Проблема с вашим утверждением в том, что оно не соответствует действительности. Посмотрите на определение ℕ с 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

Доказательство немного уродливо, учитывая, насколько интуитивно очевидно утверждение; Решение здесь заключается не в том, чтобы записать набор, который вы хотите описать, таким относительно неудобным способом. Требуется немного опыта, чтобы научиться писать вещи удобным способом.