Re: [isabelle] mutual primrecs

Hi Peter,

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).

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:


  evn :: "nat => bool"
  od :: "nat => bool"

  "evn 0 = True"
  "evn (Suc n) = od n"
  "od 0 = False"
  "od (Suc n) = evn n"
by pat_completeness auto

  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. :-)


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