[isabelle-dev] »real« considered harmful

[Johannes Hölzl]

Maybe we should resurrect the idea of using adhoc overloading for the
"real" abbreviation.

Florian, does your rework of the generic machinery for syntactic
abbreviations include moving more of the adhoc overloading into HOL?
Then we could setup real as an adhoc overloaded constant and the proof
machinery only sees of_nat, of_int, while the user has still the ability
to write "real".

 - Johannes

Am Mittwoch, den 03.06.2015, 11:20 +0200 schrieb Tobias Nipkow:
> Thank you for reminding me of the "reading" part. My ability to read formulas 
> decreases quadratically with their length. Trading in "real_of_int" for "real" 
> makes things definitely worse.
> 
> 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".
> >
> > 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
> >
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev