Re: [isabelle] Search in the whole Isabelle Library

On Mon, Nov 1, 2010 at 5:22 AM, grechukbogdan <grechukbogdan at> 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
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.