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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev