*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Search, Importing, and Naming in Isabelle*From*: grechukbogdan <grechukbogdan at yandex.ru>*Date*: Fri, 11 Jun 2010 21:38:14 +0400

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.

- Previous by Date: [isabelle] power class instantiation
- Next by Date: Re: [isabelle] Code generator "eq" instances
- Previous by Thread: Re: [isabelle] safe for boolean equality
- Next by Thread: [isabelle] Code generator: overloaded numeric constants
- Cl-isabelle-users June 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list