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

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

这是我不久前想修复的问题，但显然我忘记了。卡西吉奈特的猜测是错误的；这确实是全面评估的结果。问题在于自然数是以这种笨拙的方式打印的。

您可以执行以下操作：

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

2. 你可以加~~/src/HOL/Library/Code_Target_Numeral到您的进口。这使得 Isabelle 的代码生成器使用目标语言的任意精度整数（如果是value，即 ML 及其基于 GMP 的整数），而不是低效的后继表示法。作为副作用，这也以更好的方式打印自然数。

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

Code:

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 的组成部分。