Правильный способ повторного использования записей AFP в Изабель

Question

Скажем, я хочу формализовать предложение, которое говорит о кольцах многомерных полиномов в Изабель.

Связанная запись AFP выглядит следующим образом:

https://www.isa -afp.org / records / Polynomials.html

Однако в ИзабельЯ только нахожу распределение:

HOL / Algebra / Polynomials.thy

, которое, кажется, имеет дело только с одномерными полиномами.В соответствии с `find_theorems` в AFP я пришел к выводу, что мне нужно загрузить запись AFP и импортировать ее из некоторого каталога на моем компьютере.Это, в свою очередь, подразумевает повторение процесса для всех зависимостей записи AFP.

Это правильный / наиболее эффективный путь?

Answer 1

Да.Чтобы использовать результаты любой теории в Изабель, вы должны обработать ее и ее зависимости.

Для AFP обычно проще всего скачать весь архив и импортировать нужную вам теорию.Изабель будет затем обрабатывать только те, от которых она зависит, а не весь архив, то есть она сделает разрешение зависимостей за вас.

(См. Также документы на веб-сайте AFP об использовании другой записи AFP, чтобы узнать, как убедиться, что Изабель видит в AFP взгляды на зависимости после того, как вы ее загрузили).