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

Isabelle/HOL – это среда для формальных доказательств. Чтобы начать, достаточно скачать Isabelle с официального сайта isabelle.in.tum.de и запустить IDE на базе jEdit. После запуска в jEdit можно создать новый файл-«теорию» с расширением .thy. Например, Hello.thy и вставим в него:

theory Hello imports Main begin end

Имя теории (Hello) должно совпадать с именем файла. Строка imports Main подключает стандартную библиотеку HOL(в целом подключаем ее всегда). Begin и end это операторы начала и окончания нашей теории(кто работал с паскалем - тот поймет).

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

Внутри теории можно задавать константы и функции. Например, определим числовую константу:

definition x :: nat where "x = 5"

Здесь x – константа типа nat (натуральное число) со значением 5. Показать вычисление помогает команда value:

value "x + 2"

Аналогично можно определить функцию. Ключевое слово fun служит для задания (возможно рекурсивной) функции. Например:

fun double :: "nat ⇒ nat" where "double n = n + n"

эта функция возвращает удвоенное значение аргумента. Тогда команда

value "double 3" покажет 6. После определения Isabelle автоматически проверит, что функция корректно типизирована и «структурно сходится».

Типы данных и выражения

Isabelle/HOL имеет несколько встроенных типов: nat – натуральные числа, задаются конструкторами 0 и Suc (так что 0, Suc 0, Suc (Suc 0) и т.д.) int – целые числа (включая отрицательные). bool – булевы значения с двумя константами True и False string – строки символов (по сути списки символов).

С этими типами можно работать просто. Например, условное выражение:

value "if (2 < (5::nat)) then 1 else 0"

покажет 1, потому что 2 < 5 истинно. С булевыми значениями можно строить and, or и так далее. Со строками тоже нетрудно: их можно конкатенировать через @. Например,

value ""foo" @ "bar""

выдаст строку "foobar".

Базовый синтаксис и работа с базовыми операциями довольно простые, самые приколы начнутся позже, когда потребуется работать с доказательствами, леммами, развертками, ну и лямбдами. Но обо всем этом позже.