Организация `твоих` файлов, которые поставляются с Isabelle

Question

Я относительно новичок в Isabelle, и я озадачен организацией файлов thy, которые поставляются с Isabelle.

Почему некоторые файлы, относящиеся к одному телу знаний, находятся в ~~src/HOL, тогда как другие находятся в ~~src/HOL/<theoryname>?

E.g. Почему GCD находится в ~~src/HOL, а не в ~~src/HOL/Number_Theory?

---

Похожий вопрос: В чем разница между ex папку и Isar_Examples папку в ~~src/HOL? Не было бы более естественным объединить их?

---

Кроме того, что это document папка с ~~src/HOL для?

Answer 1

Изабель почти 30 лет и значительно изменилась за это время. Файл GCD.thy, например, был создан 12 лет назад и предоставил только константу gcd :: nat ⇒ nat ⇒ nat. Тогда я не думаю, что каталог Number_Theory даже существовал. Фактически, HOL/Number_Theory также является чем-то неправильным в наши дни: я реорганизовал большую часть его вместе с Флорианом Хафтманом в течение последних нескольких лет, и теперь такие вещи, как GCD и primality, определяются не только по номерам, но и по любому факториальному кольцу. Лучшей категоризацией будет HOL/Algebra, но это уже принято другой формализацией, которая отличается совсем другим (более абстрактным) вкусом, чем то, что мы делали.

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

Упомянем лишь несколько подкаталогов:

• Очень общий материал находится в главном каталоге HOL. (Новые файлы редко добавляют там, я бы сказал)
• вещи, касающиеся простых чисел и связанных с ними понятий в HOL/Number_Theory
• Абстрактная алгебра в HOL/Algebra.
• Продвинутый анализ и теория измерения находится в HOL/Analysis.
• теории вероятностей в HOL/Probability
• Более специализированные вещи, представляющие общего интереса в HOL/Library
• HOL/Decision_Procs содержит некоторые процедуры принятия решений для специализированных классов свойств (например, приближающихся вещественных функций, линейные вещественные арифметических), которые по сути «нажмите кнопку для доказать теорему ".
• HOL/Word содержит факты о целых числах конечных чисел (то есть с фиксированной длиной бита)
• HOL/ex содержит все виды материалов. Я думаю, что этот справочник был местом, где бы существовали всевозможные небольшие, более специализированные разработки до того, как существовал АФП.
• Isar_Examples, по-моему, представляет собой сборник теорий Макария Венцеля, чтобы продемонстрировать возможности структурированного языкового языка Isar, т. Е. Типичные шаблоны и тематические исследования в том, как писать хорошо структурированные доказательства Isar.
• Файл каталога ROOT указывает сеансы, которые представляют собой сборники теорий, которые будут «объединены». Например, изображение HOL - это тот, который Isabelle загружает по умолчанию при запуске, так что вам не нужно ждать несколько минут, пока все основные теории не будут переработаны. Если вы, например, используйте материал от HOL/Analysis, это хорошая идея для создания изображения сеанса HOL-Analysis и загрузки с isabelle jedit -l HOL-Analysis, так что вам не придется ждать, пока все теории будут построены каждый раз, когда вы запускаете Изабель.
• Каталог document работает в сочетании с файлом ROOT. В нем содержится некоторый шаблон LaTeX, в который встроен вывод Isabelle LaTeX, и из него создаются некоторые PDF-файлы (контур доказательства и доказательный документ). Лично я не нахожу эти ужасно полезные (на мой взгляд, проще просто посмотреть код непосредственно в Isabelle/jEdit).

Более подробную информацию о подготовке документов и заседаниях можно найти в the Isabelle systems manual.