*To*: Stefan Berghofer <berghofe at in.tum.de>*Subject*: Re: [isabelle] thm_deps*From*: John Matthews <matthews at galois.com>*Date*: Mon, 20 Mar 2006 17:03:17 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <441AE5F9.8000507@in.tum.de>*References*: <95CF3720-4313-420A-A45A-658FD6AE8144@galois.com> <441AE5F9.8000507@in.tum.de>

lemma test: "(x::int) * 0 + y = y" by auto ML {* val _ = map (fn str => print str) (Symtab.keys (Proofterm.thms_of_proof (proof_of (thm "test")) Symtab.empty)) *} However, this gave me not only the lemmas used in the proof of test, but

tactics I call when trying to prove theorems. Thanks, -john On Mar 17, 2006, at 8:38 AM, Stefan Berghofer wrote:

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 simplifyaway the occurrences of addition and multiplication don't show upin the graph browser.Hello John,I tried out the above example with the repository version ofIsabelle, andthm_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 toworkproperly, you already have to compile HOL with theorem dependenciesswitchedon. To achieve this, add ISABELLE_USEDIR_OPTIONS="-p 1" or HOL_USEDIR_OPTIONS="-p 1"to your isabelle/etc/settings file (the latter enables theoremdependenciesjust 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" someof thered nodes such as "[HOL]" or "[OrderedGroup]" by clicking on them(alternatively,you can also click on the "directories" in the left part of thewindow).Also, is there an existing ML function that, given a theoremproved while theorem dependencies was turned on (i.e. ML {*proofs := 1 *}), would return the list of lemmas used in theproof, or will I have to write something that traverses thetheorem'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 theterm representing the proposition (hence the "term" in the abovetype).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:*Stefan Berghofer

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

**Re: [isabelle] thm_deps***From:*Stefan Berghofer

- Previous by Date: Re: [isabelle] Parameterized Types?
- Next by Date: [isabelle] Formal Methods 2006: Call for Demos (Commercial and Research) and Posters
- Previous by Thread: Re: [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