Re: [isabelle] thm dependencies



Thanks, Makarius. Here is the SML code I wrote to extract the list of external oracle tags used in the proof of a theorem. Am I using any deprecated functions?

text {* Extract the abstract syntax of a theorem's oracle tags. *}

ML {*
fun oracle_terms_of_thm thm
  = Proofterm.oracles_of_proof [] (proof_of thm)
*}

text {* This will let us view the tagged oracles using surface syntax. *}

ML {*
fun oracle_strings_of_thm thm
= let val thy = theory_of_thm thm
in map (fn (oracle,formula) => (oracle, Sign.string_of_term thy formula))
         (oracles_of_thm thm)
  end
*}

-john



On Oct 25, 2005, at 7:19 AM, Makarius wrote:

On Tue, 25 Oct 2005, John Matthews wrote:

Similarly, how to I extract the list of external oracles used in the
proof of a tagged theorem, when theorem dependencies are turned off?

See Pure/proofterm.ML for some operations on proof terms as stored within
the "der" field of a thm.


On Oct 24, 2005, at 5:52 PM, Sean McLaughlin wrote:

  I'd like a way to extract the theorem dependencies of a theorem. I
know Isabelle has a great facility for plotting these deps with
"thm_deps", but is there a way to just extract a tree of dependencies
(that could be topologically sorted, say).

See Pure/Thy/thm_deps.ML.  You may build a Graph.T (cf.
Pure/General/graph.ML) and get a toplogically sorted list of entries like
this:

  fn G => Graph.all_succs G (Graph.minimals G)


	Makarius






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