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
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.
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
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
Maybe some of the other developers could comment on how difficult this
might be to implement.
This archive was generated by a fusion of
Pipermail (Mailman edition) and