Re: [isabelle] Search in the whole Isabelle Library



One of the things we found useful on the L4.verified project is the isabelle wwwfind tool, which starts a web server that responds to find-theorem requests.

It doesn't do anything more than the usual find theorems, but it means you can have a search context which is wider than your current context without having to keep two emacses on your desktop. We had an obvious candidate for the all-the-world image to use, which may not be so obvious in anyone else's project.

It was also handy on our project to have the server tracking the most recent stable version, since at any time the all-the-world image was likely to be broken.

This doesn't solve the problem you're interested in, which is parsing the search arguments in the current context and then searching in a wider context. I suspect the tool you want might not be difficult at all to write - just apply the parser of the existing theorem searcher, code the patterns again using their long names ("_ < _" becomes "HOL.ord_class_less _ _") and send that to the web server.

Yours,
    Thomas.

On 02/11/10 09:58, Brian Huffman wrote:
On Mon, Nov 1, 2010 at 5:22 AM, grechukbogdan<grechukbogdan at yandex.ru>  wrote:
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.
A feature I would like to see in Isabelle would be an "import
qualified" option, like Haskell has.

The idea is that you could go ahead and say "import qualified Library"
at the top of your theory file, and it would bring all of the theorems
from that theory into scope (and make them available for
find-theorems, auto-solve, etc.) but it would not bring any more
unqualified constant names into scope, or import any notations or
other syntax. Any constants imported in this way could only be
referred to by their fully-qualified names, as if they had been hidden
by the "hide_const (open)" command. The point is that a qualified
import should not affect the parsing of terms in your theory in any
way.

I think such a feature would let you do all the kinds of theorem
searching you want to do, plus it would be useful in lots of other
situations, too.

Maybe some of the other developers could comment on how difficult this
might be to implement.

- Brian







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