[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
Re: [isabelle-dev] print modes
On 05/08/2012 07:58 PM, Makarius wrote: On Wed, 2 May 2012, Brian Huffman wrote: On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel c-ste...@jaist.ac.jp wrote: is it really the case that currently the only way to obtain ASCII output using print modes is by specifying the empty string, like thm () conjE or did I miss anything? Since this print mode is occasionally useful, I suggest to provide a named variant, like 'plain', 'ASCII', or whatever. The variety of print modes were introduced to overcome certain limitations of display capabilities. In a sense most of that is legacy, but I've recently refurbished the description in the manual, see isar-ref section 7.1.3 in Isabelle2012-RC2. Mode is formally the default, the fall-back print mode. I see. Anyway, what are your remaining applications for ASCII notation? Currently only, copy-pasting examples from jedit into e-mails for the Isabelle mailing list ;). Not very convincing, is it? I would actually go a bit further, and get rid of xsymbol as a special syntax mode. It bothers me that if I want to define a constant with both ascii and symbol notation, I have to use the ascii variant in the actual definition, and then add the (far more commonly-used) symbol notation later. definition foo :: 'a = 'a = bool (infix ~~ 50) where ... notation (xsymbol) foo (infix \approx 50) I would rather write: definition foo :: 'a = 'a = bool (infix \approx 50) where ... notation (ascii) foo (infix ~~ 50) In some sense xsymbol is merely a convention. Nothing stops you from inventing other print modes on the spot. Is is a matter of library organization how this is done in practice. Since plain symbol notation now works most of the time, both in the editor and in HTML, one could eventually move on to discontinue these special modes and use more symbols by default. Then there would be only one (symbol) notation for most things. For very basic things like !! == etc. this would require thoughts, though. Makarius ___ 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
