Возможно ли получить список всех предикатов и функций, которые я могу использовать в Isabelle?Все доступные предикаты в Isabelle
Поскольку чаще всего это происходит, я начинаю определять вручную предикат, который мне нужен для доказательства (например, coprime), только чтобы понять, что он уже существует.
Существует find_consts, который может искать определенные константы по типу или по имени, аналогично find_theorems, например. find_consts "'a list => nat" или find_consts name:"lim". По-видимому, это может также найти аббревиатуры, такие как coprime (что является аббревиатурой от gcd a b = 1).
Конечно, это может найти только константы, которые были определены в одной из теорий, которые вы фактически загрузили (прямо или косвенно). Всегда есть возможность, что необходимое вам понятие уже было оформлено где-то в ~~/src/HOL/Library или в какой-либо другой части дистрибутива или в AFP.
Когда я подозреваю, что это так, я просто собираю распространение или AFP для соответствующего ключевого слова, или я спрашиваю кого-то, кто может знать об этом. Спросить здесь о StackOverflow также может быть хорошей идеей, чтобы узнать что-то подобное, так как существует множество профессиональных пользователей Isabelle, которые часто посещают этот сайт и которые хорошо знают, что есть, а что нет.
Это отличные подсказки, спасибо! Но можете ли вы сказать мне, где именно вы нашли «coprime»? Поскольку поиск 'nat => nat' не возвращал coprime. Я также немного смущен, почему 'find_consts' возвращает функции, а не константы, как я ожидал бы от именования. – nicht
Функции также являются константами, только теми, которые имеют тип функции. «Константа» в Изабель просто означает, что это некоторая ценность, которая была заявлена в теории фона, в отличие от, например, связанной или свободной переменной. –
Во всяком случае, вы должны найти 'nat ⇒ nat ⇒ bool', чтобы найти' coprime'. К сожалению, это тоже не работает, поскольку coprimality определяется с помощью GCD, а GCD не определяется на 'nat', но гораздо более широко. Единственный разумный способ найти его - по имени, т. Е. 'Find_consts name: coprime'. (Вы можете найти '⇒ ⇒ '⇒ bool', но это вернет так много других вещей, которые вы никогда не найдете там что-нибудь полезное) –