[isabelle-dev] »real« considered harmful

[Johannes Hölzl]

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