В доказательствах Изабель в стиле Isar это прекрасно работает: from `a ∨ b` have foo proof assume a show foo sorry next assume b show foo sorry qed Неявное правило, вызываемое здесь proof , называется rule conjE . Но что я должен...

У меня есть доказательство Изабель, построенное следующим образом: proof (cases "n = 0") case True (* lots of stuff here *) show ?thesis sorry next case False (* lots of stuff here too *) show ?thesis sorry qed Первый случай на...

В Изабель есть два стиля доказательства: старый стиль «применения», где доказательство - это просто цепочка доказательств. apply (this method) apply (that method) заявления и новый «структурированный» стиль Isar. Лично я нахожу оба...

Некоторые из моих местных жителей имеют довольно много предположений, очень похожих на индукцию по типам данных (отсюда и исходят предположения). При интерпретации такого языкового стандарта очень удобно было бы указать случаи. Как мне добиться...

Я хочу иметь возможность доказать утверждение индукцией по n (типа nat). Он состоит из условного оператора, антецедент которого истинен только при n> = 2. Условное выражение, антецедент которого ложно, всегда истинно. Итак, я хотел бы доказать...

Я пытаюсь сделать базовые доказательства естественного вывода в Изабель, следуя этому документу (особенно слайд 23). Я знаю, что могу делать такие вещи, как theorem ‹(A ⟶ B) ⟶ A ⟶ B› proof - { assume ‹A ⟶ B› { assume ‹A›...

Я пытаюсь что-то доказать с помощью Isar; пока что я достиг цели, которая выглядит так: (∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧ (∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧ (∃P Q. P ≠ Q ∧ (∃R. P...

Я пытаюсь доказать следующую основную теорему о существовании обратной функции у биективной функции (чтобы научиться доказательству теорем с Isabelle / HOL): Для любого множества S и его тождественного отображения 1_S, α: S → T биективно тогда и...