Isabelle 返回数字而不是 Suc(Suc( ... 0 ))

Question

当我使用 value 找出返回自然数的函数的某个值时，我总是以 0 的迭代后继函数的形式获得答案，即 Suc(Suc ( ... 0 )) 有时很难阅读。有没有办法直接输出Isabelle返回的数字？

Answer 1

这是我前段时间想修复的东西，但显然我忘记了。 Carcigenate 的猜测不正确；这确实是充分评估的结果。问题在于自然数以这种笨拙的方式打印。

您可以执行以下操作:

1. 最简单的方法是将数字转换为整数，即代替 value "foo x y z"(其中 foo x y z 是类型 nat，你想评估)你写 value "int (foo x y z)"。

2. 您可以将 ~~/src/HOL/Library/Code_Target_Numeral 添加到您的导入中。这使得 Isabelle 的代码生成器使用目标语言的任意精度整数(在 value 的情况下，这是 ML 及其基于 GMP 的整数)而不是低效的后继表示法。作为副作用，这也以更好的方式打印自然数。

3. 您可以将以下代码添加到您的理论中，这会改变 value 命令显示自然数的方式:

代码:

lemma Suc_numeral_bit0: "Suc (numeral (Num.Bit0 n)) = numeral (Num.Bit1 n)"
  by (subst Suc_numeral) simp

lemma Suc_numeral_bit1: "Suc (numeral (Num.Bit1 n)) = numeral (Num.Bit0 (n + Num.One))"
  by (subst Suc_numeral) simp

lemmas [code_post] = 
  One_nat_def [symmetric] Suc_numeral_bit0 Suc_numeral_bit1 Num.Suc_1 Num.arith_simps

请注意，value 命令只是一个诊断命令。它主要用于快速合理性测试和代码生成设置的调试，让它工作有时会很棘手。

默认情况下，value 依赖于代码生成器，即 Isabelle 需要知道如何为表达式生成可执行代码，如果它做不到，value 将可能会失败。 (它有时也可以回退到一些其他策略，通过评估进行归一化或通过简化进行评估，但这些通常不会提供有用的输出)

我告诉你这些只是为了让你知道从 value 命令中可以得到什么，并且不要以为这是人们一直使用的 Isabelle 不可或缺的一部分。