Organisation de `thy` fichiers qui viennent avec Isabelle

Question

Je suis relativement nouveau à Isabelle et je suis intrigué par l'organisation des fichiers thy qui viennent avec Isabelle.

Pourquoi certains fichiers concernent-ils le même corpus de connaissances dans ~~src/HOL, alors que d'autres sont dans ~~src/HOL/<theoryname>?

E.g. Pourquoi GCD est dans ~~src/HOL et pas dans ~~src/HOL/Number_Theory?

---

question similaire: Quelle est la différence entre le dossier et le dossier exIsar_Examples dans ~~src/HOL? Cela n'aurait-il pas été plus naturel de les fusionner?

---

Aussi, quel est le dossier document de ~~src/HOL pour?

Answer 1

Isabelle a presque 30 ans et a beaucoup changé au cours de cette période. Le fichier GCD.thy, par exemple, a été créé il y a 12 ans et ne fournissait que la constante gcd :: nat ⇒ nat ⇒ nat. À l'époque, je ne pense pas que le répertoire Number_Theory ait existé. En fait, HOL/Number_Theory est aussi quelque chose d'un abus de langage de nos jours: J'ai réorganisé beaucoup de choses avec Florian Haftmann au cours des dernières années et maintenant des choses comme GCD et la primalité sont définies non seulement sur les nombres, mais sur n'importe quel anneau factoriel. Une meilleure catégorisation serait HOL/Algebra, mais cela est déjà pris par une autre formalisation qui a une saveur très différente (plus abstraite) que ce que nous avons fait. Donc, vous voyez, une grande partie de l'organisation de la distribution est principalement un accident historique. Parfois, les gens vont généraliser/nettoyer/réorganiser les choses, mais il y a parfois des théories curieusement placées à cause de telles choses.

pour ne citer que quelques sous-répertoires:

• Substance très générale est dans le répertoire principal de HOL. (Nouveaux fichiers sont rarement ajoutés là, je dirais)
• choses concernant les nombres premiers et les concepts liés sont HOL/Number_Theory
• algèbre abstraite est HOL/Algebra.
• L'analyse avancée et la théorie de mesure est dans HOL/Analysis.
• La théorie des probabilités est HOL/Probability
• choses d'intérêt général sont plus spécialisés dans HOL/Library
• HOL/Decision_Procs contient des procédures de décision pour les classes spécialisées de propriétés (par exemple, se rapprochant des fonctions réelles, l'arithmétique réelle linéaire) qui sont essentiellement « bouton de presse prouver le théorème '.
• HOL/Word contient des faits sur des nombres entiers de taille finie (par exemple avec une longueur de bit fixe)
• HOL/ex contient toutes sortes de choses. Je pense que ce répertoire était l'endroit pour mettre toutes sortes de petits développements plus spécialisés avant l'existence de l'AFP.
• Isar_Examples, je pense, est essentiellement la collection de théories de Makarius Wenzel pour démontrer les capacités du langage de preuve structurée Isar, c'est-à-dire des modèles typiques et des études de cas pour écrire des preuves Isar bien structurées.
• Le fichier ROOT d'un répertoire spécifie sessions, qui sont des regroupements de théories à regrouper. Par exemple, l'image HOL est celle que Isabelle charge par défaut au démarrage, de sorte que vous n'avez pas à attendre plusieurs minutes avant que toutes les théories de base ne soient retraitées. Si par exemple vous utilisez des trucs de HOL/Analysis, c'est une bonne idée de construire l'image de session HOL-Analysis et chargez-la avec isabelle jedit -l HOL-Analysis afin que vous n'ayez pas à attendre que toutes les théories soient construites chaque fois que vous démarrez Isabelle. Le répertoire document fonctionne en combinaison avec le fichier ROOT. Il contient un modèle LaTeX dans lequel la sortie LaTeX d'Isabelle est intégrée, et à partir de là, certains PDF (le contour d'épreuve et le document d'épreuve) sont générés. Personnellement, je ne trouve pas cela terriblement utile (à mon avis, il est plus facile de regarder le code directement dans Isabelle/jEdit).

Vous trouverez plus d'informations sur la préparation de documents et les sessions dans the Isabelle systems manual.