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

Question

我是维姆的粉丝，但只有伊莎贝尔/霍尔这样的环境。jEdit很好，但我不能用

using [[simp_trace=true]]

就像艾玛奇一样。

如何在jEdit中启用“跟踪”

Answer 1

实际上，您可以在Isabelle/jEdit中使用simp_trace，如下所示：

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

或者，您可以在全球范围内声明它，如下所示：

declare [[simp_trace]]

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

当光标刚好在apply simp语句之后时，两者都会在“输出”窗口中给出简化器的跟踪。

Answer 2

如果您需要一个比1更深的跟踪深度(默认)，则可以通过以下方法对其进行微调。

declare [[simp_trace_depth_limit=4]] 

然后，这个例子给出了4的跟踪深度。

Answer 3

正如其他人所指出的，您可以使用simp_trace。然而，您也可以使用simp_trace_new与“简单程序跟踪”窗口相结合。这在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。 这提供了由简化器执行的重写步骤的分层表示。 用户可以通过指定断点、详细以及启用或禁用交互模式来配置行为。 在通常的冗长(默认)中，只有匹配断点的规则应用程序才会显示给用户。所有规则应用程序都将被记录下来。交互模式中断了简化器的正常流程，并推迟了如何通过一些GUI对话框继续给用户的决定。

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

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