[isabelle] Quickcheck setup for finite sets

Dear list,

is there any reason why there's no Quickcheck setup for finite sets? I
couldn't find any, so I tried setting it up (see attached theory). I'm
hardly a Quickcheck expert, so I have no idea whether it makes sense â
at least it works for some cases I tried.

Slightly related question: How does the interaction between the datatype
package and Quickcheck work? It appears that it produces instances of
full_exhaustive in certain cases and not in others, but I'm not quite
sure in which cases. (Current working hypothesis: It doesn't when nested
recursion is involved.) Is there any other way to conveniently obtain
full_exhaustive instances?


Attachment: FSet_Quickcheck.thy
Description: application/extension-thy

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