I would want to see a concrete figures how much duplication is avoided in the current theories and how much additional annotation is needed. Note also that if some device helps to make the foundations elegant but complicates the applications it can be detrimental if the foundations remain fixed but the applications keep growing.
Tobias On 03/06/2015 10:55, Fabian Immler wrote:
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". FabianAm 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
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
