Re: [isabelle-dev] [isabelle] Countable instantiation addition
That is such a bad luck for me... It seems I had verified it wasn't in the repository a little too soon (like for Imperative_HOL...). But at least I have learned Isabelle/ML. I don't think there is any additional feature in my version. It defines mutual recursive functions from the mutual types to natural numbers and proves their injectivity in a separate lemma that is used in the instantiation. So as I understand your method, the only addition would be the definition of these executable functions, which does not seem so useful. It also proves countability only from the type names and without "instance ..." but then what it does is less clear (less integrated into existing features). In the case of typedef and records, countability can easily be proven by using: countable_classI[of "to_nat o Rep_"] and Rep__inject It can perhaps allow to write a simpler method. My version also does not need "instance ..." and can infer the needed constrains (sorts) thanks to the Isabelle type inference but then what we obtain is not so explicit. Regards, Mathieu Le jeudi 21 juillet 2011 13:51:17 Brian Huffman a écrit : > Hello everyone, > > Attached is an implementation of a "countable_typedef" method that I > just wrote. (It works in a very similar manner to the > "countable_datatype" method.) Since records are implemented as > typedefs of product types, the same method works for record types as > well. I'd be happy to add this to Library/Countable.thy if anyone > wants me to. > > I haven't had time to study Mathieu's ML library yet, but if it has > any features or capabilities that my system lacks, we should > definitely try to incorporate those into whatever ends up in the next > Isabelle release. I also need to remember to add an item to the NEWS > file letting people know that these new proof methods exist. > > - Brian > > On Thu, Jul 21, 2011 at 11:15 AM, Alexander Krauss wrote: > > Hi Matthieu, > > > >> I have written a little ML library allowing to automatically prove, in > >> most > >> cases, instantiations of types (typedefs, records and datatypes) as > >> countable > >> (see ~~/src/HOL/Library/Countable). > > > > It seems that for datatypes we now have such functionality, implemented > > four weeks ago by Brian Huffman: > > > > http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f > > > > It comes in the form of a method, so it has to be invoked explicitly, > > but > > like this it doesn't produce any penalty when it is not used. If you > > want to contribute an extension to records/typedefs, you are welcome, > > but you probably want to study Brian's implementation first. I assume > > that he is also the most appropriate person to review patches for this > > functionality. > > > > Alex > > ___ > > 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] [isabelle] Countable instantiation addition
It does not work for any datatype (for example as soon as a non-countable type is used in the datatype) but it could be integrated in the datatype package with some checks. However, I don't know if the time penalty (which isn't so big but there anyway) on a so much used feature worth the benefit... unless it would be present as an option (perhaps even with a recursive call on included non- instantiated types). And an option would be mostly equivalent to (in fact even less flexible than) a new command or an ML call subsequent to the datatype definition. Mathieu Le jeudi 21 juillet 2011 19:02:41 Peter Lammich a écrit : > This is definitely a useful tool for ImperativeHOL ... One could > probably integrate > it into the datatype package, such that datatypes automatically become > countable (like Haskell infers some typeclasses automatically (on demand)) > > Peter > > Mathieu Giorgino schrieb: > > Hi all, > > > > I have written a little ML library allowing to automatically prove, in > > most cases, instantiations of types (typedefs, records and datatypes) > > as countable (see ~~/src/HOL/Library/Countable). The style of the > > library is still a little rough but I think it could be a nice addition > > to the Isabelle Library with some more work, mostly for Imperative_HOL > > (~~/src/HOL/Imperative_HOL) which can only store values of countable > > types in its heap. > > > > However, as Lukas Bulwhan said to me, improving it and integrating it in > > Isabelle while nobody use it would certainly be a lost of time. > > > > So here is my question: would anybody be interested in this addition ? > > > > I attach this library with a theory containing tests/examples. > > > > Anyway, if you have some advices for improving it, they would be > > welcome. > > > > Regards, > > > > Mathieu Giorgino > > ___ > 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] [isabelle] Countable instantiation addition
Hello everyone, Attached is an implementation of a "countable_typedef" method that I just wrote. (It works in a very similar manner to the "countable_datatype" method.) Since records are implemented as typedefs of product types, the same method works for record types as well. I'd be happy to add this to Library/Countable.thy if anyone wants me to. I haven't had time to study Mathieu's ML library yet, but if it has any features or capabilities that my system lacks, we should definitely try to incorporate those into whatever ends up in the next Isabelle release. I also need to remember to add an item to the NEWS file letting people know that these new proof methods exist. - Brian On Thu, Jul 21, 2011 at 11:15 AM, Alexander Krauss wrote: > Hi Matthieu, > >> I have written a little ML library allowing to automatically prove, in >> most >> cases, instantiations of types (typedefs, records and datatypes) as >> countable >> (see ~~/src/HOL/Library/Countable). > > It seems that for datatypes we now have such functionality, implemented four > weeks ago by Brian Huffman: > > http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f > > It comes in the form of a method, so it has to be invoked explicitly, but > like this it doesn't produce any penalty when it is not used. If you want to > contribute an extension to records/typedefs, you are welcome, but you > probably want to study Brian's implementation first. I assume that he is > also the most appropriate person to review patches for this functionality. > > Alex > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > Countable_Typedef.thy Description: application/isabelle-theory ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
On 21/07/2011, at 8:15 PM, Alexander Krauss wrote: > It comes in the form of a method, so it has to be invoked explicitly, but > like this it doesn't produce any penalty when it is not used. A separate command like this method looks like the right way to do such things. The idea has potential for generalisation. Could we turn this into something similar to Haskell's "deriving"? The command would take a datatype and a list of instantiation methods that each know how to instantiate a datatype for a specific type class, e.g. enum, countable, order, etc. An instantiation method would be basically a usual proof method plus some small part that knows how to set up the specific instantiation goal (probably the same code for pretty much all applications of this) plus some background theory that provides the basic setup. The methods would not have to work on every kind of data type (just failing if they can't prove their goal), and the list of available ones could be easily extended using the same Isar setup mechanisms that we use for proof methods, attributes, and other things. The command would not pollute normal datatype usage and would not need to be integrated with the datatype package, keeping the code separate. The interface would just be the user-visible final definition of the datatype as in Brian's case. Cheers, Gerwin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
Hi Matthieu, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). It seems that for datatypes we now have such functionality, implemented four weeks ago by Brian Huffman: http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f It comes in the form of a method, so it has to be invoked explicitly, but like this it doesn't produce any penalty when it is not used. If you want to contribute an extension to records/typedefs, you are welcome, but you probably want to study Brian's implementation first. I assume that he is also the most appropriate person to review patches for this functionality. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Countable instantiation addition
This is definitely a useful tool for ImperativeHOL ... One could probably integrate it into the datatype package, such that datatypes automatically become countable (like Haskell infers some typeclasses automatically (on demand)) Peter Mathieu Giorgino schrieb: Hi all, I have written a little ML library allowing to automatically prove, in most cases, instantiations of types (typedefs, records and datatypes) as countable (see ~~/src/HOL/Library/Countable). The style of the library is still a little rough but I think it could be a nice addition to the Isabelle Library with some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which can only store values of countable types in its heap. However, as Lukas Bulwhan said to me, improving it and integrating it in Isabelle while nobody use it would certainly be a lost of time. So here is my question: would anybody be interested in this addition ? I attach this library with a theory containing tests/examples. Anyway, if you have some advices for improving it, they would be welcome. Regards, Mathieu Giorgino ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
