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 <nip...@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-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev