Знание, когда доказательство в стиле Изара действительно в Изабель

Question

Я работаю над упражнением, пытаясь выучить язык изар. У меня есть следующий скрипт для леммы о списках.

lemma "EX ys zs. xs = ys @ zs ∧ (length ys = length zs ∨ length ys = length zs + 1)"
proof -
show ?thesis by blast (* L *) 
qed

Кажется, Изабель принимает это, но некоторые вещи меня смущают.

Во-первых, хотя Изабель заявляет "Успешная попытка решить цель" и "Нет подцелей!" в позиции (* L *) строка "by blast" продолжает выделяться, что говорит о том, что этот метод не завершен. Это тот случай? Если да, действительно ли мое доказательство действительно в соответствии с Изабель?

В общем, я заметил, что если я напишу что-нибудь вместо "взрыва" в моем сценарии, то Изабель сообщит те же самые вещи в выводе, за исключением того, что она также может указать внизу красным, что произошел какой-то сбой. Тем не менее, если я напишу "qed" впоследствии, Изабель, кажется, принимает лемму как доказанную. Что здесь происходит? Как именно я узнаю, когда мое доказательство считается действительным?

Любое понимание высоко ценится!

Answer 1

Если какой-либо метод не завершился, или есть какое-то явное сообщение об ошибке, ваше доказательство не принимается. Только параллельная обработка IDE-Prover позволяет вам продолжать, как если бы доказательство было успешным.

Чтобы проверить, все ли ваши доказательства в порядке, самый безопасный способ - запустить isabelle buildили вы можете проверить на панели теории в Isabelle/jEdit, имеет ли ваша теория жирную черную рамку, что также указывает на успешную обработку.