[isabelle-dev] »real« considered harmful

[Fabian Immler]

I think I could live without "real": coercions save a lot of the writing.
Moreover, the "real_of_foo" abbreviations help to avoid type annotations:
I suppose that all of the current occurrences of "real" could be replaced with one particular "real_of_foo".

For reading (subgoals etc), one could perhaps think about less obstructive abbreviations like e.g., "real_N" and "real_Z", or "real⇩N" and "real⇩Z".
But I see that "real_of_foo" is much more uniform and you can immediately read off the type "foo".

Fabian

> Am 03.06.2015 um 10:11 schrieb Tobias Nipkow <nipkow at in.tum.de>:
> 
> 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
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev