Isabelle 证明助手中如何证明“3 是素数”？

Question

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

Answer 1

有 simp 规则允许简化器自动执行此操作：

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

对于较大的数字（例如137），这将需要几秒钟，对于更大的数字，它完全无法使用。

您也可以使用eval 代替simp，它通过 Isabelle 的评估 oracle 来评估标准 ML 中的语句，然后将结果重新解释为 Isabelle 中的定理。根据您询问的对象，这可能被视为比 simp 稍不可信。

最后，形式证明存档中Pratt Certificates 上的条目还提供了一种称为pratt 的证明方法，它可以使用Pratt 证书自动证明数字的素数。这比使用simp 稍微高效一些，但对于非常大的数字仍然不是很好。

无论如何，对于像 5 和 7 这样的小数字，by simp 是要走的路。

但是请注意，您必须给出一个类型，即prime (5 :: nat) 或prime (7 :: int)。如果只写prime 5，那么推断为5的类型太笼统了。例如，prime (5 :: real) 不为真，因为字段不包含素数。