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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
