[isabelle-dev] New (Co)datatypes: Status & Plan (FYI)

[Jasmin Blanchette]

Hi Florian,

> An example could be something like
> 
> primitive_recursion card :: "'a set => nat"
> where
>  "card {} = 0"
>  "card (insert x A) = Suc (card A)"
> proof -
>  show "!!x y. insert x o insert y = insert y o insert x"
>  show "!!x. insert x o insert x = insert x"
> qed
> 
> thm card.simps -- {*
>  "card {} = 0"
>  "finite A ==> card (insert x A) = Suc (card A)"
> *}
> 
> using Finite_Set.fold internally.

Andy answered this much better than I could have. :)

> Apart from that aside, are separated keywords for primrec and primcorec
> really needed, or can they be distinguished just syntactically?

They can be distinguished syntactically, but I see no good reason _not_ to use a different keyword. It's not as if keywords were expensive, and it would feel wrong to type "primrec" when ones mean "primcorec" or vice versa.

Have you ever programmed in C/C++? If so, you would surely have noticed that the reuse of keywords there (esp. "static", which has something like four distinct meanings). The C/C++ motivation for this reuse was to avoid breaking applications, which matters a lot when there are billions of LOCs out there, but in Isabelle we have a more reasonable amount of users and also a distinction between outer and inner syntax that makes most clashes harmless (and who is going to call anything "primcorec" anyway?).

> I guess (co)primrec(_new) has no problem with performance.

Nothing worse than quadratic in the number of constructors, I believe.

> We have still some recdef applications not migrated yet to function due to
> performance issues.

Right.

Jasmin