[isabelle] Search in the whole Isabelle Library

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? 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.