*To*: John Matthews <matthews at galois.com>*Subject*: Re: [isabelle] thm_deps*From*: Stefan Berghofer <berghofe at in.tum.de>*Date*: Fri, 17 Mar 2006 17:38:17 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <95CF3720-4313-420A-A45A-658FD6AE8144@galois.com>*Organization*: Technische Universität München*References*: <95CF3720-4313-420A-A45A-658FD6AE8144@galois.com>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.12) Gecko/20050920

John Matthews wrote:

Hi, I'm trying to see what lemmas end up being used by auto in anIsabelle proof. Here's what I did:ML {* ThmDeps.enable () *} lemma test: "(x::int) * 0 + y = y" by auto thm_deps testHowever, as far as I can see the lemmas auto used to simplify away theoccurrences of addition and multiplication don't show up in the graphbrowser.

Hello John, I tried out the above example with the repository version of Isabelle, and thm_deps displayed a dependency on the theorems mult_zero_right, add_0_right, and add_left_cancel (among others). Note that in order for this to work properly, you already have to compile HOL with theorem dependencies switched on. To achieve this, add ISABELLE_USEDIR_OPTIONS="-p 1" or HOL_USEDIR_OPTIONS="-p 1" to your isabelle/etc/settings file (the latter enables theorem dependencies just for the HOL images, but not for other images such as HOL-Complex etc.). Of course, "-p 2" works as well, although it is a lot slower. Also note that in the graph browser, you may have to "unfold" some of the red nodes such as "[HOL]" or "[OrderedGroup]" by clicking on them (alternatively, you can also click on the "directories" in the left part of the window).

Also, is there an existing ML function that, given a theorem provedwhile theorem dependencies was turned on (i.e. ML {* proofs := 1 *}),would return the list of lemmas used in the proof, or will I have towrite something that traverses the theorem's proof object?

There is a function Proofterm.thms_of_proof: Proofterm.proof -> (Term.term * Proofterm.proof) list Symtab.table -> (Term.term * Proofterm.proof) list Symtab.table that recursively adds all lemmas (i.e. proofs of the form "PThm ...") occurring in a proof to a table. Since there can be several theorems with same name but different propositions, we also have to record the term representing the proposition (hence the "term" in the above type). The function call Proofterm.thms_of_proof (proof_of (thm "test")) Symtab.empty produces a table of all lemmas used in the proof of "test". 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

**Follow-Ups**:**Re: [isabelle] thm_deps***From:*John Matthews

**References**:**[isabelle] thm_deps***From:*John Matthews

- Previous by Date: Re: [isabelle] Help with simplification loops.
- Next by Date: Re: [isabelle] mutual recdefs
- Previous by Thread: [isabelle] thm_deps
- Next by Thread: Re: [isabelle] thm_deps
- Cl-isabelle-users March 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list