[isabelle-dev] show "A ==> B"

[Brian Huffman]

On Fri, Jul 11, 2014 at 5:54 AM, Askar Safin <safinaskar at 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