Re: [isabelle] nested datatypes
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
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, ).
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
. 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.
Am 08.08.2013 06:18, schrieb Jeremy Dawson:
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
val it =
"[| !!list. ?P2.0 list ==> ?P1.0 (Rtree list); !!a. ?P1.0 (Ritem a);
[| ?P1.0 rose_tree; ?P2.0 list |] ==> ?P2.0 (rose_tree #
==> ?P1.0 ?rose_tree & ?P2.0 ?list" : Thm.thm
But I want to do the same sort of thing with multisets instead of
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
Is there any way around this problem?
This archive was generated by a fusion of
Pipermail (Mailman edition) and