Isabelle/HOL: первые шаги

Если коротко, Isabelle/HOL - это среда для формальных доказательств, где математика жестко доминирует на кодом.

Как начать:

1)Скачиваем с isabelle.in.tum.de 2)Запускаем jEdit, да у изабельки своя собственная IDE 3)Создаём файл с расширением .thy (например, Hello.thy) `theory Hello imports Main begin end Имя теории должно совпадать с именем файла. imports Main всегда нужен - он подключает стандартную библиотеку HOL, в которой уже реализована и доказана вся школьная и университетская алгебра.

Константы и функции

Константа: `definition x :: nat where "x = 5" value "x + 2" вернёт 7

Функция (рекурсия тоже работает): `fun double :: "nat ⇒ nat" where "double n = n + n

Isabelle сам проверит типы и что рекурсия корректна. Если что-то не так - отметит место с ошибкой.

Типы данных: nat - натуральные числа (0, Suc 0, Suc (Suc 0) …) int - целые (включая отрицательные) bool - True / False string - строки (по сути, списки символов)

Примеры: `value "if (2 < (5::nat)) then 1 else 0" вернёт 1 value ""foo" @ "bar"" вернёт "foobar"

Доказательства, леммы, свёртки, лямбды рассмотрим в следующих постах серии, там все намного сложнее и интереснее, чем просто в объявлении переменных и функций.````