Re: [isabelle] nested datatypes

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.



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

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?



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