On Fri, Jul 11, 2014 at 5:54 AM, Askar Safin <safinas...@mail.ru> wrote: > Hi. I think I found a bug in the Isabelle 2013-2 (OS: Debian GNU/Linux 7, > Interface: jEdit). For example, I type the following in the jEdit Isabelle > interface: > > ==begin== > notepad begin > have "A ==> B" and "C" proof - > show "A ==> B" sorry > ==end== > > Then, Isabelle will accept this "show" and the "Output" section of jEdit will > show me: [...] > goal (2 subgoals): > 1. A ⟹ A > 2. C > ==end== > > So, we see strange "A ==> A" goal. Then I can continue:
Hi Askar, This exact issue has been discussed previously (multiple times!) on the isabelle-users list. https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-November/msg00024.html https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-April/msg00052.html https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2009-September/msg00044.html I still agree with what I said back then: This behavior of "show" with meta-implication is surprising and confusing to ordinary users, and we really should change it. > ==begin== > show "C" sorry > qed > ==end== > > And Isabelle will accept my proof. So, proof checking is OK, but the "Output" > shows confusing output. When you write "qed", the default behavior is to try to solve any remaining goals by assumption, which is why your proof script still works. (In case you didn't know, you can also use e.g. "qed auto" to try to solve remaining goals with "auto". This is useful for proofs with lots of uninteresting trivial cases.) You are fortunate that your proof script still works; as discussed in the linked posts from 2009, proving an if-and-only-if proposition in this style will fail due to quirks of this "show" behavior. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
