Email Gateway (Aug 18 2022 at 12:51): Email Gateway (Aug 18 2022 at 12:51):From: Chris Capel <pdf23ds@gmail.com>
I'm working through the isar tutorial by Tobias Nipkow, and didn't get
very far before finding a problem.
lemma "A --> A"
assume "A"
shows "A" .
qed
This example fails at the proof of shows, with an empty result
sequence. I am using the repository version of isabelle with the HOL
theory loaded, and my theory imports Main and doesn't do anything
else. I'm using ProofGeneral. The preceding example, where the
assumption is named and referenced with "by (rule a)" works. Is this
something broken in the repository?
Chris Capel
Email Gateway (Aug 18 2022 at 12:52):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Chris Capel schrieb:
lemma "A --> A"
assume "A"
shows "A" .
qed
Note that fixes/ assumes / shows is just a different way to write
down propositions to prove. What you probably meant was something like:
lemma "A --> A"
proof
assume "A"
then show "A" .
qed
Something similar with assumes, shows:
lemma
assumes A
shows A
proof -
from assms show A .
qed
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 12:52):From: Amine Chaieb <ac638@cam.ac.uk>
Hi,
Assuming you meant the right (assume, and show + proof).
You can not prove "A" even after assuming "A", when you don't use it.
so something like
assume "A" show "A"
is the same as
show "A" (which is a little bit difficult to prove).
Indeed
assume "A"
show "A" .
used to work, where Isabelle/Isar used to figure out that you meant to
use an assumption. This "feature" was judged later to be "bug" and that
for readable natural deduction proofs, one needs to specify all the
assmptions one uses. (For a year or so, the system used to output a
legacy feature message I think).
Amine.
Chris Capel wrote:
Email Gateway (Aug 18 2022 at 12:52):From: Tobias Nipkow <nipkow@in.tum.de>
As Amine explained, modulo your typos, that proof used to work but
Makarius no longer liked that style and switched it off.
Tobias
Chris Capel schrieb:
Email Gateway (Aug 18 2022 at 12:52):From: Makarius <makarius@sketis.net>
It should work if you use the version of the tuturial from the same
repository snapshot.
Using assumptions implicitly is considered harmful for many years already
-- it stems from very early stage of Isar, where the exact relation to old
tactical proof style was not yet fully understood.
Makarius
Email Gateway (Aug 18 2022 at 12:53):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
In Isabelle2008 (I don't know about the current cvs version) this legacy
feature is still working. But of course you are right, that it should
not be used any longer. I think the problem in the proof was just a
forgotten `proof' command at the beginning.
cheers
christian
Amine Chaieb wrote:
Last updated: May 03 2024 at 04:19 UTC