syntax-error - 如何在 Isabelle 中正确使用关键字 'theorem'？

Question

我从 Isabelle 的维基百科页面获得了以下代码:

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 中检查的正确方法是什么？

Answer 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