如何在 Isabelle 中正确使用关键字“定理”？答案

【问题标题】：How to properly use keyword 'theorem' in Isabelle?如何在 Isabelle 中正确使用关键字“定理”？
【发布时间】：2014-07-30 18:26:28
【问题描述】：

我从伊莎贝尔的维基百科页面获得了以下代码：

theorem sqrt2_not_rational:
  "sqrt (real 2) ∉ ℚ"
proof
  assume "sqrt (real 2) ∈ ℚ"
  then obtain m n :: nat where
    n_nonzero: "n ≠ 0" and sqrt_rat: "¦sqrt (real 2)¦ = real m / real n"
    and lowest_terms: "gcd m n = 1" ..
  from n_nonzero and sqrt_rat have "real m = ¦sqrt (real 2)¦ * real n" by simp
  then have "real (m²) = (sqrt (real 2))² * real (n²)" by (auto simp add: power2_eq_square)
  also have "(sqrt (real 2))² = real 2" by simp
  also have "... * real (m²) = real (2 * n²)" by simp
  finally have eq: "m² = 2 * n²" ..
  hence "2 dvd m²" ..
  with two_is_prime have dvd_m: "2 dvd m" by (rule prime_dvd_power_two)
  then obtain k where "m = 2 * k" ..
  with eq have "2 * n² = 2² * k²" by (auto simp add: power2_eq_square mult_ac)
  hence "n² = 2 * k²" by simp
  hence "2 dvd n²" ..
  with two_is_prime have "2 dvd n" by (rule prime_dvd_power_two)
  with dvd_m have "2 dvd gcd m n" by (rule gcd_greatest)
  with lowest_terms have "2 dvd 1" by simp
  thus False by arith
qed

但是，当我将此文本复制到 Isabelle 实例中时，每行左侧有多个“请勿输入”符号。有人说'在顶层非法应用命令“定理”'，所以我假设你不能简单地在顶层定义一个定理，并且维基百科页面没有提供完整的初始示例。我把这个定理包装成一个理论如下：

theory Scratch
imports Main
begin

(* Theorem *)

end

Isabelle 不再抱怨这个定理，但是，在定理的第二行，它现在说：

Inner lexical error at: ℚ
Failed to parse proposition

也是在抱怨证明线：

Illegal application of command "proof" in theory mode

定理的其余行也有错误。将维基百科提供的这个定理包装起来以便在 Isabelle 中检查的正确方法是什么？

【问题讨论】：

标签： syntax-error proof isabelle theorem

【解决方案1】：

我完全同意 Manuel 的观点，仅仅导入 Main 是不够的。如果您对证明不感兴趣，而只是对测试不合理性感兴趣，那么最好将 $AFP/Real_Impl/Real_Impl 包括在形式证明存档中：然后测试不合理性变得非常容易：

theory Test
imports "$AFP/Real_Impl/Real_Impl"
begin

lemma "sqrt 2 ∉ ℚ" by eval
lemma "sqrt 1.21 ∈ ℚ" by eval
lemma "sqrt 3.45 ∉ ℚ" by eval

end

【讨论】：

很好，我不知道我们有一个决策程序。但是，我认为值得注意的是，eval 在某种程度上不如“真实”证明，因为虽然决策过程本身被证明是合理的，但eval 依赖于代码生成器来生成可执行代码决策过程和代码生成器未经验证——尽管根据我的经验它非常可靠。

【解决方案2】：

您猜测必须以您所做的方式将“定理”命令包装在理论中是正确的。但是，您需要更多的导入，imports Main 甚至不加载包含 sqrt、有理数和素数的理论。

此外，维基百科上的证明有些过时了。 Isabelle 是一个非常动态的系统。它的维护者将库中的所有证明和Archive of Formal Proofs 移植到每个版本中，但是位于某个地方（例如维基百科）的代码 sn-ps 往往会在一段时间后变得过时，我认为这个特定的代码非常古老。

对于几乎相同事物的最新证明，正确嵌入到具有正确导入的理论中，请看这里： http://isabelle.in.tum.de/repos/isabelle/file/4546c9fdd8a7/src/HOL/ex/Sqrt.thy

请注意，这是针对 Isabelle 的开发版本；它可能不适用于您的版本。无论如何，您应该在下载的 Isabelle 发行版中拥有与 src/HOL/ex/Sqrt.thy 相同版本的正确文件。

【讨论】：

【解决方案3】：

您可能遇到了一些编码困难 - 这就是我的问题（我遇到了同样的错误）。

Isabelle 使用所谓的“Isabelle 符号”来表示 unicode 字符（参见三个（参考手册）[http://isabelle.in.tum.de/doc/isar-ref.pdf] 来自第 307 页）。

如果您使用与Isabelle 2014 一起分发的jEdit IDE，那么--> 看起来与\<longrightarrow>（伊莎贝尔符号）相同。第一个无法解析，第二个是正确的。如果您复制并粘贴 wiki 代码，这就是它损坏的原因。

您还可以查看<yourIsabelleInstallFolder/src/HOL/Isar_Examples.thy 中的示例，以进一步使用伊莎贝尔符号和用 Isar 语言编写的证明的一般结构。

【讨论】：