如何证明"3是质数“中的伊莎贝尔证明助理？

Question

为了证明我在伊莎贝尔工作，我需要3和5是素数的事实。建立这种关系的最简单的方法是什么？

Answer 1

有一些simp规则允许简化器自动完成此操作：

lemma "prime (5 :: nat)"
  by simp

对于较大的数字(如137)，这将花费几秒钟时间，对于大得多的数字，它是完全不可用的。

您还可以使用eval而不是simp，后者通过伊莎贝尔的评估神谕计算标准ML中的语句，然后将结果重新解释为伊莎贝尔中的一个定理。根据您的要求，这可能会被认为比simp稍微不可信。

最后，正式证明档案中的普拉特证书条目还提供了一种称为pratt的证明方法，它可以使用Pratt证书自动证明一个数字的素数。这比使用simp略高一些，但对于真正的大数字来说仍然不是很好。

无论如何，对于5和7这样的小数字来说，by simp是最好的选择。

但是，请注意，您必须提供一个类型，即prime (5 :: nat)或prime (7 :: int)。如果只编写prime 5，则推断为5的类型过于笼统。例如，prime (5 :: real)不是真，因为字段不包含素数。