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

[Florian Haftmann]

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121215/76165513/attachment.sig>