Email Gateway (Aug 18 2022 at 16:25): Email Gateway (Aug 18 2022 at 16:25):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear members of Isabelle group
Recently, my formalization of convex analysis was added to Isabelle repository. Before doing this, it was important to decide which lemma should go to which theory. For example, I proved some lemmas which do not mention convexity at all, and it was logical to move them up to Euclidean_Space, or, say, Topology_Euclidean_Space.
While doing this, I noticed, that in absolutely every case the correct theory was the highest possible theory in the hierarchy, namely the highest possible theory where all the notions needed to formulate and prove a lemma was introduced. This suggests that this process could be automated: user adds a (finished) theory to repository, press a button, and all the lemmas automatically “travel” to the correct theory. This would not only simplify the job for theory organization, but, more importantly, significantly simplify the search in Isabelle. If I want to find a lemma about, say, dimension, which does not use any other notion, I can be sure that it is in the same theory, where the notion of dimension is defined. Now the relevant lemma may be inside some unexpected theory (in the Library or even in the archive of formal proof) whose author was just too lazy to move it up.
The next question is where to put a lemma inside a theory. An obvious answer would be to add new lemmas to the end of a theory. If, however, a theory contains many definitions, this would lead to a collection of many unrelated lemmas at the end of a theory. Let us define a “block” inside the theory to be a part from one definition to another one, and add new lemmas to the end of the “highest” possible block. This would group lemmas inside a theory nicely. Ideally, if you would like to have many small theories, in the Library, you could introduce an informal rule “Let us put just one definition per theory” (clearly, except that related definitions like Sup and Inf should be in one theory) and give it a corresponding name. In this case we would have, say, theory “affine_dimension.thy” containing all the lemmas about affine_dimension which do not involve further concepts.
Clearly, every rule has exceptions. A user may want to move some lemmas “down in the hierarchy” for some specific reasons. For such a situation, you could introduce, say, some attribute like “Force” to force this lemma(s) to stay in this theory and do not apply an automated theory reorganization for it. But this situation seems to be rather exceptional (never happens for my big theory with hundred of lemmas). In general, the suggested functionality would simplify the theory reorganization now, and make it possible in the future, when the size of the libraries would be so huge that it would be practically impossible to reorganize it by hand.
Sincerely,
Bogdan
Email Gateway (Aug 18 2022 at 16:25):From: Tobias Nipkow <nipkow@in.tum.de>
It turns out that the NICTA group in Sydney have such a tool and I
expect they will make it available at some point in the not too far future.
Tobias
grechukbogdan schrieb:
Email Gateway (Aug 18 2022 at 16:26):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Tobias
Thank you! I am happy to hear this.
It would be extremely interesting to apply such a tool to the existing Isabelle library (including The Archive of Formal Proofs) and look for the result.
After such a reorganization, it should be much easier to search for lemmas in Isabelle: You are sure that a lemma is in the same theory where is the last definition it uses.
It would remain to have a convenient search tool for definitions, notation, etc.
Sincerely,
Bogdan
Last updated: Nov 21 2024 at 12:39 UTC