Re: [isabelle] Quickcheck setup for finite sets

Hi Lars,

quickcheck in its current form was mainly developed by Lukas Bulwahn, who left academia before fset became usable. So far, nobody cared to add the quickcheck setup. From my experience with quickcheck, your setup is fine. However, you could also just have used the command

quickcheck_generator fset constructors: "{||}", finsert

which generates almost the same instances as you did manually. The difference is that the your instances check whether an new element is already present in the set and if so, they skip the execution assuming that it has been tested before. This is just an optimisation which avoids to run the code on equivalent test case several times, but I doubt that this redundancy causes any problems in practice.

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.


On 07/07/15 14:41, Lars Hupel wrote:
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?


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