[isabelle-dev] Looking up things (Re: Function Package questions)

[Alexander Krauss]

Hi Moa,

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 
user.

* 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

Cheers,
Alex