*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Beginner's struggles*From*: Ian Lynagh <igloo at earth.li>*Date*: Sat, 14 Aug 2010 01:41:17 +0100*User-agent*: Mutt/1.5.18 (2008-05-17)

Hi all, Here are some of the things I have been struggling with as an Isabelle complete beginner (but with a some knowledge of coq). I hope you will find this useful in improving the Isabelle language and/or docs. I have "(Isabelle2009-1: December 2009)". How does Isabelle know how much to process when I click the "Process the next proof command" in Proof-General? In coq this is nice and simple: It processes up to the next "." (that's actually a slight simplification, but that's not relevant here). With Isabelle, I'm not really sure what happens. If I have this source: theory Test imports Main begin lemma "A & B ==> B & A" proof and I have processed up to, but not including, "proof", then pressing the arrow processes "proof" and succeeds. But if I also write "foo" after "proof", even with some whitespace: theory Test imports Main begin lemma "A & B ==> B & A" proof foo Isabelle says *** Unknown proof method: "foo" *** At command "proof". and if I had put a "." after "proof" theory Test imports Main begin lemma "A & B ==> B & A" proof. then now the "lemma" line fails with *** Outer syntax error: end of input expected, *** but command proof was found I can't emphasise enough just how thoroughly confused I am by this. =================================================================== It also makes Isabelle hard to use for me. My coq scripts generally look like: <valid proof that I've finished>. <the line I'm working on>. <invalid stuff, alternate possibilities for the next line, etc> and the invalid stuff, coming after a ".", doesn't interfere with my work on the current line. I have to keep fiddling with comments to do this in Isabelle. How does one write a comment in Isabelle? If I search for "comment" in tutorial.pdf then the first real mention is on p67(p57), in the "Document Preparation" section. Three pages later, in the same section, says Isabelle source comments, which are of the form (* ... *) and as far as I can see this is the only mention in the document - a section I didn't look at, as I wasn't concerned with making PDFs at this stage. "comments" is also not in the index; I would never have thought to look up "source comments". I would expect to be told what comments look like around p14-15(p4-5). Am I right in thinking that "--" does not start a comment in a source file? Because while trying to copy/paste/run this example: lemma assumes P: "! x. P x" shows "! x. P(f x)" proof -- allI: (!! x. ?P x) = ! x. ?P x fix a from P show "P(f a)" .. -- allE : [[ x. ?P x; ?P ?x = ?R ]] = ?R qed from p9 of isar-overview.pdf I certainly assumed that it did. Having to look up the ASCII names of the symbols is annoying enough; why not use Isabelle comment syntax when putting comments in the middle of example Isabelle code? I was very surprised to not find Isabelle packaged in Debian. This was a significant factor in me not also trying Isabelle about 2 years ago, when I started with coq, and if coq's Czar showed more signs of life I would not have considered trying Isabelle. I am sad to see in http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=494491 that this seems to be deliberate. Thanks for reading, and I hope you found this useful. Thanks Ian

**Follow-Ups**:**Re: [isabelle] Beginner's struggles***From:*Makarius

- Previous by Date: Re: [isabelle] simple proof question
- Next by Date: Re: [isabelle] Beginner's struggles
- Previous by Thread: Re: [isabelle] simple proof question
- Next by Thread: Re: [isabelle] Beginner's struggles
- Cl-isabelle-users August 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