[isabelle-dev] »real« considered harmful

[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'_ℚ")




-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150605/54bb5ba2/attachment.sig>