Email Gateway (Aug 18 2022 at 15:29): Email Gateway (Aug 18 2022 at 15:29):From: grechukbogdan <grechukbogdan@yandex.ru>
Dear Isabelle Users
My theory imports Topology_Euclidean_Space. Recently, I needed some definition and lemmas, search gives no results, I proved everything myself, spending a lot of time, and then discover exactly the same lemmas in SetAndFunctions.thy in the Library. As a result, duplicate work was done. The problem was is that Topology_Euclidean_Space.thy do not import this theory. Clearly, I can import SetAndFunctions.thy, but then other useful lemmas can be in other theories, and the same problem would happen.
Question 1. To avoid duplicate job, I want to be able to search over the whole Isabelle library. If search gives no results, I want to be sure that exactly this lemma do not exists in ANY existing theory in Isabelle. Ideally, lemma suggesting mechanism and Sledgehammer also should work in a similar way. Does there exists a way to do this?
An obvious answer would be to import the “last” theory in the whole hierarchy, which would import everything, all the theories that I have in the HOL folder on my computer, including subfolders Multivariate_Analysis, Library, and all the others.
Question 2. Does there exists such a “last” theory in, say, Isabelle_2009 version?
I have tried to import at least Library.thy, which imports all the theories from Library folder.
imports Topology_Euclidean_Space, Library
But after this my theory stopped working. For example, by “ball” Isabelle understands now some “dist_class.ball” instead of “ Topology_Euclidean_Space.ball”. Interestingly, writing
imports Library, Topology_Euclidean_Space
fixes this problem.
Question 3. How this naming conflicts are resolved in Isabelle? In parallel (independent) theories, I can prove two theorems with the same name, or define two different notions with the same name. Now, when I import both these theories, what happens? The names from the last imported theory have the first priority?
Moreover, not only “ball” has different meaning. Even letter B is now reserved for some “Operand B :: color”....
Question 4. May be, there is some way to say which notation I want to import, and which I do not want? In mathematics, if I want to refer to some paper and use its results, and letter B in that paper is reserved for color operand, it does not mean that I cannot use notation B as a free variable in my paper...
May be, these problem imply that I just should not import everything? But in this case, returning to question 1, how to do a general search, which would include theories which I do not import?
Sincerely,
Bogdan Grechuk.
Last updated: Apr 25 2024 at 04:18 UTC