[isabelle] Search, Importing, and Naming in Isabelle



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. 





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