Isabelle:如何打印1 + 2的结果？

Question

这是一个初学者的问题.

我正在阅读教程"在Isabelle/HOL中编程和证明".

我想打印"1 + 2"的结果.

所以我写道:

value "1 + 2"

这使:

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

我想看看结果,即"3".我怎么能在伊莎贝尔那里做到这一点？如果我在定理证明器中标准化"1 + 2",则显示结果3.我只想在伊莎贝尔做同样的事情.

请注意,我昨天开始使用Isabelle.

Answer 1

在伊莎贝尔,整数常量(也称为数字常数)等..., ,-2,-1,,0 ,...的过载.12

有零(zero),一(one),正数(numeral)和负数(neg_numeral)的类型类.后两者还包括添加剂半组的类型(semigroup_add) - 允许使用+- 和添加剂组(group_add) - 允许使用+和-(也一元) - 分别.(另请注意,加号本身(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 + ...))但是不要混淆(这是任意类型的numeral).这种"Peano数字"构成了适当的自然数,好像nat定义如下:

datatype nat = 0 | Suc nat

所以这仅仅是关于漂亮印刷,但逻辑上无关紧要.