Email Gateway (Aug 18 2022 at 15:35): Email Gateway (Aug 18 2022 at 15:35):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Dear Isabelle Gurus,
Once more I am wishing for enlightenment. Since I'm doing dependency
tracking of theorems, I want to basically go up the chain of theorems to
get to the top, finding dependencies.
There is a command which does something like this, called thm_deps,
which works nicely in a graphical context. However, I am unable to
replicate the functionality at the ML level.
The problem is as follows, thm_deps is defined in isar_cmd as:
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
Thm_Deps.thm_deps (Proof.get_thmss (Toplevel.enter_proof_body
state) args))
I have a simple theory:
theory DeepDepends imports Plain begin
lemma lem1: "A --> A" by simp
thm_deps "lem1" (* this works great *)
ML {* (* this does not work *)
Proof.get_thmss (Proof.init @{context}) [pair (Facts.Fact "lem1") []]
*}
I've examined IsarCmd.thm_deps using tracing, and it really only has
[(Facts.Fact "lem1" [])] passed in to it.
The error I get is:
*** Failed to retrieve literal fact:
*** lem1
I've been running around in the code in circles. The problem is most
likely that I have no idea how to get the proper proof context / proof
state from the toplevel.
The reason I'm digging so deep, is because when I get the names of
depended-on theorems from the proof term for a theorem, I get names like
HOL.simp_thms_17, not theorems. To go any further up the dependency
hierarchy, I need to look up HOL.simp_thms_17, which Isabelle has no
idea about, as it's the 17th theorem in HOL.simps and its original name
is something else entirely. This behaviour has always puzzled me, but
this time it has really stopped me in my tracks.
At one point I got Thm_Deps.thm_deps to get going with my request, but
then it also bailed on unknown fact "HOL.simp_thms_17". At this point I
am considering catching the exception, stripping the _ and number from
the end, looking up the theorem list without the number, and if that
exists, getting the nth theorem in the theorem list, which is a very
ugly thing to be doing.
Does anyone see where I went wrong?
Sincerely,
Rafal Kolanski.
Last updated: Nov 21 2024 at 12:39 UTC