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

我正在阅读“编程和在Isabelle/HOL中进行验证”教程。

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

所以我写了：

value "1 + 2"

其中给出：

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

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

请注意，我昨天开始使用伊莎贝尔。

来源

2013-05-19 mrsteve

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

我不知道所有的细节，但是当你没有指定常量1和2的类型时，那么你正在使用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。

来源

2013-05-20 00:10:17

这可能是挑剔的;），但它自己的'1'实际上是类'一'而不是'数字'。为什么'1 + 2'是''a :: numbers'类型的原因是'2'，正如你所说的，是类'数字'的。但是，例如，“1 + 1”的类型为“a :: {one，plus}”（即，“a”是类型类“one”和“plus”的一个实例）。 – chris

@chris，nitpicking的没关系。不知道微妙可能是致命的。你所说的是提醒。我已经看到0和1是特殊的。我必须证明一些关于他们的一些额外的东西的一些NAT东西。然而，Num.thy一直在我脑海里，因为我最近看到很多东西都是通过数字和数字过滤的。 Num.thy有一些很好的魔法。感谢哈夫曼和霍夫曼，当你看到他们时，考虑到这是一个Isa2012的补充。 Mrsteve，如果你倾向于，我建议你把我接受的答案从我的答案转到Chris'，所以他是第一个。他更完整。 – 2013-05-20 04:36:58

不需要切换接受;） – chris

在伊莎贝尔，整数常量（也称为数值常量）等...，-2，-1，0，1，2，...的过载。

有类型类零（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 -click 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）。这种“皮亚诺号”构成适当的自然数，仿佛nat定义如下：

datatype nat = 0 | Suc nat

所以这只是约相当印刷，但逻辑无关。

来源

2013-05-20 02:09:02 chris

我写'value“（8 :: nat）+（3 :: nat）”'但我仍然看到输出为“Suc（Suc（Suc ...”）。？我正在使用Isabelle2015 –

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

回答

相关问题