Re: [isabelle] Beginner's struggles



On Sat, 14 Aug 2010, Ian Lynagh wrote:

I have "(Isabelle2009-1: December 2009)".

There is no problem with it, but you might want to try the current version Isabelle2009-2 (June 2010).


How does Isabelle know how much to process when I click the "Process the next proof command" in Proof-General?

It processes the next command, up to the last non-whitespace text before the following command. Of course, the question here is what a "command" actually means in Isabelle/Isar. The quick reference in Appendix A of the isar-ref manual might be helpful.

In particular, "." is a command of its own, not a command terminator like in Coq. (We have the more conventional ";" for that, but it has almost come out of use in recent years, since Proof General is good enough to determine command boundaries from the keywords alone.)


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".

In Isar 'proof' and 'qed' are not just parentheses, but actually do something. See the quick reference again, especially for important abbreviations like "by m1 m2 == proof m1 qed m2". Extra whitespace never makes a difference in syntax recognition.


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

Here the confusion is again that "." is completely different from Coq. Put a space between these two commands, and you should see proper font-lock highlighting in Emacs and less confusing Isabelle


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.

As mentioned above, Proof General will stop before the next proper command keyword. E.g. you can put a dummy stopper like 'done' or '.' before the invalid stuff to prevent it from running into it.


How does one write a comment in Isabelle?

Normally you don't, but you intersperse the formal text with informal one, using commands like 'text' or 'section' or 'subsection'. Small marginal
attachments can be written everywhere like this:

  assume A  -- "blah blah"

In any case you need to quote such text using "..." or the more convenient {* ... *} The latter allows to have quoted text inside without further escapes.


Isabelle source comments, which are of the form (* ... *) and as far as I can see this is the only mention in the document

Think of these "source comments" like % in LaTeX, i.e. they are not really part of what you write.


Am I right in thinking that "--" does not start a comment in a source file? Because while trying to copy/paste/run this example:

After all these years, the generated PDF/LaTeX files are still unsuitable for copy/paste. There have been some recent movements in the pdflatex camp towards more serious "tagged PDF", and there is some hope that we will be able to use it soon.

For now you should start with real example source files, to get an idea how to type things, especially where to put quotes and where not.


	Makarius





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