isabelle - Isabelle：如何打印 1 + 2 的结果？

Question

这是一个初学者的问题。

我正在阅读教程“Isabelle/HOL 中的编程和证明”。

我想打印“1 + 2”的结果。

所以我写道：

value "1 + 2"

这使：

"1 + (1 + 1)"
 :: "'a"

我想看看结果，即“3”。我怎么能在伊莎贝尔做到这一点？如果我在定理证明器中对“1+2”进行归一化，则会显示结果 3。我只想在伊莎贝尔做同样的事情。

请注意，我昨天开始使用 Isabelle。

Answer 1

在 Isabelle 中，像 ..., , , , , , ... 这样的整数文字（也称为数值常量）被重载。-2-1012

有零 ( zero)、一 ( one)、正数 ( numeral) 和负数 ( ) 的类型类neg_numeral。后两者还分别包含了加法半群 ( semigroup_add) 的类型类 - 允许使用+- 和加法组 ( group_add) - 分别允许使用+and -（也是一元的）。（另请注意，加号本身 ( op +) 在类中被重载plus。）

现在，如果您输入一个表达式，Isabelle 会推断出最一般的类型。这通常比人们预期的更普遍。这正是你遇到的。考虑一些例子：

input      inferred type      type class
 0           'a                 'a::zero
 1           'a                 'a::one
 op +        'a => 'a => 'a     'a::plus
 1 + 2       'a                 'a::numeral
 x + y       'a                 'a::plus
 Suc 0 + y   nat                (nat is an instance, among others,
                                of class semigroup_add)

在这种情况下，您可以通过显式添加类型约束来告诉系统您的意思是不太通用的类型，例如，(1::nat) + 2导致整体类型nat。

如果您使用 Isabelle/jEdit，您可以方便地调查此类情况，而不会像declare [[...]]您的理论那样引入噪音。例如输入时

value "1 + 2"

在您看到的输出面板中

"1 + (1 + 1)"
  :: "'a"

现在您可以在输出中Ctrl单击（即按住控制按钮并用鼠标单击）'a。这会告诉你那'a是在课堂numeral上。您可以进一步Ctrl单击numeral以获取此类型类的定义。

如果您将输入更改为（对于自然数）

value "(1::nat) + 2"

或（对于整数）

value "(1::int) + 2"

输出将是

"Suc (Suc (Suc 0)))" :: "nat"

和

"3" :: "int"

正如预期的那样。

更新：请注意，自然数（类型nat）将以一元表示形式打印，例如：0, Suc 0, Suc (Suc 0), ... 。然而，这不要与1 + (1 + (1 + ...))（它是任意类型的 class numeral）混淆。这样的“皮亚诺数”构成了适当的自然数，就好像nat定义如下：

datatype nat = 0 | Suc nat

所以这只是关于漂亮的印刷，但在逻辑上无关紧要。

Answer 2

这是我的问题。一个初学者到另一个，多么幸运。

我不知道所有细节，但是当您没有为常量 1 和 2 指定类型时，您正在使用 a numeral，这一切都在Num.thy中列出。

试试这个并查看输出面板：

declare[[show_consts=true]]
declare[[show_types=true]]
declare[[show_sorts=true]]
value "1 + 2"
value "1 + (2::nat)"

theorem "1 + 2 = z"
  apply simp
  oops

您会看到,1+2并numeral没有自动简化，或者更确切地说，通过扩展为“后继”形式的加法，得到了太多的简化。

value "1 + (2::nat)"确实被简化为“首选的人类形式” 。

之后simp，1 + 2尽管它是numeral.