[isabelle-dev] Proposing extensions to the Isabelle library?

[Alessandro Coglio]

Hello Florian et al.,

I finally got around to work on what we discussed back in December (see email below) and now I have a patch that works with changeset 52498:d802431fe356. The command

./bin/isabelle build -a -o browser_info -o document=pdf -o document_graph

succeeds (after applying the patch), even though the output says that some theories are skipped due to what look like some undefined environment variables -- I can send more precise information on this.

The patch follows exactly Florian's suggestion below, and also slightly redefines class complete_lattice in a perhaps cleaner way, taking advantage of the new syntactic type classes. A few proofs here and there had to be adapted.

These changes may affect the AFP, but I haven't looked at that. What is the process for testing and propagating library changes to the AFP?

Should I send the patch for review to anyone in particular, or to this whole mailing list?



On Dec 18, 2012, at 12:18 PM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:

> Hi Alessandro,
> 
>> Is there any plan to make things in the library more uniform (one way or
>> the other)? Is there a preference for new type classes should be
>> developed (purely syntactic or with assumptions)?
> 
> well, there is no big masterplan.  Usually things evolve: somebody
> thinks about an extended or more fine-grained hierarchy and thinks how
> to accomplish things without breaking more than necessary.
> 
>> Personally, I like syntactic classes because they are more modular. For
>> example, in the library extensions that I sent the other day, the
>> definition of type class finite_lattice_complete would be perhaps
>> slightly cleaner if bot and top were syntactic classes like Inf and Sup.
>> Just my 2 cents.
> 
> I.e. something like
> 
> 	class bot ~> class order_bot
> 	class top ~> class order_top
> 	class bot = fixes bot :: "'a"
> 	class top = fixes top :: "'a"
> 
> Could make sense.  The question is whether somebody is willing to
> undertake this change.  If you would consider this, you find the first
> clues at
> http://isabelle.in.tum.de/repos/isabelle/file/c5e0073558f3/README_REPOSITORY.
> Get back here if questions remain.
> 
> Note that currently we are heading towards a next release in January or
> February, and time might be too terse to polish and incorporate a change
> like the one sketched above.
> 
> Hope this helps,
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>