Email Gateway (Aug 17 2022 at 14:14): Email Gateway (Aug 17 2022 at 14:14):From: John Matthews <matthews@galois.com>
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.
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?
Thanks,
-john
Email Gateway (Aug 17 2022 at 14:14):From: Stefan Berghofer <berghofe@in.tum.de>
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 autothm_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
Email Gateway (Aug 17 2022 at 14:15):From: John Matthews <matthews@galois.com>
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
Email Gateway (Aug 17 2022 at 14:15):From: Stefan Berghofer <berghofe@in.tum.de>
John Matthews wrote:
Dear John,
the following variant of thms_of_proof, which is currently not part of
proofterm.ML, should do what you want:
fun thms_of_proof' (Abst (_, _, prf)) = thms_of_proof' prf
| thms_of_proof' (AbsP (_, _, prf)) = thms_of_proof' prf
| thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2
| thms_of_proof' (prf % _) = thms_of_proof' prf
| thms_of_proof' (PThm (("", _), prf, prop, _)) = thms_of_proof' prf
| thms_of_proof' (prf' as PThm ((s, _), _, prop, _)) = (fn tab =>
case Symtab.lookup tab s of
NONE => Symtab.update (s, [(prop, prf')]) tab
| SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
Symtab.update (s, (prop, prf')::ps) tab)
| thms_of_proof' (MinProof (prfs, _, _)) = fold (thms_of_proof' o Proofterm.proof_of_min_thm) prfs
| thms_of_proof' _ = I;
With the above function, you can compute the table of lemmas directly used in
the proof of "test" as follows:
thms_of_proof' (Proofterm.strip_thm (proof_of (thm "test"))) Symtab.empty
Note that you have to strip off the outermost PThm constructor first,
otherwise the table of lemmas used in the proof would only consist
of "test" itself.
Greetings,
Stefan
Email Gateway (Aug 17 2022 at 14:15):From: John Matthews <matthews@galois.com>
Thanks Stefan, your function works exactly as advertised. Please let
me know if you decide to add this to the Isabelle repository, so that
I use the official version.
Best,
-john
Email Gateway (Aug 17 2022 at 14:15):From: Stefan Berghofer <berghofe@in.tum.de>
John Matthews wrote:
Dear John,
I have just added the function to the repository. If nothing goes wrong,
it should appear in the development snapshot tomorrow.
Greetings,
Stefan
Last updated: May 03 2024 at 04:19 UTC