Email Gateway (Aug 19 2022 at 14:36): Email Gateway (Aug 19 2022 at 14:36):From: Gergely Buday <gbuday@gmail.com>
Hi,
on the bottom of page 3 of
http://arachne.it.uu.se/grad/courses/gc0910/isabelle/isar-overview.pdf#page=3
there is a proof
lemma "A ⟶ A"
proof
assume "A"
show "A" .
introducing dot as a trivial proof. In my 2013-2 installation it does not work:
Failed to finish proof:
goal (1 subgoal):
What is the problem here?
Email Gateway (Aug 19 2022 at 14:36):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Gergely,
The overview seems wrong (or obsolete) there. If you replace the keyword "show" by "thus" (or "then show" or "from this show"), the assumption correctly gets chained into the goal, and "." works as expected.
Jasmin
Email Gateway (Aug 19 2022 at 14:36):From: Tobias Nipkow <nipkow@in.tum.de>
It worked at the time (like 12 years ago) but systems change. Arbitrary
documents you find somewhere on the web have the tendency to be outdated.
Tobias
Email Gateway (Aug 19 2022 at 14:36):From: Gergely Buday <gbuday@gmail.com>
Tobias Nipkow wrote:
It worked at the time (like 12 years ago) but systems change. Arbitrary
documents you find somewhere on the web have the tendency to be outdated.
What is an up-to-date tutorial for Isar then? What I have found was
the Proofs chapter of the Isabelle/Isar Reference:
http://isabelle.in.tum.de/doc/isar-ref.pdf#page=118
but that is terse and dry for a beginner.
Email Gateway (Aug 19 2022 at 14:36):From: Tobias Nipkow <nipkow@in.tum.de>
On 20/06/2014 14:25, Gergely Buday wrote:
Tobias Nipkow wrote:
It worked at the time (like 12 years ago) but systems change. Arbitrary
documents you find somewhere on the web have the tendency to be outdated.What is an up-to-date tutorial for Isar then? What I have found was
the Proofs chapter of the Isabelle/Isar Reference:http://isabelle.in.tum.de/doc/isar-ref.pdf#page=118
but that is terse and dry for a beginner.
You have found the documentation directory but have chosen the reference manual.
Maybe you are looking for a tutorial? Then I recommend the first item in the
Tutorials section: "Programming and Proving in Isabelle/HOL."
Tobias
- Gergely
Email Gateway (Aug 19 2022 at 14:36):From: Lawrence Paulson <lp15@cam.ac.uk>
Note that when you launch Isabelle, a Documentation tab is available, where you can just click on title and it will open for you in a PDF reader. These documents are supplied as part of the Isabelle distribution package.
Larry
Last updated: Apr 26 2024 at 12:28 UTC