Блог

Мне было интересно, есть ли способ прервать доказательство в Isabelle / jEdit?

Я искал такие команды, как «Сброс», «Прервать», но не смог их найти.

Я знаю , что есть Sorry . Но я не уверен, что если кто-то использует Sorry , то рассматриваемая теорема считается истинной или отвергнутой. Кроме того, похоже, Sorry что он не работает в этом apply..done режиме.

В настоящее время я комментирую теоремы, которые не могу доказать. Но для того, чтобы что-то прокомментировать или раскомментировать, требуется много текста (по четыре символа в каждом (* *)), что довольно громоздко.

Итак, существует ли стандартный / универсальный способ прервать доказательство в Isabelle?

Во-первых, команда есть sorry , и она работает (но только) в стиле apply:

 lemma 
  ‹False ∧ True›
  apply (rule conjI)
   apply auto
  sorry
 

Что касается фактического вопроса, oops прерывает доказательства, будь то в стиле apply или нет:

 lemma 
  ‹False ∧ True›
proof -
  have True
    by auto
  oops
 

На oops отредактированное доказательство нельзя ссылаться позже.