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

[Alessandro Coglio]

Hi Florian, thank you for your answer. I understand.

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)?

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.



On 12/15/12 2:18 AM, Florian Haftmann wrote:
> Hi Alessandro,
>
>> On a semi-related topic, I was wondering why the Isabelle library has
>> syntactic type classes for many (most?) operators but not for bot and top.
> this is mainly a result of historic developments and compromises.
>
> Especially the long-standing operators plus, times etc. have been merely
> syntactic right from the beginning – in lack of type »class«es as they
> are today, there was barely any other choice.  Operators added later on
> often were not purely syntactic.
>
> An advantage of syntactic type classes is that they allow to reuse
> (infix) syntax without reference to particular semantic properties.  A
> disadvantage is that they allow to write down things which to the naive
> user appear more specific then they are.  E.g. »a + b = b + a«, does not
> hold necessarily, unlike in typical notation in algebra where + is
> always commutative.  A similar joke has been "2 + 2 = 4", which was not
> true in general before Isabelle2012.  But note that min/max is defined
> purely syntactically, which can also lead to surprises.
>
> Hope this helps,	
> 	Florian
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 3735 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121215/e36e3ad4/attachment.bin>