[isabelle-dev] Finding unused theorems

[Stefan Berghofer]

Dear all,

the CVS version of Isabelle now contains a new command called "unused_thms"
for finding unused theorems. There are three ways of invoking it:

(1) unused_thms
     Only finds unused theorems in the current theory.

(2) unused_thms thy_1 ... thy_n -
     Finds unused theorems in the current theory and all of its ancestors,
     excluding the theories thy_1 ... thy_n and all of their ancestors.

(3) unused_thms thy_1 ... thy_n - thy'_1 ... thy'_m
     Finds unused theorems in the theories thy'_1 ... thy'_m and all of
     their ancestors, excluding the theories thy_1 ... thy_n and all of
     their ancestors.

In order to increase the readability of the list produced by unused_thms,
theorems that have been created by a particular instance of a theory
command such as inductive or fun(ction) are considered to belong to the
same "group", meaning that if at least one theorem in this group is used,
the other theorems in the same group are no longer reported as unused.
Moreover, if all theorems in the group are unused, only one theorem in
the group is displayed.
There are still a few rough edges, though: at the moment the "grouping"
mechanism is not yet implemented for old packages (such as datatype and
record), and the "group" tags of theorems proved in a locale currently
get lost when interpreting the locale.

Note that proof objects have to be switched on in order for unused_thms
to work properly (i.e. !proofs must be >= 1, which is usually the case
when using ProofGeneral with the default settings). Since unused_thms relies
on the information stored in the theorem database, overwriting theorems
(which in my opinion is a bad idea anyway), as well as producing unnamed
theorems may cause wrong results to be displayed.

Suggestions for improvement are highly welcome.

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe