*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Automated theory reorganization in Isabelle*From*: grechukbogdan <grechukbogdan at yandex.ru>*Date*: Thu, 11 Nov 2010 13:54:31 +0300*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4CDADBBE.9080008@in.tum.de>*References*: <301131288614303@web79.yandex.ru> <4CDADBBE.9080008@in.tum.de>

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 10.11.10, 20:51, "Tobias Nipkow" <nipkow at 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: > > 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 > > > > -- Здесь спама нет http://mail.yandex.ru/nospam/sign

**References**:**[isabelle] Automated theory reorganization in Isabelle***From:*grechukbogdan

**Re: [isabelle] Automated theory reorganization in Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] rewriting with assumptions from right to left
- Next by Date: [isabelle] Isabelle and model checkers
- Previous by Thread: Re: [isabelle] Automated theory reorganization in Isabelle
- Next by Thread: Re: [isabelle] Specializing types in locales
- Cl-isabelle-users November 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list