Email Gateway (Aug 19 2022 at 11:36): 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
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: Nov 21 2024 at 12:39 UTC