[isabelle-dev] »real« considered harmful

[Tobias Nipkow]

For me the main point of "real" is the ease of writing. If we get rid of some 
lemma duplications but trade that in for many type annotations, I am not in favour.

Tobias

On 02/06/2015 20:18, Florian Haftmann wrote:
> 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
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

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