[isabelle-dev] [isabelle] primcorec complains about invalid map function

[Andreas Lochbihler]

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