Email Gateway (Aug 18 2022 at 16:24): Email Gateway (Aug 18 2022 at 16:24):From: grechukbogdan <grechukbogdan@yandex.ru>
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:
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
Email Gateway (Aug 18 2022 at 16:26):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Email Gateway (Aug 18 2022 at 16:27):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
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.
Email Gateway (Aug 18 2022 at 16:30):From: Makarius <makarius@sketis.net>
This is a recurrent theme on isabelle-users or isabelle-dev for several
years already. It is indeed difficult, but we are moving towards more or
less exactly that for some years, getting closer after each round of
reforms and cleaning up legacy features that are in the way.
It will work via the advanced infrastructure of local theories (and global
specifications will be a special case). Most likely, this means that once
the infrastructure is up and running, packages that are not "localized"
would still emit their global declarations.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC