如何在Isabelle/ML中将proof_body类型转换为字符串？

问题场景 #

以下是测试用的Isabelle理论代码：

theory Scratch2
  imports Main
begin

lemma ex: "A ∧ B ⟶ B ∧ A"
proof
  assume "A ∧ B"
  then obtain B and A ..
  then show "B ∧ A" ..
qed

ML_val ‹
  val thm = @{thm ex};
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
›

end

在jEdit中运行该代码后，将光标置于body变量上方时，Output标签页会显示该变量的字符串形式，但直接使用writeln body输出时会触发类型错误：

ML error⌂:
Type error in function application.
   Function: writeln : string -> unit
   Argument: (body) : proof_body
   Reason:
      Can't unify string (*In Basis*) with proof_body
         (Different type constructors)

解决方案 #

Isabelle/ML中，jEdit悬停显示的内容是通过Pretty打印机制生成的。要实现和Output标签页一致的字符串输出，需要先将proof_body转换为Isabelle的Pretty格式，再转成标准字符串：

修改后的ML代码如下：

ML_val ‹
  val thm = @{thm ex};
  val body = Proofterm.strip_thm_body (Thm.proof_body_of thm);
  -- 将proof_body转为字符串
  val body_str = Pretty.string_of (Proof_Display.pretty_proof_body body);
  writeln body_str;
›

说明 #

• Proof_Display.pretty_proof_body：负责将proof_body类型转换为Isabelle内部的Pretty结构化表示，这和jEdit悬停时调用的打印逻辑一致
• Pretty.string_of：将Pretty结构转换为可输出的标准字符串，此时就能直接用writeln输出结果

内容的提问来源于stack exchange，提问作者justF