Как правильно использовать ключевое слово «теорема» в Изабель?

Я получил следующий код со страницы Википедии Изабель:

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

Изабель перестала жаловаться на теорему, но теперь во второй строке теоремы говорится:

Inner lexical error at: ℚ
Failed to parse proposition

Он также жалуется на строку доказательства:

Illegal application of command "proof" in theory mode

Также есть ошибка для остальных строк теоремы. Как правильно обернуть эту теорему из Википедии, чтобы ее можно было проверить в Изабель?


syntax-error theorem proof isabelle
person Timothy Swan    schedule 30.07.2014    source источник

Ответы (3)


arrow_upward
2
arrow_downward

Я полностью согласен с Мануэлем, что простого импорта 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
person René Thiemann    schedule 31.07.2014
comment
Хорошо, я не знал, что у нас есть процедура принятия решения по этому поводу. Однако я думаю, что стоит отметить, что eval в каком-то смысле не так хорош, как «реальное» доказательство, потому что, хотя сама процедура принятия решения является надежной, eval полагается на генератор кода для генерации исполняемого кода для процедуры принятия решения, а генератор кода не проверен, хотя, по моему опыту, он очень надежен. - person Manuel Eberl; 31.07.2014

arrow_upward
2
arrow_downward

Ваше предположение о том, что вам нужно обернуть команду «теорема» в теорию так, как вы это сделали, верно. Однако вам нужно еще несколько импортов, imports Main даже не загружает теории, содержащие sqrt, рациональные числа и простые числа.

Более того, доказательство в Википедии несколько устарело. Изабель - очень динамичная система; его сопровождающие переносят все доказательства в библиотеке и Архив формальных доказательств с каждым выпуском, но фрагменты кода валяются где-то (например, Википедия) через какое-то время устаревает, и я думаю, что это определенно древнее.

Актуальное доказательство того же самого, правильно встроенного в теорию с правильным импортом, можно найти здесь: http://isabelle.in.tum.de/repos/isabelle/file/4546c9fdd8a7/src/HOL/ex/Sqrt.thy

Обратите внимание, что это для разрабатываемой версии Isabelle; это может не работать с вашей версией. В любом случае у вас должен быть тот же файл в правильной версии, что и src / HOL / ex / Sqrt.thy в загруженном вами дистрибутиве Isabelle.

person Manuel Eberl    schedule 30.07.2014

arrow_upward
1
arrow_downward

Возможно, вы столкнулись с некоторыми трудностями при кодировании - это была проблема в моем случае (у меня такая же ошибка).

Изабель использует так называемые «символы Изабель» для представления символов Юникода (см. Три (справочное руководство) [http://isabelle.in.tum.de/doc/isar-ref.pdf] со страницы 307).

Если вы используете jEdit IDE, которая распространяется с Isabelle 2014, то --> выглядит так же, как \<longrightarrow> (символ Изабель). Первый не поддается синтаксическому анализу, второй правильный. Если вы скопируете и вставите вики-код, это причина того, что он сломался.

Вы также можете взглянуть на примеры в <yourIsabelleInstallFolder/src/HOL/Isar_Examples.thy для дальнейшего использования символов isabelle и общей структуры доказательств, написанных на языке Isar.

person jules    schedule 26.11.2014