bulwahn at in.tum.de
Fri Dec 9 16:39:31 CET 2011
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
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
More information about the isabelle-dev