Email Gateway (Aug 18 2022 at 09:36): Email Gateway (Aug 18 2022 at 09:36):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
A while back, Tobias suggested that better support for mutually
recursive function definitions was in the pipeline. It would be
useful to know when we might hope for them, if there are any concrete
plans for them in a near-term release? (so that we could avoid
embarking on tupling or higher-order encodings, eg for primrecs of n*m
mutually recursive functions, n each over m mutually recursive datatypes).
many thanks,
Peter
Email Gateway (Aug 18 2022 at 09:36):From: Alexander Krauss <krauss@in.tum.de>
Hi Peter,
My new function package can do mutual recursion (by automatically
constructing a function over the sum type internally). It is already
available in the CVS version and will be included in the next release
(but don't ask me when that is :-)).
The package has some more features concerning partiality, exotic pattern
matching and so on, but you can safely ignore this if you stick to the
following pattern:
consts
evn :: "nat => bool"
od :: "nat => bool"
function
"evn 0 = True"
"evn (Suc n) = od n"
and
"od 0 = False"
"od (Suc n) = evn n"
by pat_completeness auto
termination
by (auto_term "measure (sum_case (%n. n) (%n. n))")
thm evn.simps
thm od.simps
thm evn_od.induct
Note that since general recursion is supported, you need to do a
termination proof. Just specifying an appropriate relation to the
auto-term method (as with recdef) should do. But the relation must be
specified over the sum type in the case of mutual recursion.
The "by pat_completeness auto" thing solves proof obligations about the
pattern matching. You can read more about it in my IJCAR 2006 paper, but
if your functions are just primrec-style, you can just ignore it.
HOL/ex/Fundefs.thy contains a few more "function"-Examples. Note that
especially mutual recursion is only poorly tested, and that the syntax
will change again in the near future. If this doesn't frighten you, you
are invited to try it, and I'll be happy about every feedback. :-)
Alex
Last updated: Nov 21 2024 at 12:39 UTC