*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Search in the whole Isabelle Library*From*: grechukbogdan <grechukbogdan at yandex.ru>*Date*: Mon, 01 Nov 2010 15:22:34 +0300

Dear members of Isabelle group During my trip to Munich, we had an interesting discussion about search in the Isabelle Library. My point was that I would like to have a search in the whole library (not only imported theories), and we discussed some (complicated) ways for realization. I am thinking whether the following observation could simplify the situation. The naive way to use the current search facility in Isabelle to do global search would be to try to import everything. This, however, does not work directly: for example, if I try to write “imports Library” and than type lemma “(A :: real set)<B” I have an error, because “B” is reserved for something else. Moreover, even symbol “<” can have different meaning in different places of the library. In other words, Isabelle cannot parse (understand) mathematical expressions in this case. As I understand, any search can be divided by two steps. First one is parsing, understanding the search string typed by a user. Second – search for relevant lemmas in the Library. Now, I would imagine the following simple search algorithm. 1) At the level of parsing, look at the imported theories only, as it is now. For example, string like “(A :: real set)<B” should be correctly understood, that “user wants to find lemmas where one set of real numbers is a subset of another one”. 2) Next, do the search in such a way as if the whole Library would be imported. Now: - If in some theory there is a lemma containing “A<B” where A and B are real sets, and “<” means “be a subset”, it will be founded. - If in some theory there is a lemma looking like “A<B”, but with “<” having completely different meaning, it will not be founded, because “user wants to find lemmas where one set of real numbers is a subset of another one”. As I understand, this is just a modification of the current search facility, and should be easier to implement that what we were discussing. Moreover, I would like “auto solve” to work in a similar way – UNDERSTAND the lemma based on imported theories only, but then look in the whole library if exactly such a lemma is already proved. Are there any principal problems with this? Sincerely, Bogdan

**Follow-Ups**:**Re: [isabelle] Search in the whole Isabelle Library***From:*Brian Huffman

- Previous by Date: [isabelle] MetiTarski 1.7 released!
- Next by Date: [isabelle] Automated theory reorganization in Isabelle
- Previous by Thread: [isabelle] MetiTarski 1.7 released!
- Next by Thread: Re: [isabelle] Search in the whole Isabelle Library
- 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