Re: [isabelle] Quickcheck setup for finite sets

Hi Andreas,

> However, you could also just have used the command
> quickcheck_generator fset constructors: "{||}", finsert
> which generates almost the same instances as you did manually.

first of all, I didn't know about that command :-)

Anyway, the way I implemented the generator for 'fset's was to copy the
generator for 'set's and changed the constants (e.g. 'insert' â 'finsert').

If nobody objects, I would add these instances to the 'FSet' theory in

> According to the documentation in isar-ref, quickcheck installs random
> and exhaustive generators for first-order datatypes. I do not know
> whether the documentation has been kept up to date during the transition
> to the BNF package, but it looks as if it is still correct. So no nested
> recursion.

Maybe this is a candidate for consolidation with the 'Derive' AFP entry.
(On the other hand, as far as I know, that one doesn't support nested
recursion through non-datatypes.)

Because you mentioned it in your mail, I also tried
'quickcheck_generator' on my datatype, but it (silently!) fails to
produce instances.


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