[isabelle] Search in Isabelle



Dear Isabelle Users,
I am working on project, which includes 1) convex analysis formalization in Isabelle, and 2) provide a feedback about Isabelle, including comments and suggestions.
Here is my first feedback letter, mostly about the search in Isabelle.
When I want to prove some result, the first question is if this result new or not, and it would be nice to know this without reading the theories from the Library. Fortunately, if I guess the exact formulation of existing lemma, I can do search, or just formulate the lemma and get message like “The current goal could be solved directly with...”. The first important problem here is that if I formulate such a lemma inside the proof in command “have”, no suggestion is given, and it is hard to guess to check every time, as a result I already reproved some existing results. 

Suggestion 1. The message like  “The current goal could be solved directly with...” should appear not only after I formulate the existing result as a lemma, but also when I formulate it inside the proof, say after have. Ideally, something like this should work when the existing result appears as a subgoal in the proof, etc. 

The first part of this (about “have”) I have suggested during my first visit in June, and the reply was “good point. We will think about it”. This is very important because it will help to avoid duplicate job. Is it hard for realization?

Unfortunately, this mechanism is very sensitive for reformulations. For example, there exist a lemma “id x = x”, but I have no suggestions for lemma “x = id x”. In this and many similar cases Sledgehammer can help, but the same question arises: is it possible to run it in the background automatically, every time when I formulate a lemma or “have” statement? 

Suggestion 2: It should be a possibility to run Sledgehammer in the background automatically, every time when I formulate a lemma or “have” statement . If this is already possible, the suggestion is to make it more clear how to turn it on, because I cannot find the way to do this.

Unfortunately, even Sledgehammer does not help for a little bit more complicated lemmas. For example, it cannot prove the lemma 
f = g ↔ (!x. f x = g x)                            (1)
although this lemma is present in the library. As a result, a reformulation like
f = g ↔ (!x. g x = f x)                            (2)
is not addressed neither by Sledgehammer nor by lemma suggestion mechanism, and  I see no simple way for the user to find out that this lemma is not essentially new. May be, this way exists, and I just do not know about it?

Suggestion 3: As a minimum, merge lemma suggestion with Sledgehammer to create a new Sledgehammer which would prove at least (1). Ideally, it should be a mechanism which proves a reformulations like (2), and it should work automatically, to prevent user from reproving result. If there is another simple way to see that statements like (2) are not essentially new, it should be more clear documented,  because I cannot find a simple way to do this.

In my work, I need a definition of dimension. It states
dim V = (SOME n. EX B<=V. independent B & V<=span B & card B =n)   
I know from the tutorial that SOME is Hilbert operator, but when I tried to find the definition of SOME in Isabelle, the search failed. It turned out this was because SOME is an abbreviation, but it took me a long time and finally I needed help of another person.

Suggestion 4: There should be a simple way to see the any definition in Isabelle, even if I do not know in advance, is this a lemma, method, term, abbreviation,  notation, or something else. 

But even knowing the definition, I do not know how to work with this SOME. For example, if I assume that “dim V = m” I have “(SOME n. EX B<=V. independent B & V<=span B & card B =n) = m”, but I do not know how to extract this B from this definition and derive, say, that 
dim V = m ==> (EX B<=V. independent B & V<=span B & card B =m)            (3)
Ideally, together with definition it should be small set of example how to work with, say, SOME, but may be it is too much to formulate this as a suggestion (although such a help exists in many systems like Mathematica). Ok, could you please just tell me how to work with SOME, for example, how to prove (3)?
Also, to proceed with proof of my lemma, I will need to obtain this B and say that it is a basis in R^n, whence affine hull V = R^n But again, I cannot understand the definition of basis in Isabelle, because it contains symbol \<chi>, which is not in table A.1 in the tutorial, and it is hard to find what it means, see suggestion 4. Could you please explain me this notation, and how to work with basis, for example, how to prove that n independent vectors form a basis in R^n.

Sincerely,
Bogdan.





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