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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
