[isabelle] Feature suggestions: More useful output



Dear developers,

I’d like to share some ideas how working with Isabelle could be a bit
more efficient, at least for me and my workflow.

All I am describing is the 2012 release, used via jEdit.

Generally, I could imagine the output window being a bit more
informative, in particular with error messages.

For example, a failed "by method" currently just prints “Failed to
finish proof.” To fix this, I now have to change the "by" to "apply",
look at the result, fix it, and change it back. Could it not print
“Failed to finish proof. Remaining goals: ....”?

A command that does not provide any output at all is “lemma” (and also
“lemmas”). Sometimes, I feel the need to check how Isabelle actually
sees the lemma, e.g. to see what types she has inferred, or to check
whether I am really done or if there is still a [!] behind the lemma¹.
Currently, I have to use “thm name” after the lemma for that (and give
the lemma a name if it does not have one yet). Would it be possible to
have the lemma command already print that information?

Another error that could be make more helpful is “Unknown fact "..."”.
Often I don’t remember the name of a lemma exactly – was it set_finite
or finite_set? I then have to fire up "find_theorems name:..", which is
quite a bit of typing.
GHC recently has started to give spelling corrections (the 10 best fits
based on edit distance, IIRC) for every kind of unknown-something error.
If Isabelle could do the same, this would be great. I’d imagine that in
the context of Isabelle lemmas the edit distance should give special
treatment to reordering the parts of the string that are separated by
‘_’, as it is often the order of the components of the name that I fail
to remember, and count that as one step.
I guess Isabelle usually has many more lemmas in scope than GHC has
functions and this might be a bit slow. But the output does not have to
be generated at once and if the error message is printed before the list
is calculated, this should not harm anyone.²

Last on my list for today is a more interactive variant of print_cases.
When I currently write
        lemma "n + 1 = 1 + (n::nat)"
        proof(induct n)
I have
        proof (state): step 1
        
        goal (2 subgoals):
         1. 0 + 1 = 1 + 0
         2. ⋀n. n + 1 = 1 + n ⟹ Suc n + 1 = 1 + Suc n 
and with 
        print_cases
it prints
        cases:
          0:
            let "?case" = "0 + 1 = 1 + 0"
          Suc:
            fix n_
            let "?case" = "Suc n_ + 1 = 1 + Suc n_"
            assume Suc.hyps: "n_ + 1 = 1 + n_" and Suc.prems: 

What I am missing is a combination of both that is ready to be used as
the structure of an Isar proof, e.g. either completely explicit:

          show "0 + 1 = 1 + 0"
            sorry
        next
          fix n
          assume "n + 1 = 1 + (n::nat)"
          show "Suc n + 1 = 1 + Suc n"
            sorry
        qed

or, depending on personal preference and number and complexity of the
hypotheses, using the provided case names (and using "case goal1..." if
there are no case names):
        
          case 0
          show ?case
            sorry
        next
          case (Suc n)
          show ?case
            sorry
        qed

From there I guess it would be a small step to allow the user to insert
the output of this command (say print_isar_structure) into the proof
document with one click, similar to how sledgehammer works.

That’s it for today. Thanks for your work,
Joachim


¹ And just to not only list things that I am missing: I find this
marking of lemmas whose prove contains a sorry very useful feedback. It
it were not done, I’d have to ask for it :-)

² Actually, it seems that implementing this feature would be a very
local task that is suitable for first-time Isabelle contributors. If you
say that such a feature would be accepted, I could give it a shot.


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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