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

[Moa Johansson]

Hi,

Sorry for being mysterious, we've just started working on a new idea 
about synthesising conjectures in inductive theories. Me and Lucas have 
written a note about it (attached) if anyone is interested to read. Any 
comments always welcome. We want to use existing definitions and 
theorems to help restrict what is allowed to be generated by synthesis, 
hence my question about looking up definitions. Initially at least, 
we'll be interested in recursively defined functions (as we like 
inductive theorem proving up in Edinburgh :) so I think we'll be fine 
getting the information from the function package for starters. Thanks 
for the programming tips!

Cheers,
Moa

Alexander Krauss wrote:
> 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
>


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: note-1642.pdf
Type: application/pdf
Size: 108587 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080421/747f614b/attachment-0002.pdf>