isabelle - 简化自然的漂亮打印

Question

假设我编写了一个用于反转列表的函数。我想使用 value 命令对其进行测试，只是为了向自己保证我可能做对了。但是输出看起来很糟糕:

value "reverse [1,8,3]"
> "[1 + 1 + 1, 1 + 1 + (1 + 1) + (1 + 1 + (1 + 1)), 1]" :: "'a list"

如果我告诉 Isabelle 将这些数字字符视为自然字符，输出会更糟:

value "reverse [1::nat,8,3]"
> "[Suc (Suc (Suc 0)), Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))), Suc 0]" :: "nat list"

有时我求助于使用字符串，但到处都是撇号，这看起来有点滑稽:

value "reverse [''1'',''8'',''3'']"
> "[''3'', ''8'', ''1'']" :: "char list list"

我能否指示 Isabelle 的 pretty-print 将 Suc (Suc (Suc 0)) 打印为 3，等等？也许通过给 syntax 或 translations 命令一些魔法咒语？

---

这是我的完整示例，如果您想将其粘贴到 Isabelle 中:

theory Scratch imports Main begin

fun reverse where 
  "reverse [] = []"
| "reverse (x#xs) = reverse xs @ [x]"

value "reverse [1,8,3]"
value "reverse [1::nat,8,3]"
value "reverse [''1'',''8'',''3'']"

end

Answer 1

简答:我的第一个想法是使用类型 int , 因为(与 nat 不同)它的代码生成器设置默认使用二进制数字表示。

导入 "~~/src/HOL/Library/Code_Target_Nat" , 正如 naT 所建议的那样，如果您不想使用 Suc 也是一个好主意。类型的表示 nat .

说明: Isabelle 中的数字使用 Num.thy 中定义的构造函数进行编码;例如5是 numeral (Bit1 (Bit0 One)) 的缩写.这里One , Bit0和 Bit1是 num 类型的构造函数. numeral已过载，适用于具有 1 的任何类型和关联 + .这是 numeral 的代码方程式:

lemma numeral_code [code]:
  "numeral One = 1"
  "numeral (Bit0 n) = (let m = numeral n in m + m)"
  "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"

如果我们为 5::'a::numeral 生成代码, 然后 1和 +在类型上 'a被视为未解释的常量，因此它们保留在输出中:(1 + 1) + (1 + 1) + 1 .

为 5::nat 生成代码工作方式相同，除了我们确实有 1 的代码和 +在类型上 nat , 就 Suc 而言.因此 (1 + 1) + (1 + 1) + 1进一步减少到 Suc (Suc (Suc (Suc (Suc 0)))) .

输入 int工作方式不同。 Int.thy 中的代码生成器设置为类型 int 使用三个构造函数: Pos和 Neg类型 num => int ，以及 0 . code_abbrev声明导致每次出现 numeral在类型 num => int将被 Pos 取代在代码生成期间。代码运行后，Pos然后变回 numeral在 Isabelle 显示结果之前。因此 5::int计算结果为 5 .

特殊代码设置理论: src/HOL/Library包含一些用于自定义数字代码生成的不同理论。

• "~~/src/HOL/Library/Code_Target_Nat"告诉代码生成器使用目标语言(例如 SML 或 Haskell 的)内置数字来表示类型 nat .例如，5::nat通常翻译成 SML 为 numeral (Bit1 (Bit0 One)) ;但是，加载此库后，它会被翻译为 5在 SML 中。 value的结果之后被翻译回伊莎贝尔数字表示。

• "~~/src/HOL/Library/Code_Target_Int"是相同的，但对于类型 int而不是 nat .

• "~~/src/HOL/Library/Code_Target_Numeral"只需加载前两个库。它只影响类型 nat和 int ，而不是类中的任何其他类型 numeral .

• "~~/src/HOL/Library/Code_Binary_Nat"配置 nat与 int 的默认代码设置相同的样式: 与构造函数 0和 nat_of_num::num => nat和一个 code_abbrev声明。有了这个图书馆，value "5::nat"还返回 5 .