[isabelle] nested datatypes




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







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