Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] nested datatypes


view this post on Zulip Email Gateway (Aug 19 2022 at 11:36):

From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
I'm familiar with a datatype declaration such as

datatype 'a rose_tree = Rtree "'a rose_tree list"
| Ritem "'a"

and this gives the induction theorem

rose_tree.induct ;
val it =
"[| !!list. ?P2.0 list ==> ?P1.0 (Rtree list); !!a. ?P1.0 (Ritem a);
?P2.0 [];
!!rose_tree list.
[| ?P1.0 rose_tree; ?P2.0 list |] ==> ?P2.0 (rose_tree #
list) |]
==> ?P1.0 ?rose_tree & ?P2.0 ?list" : Thm.thm

But I want to do the same sort of thing with multisets instead of lists, ie

datatype 'a mrose_tree = MRtree "'a mrose_tree multiset"
| MRitem "'a"

but this is not allowed,

*** Non-admissible type expression
*** 'a mrose_tree multiset
*** Multiset_no_le.multiset is not a datatype - can't use it in nested
recursion

Is there any way around this problem?

Cheers,

Jeremy

view this post on Zulip Email Gateway (Aug 19 2022 at 11:36):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Jeremy,

in Isabelle2013 there is a new datatype package (session HOL-BNF, entry
theory "src/HOL/BNF/BNF") that covers nested recursion through many
non-free data structures (including finite sets, countable sets, and
multisets).

It allows you to define

data 'a rose_tree = Rtree "'a rose_tree multiset" | Ritem "'a"

Here multiset is the type defined in src/HOL/Library/Multiset. From your
error message I see that you use a different multiset type (from a
different theory). In order to use this type in datatype declarations it
must be proved to be a so called bounded natural functor (BNF, [1]).
This (admittedly tedious) work we have done for multiset from
src/HOL/Library/Multiset in src/HOL/BNF/More_BNFs (search for "bnf_def
multiset_map"). You would need to do a similar thing for your custom
multiset (so far there is also no documentation on bnf_def, only
examples---I can help to sort out the details).

Moreover, the proper integration of the package is happening right now
[2]. Currently, in order to define recursive functions on the defined
datatype you will have to use low level combinators (rose_tree_fold,
rose_tree_rec) rather than primrec/fun. The plan is to have at least
primrec support in the next Isabelle release.

Cheers,
Dmitriy

[1] http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/codat.pdf
[2]
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-July/004390.html


Last updated: Mar 28 2024 at 12:29 UTC