Re: [isabelle-dev] Definite name for case combinator on products [was: NEWS]
In fb95d06fb21f, find my attempt to reach a stable status again after opening too many loose ends. * The combinator is named »case_prod« uniformly; no aliasses remain, in order not to obfuscate the now reached state of uniformity. * The most popular theorem names with »split« are retained (see end of HOL/Product_Type.thy); there could be room for further cleanup there, e. g. getting rid of the alias »split« and reducing the variants regarding eta-contraction further. But I did not attempt this at this moment. * Some discontinuities introduced unconsciously in the past (e. g. wrong trigger terms for simprocs) have been repaired silently. * I encountered a borderline case of printing and just reinstallated a print translation believed to be totally obsolete; my conclusion at the moment is that it is not feasible to refine anything regarding the parsing / printing of products without reconsidering / remoulding the eta-expansion issue. This is the state of affairs. Please report any remaning suspicious behaviour. Florian Am 22.09.2015 um 16:20 schrieb Florian Haftmann: > So, the direction is going towards prod_case. > > If this is settled, the consequences are: > * Abbreviation »uncurry« will disappear again. > * Abbreviation »split« will disappear finally (using the distribution > and AFP as indicator whether this is »now« or »later«). > * Theorem names contain »prod_case« instead of »split«; the latter are > retained as aliasses, but documentation etc. is updated to prefer the > first version. > * There is no way to have something like »curry (uncurry f) = f« > printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f > x y) = f« by default. > > Any headache with this? > > Florian > > Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: >> Hi Florian, >> >> while I very much welcome the simplified printing rules and your effort >> of unifying case_prod/split, I am not sure if adding a third alternative >> name is the way to go. The situation reminds me of the one depicted in [1]. >> >> Clearly, case_prod is the "right" name from the perspective of the >> (co)datatype package. >> >> Dmitriy >> >> [1] https://xkcd.com/927/ >> >> On 10.09.2015 12:02, Florian Haftmann wrote: >>> * Combinator to represent case distinction on products is named >>> "uncurry", with "split" and "prod_case" retained as input abbreviations. >>> >>> Partially applied occurences of "uncurry" with eta-contracted body >>> terms are not printed with special syntax, to provide a compact >>> notation and getting rid of a special-case print translation. >>> >>> Hence, the "uncurry"-expressions are printed the following way: >>> >>> a) fully applied "uncurry f p": explicit case-expression; >>> >>> b) partially applied with explicit double lambda abstraction in >>> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >>> >>> c) partially applied with eta-contracted body term "uncurry f": >>> no special syntax, plain "uncurry" combinator. >>> This aims for maximum readability in a given subterm. >>> INCOMPATIBILITY. >>> >>> This refers to e6b1236f9b3d. >>> >>> This schema emerged after some experimentation and seems to be a >>> convenient compromise. The longer perspective is to overcome the >>> case_prod/split schism eventually and consolidate theorem names accordingly. >>> >>> The next step after this initial cleanup is to tackle the »let (a, b) = >>> … in …« issue. >>> >>> Florian >>> >>> >>> >>> ___ >>> isabelle-dev mailing list >>> isabelle-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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
[isabelle-dev] Definite name for case combinator on products [was: NEWS]
So, the direction is going towards prod_case. If this is settled, the consequences are: * Abbreviation »uncurry« will disappear again. * Abbreviation »split« will disappear finally (using the distribution and AFP as indicator whether this is »now« or »later«). * Theorem names contain »prod_case« instead of »split«; the latter are retained as aliasses, but documentation etc. is updated to prefer the first version. * There is no way to have something like »curry (uncurry f) = f« printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f x y) = f« by default. Any headache with this? Florian Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: > Hi Florian, > > while I very much welcome the simplified printing rules and your effort > of unifying case_prod/split, I am not sure if adding a third alternative > name is the way to go. The situation reminds me of the one depicted in [1]. > > Clearly, case_prod is the "right" name from the perspective of the > (co)datatype package. > > Dmitriy > > [1] https://xkcd.com/927/ > > On 10.09.2015 12:02, Florian Haftmann wrote: >> * Combinator to represent case distinction on products is named >> "uncurry", with "split" and "prod_case" retained as input abbreviations. >> >> Partially applied occurences of "uncurry" with eta-contracted body >> terms are not printed with special syntax, to provide a compact >> notation and getting rid of a special-case print translation. >> >> Hence, the "uncurry"-expressions are printed the following way: >> >> a) fully applied "uncurry f p": explicit case-expression; >> >> b) partially applied with explicit double lambda abstraction in >> the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; >> >> c) partially applied with eta-contracted body term "uncurry f": >> no special syntax, plain "uncurry" combinator. >> This aims for maximum readability in a given subterm. >> INCOMPATIBILITY. >> >> This refers to e6b1236f9b3d. >> >> This schema emerged after some experimentation and seems to be a >> convenient compromise. The longer perspective is to overcome the >> case_prod/split schism eventually and consolidate theorem names accordingly. >> >> The next step after this initial cleanup is to tackle the »let (a, b) = >> … in …« issue. >> >> Florian >> >> >> >> ___ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- 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] Definite name for case combinator on products [was: NEWS]
Sounds good to me. Dmitriy On 22.09.2015 16:20, Florian Haftmann wrote: So, the direction is going towards prod_case. If this is settled, the consequences are: * Abbreviation »uncurry« will disappear again. * Abbreviation »split« will disappear finally (using the distribution and AFP as indicator whether this is »now« or »later«). * Theorem names contain »prod_case« instead of »split«; the latter are retained as aliasses, but documentation etc. is updated to prefer the first version. * There is no way to have something like »curry (uncurry f) = f« printed; entering »curry (prod_case f) = f« prints as »curry (λ(x, y). f x y) = f« by default. Any headache with this? Florian Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel: Hi Florian, while I very much welcome the simplified printing rules and your effort of unifying case_prod/split, I am not sure if adding a third alternative name is the way to go. The situation reminds me of the one depicted in [1]. Clearly, case_prod is the "right" name from the perspective of the (co)datatype package. Dmitriy [1] https://xkcd.com/927/ On 10.09.2015 12:02, Florian Haftmann wrote: * Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. Partially applied occurences of "uncurry" with eta-contracted body terms are not printed with special syntax, to provide a compact notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; b) partially applied with explicit double lambda abstraction in the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; c) partially applied with eta-contracted body term "uncurry f": no special syntax, plain "uncurry" combinator. This aims for maximum readability in a given subterm. INCOMPATIBILITY. This refers to e6b1236f9b3d. This schema emerged after some experimentation and seems to be a convenient compromise. The longer perspective is to overcome the case_prod/split schism eventually and consolidate theorem names accordingly. The next step after this initial cleanup is to tackle the »let (a, b) = … in …« issue. Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
