*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Feature suggestions: More useful output*From*: Joachim Breitner <breitner at kit.edu>*Date*: Fri, 23 Nov 2012 09:41:02 +0100

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**

**Follow-Ups**:**Re: [isabelle] Feature suggestions: More useful output***From:*Makarius

**Re: [isabelle] Feature suggestions: More useful output***From:*Makarius

**Re: [isabelle] Feature suggestions: More useful output***From:*Makarius

**Re: [isabelle] Feature suggestions: More useful output***From:*Makarius

**Re: [isabelle] Feature suggestions: More useful output***From:*Makarius

- Previous by Date: Re: [isabelle] ?spam? Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]
- Next by Date: [isabelle] Context Free Language
- Previous by Thread: [isabelle] Preprocessor for code_pred
- Next by Thread: Re: [isabelle] Feature suggestions: More useful output
- Cl-isabelle-users November 2012 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