Re: [isabelle] Isar tutorial example broken?



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:
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:

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







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