Re: [isabelle] ?spam? Re: Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]

2012-11-22 14:31 Tobias Nipkow:
fixes ... and i
assumes "p x"
shows "q x"

Unless you want to give the type of i, you don't need to fix it.

Thanks! Now I'm not quite sure what's better style. On paper you do not always give types, if it's clear from the context. But when it is not clear, it helps to mention types explicitly.

"If you look at the documentation page you will find that the first
document is the relatively new Programming and Proving in Isabelle/HOL, which
does cover structured proofs (which is why I wrote it). The Tutorial is now only
second choice because of the foucus on "apply"."

Sorry, I just had not yet got back to that old recommendation you made. Indeed I had had a look into "Programming and Proving" meanwhile and found it very instructive. Thanks!

That is also where you find the induction method.

That's right, but "Programming and Proving" is not a full reference of all proof methods and their options; that's what I was referring to.

Is there a single, up to
date reference manual that documents all proof methods?

Yes, the reference manual (more or less).

OK, thanks, I see.

BTW, about "Programming and Proving": I had noticed this manual when I got started with Isabelle, but then didn't take a closer look, as I was misled by the "Programming". I thought it was some specific guide on verifying functional programs.

Indeed, for inductions, the most convenient way is stating them as implications
(with ==>). The manuals above will also tell you about the naming conventions of
assumptions in each case.

OK, I'll add this to my to-do list.



Christoph Lange, School of Computer Science, University of Birmingham, Skype duke4701

→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  2–5 April 2013, Exeter, UK.  Deadlines 10 Dec (stage 1), 14 Jan (st. 2)

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