Email Gateway (Aug 18 2022 at 11:30): Email Gateway (Aug 18 2022 at 11:30):From: George Karabotsos <g_karab@cs.concordia.ca>
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.
TIA,
George
Email Gateway (Aug 18 2022 at 11:30):From: Randy Pollack <rpollack@inf.ed.ac.uk>
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.
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?
Best,
Randy
Email Gateway (Aug 18 2022 at 11:30):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 11:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
It is worth noting that future Isabelle versions still technically will
permit to separate constant declaration from constant definition by
means of the overloading target:
consts foo :: "'a => 'a"
overloading
foo == "foo :: 'a => 'a"
begin
definition foo :: "'a => 'a" where
"foo x = x"
end
thm foo_def
Obviously, this only works on the theory level (not in locales etc.).
Presumably this was one reason to sacrifice the separation of consts and
defs on the Isar level.
Florian
signature.asc
Last updated: May 03 2024 at 04:19 UTC