[isabelle-dev] Looking up things (Re: Function Package questions)
krauss at in.tum.de
Thu Apr 17 10:41:23 CEST 2008
I'm forwarding your questions to the isabelle-dev list, since they are
not actually Function Package questions, and more people might want to
comment on this.
> We're currently trying to get some information out about what's defined
> in a particular theory. Working on the ML level is it possible to:
> - Get the names of any functions/constants defined *by the user* in a
> given theory?
I am not an expert here, but there are several options, depending on
what you want to do exactly.
* First you can try to do Sign.consts_of, and look at the actual
constant tables (cf. Pure/sign.ML, Pure/consts.ML). But this will give
you all constants, including those that are defined by packages, not the
* Then you could ask the individual packages, as they usually keep a
record of what they have defined. For example, the function package
stores a record for all functions it has defined. See
HOL/Tools/function_package/fundef_common.ML. I am not sure about
"primrec" and "definition". Obviously, this is ugly since you have to
talk to all packages...
Maybe others can comment...
> - Get the theorems involving a particular function symbol/constant
> given a theory?
This sounds like an ML level counterpart for find_theorems. It seems
that this doen't exist, but I think it could be done easily.
> - Get the theorems defining a particular function?
Not really. You can try to do some fishing via names... eg, the function
package stores the recursive equations as f.simps for a function f.
What you are trying to do is difficult since the distinction between
definitions and derifvd facts is usually not important in the system.
Even worse, definitions by packages like "function" or "inductive" are
not actually definitions but derived facts that work like definitions
from the user's point of view.
I guess that for some applications it might be useful to tag these facts
as "user-level specifications", such that they can be treated specially
for presentation, searching, and other "soft" purposes.
So I'd like to know where your particular need arises for these things.
> Also, do you know if it is possible to get the names of user defined
> datatypes given a theory?
Yes: See HOL/Tools/datatype_package.ML: DatatypePackage.get_datatype(s)
But again, this covers only datatypes not eg. typedefs
More information about the isabelle-dev