How to properly use keyword 'theorem' in Isabelle?

Question

I obtained the following code from Isabelle's wikipedia page:

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

However, when I copy this text into an Isabelle instance, there are multiple 'do not enter' symbols to the left of each line. One says 'Illegal application of command "theorem" at top level' so I assumed that you cannot simply define a theorem at the top level and the wikipedia page was not supplying a complete initial example. I wrapped the theorem in a theory as follows:

theory Scratch
imports Main
begin

(* Theorem *)

end

Isabelle stopped complaining about the theorem, but, on the second line of the theorem, it now says:

Inner lexical error at: ℚ
Failed to parse proposition

It is also complaining about the proof line:

Illegal application of command "proof" in theory mode

It also has an error for the remaining lines in the theorem. What is the proper way to wrap this theorem provided by wikipedia so that it can be checked in Isabelle?

Answer 1

Probably you encountered some encoding difficulties - this was the problem in my case (I got the same error).

Isabelle uses so called 'Isabelle symbols' to represent unicode characters (see three (reference manual)[http://isabelle.in.tum.de/doc/isar-ref.pdf] from page 307).

If you use the jEdit IDE that gets distributed with Isabelle 2014 then --> looks the same as the \<longrightarrow> (the Isabelle symbol). The first cannot be parsed, the second is correct. If you copy and pasted the wiki-code this is the reason why it broke.

You can also take a look at the examples in <yourIsabelleInstallFolder/src/HOL/Isar_Examples.thy for further use of the isabelle symbols and the general structure of proofs written in the Isar language.

Answer 2

Your guess that you have to wrap the “theorem” command in a theory in the way you did is correct. However, you need a few more imports, imports Main does not even load the theories containing sqrt, rational numbers, and prime numbers.

Moreover, the proof on Wikipedia is somewhat outdated. Isabelle is a very dynamic system; its maintainers port all the proofs in the library and the Archive of Formal Proofs with every release, but code snippets lying around somewhere (e.g. Wikipedia) tend to become outdated after a while, and I think this particular one is positively ancient.

For an up-to-date proof of pretty much the same thing, properly embedded in a theory with the right imports, look here: http://isabelle.in.tum.de/repos/isabelle/file/4546c9fdd8a7/src/HOL/ex/Sqrt.thy

Note that this is for the development version of Isabelle; it may not work with your version. In any case, you should have the same file in the correct version as src/HOL/ex/Sqrt.thy in your downloaded Isabelle distribution.

Answer 3

I completely agree to Manuel, that just importing Main is not sufficient. If you're not interested in proofs, but just on testing irrationality then a good possibility would be to include $AFP/Real_Impl/Real_Impl from the Archive of Formal Proofs: then testing irrationality becomes very easy:

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