*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] show "A ==> B"*From*: Askar Safin <safinaskar at mail.ru>*Date*: Fri, 11 Jul 2014 17:56:55 +0400*Reply-to*: Askar Safin <safinaskar at mail.ru>

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. (Redirected from https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2014-July/005564.html ) == Askar Safin

- Previous by Date: Re: [isabelle] Isabelle2014-RC0: symbol completion in antiquotations
- Next by Date: Re: [isabelle] Isabelle2014-RC0 available for testing
- Previous by Thread: Re: [isabelle] proof by contradiction
- Next by Thread: [isabelle] lemmas-command normalizes theorems
- Cl-isabelle-users July 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list