Re: [isabelle] Separating function declaration from implementation



Randy Pollack wrote:
George Karabotsos writes:
 > Hello all,
> > I am wondering if there is a way to separate the declaration of a > function (as defined by the fun or function keywords) by its implementation. > This is possible using the older consts and primrec or refdef way for > declaring functions but I cannot see how it can be done with the new way.

It cannot be done. The new definitional packages (function, inductive(_set)) all declare and define constants simultaneously. The reason is that the (internal) local theory interface (which allows these packages to work in locale/class/instantiation/... contexts too) supports only that.

I noticed this too, and to take it one step further, why can't the
syntactic outlines of these tools be similar; i.e. just replace
"primrec" with "function".  The reason I request this is that when
primrec fails (e.g. even on some primitive recursive functions in the
nominal package) I just switch to function.  Why should this require
changing more than one keyword?

You are right. This is why primrec will also change its syntax to the simultaneous style. The new syntax, which works just like "function", is already supported (and preferred) in the developers version.

Eventually, primitive "const" declarations will mostly disappear from user theories, and you will use the "definition", "inductive", "primrec", "function"... packages, which all share a common syntax.

Alex








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.