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
