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

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

0 голосов
/ 12 января 2019

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

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» впоследствии, Изабель, кажется, принимает лемму как доказанную. Что здесь происходит? Как именно я узнаю, когда мое доказательство считается действительным?

Любое понимание очень ценится!

1 Ответ

0 голосов
/ 17 января 2019

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

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

...