Re: [isabelle-dev] »real« considered harmful
On 5 Jun 2015, at 22:22, Florian Haftmann wrote: > >> Why do we need abbreviations such as these? >> >> abbreviation real_of_nat :: "nat \ real” >> where "real_of_nat \ of_nat" >> >> abbreviation real_of_int :: "int \ real” >> where "real_of_int \ of_int" >> >> abbreviation real_of_rat :: "rat \ real” >> where "real_of_rat \ of_rat" >> >> abbreviation complex_of_real :: "real \ complex" >> where "complex_of_real \ of_real" > > The deeper reason why these have been introduced is that such > conversions of type T => 'a::c can be difficult to write in presence of > type ambiguities. If you need more special types, you can do barely > anything else than writing »(of_foo x :: T)« which clutters readability. OK — but that’s no reason to introduce “real” as another way to write these coercions, while introducing precisely the sort of type ambiguity that is the root of such problems. Conceivably we could introduce a prefix syntax for type constraints, e.g. [:real:]of_nat k I’d find such a thing useful from time to time. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
I’d be happy to see the complete phasing out of TFL. It’s had its day. It was always a tricky thing to maintain. I’m amazed that it still works despite all of the many fundamental changes to system APIs. Larry > On 5 Jun 2015, at 21:42, Florian Haftmann > wrote: > >> Cleaning up some obscure corners of the system, I've come across the old >> defer_recdef command. >> >> Are there any remaining uses of this historical relic? I don't see any >> in the main Isabelle repository + AFP. > > Some years ago the idea was to let recdef stand as long as there are > examples in the distribution. The consequence would be to dismantle > unused parts altogether. > > Further suggestios? > > Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
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
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
> Why do we need abbreviations such as these? > > abbreviation real_of_nat :: "nat \ real” > where "real_of_nat \ of_nat" > > abbreviation real_of_int :: "int \ real” > where "real_of_int \ of_int" > > abbreviation real_of_rat :: "rat \ real” > where "real_of_rat \ of_rat" > > abbreviation complex_of_real :: "real \ complex" > where "complex_of_real \ of_real" The deeper reason why these have been introduced is that such conversions of type T => 'a::c can be difficult to write in presence of type ambiguities. If you need more special types, you can do barely anything else than writing »(of_foo x :: T)« which clutters readability. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
> Maybe we should resurrect the idea of using adhoc overloading for the > "real" abbreviation. The idea in itself is not bad, but I am reluctant to pull ad-hoc overloading into the HOL theories itself. There are still too many dragons sitting in the dark. > Florian, does your rework of the generic machinery for syntactic > abbreviations include moving more of the adhoc overloading into HOL? This work has not even started yet… Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of defer_recdef?
> Cleaning up some obscure corners of the system, I've come across the old > defer_recdef command. > > Are there any remaining uses of this historical relic? I don't see any > in the main Isabelle repository + AFP. Some years ago the idea was to let recdef stand as long as there are examples in the distribution. The consequence would be to dismantle unused parts altogether. Further suggestios? Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Infix syntax for division?
Hi Manuel, > I also vote for b). I would also like to add that I ran into situations > where I required the notation of an inverse element in a ring. I defined > this as "ring_inv x = 1 div x". For instance, on int, we have "ring_inv > 1 = 1" and "ring_inv (-1) = -1" and everything else is basically > ill-defined, because 1 and -1 are the only units in ℤ. > > Using "inverse" for this would be an idea, since ring_inv and inverse > are equivalent on fields anyway, but that, I think, would also > automatically introduce a rather useless "/" for all rings, which we > probably do not want. indeed your work on rings inspired me to introduce a unified division. My idea is to have a type class based on (semi)rings which adds the necessary algebraic notion to formulate euclidean rings. Somewhere in the typeclass hierarchy should be a proper fork in order not to pollute rings with field-specific notions like »/« and vice versa (e.g. is_unit). Of course you can define all those logically consistenty in the »wrong« structures, but they do not make much sense. Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
