Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit FAILED
Hi Lars, On 29.06.2014 21:35, Lars Noschinski wrote: On 28.06.2014 17:24, Makarius wrote: On Sat, 28 Jun 2014, Makarius wrote: On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component within Isabelle. So it should normally be there, although I don't understand the mira setup. Another guess: Isabelle/jEdit is really missing, because of a lacking isabelle jedit -b that is done in regular makedist (e.g. in isatest). mira just executes isabelle build -s -v with job specific options (can be seen in Admin/mira.py). If isabelle jedit -b is a necessary step to setup a fresh Isabelle installation, I can add that to the setup script. I would like to say: go ahead with that. Red signs are supposed to disappear while approaching an release. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] show A == B
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
Re: [isabelle-dev] *** Spam *** show A == B
On Fri, 11 Jul 2014, Askar Safin wrote: I think I found a bug in the Isabelle 2013-2 (OS: Debian GNU/Linux 7, Interface: jEdit). ... So, please fix this issue or say how to workaround it Just formally and grammatically, this looks off-topic for this mailing list. If you want to discuss anything about official Isabelle releases, e.g. how Isar proofs work, you can do that on the isabelle-users mailing list. or document it. There is a lot of documentation, in fact too much of it. New users and old users get routinely swamped by the amount of Isabelle manuals. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
On Fri, 11 Jul 2014, Andreas Lochbihler wrote: If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. I can't say anything myself how it would impact the bootstrap of Main HOL. As long as this question does not arise for the Isabelle2014 release, I would say: go ahead and renovate it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Dead and broken theory src/HOL/Library/Quickcheck_Types.thy
Quickcheck does not use these types, because it is currently configures to only use the types finite_1 to finite_3 from Enum, because the finite_types parameter is set by default. Quickcheck internally also seems to work differently depending on whether the finite_types flag is set. I have only little insight how the parameters affect the performance of quickcheck, but I remember that Quickcheck originally used int as a replacement. Quickcheck_Types clearly is from that time. However, int is an infinite type and therefore, quantifiers, set comprehensions and function equality are not executable. Later, he switched to the finite_X types, which instantiate enum, but not the other type classes. Therefore, I recommend the following: 1. Temporarily fix Quickcheck_Types such that it works again, but leave it in HOL/Library. Then, anyone who wants to use quickcheck with infinite types can do so. This way, the Quickcheck_Examples session can also be reactivated. 2. Instead of moving Quickcheck_Types to Main, it suffices to make the finite_X types instances of the lattice type class hierarchy. Probably most of the stuff in Quickcheck_Types can be adapted to work with the Enum types as well. Maybe even all the test cases in Quickcheck_Lattice_Examples work with the Enum types, too. I have already done step 1 in 36041934e429 and 8840fa17e17c, but I won't have time for step 2 before the fork of the release branch. Andreas On 11/07/14 14:28, Tobias Nipkow wrote: On 11/07/2014 13:43, Andreas Lochbihler wrote: Quickcheck_Types defines a number of artificial types that quickcheck can use to instantiate type variables that occur in a theorem. Normally, quickcheck instantiates them with int provided that the sort constraints do not prevent this. In Enum.thy, there are already the types finite_X that quickcheck uses for enumerable types (type class enum) such that quantifiers can be unfolded into conjunctions or disjunctions. The types in Quickcheck_Types now do the same for the lattices type class hierarchy, because int and the finite_X types cannot be used for type variables with sort lattice (or top/bot/...). I believe that it should be fairly simple to adjust Quickcheck_Types to Isabelle2014. However, this only makes sense if it becomes part of Main. Otherwise, it will remain just a library theory that hardly anyone knows about and no one uses. Moreover, we should make sure that Quickcheck_Types fits to the current code generator setup for lattices. IIRC, Florian has reworked a lot there over the past years. At the very least, we should have some test cases (e.g. in HOL/ex) to check that Quickcheck_Types works as expected. If there's consensus on reviving this theory, I can do the changes to Quickcheck_Types such that Isabelle2014 digests it. This is probably all that can be done before the release as most of us will be busy in Vienna next week. A move to Main is something for the next release. It looks mildly useful. But then Qickcheck would need to use it, which it currently obviously does not. If you (or somebody) is able to make that happen, then I am in favour of reviving that theory. Tobias Andreas On 11/07/14 13:22, Lawrence Paulson wrote: I’m afraid that I don’t even know what it is. Larry On 11 Jul 2014, at 12:21, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken has not been addressed since before the last release. So, which path to follow? Is there any interested in a serious repair effort? Otherwise, we should honestly drop it. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Old 'defs'
On Mon, 7 Jul 2014, Andreas Lochbihler wrote: The constants sc_spurious_wakeups are declared in MM/SC_Collections.thy and MM/SC.thy, but intentionally not defined. This expresses that the remaining proofs are independent of the value of the constant, which is in fact just a configuration option. Only later, in Execute/SC_Schedulers, there is the definition that sets this configuration option. One could convert this into overloading+definition, but it would be a very degenerate form of overloading, as the configuration option is a plain boolean, there are no type variables involved. This use is no counter example yet, and very rare in practice. IIRC, Florian Haftmann made the overloading target to include such boundary cases, or rather he did not do anything specific to exclude them. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] show A == B
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
