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

[Askar Safin]

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:

==begin==
show A ⟹ B 
Successful attempt to solve goal by exported rule:
  A ⟹ B 
proof (state): step 4

this:
  A ⟹ B

goal (2 subgoals):
 1. A ⟹ A
 2. C
==end==

So, we see strange "A ==> A" goal. Then I can continue:

==begin==
  show "C" sorry
qed
==end==

And Isabelle will accept my proof. So, proof checking is OK, but the "Output" shows confusing output.

You may say "just use A --> B". Yes, this works, but in some cases I have to deal with namely "A ==> B"-like goals. For example, when I prove something by induction, I deal with goals like "P n ==> P (Suc n)" (and when I try to solve such goal using 'show "P n ==> P (Suc n)"' I see confusing output in the "Output").

You may say: just use 'assume "A" thus "B"' instead of 'show "A ==> B"'. Yes, this works, too. But in some cases the resulting proof will became bigger. For example, I have a lot of goals A1 ==> B1, A2 ==> B2, etc, for example, created by induction on some datatype with many constructors. Then the following proof:
==begin==
assume A1
show B1 sorry
next
assume A2
show B2 sorry
next
...
==end==
is bigger than the following:
==begin==
show "A1 ==> B1" sorry
show "A2 ==> B2" sorry
...
==end==

Moreover, imagine the following situation:
==begin==
datatype t =
  c0
| c1 t
| c2 t
| c3 t

lemma
  fixes x :: t
  assumes prem: "A x"
  shows "B x"
using prem proof (induct x)
  fix x
  assume "A x ⟹ B x"
  hence "C x" sorry (* Some intermediate fact *)
  thus
    "A (c1 x) ⟹ B (c1 x)" and
    "A (c2 x) ⟹ B (c2 x)" and
    "A (c3 x) ⟹ B (c3 x)"
  sorry (* Let's image "C x" can prove all this goals at once using some simple method, for example, auto *)
next
  show "A c0 ⟹ B c0" sorry
qed
==end==

Any attempt to rewrite this proof not using 'thus "A (c1 x) ==> B (c1 x)"' will result in bigger proof (even if we will use "cases"). Of course, all this are toy examples. In real proofs size increase will be more noticeable. In either case user should be able to write 'show "A ==> B"' and not to see strange "Output".

Also, the last example shows very strange behavior: "thus" solve goals, but simultaneously they leave unchanged (according to the "Output")! If I put cursor between "sorry" and "next" words, I will see in the jEdit "Output":
==begin==
show A (c1 x) ⟹ B (c1 x)
  and A (c2 x) ⟹ B (c2 x)
  and A (c3 x) ⟹ B (c3 x) 
Successful attempt to solve goal by exported rule:
  (A ?xa2 ⟹ B ?xa2) ⟹ A (c1 ?xa2) ⟹ B (c1 ?xa2) 
Successful attempt to solve goal by exported rule:
  (A ?xa2 ⟹ B ?xa2) ⟹ A (c2 ?xa2) ⟹ B (c2 ?xa2) 
Successful attempt to solve goal by exported rule:
  (A ?xa2 ⟹ B ?xa2) ⟹ A (c3 ?xa2) ⟹ B (c3 ?xa2) 
proof (state): step 6

this:
    A (c1 x) ⟹ B (c1 x)
    A (c2 x) ⟹ B (c2 x)
    A (c3 x) ⟹ B (c3 x)

goal (4 subgoals):
 1. A c0 ⟹ B c0
 2. ⋀x. (A x ⟹ B x) ⟹ A (c1 x) ⟹ A (c1 x)
 3. ⋀x. (A x ⟹ B x) ⟹ A (c2 x) ⟹ A (c2 x)
 4. ⋀x. (A x ⟹ B x) ⟹ A (c3 x) ⟹ A (c3 x)
==end==

I see lots of "Successful attempt to solve goal by exported rule" and then I see this goals again in "goal (4 subgoals)". Even if I put the cursor at the following "next" I will see:
==begin==
proof (state): step 7

goal (4 subgoals):
 1. A c0 ⟹ B c0
 2. ⋀x. (A x ⟹ B x) ⟹ A (c1 x) ⟹ A (c1 x)
 3. ⋀x. (A x ⟹ B x) ⟹ A (c2 x) ⟹ A (c2 x)
 4. ⋀x. (A x ⟹ B x) ⟹ A (c3 x) ⟹ A (c3 x)
==end==

And despite of all this the proof works! I. e. the last "qed" successfully finishes proof despite lots of goals present at the "Output" (for example, if I put the cursor to "next" or before "qed").

So, please fix this issue or say how to workaround it or document it.

==
Askar Safin