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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
