[isabelle-dev] Quickcheck_Exhaustive.unknown

[Lukas Bulwahn]

On 11/30/2011 03:17 PM, Tobias Nipkow wrote:
> Am 30/11/2011 12:27, schrieb Makarius:
>> This concerns Isabelle/3d6ee9c7d7ef:
>>
>> Adding a global constant Quickcheck_Exhaustive.unknown with rather
>> generic notation "?" to main HOL is a bit dangerous.  The name "unknown"
>> is also a candidate for "hide_const (open)".
> I would like to emphasize this. Local names (i.e. those that the clients
> of a package or theory do not need to know) should stay local, i.e.
> should be hidden at the end. This is particularly important if the name
> is something generic like "Times" or "unknown" that other people may
> want to use, too, w/o suffering from long names. Quickcheck is
> particularly generous in what it exports...
I looked into this issue this afternoon.

First of all, I agree, Quickcheck is particularly generous defining 
constants: All of its infrastructure must exist in the logic, as it 
relies on the code generator.

The existing hide_const declarations already were hiding all constants 
in Quickcheck.
Changeset 5616fbda86e6 now also hides all definitional theorems. So even 
the names of theorems are now hidden.

Unfortunately, the find_theorems command is quite ignorant to any means 
to hide facts:
Facts that have been hidden, can be found.
And also facts that were properly concealed in the ML sources are found.

This surprises me as the authors of "find_theorems" seem to be expecting 
that they are filtering them out, cf. line 524 in find_theorems.ML 
(changeset e832acb88f43).


Lukas