# [isabelle] Proof state, proof context, @{context} and get_thmss?

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Proof state, proof context, @{context} and get_thmss?
*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>
*Date*: Fri, 25 Jun 2010 03:51:46 +1000
*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

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.

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