Re: [isabelle] thm_deps



Thanks Stefan, that was helpful. I rebuilt the latest repository Isabelle with "-p 2", and then tried the following:

  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
the transitive closure of all the lemmas used in the proof of any lemma used by test as well. What I would like is to just get the names of the lemmas directly used in the proof of test itself. That way I can prune the list of lemmas given to
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 an Isabelle proof. Here's what I did:
  ML {* ThmDeps.enable () *}
  lemma test: "(x::int) * 0 + y = y"
  by auto
  thm_deps test
However, as far as I can see the lemmas auto used to simplify away the occurrences of addition and multiplication don't show up in the graph browser.

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 proved while theorem dependencies was turned on (i.e. ML {* proofs := 1 *}), would return the list of lemmas used in the proof, or will I have to write 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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.