Re: [isabelle] Isar tutorial example broken?


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).


 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).



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.