Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function
Hi Jasmin,
On 12/02/14 12:11, Jasmin Blanchette wrote:
Hi Andreas,
I saw that you used the discriminator =, but we already have functions
Option.is_none and List.null. So far, they have been mainly used for code generation, but
I have found them very convenient in in my codatatype usages when using the destructor
style. I think it might be worth a try to give these discriminators official status.
I worked from the principle that is_none and List.null are internal constructs and
used = to avoid generating more theorems about internal things. Can you confirm that the
convenience you found in your codatatype usage also applies to datatypes?
If there is a concensus about making them more public, we can remove the =
trick.
No, the destructor view is not at all convenient for datatypes, because most functions
pattern match on the constructors. Therefore, it is better the have the constructors
explicit. Conditional rewrite rules such as List.null xs == set xs = {} help a bit with
the destructor view, but having many of them in the simpset considerably slows down the
simplifier.
However, I found the destructor view very useful even for datatypes when codatatypes are
mixed with datatypes as in the examples that I have posted earlier in this thread
(https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-February/msg00028.html). In the
destructor view, selectors and discriminators nicely accumulate, so in my proofs, it
worked better not to switch to the constructor view.
In summary, I do not want to replace _ = None and _ = [] with null and is_none, I'd
just like to make null and is_none somewhat official. I am not sure when these
discriminators can show up in practice, but I thought that only primcorec needs them. So
from my point of view, it seems sensible to make them the official discriminators.
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function
Hi Jasmin, On 13/02/14 13:47, Jasmin Blanchette wrote: Hi Andreas, Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler andreas.lochbih...@inf.ethz.ch: In summary, I do not want to replace _ = None and _ = [] with null and is_none, I'd just like to make null and is_none somewhat official. I am not sure when these discriminators can show up in practice, but I thought that only primcorec needs them. So from my point of view, it seems sensible to make them the official discriminators. Now I'm confused. If we do what you just proposed, the discriminators end up appearing in some of the generated theorems -- and you observed yourself that the destructor view is not at all convenient for datatypes, because most functions pattern match on the constructors. Therefore, it is better the have the constructors explicit. For a datatype, being an official discriminator basically amounts to appearing in generated theorems. Or did I misunderstood something? I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in theorems generated by primcorec. This is fine, because the destructor view for codatatypes goes well with discriminators and selectors for datatypes. As I do not know where discriminators show up in theorems generated by datatype_new, but my guess is that they only show up in theorems that the old datatype package does not generate. Moreover, I expect that they do not show up in anyhing generated by primrec. So where would it harm to make them the official discriminators? Andreas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] primcorec complains about invalid map function
Hi Andreas, I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in theorems generated by primcorec. This is fine, because the destructor view for codatatypes goes well with discriminators and selectors for datatypes. As I do not know where discriminators show up in theorems generated by datatype_new, but my guess is that they only show up in theorems that the old datatype package does not generate. Moreover, I expect that they do not show up in anyhing generated by primrec. So where would it harm to make them the official discriminators? There's certainly no big harm in making them the official discriminators. My main fear is inconsistency: There are many theorems in Isabelle that have xs ~= [] as a premise. If we start generating some with null xs or List.null xs, we end up with an unpleasing mixture, whose only satisfactory resolution is to have both versions of everything (cf. the duplication of Suc vs + 1 theorems). Hence, until there is a wider concensus about the merits of null and is_none, I am reluctant to go that way (but will not stop anybody who wants to change the statu quo). For pred, the situation is even worse: Ideally we would have %x. x - 1 in there. Right now I'm just hiding the theorems and constants, but they might resurface e.g. in the constructor and destructor views generated from a code view of primcorec. My ultimate goal is to have a more or less ad hoc setup that replaces prec by - 1 and then make the theorems public. Hiding the theorems is an intermediate step toward this. Cheers, Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
