Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
On 2017-08-24 09:38, Thiemann, Rene wrote: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. Unless I hear otherwise I will replace \mu by LFP and \nu by GFP. I have done so now. I also restored the original import order. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
On 2017-08-31 13:54, Florian Haftmann wrote: The theorem in question requires both the notion of subgroup and complete lattices, hence the import order dictates in which theory the theorem has to reside (btw. the current import order is similar to HOL-Main where Complete_Lattices comes after Groups). The theorem in question is that of the subgroups of a group forming a complete lattice. Such theorems exist for many algebraic structures. Following your approach they would all end up in Complete_Lattice, making that a very big theory. I had decided against that. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
Hi Clemens, >> If one imports HOL-Algebra.Multiplicative_Group (which we actually do >> via some transitive import), then \mu (LFP), \nu (GFP) and >> \phi (Euler’s totient function) become constants. > > Unless I hear otherwise I will replace \mu by LFP and \nu by GFP. sorry, I didn't recognize your follow-up message to this thread until now. Of course you are free to go ahead and revert the workaround e.g. using hg backout 5a42eddc11c1 Cheers, Florian -- PGP available: http://isabelle.in.tum.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
Re: [isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
Hi Clemens, >>> Concerning \mu and \nu, I am currently investigating whether an import >>> swap could re-establish the situation known from Isabelle2016-1 >> >> see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1 > I had overlooked that \mu and \nu are global constants when importing > this material, which I had received from Simon Foster. This needs to be > addressed properly. I did have a look at the overall situation but IMHO there are too many open ends which cannot be resolved before the upcoming release: * »no_notation« would mess up the material considerably and is difficult to place: traditionally, HOL-Algebra has no universal entry point which is guaranteed to be imported after all other theories. * Specific syntax could be placed into bundles, but this cannot be done incrementally. * Giving up \mu and \nu and coming up with an alternative syntax. * … Each of these requires subtantial thinking and appears much too invasive to me. > Your workaround merely helps users of Group, not of Complete_Lattice. That is the relevant point for the upcoming release: users of Group in Isabelle2016-1 (and there are many, since Group is used in substantial parts of both distribution of AFP) need not to worry about additional syntactic artefacts in Isabelle2017 either; Complete_Lattice is new in Isabelle2017 and does not induce any regression problems. > Moreover, it doesn't make sense that Complete_Lattice imports Group, and > that the structure theorem about subgroups is now in lattice theory. The theorem in question requires both the notion of subgroup and complete lattices, hence the import order dictates in which theory the theorem has to reside (btw. the current import order is similar to HOL-Main where Complete_Lattices comes after Groups). When placing it, I followed the pre-existing textual reference (http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1#l1.16). I am happy to add the symmetric textual reference to Group.thy if this clarifies the situation. Cheers, Florian -- PGP available: http://isabelle.in.tum.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] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
On 2017-08-24 09:38, Thiemann, Rene wrote: If one imports HOL-Algebra.Multiplicative_Group (which we actually do via some transitive import), then \mu (LFP), \nu (GFP) and \phi (Euler’s totient function) become constants. Unless I hear otherwise I will replace \mu by LFP and \nu by GFP. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] \mu and \nu in HOL-Algebra [was Re: Towards the Isabelle2017 release]
Dear Florian, For the final record: Concerning \mu and \nu, I am currently investigating whether an import swap could re-establish the situation known from Isabelle2016-1 see http://isabelle.in.tum.de/repos/isabelle/rev/5a42eddc11c1 I had overlooked that \mu and \nu are global constants when importing this material, which I had received from Simon Foster. This needs to be addressed properly. Your workaround merely helps users of Group, not of Complete_Lattice. Moreover, it doesn't make sense that Complete_Lattice imports Group, and that the structure theorem about subgroups is now in lattice theory. I request you revert this patch. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
