Распечатка / показ подробных шагов методов доказательства (например, простого) в доказательстве в Изабель

Question

Предположим, у меня есть следующий код в Изабель:

lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*)
apply simp
done

В приведенном выше коде метод simp доказывает лемму. Мне интересно увидеть и распечатать подробные (переписывание / упрощение) шаги, которые метод упрощения предпринимает, чтобы доказать эту лемму (и, возможно, быть в состоянии сделать то же самое для всех других методов доказательства). Как это возможно?

Я использую Изабель 2014 с редактором JEdit.

Большое спасибо

Answer 1

Трассировку упрощения можно включить, указав атрибуты simp_trace или же simp_trace_new:

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace]]
  apply simp
done

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

simp_trace_new позволяет увидеть более компактный вариант трассы (что переписывается) в отдельном окне (панель трассировки активируется нажатием выделенной части сообщения. См. трассировку упрощения на панели вывода, сама трасса отображается нажатием кнопки Показать след). Добавление опции mode=full генерирует более подробный вывод, похожий на simp_trace, но более структурированным образом:

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace_new mode=full]]
  apply simp
done

Вы можете найти более подробную информацию в Справочном руководстве Isabelle/Isar, которое также включено в установку Isabelle2014.

Answer 2

Если вы счастливы, загрузив один или два файла, проект l4.verified включает в себя инструмент под названием Apply Trace, написанный Дэниелом Матичуком. Это дает вам новую команду apply_trace которые можно использовать везде, где вы обычно используете apply, но покажет вам теоремы, используемые в шаге.

Например, написание:

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  apply_trace simp

производит:

used theorems:
  simp_thms(6): (?x = ?x) = True
  append_Nil: [] @ ?ys = ?ys
  append_Nil2: ?xs @ [] = ?xs

В отличие от simp_trace, он не скажет вам, в каком порядке были применены теоремы. Однако он способен работать с любым методом (simp, clarsimp, fastforce, auto и т. д.) simp_trace работает только с методами, основанными на упрощении.

Чтобы использовать его, вам нужно будет захватить оба файла Apply_Trace_Cmd.thy а также Apply_Trace.thy и импорт Apply_Trace_Cmd,