Email Gateway (Aug 18 2022 at 10:29): Email Gateway (Aug 18 2022 at 10:29):From: Makarius <makarius@sketis.net>
There is no proper Isar manual so far. Still the following texts
may turn out as helpful:
http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.pdf
Section 5.4 "Proof by cases and induction" (covers
induction in pre-Isabelle2002)
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf
Section 3 (covers induction in Isabelle2002-2005)
http://isabelle.in.tum.de/Isar/Isar-induct.pdf
(covers induction in pre-Isabelle2007)
Once you have got the basic idea just look through existing examples, e.g.
in HOL/Induct, or virtually any other large scale application.
Makarius
Email Gateway (Aug 18 2022 at 10:29):From: "Janney, Mark-P26816" <Mark.Janney@gdc4s.com>
The best guide that I have found is Wenzel's PhD thesis (updated for
Isabell2002)
http://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf
Sections II and III provide a lot of practical material.
The other book that I keep handy is the Isabelle/Issr Reference Manaul
http://isabelle.in.tum.de/doc/isar-ref.pdf (part of the Isabelle
distribution)
For induction in particuar see the paper "Structured Induction Proofs in
Isabelle/Isar"
http://isabelle.in.tum.de/Isar/Isar-induct.pdf
However there is still a need for an "Isar 101" text. I've been doing
structured proofs for about 6 months now and I'm still trying to
formulate a clear, simple conceptual model of how Isar works.
Email Gateway (Aug 18 2022 at 10:29):From: Makarius <makarius@sketis.net>
Definitely. Maybe the following new text will help a little:
http://www4.in.tum.de/~wenzelm/papers/isar-framework.pdf
Makarius
Email Gateway (Aug 18 2022 at 10:30):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
David Streader wrote:
In short, no. Although I am looking into using IsaPlanner with proof
general to help automate some script manipulations and to provide an
interface for working with proof scripts, any kind of working system is
still a good bit in the future/imagination. When such a thing is usable,
I think it would just be another way to interact with Isabelle, along
side ML and Isar.
However, if you are interested in working on proof script morphisms, I'd
welcome your thoughts and ideas (although perhaps off the email list, as
it is slightly off topic).
best,
lucas
Lukas Stevens (Aug 24 2022 at 08:17):Initial message was bounced. This is the original first message of the thread.
From: David Streader <dstr@cs.waikato.ac.nz>
Hi
I am trying to use Isar but still lack a good over view of proof by induction/cases.
Is there an Isar manual (something like the excellent Isabelle manual in LNCS)?
Is IsaPlanner set to become the new front end?
David
Last updated: Apr 20 2024 at 08:16 UTC