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



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.