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

Question

对于我正在 Isabelle 中进行的证明，我需要 3 和 5 是素数的事实。建立它的最简单方法是什么？

Answer 1

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

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

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

您也可以使用 eval 而不是 simp，它通过 Isabelle 的评估 oracle 来评估 Standard ML 中的语句，然后将结果重新解释为 Isabelle 中的定理。根据您询问的对象，这可能被认为比 simp.

稍微不值得信赖

最后，Archive of Formal Proofs中关于Pratt Certificates的条目也提供了一种证明方法，叫做pratt，可以自动证明素性使用 Pratt 证书的数字。这比使用 simp 稍微高效一些，但对于非常大的数字来说仍然不是很好。

无论如何，对于像 5 和 7 这样的小数字，by simp 是可行的方法。

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