[isabelle-dev] »real« considered harmful
Johannes Hölzl
hoelzl at in.tum.de
Mon Jun 8 14:08:39 CEST 2015
The syntax is nice, but I would interpret "_⇩ℕ" not as of_nat but as
into nat, or more specifically I would read: _⇩ℝ == real _.
- Johannes
Am Freitag, den 05.06.2015, 23:58 +0200 schrieb Florian Haftmann:
> Hi again,
>
> after I first iteration of discussion I see a list of three requirements:
>
> 1. Conversions can be written succinctly.
> 2. Conversions are printed succinctly.
> 3. Conversions are unique, there are no accidental equivalences which
> require explicit conversions.
>
> Concerning (1), my guess indeed is the implicit conversions should do
> the job. There is the borderline case with required explicit type
> annotations (»of_nat n :: rat«) which is currently handled by distinct
> abbreviations, but these could be dropped.
>
> (2) is not so trivial if you want to make sure that the printed terms
> are compact but still complete in the sense that they are invariant
> under copy-and-paste. I think of_nat/of_int/of_rat is fine, but
> real_of_int etc. is definitely not. Anyway, like in (1) these
> abbreviations might be entirely superfluous. The disadvantage of the
> algebraic conversions is that the do not tell what the result type is --
> which is usually the more important information, since the argument
> type's is usually easily inferred. Maybe suitable symbol syntax can
> help here.
>
> Below I made some experiments how fancy symbol syntax could look like,
> but I am still lacking a conclusive idea.
>
> (3) Everything has been said about this already.
>
> So, I would suggest we spend thoughts how *printing* of
> of_foo-Conversions can be improved with reasonable means (2). We are
> still at the beginngin…
>
> Cheers,
> Florian
>
> > notation of_nat ("_⇩ℕ" [999])
> > notation of_int ("_⇩ℤ" [999])
> > notation of_rat ("_⇩ℚ" [999])
> >
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> >
> > notation real_of_nat ("of'_nat⇩ℝ")
> > notation real_of_int ("of'_int⇩ℝ")
> > notation real_of_rat ("of'_int⇩ℚ")
> >
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> >
> > notation of_nat ("of'_ℕ")
> > notation of_int ("of'_ℤ")
> > notation of_rat ("of'_ℚ")
> >
> > term "rep_real (of_nat (Suc n) + of_int (k div l))"
> > thm of_nat_diff
> >
> > notation real_of_nat ("ℝ'_of'_ℕ")
> > notation real_of_int ("ℝ'_of'_ℤ")
> > notation real_of_rat ("ℝ'_of'_ℚ")
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
More information about the isabelle-dev
mailing list