isabelle - 如何在 Isabelle/jEdit 中启用“跟踪”

Question

我是vim的粉丝，但只有emacs有这个 Isabelle/HOL 环境。jEdit很棒，但我不能使用

using [[simp_trace=true]]

就像在emacs中一样。

如何在jEdit中启用“跟踪” ？

Answer 1

You can indeed use simp_trace in the middle of a proof in Isabelle/jEdit, like so:

lemma "(2 :: nat) + 2 = 4"
  using [[simp_trace]]
  apply simp
  done

Alternatively, you can declare it globally, like so:

declare [[simp_trace]]

lemma "(2 :: nat) + 2 = 4"
  apply simp
  done

Both give you the simplifier's trace in the "Output" window when your cursor is just after the apply simp statement in jEdit.

Answer 2

如果您需要深度大于 1（默认）的跟踪深度，您可以通过以下方式对其进行微调

declare [[simp_trace_depth_limit=4]] 

然后，此示例给出的跟踪深度为 4。

Answer 3

正如其他人指出的那样，您可以使用simp_trace。但是，您也可以将simp_trace_new与“Simplifier Trace”窗口结合使用。这提供了比simp_trace更好的输出：

lemma "rev (rev xs) = xs"
  using [[simp_trace_new]]
  apply(induction xs)
  apply(auto)
  done

要查看跟踪，请将光标放在“应用（自动）”上，然后单击“查看简化跟踪”。“简化器跟踪”窗口（选项卡）应该打开。单击“显示跟踪”，应出现一个新窗口，显示每个子目标的跟踪。

Isabelle/Isar参考提供了更多详细信息：

simp_trace_new控制 Isabelle/PIDE 应用程序中的简化程序跟踪，特别是 Isabelle/jEdit。
这提供了简化器执行的重写步骤的分层表示。
用户可以通过指定断点、详细程度以及启用或禁用交互模式来配置行为。
在正常冗长（默认）下，只有匹配断点的规则应用程序才会显示给用户。在完全详细的情况下，将记录所有规则应用程序。交互模式会中断 Simplifier 的正常流程，并通过一些 GUI 对话框将如何继续的决定推迟给用户。

或者，您可以在此处指定“使用 [[simp_trace_new mode=full]]”链接 查看简化器采取的所有步骤。

注意：在前面的示例中，显示“apply(induction xs)”的跟踪不会产生任何输出。