[isabelle-dev] »real« considered harmful

[Florian Haftmann]

Dear all,

recently, I stumbled (once again) over the matter of the »real« conversion.

There is an inclusion hierarchy (⊆) of numerical types

	(num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex

We can embed »smaller« into »bigger« types using conversions

	(numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real

These conversions have solid generic algebraic definitions!

For historic reasons, there is also the conversion real :: 'a ⇒ real
which is overloaded and can be instantiated to arbitrary types. This
(co)conversion works in the other direction without any algebraic
foundation!

My impression is that having this conversion is a bad idea. For
illustration have a look at
http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
which gives a wonderful generic lemma relating fraction division and
integer division:

	»floor (of_int k / of_int l) = k div l«

Note that the result type of the of_int conversion is polymorphic and
can be instantiated to rat and real likewise!

In the presence of the »real« conversion, there is a second variant

	»floor (real k / real l) = k div l«

which must be given separately!

For uniformity it would be much better to have »real« disappear in the
middle run. I see two potential inconveniences at the moment:
* Writing »of_foo« might demand a type annotation on its result in many
cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
explicit type annotations must be given in terms rather than at »fixes«).
* We have the existing abbreviations »real_of_foo« which have no type
ambiguity, but might seem a little bit verbose.
Anyway, the duplication seems more grivious to me than such syntax issues.

Any comments?
	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: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150602/459f738d/attachment.asc>