Email Gateway (Aug 19 2022 at 09:09): Email Gateway (Aug 19 2022 at 09:09):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
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
http://isabelle.in.tum.de/documentation.html 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.
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 09:10):From: Tobias Nipkow <nipkow@in.tum.de>
In a way it is. It starts from a functional programming perspective. If you have
a suggestion for a better title, let me know.
Tobias
Last updated: Apr 26 2024 at 08:19 UTC