Re: [isabelle-dev] Nominal and FinFuns from the AFP
On Sun, 13 May 2012, Florian Haftmann wrote: c) I strongly object to clutter the HOL syntax even more than now by incorporating just another fancy syntax. I would prefer the lattice solution (delete syntax immediately after use and provide a library theory to optionally include it later), or maybe it is also possible to use context blocks for this (another nice case study). This is indeed still the canonical solution to the syntax problem for library material, and I see it now in Isabelle/d60f6b41bf2d for FinFun. At some point, when I have bundles ready to work with the existing notation commands, we can fine-tune this scheme further, to allow users to 'include' syntax in local situations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
Hi Makarius, At some point, when I have bundles ready to work with the existing notation commands, we can fine-tune this scheme further, to allow users to 'include' syntax in local situations. I tried to implement the new syntax for FinFuns with bundles and Brian's notation attribute (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html), but it was not satisfactory. There were two show stoppers: 1. I did not know how to get dynamic bundles, i.e., how to add declarations one after the other to a bundle. Hence, I would have to introduce all the notation in a single place before which all constants must have been defined. 2. Theory-level commands like interpretation do not work inside an auxiliary context and neither can they cope wth includes. Hence, I cannot use such pretty syntax in the parameter instantiations for interpretation. This possibly also applies to the where clause although I did not need that for FinFun. Andreas -- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbih...@kit.edu http://pp.info.uni-karlsruhe.de KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
On Thu, May 31, 2012 at 1:36 PM, Makarius makar...@sketis.net wrote: On Thu, 31 May 2012, Andreas Lochbihler wrote: At some point, when I have bundles ready to work with the existing notation commands, we can fine-tune this scheme further, to allow users to 'include' syntax in local situations. I tried to implement the new syntax for FinFuns with bundles and Brian's notation attribute (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html), but it was not satisfactory. I did not have time yet to look more closely at that. Note that notation is based on syntax declarations of the local theory infrastructure, which is slightly different from what you have in attributes. So notation as attributes is a bad idea. Makarius: If you want to call one of my ideas a bad idea, then I hope you have a better justification for this statement. - Brian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
On Thu, 31 May 2012, Brian Huffman wrote: On Thu, May 31, 2012 at 1:36 PM, Makarius makar...@sketis.net wrote: On Thu, 31 May 2012, Andreas Lochbihler wrote: At some point, when I have bundles ready to work with the existing notation commands, we can fine-tune this scheme further, to allow users to 'include' syntax in local situations. I tried to implement the new syntax for FinFuns with bundles and Brian's notation attribute (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html), but it was not satisfactory. I did not have time yet to look more closely at that. Note that notation is based on syntax declarations of the local theory infrastructure, which is slightly different from what you have in attributes. So notation as attributes is a bad idea. Makarius: If you want to call one of my ideas a bad idea, then I hope you have a better justification for this statement. Formally, if you look what notation does, it is not like an attribute, but a syntax declaration. This can be seen immediately in the sources. What is not immediately visible is the long history around it, but quite a bit of it was discussed even on this mailing list in the past few years. Right now I don't have time to sort out the details, but I also don't want to waste time repeating mistakes from the past that are already known by the veterans on these mechanisms. Anyway, there is nothing wrong with bad ideas. Most of my own ideas are bad. One merely needs to sort them out and isolate the good ones from the many ideas that are floating around. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
Hi all, In the short term, we could move the FinFun theory into the HOL library of the development version after Isabelle 2012 and the AFP 2012 has been released, if we agree that this moves this contribution in the right direction. some remarks on my behalf: a) Ideally, tools and library theories span a product space: tools should provide configuration means such that theories »not forseen by the author« can be integrated into its scope, typically by a series of declarations. AFP library theories are a nice case study for this – if the AFP infrastructure would not allow for such organization (dependencies etc.), it does not fullfil its promise. b) In the particular case of FinFun, more and more tools seem to regard this as so fundamental (or fundamentally helpful) that incorporation into the distribution could indeed be the answer. Nevertheless, I would like to see explicit statements on this. For the moment, we have a claim for Nominal. I want to add that I would like to see a type for executable mappings in the distribution, and FinFuns seems to be the most reasonable candidate. More claims? c) I strongly object to clutter the HOL syntax even more than now by incorporating just another fancy syntax. I would prefer the lattice solution (delete syntax immediately after use and provide a library theory to optionally include it later), or maybe it is also possible to use context blocks for this (another nice case study). d) In personal conversation Alex and I discussed whether it would be preferable to swap FinFun.thy into HOL-Main and Map.thy into HOL-Library, but I don't recall the arguments in particular. Cheers, 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] Nominal and FinFuns from the AFP
Dear All, In Nominal I am usually relying on types that are defined in HOL or that I define myself. However, I now came across the FinFun development in the AFP by Andreas Lochbihler (thanks to Larry). The finfun type seems to be rather useful to Nominal users, since it has finite support, in contrast to the function type, which in general hasn't. My question is how I should I interface with something that is in the AFP and with something that is (eventually) in the distribution? The problem is that Nominal always needs a wrapper infrastructure for types, such as a definition of a permutation. How should I write this wrapper, especially what should the import paths be, so that users can conveniently use FinFuns and Nominal? Should this wrapper be part of the AFP entry (in which case the paths are clear, but then Nominal users have to fetch the AFP explicitly and no Nominal example in the distribution can depend on it)? Or should the wrapper be part of Nominal (in which case I can use it in examples, but I have no idea what the import paths should be...the AFP can be anywhere)? Or, should FinFun be part of the distribution (which would make my life normal again)? Is there any received wisdom for this problem? Best wishes, Christian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
Hi Christian, For code generation purposes and especially Quickcheck, it is necessary that the FinFun theory would be imported by any user. With the new developments lifting and transfer, we are getting very close that FinFun can be used without any further ado. I do have some latest experiments and patches in the shelf to be published after the release. Therefore, I am also in strong favour for moving the AFP entry FinFun into the distribution. In the long run, it should probably even become part of the HOL-Main image. In the short term, we could move the FinFun theory into the HOL library of the development version after Isabelle 2012 and the AFP 2012 has been released, if we agree that this moves this contribution in the right direction. As Andreas has access to the Isabelle development and can freely change and contribute the entry, I do not see any further difficulties. Lukas P.S.: The topic is interesting for isabelle-users as well in my opinion. On 05/10/2012 05:09 PM, Christian Urban wrote: Dear All, In Nominal I am usually relying on types that are defined in HOL or that I define myself. However, I now came across the FinFun development in the AFP by Andreas Lochbihler (thanks to Larry). The finfun type seems to be rather useful to Nominal users, since it has finite support, in contrast to the function type, which in general hasn't. My question is how I should I interface with something that is in the AFP and with something that is (eventually) in the distribution? The problem is that Nominal always needs a wrapper infrastructure for types, such as a definition of a permutation. How should I write this wrapper, especially what should the import paths be, so that users can conveniently use FinFuns and Nominal? Should this wrapper be part of the AFP entry (in which case the paths are clear, but then Nominal users have to fetch the AFP explicitly and no Nominal example in the distribution can depend on it)? Or should the wrapper be part of Nominal (in which case I can use it in examples, but I have no idea what the import paths should be...the AFP can be anywhere)? Or, should FinFun be part of the distribution (which would make my life normal again)? Is there any received wisdom for this problem? Best wishes, Christian ___ 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
