[isabelle] Beginner's struggles



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






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